Maths - Groupoid

As discussed on the page here groupoids can be thought of as a weakening of a setiod. Instead of equivalences we have isomorphisms, that is the permutations show how objects are equal in multiple ways.

contractible singleton

(Unit Type)

subsingleton

(Mere proposition)

reflexive

a~a

symmetric

if a~b then b~a

transitive

if a~b and b~c then a~c

There used to be a puzzle, sometimes called the 15 puzzle, consisting of 15 sliding plastic tiles in a 4 by 4 frame. There is only one space without a tile, so the only moves possible are to slide the adjacent tiles into that space.

The tiles have letters or numbers on them and the goal is to get them in a certain order.

• We could think of the position of all the tiles as being its state. There is then a mapping from state to state, but this mapping is partial because only certain moves will be possible depending on where the space is.

• Rather than one set of endo functions we could have a set of states, one for each possible location of the space. So now instead of the functions being endofunctions they go between these states. These functions are no longer partial but they are still permutations.

Imagine if we have multiple sets, all of the same size, then they can all be 'equal' in multiple ways. That is we may have:

• 0 = false and 1=true
• or 1= false and 0=true

and so on for the other sets of the same size.

This gives a groupoid like structure.

Does this diagram show a groupoid?

No, because the mappings are not all reversible.

We can reverse a degeneracy map with a face map but the face map is not reversed by the degeneracy map unless it is already degenerate.

What if we take the more complicated situation where multiple faces are glued together.

Is there some way we can characterise this as a groupoid?

It feels like the fifteen puzzle above in that jumping between vertices, edges, triangles, etc. allows us to get to different faces.

In Nat consider 'n', '0+n' and 'n+0' they are equal terms in some way.

'n' and '0+n' are definitionally equal because they automatically normalise to the same. Definitionally equality is denoted with a 3-bar equals sign (≡) or just by using the same symbol.

But 'N+0' is propositionally (but not definitionally) equal to N. It is denoted with a normal equals sign (=) and shown as an arrow between nodes.

This can get more complicated when we have types involving containers within containers.

a,b : A
p,q : a=b
α,β : p=q
...

All arrows can be reversed.

f • f^-1 = Id

In an ordinary group (represented a permutation group) the functors are endofunctors with only a single object.

Its possible to have permutations such that we can only permute the elements if we go round the loop but not if we reverse the path.

Depending on the complexity of the groupoid there may be multiple paths round the loop which produce the same permutation so we have possible equivalences between paths. That is, higher order equivalences.

Id(x,y)

paths from x to y in the space.

Setoid

This imposes an external equivalence relation and internalises it.

The single object needs to have the reflexive relation, that is, be equal to itself.

An example would be a set with a set with a fixed number of elements.

Groupoid

This can be thought of as a weakening of a setiod. Instead of equivalences we have isomorphisms, that is the permutations show how objects are equal in multiple ways.

Category

Just to confuse things the naming conventions have changed here. Monoid has an 'oid' but this is the single object case. A Monoidoid is a category.

||| Groupoid where base type is a
||| finite set (implemented as a list)
record Groupoid (level : Nat) where
    constructor MkGroupoid
    source : Nat
    dest : Nat
    Path : List (Groupoid (level + 1))

fifteenPuzzle : Groupoid 0
fifteenPuzzle = 
  let
    c1:Groupoid 2 = MkGroupoid 1 2 []
    c2:Groupoid 2 = MkGroupoid 2 1 []
    swap = [c1,c2]
    b1_2:Groupoid 1 =MkGroupoid 1 2 swap
    b1_5:Groupoid 1 =MkGroupoid 1 5 swap
    b2_3:Groupoid 1 =MkGroupoid 2 3 swap
    b2_6:Groupoid 1 =MkGroupoid 2 6 swap
    b3_4:Groupoid 1 =MkGroupoid 3 4 swap
    b3_7:Groupoid 1 =MkGroupoid 3 7 swap
    b4_8:Groupoid 1 =MkGroupoid 4 8 swap
    b5_6:Groupoid 1 =MkGroupoid 5 6 swap
    b5_9:Groupoid 1 =MkGroupoid 5 9 swap
    b6_7:Groupoid 1 =MkGroupoid 6 7 swap
    b6_10:Groupoid 1 =MkGroupoid 6 10 swap
    b7_8:Groupoid 1 =MkGroupoid 7 8 swap
    b7_11:Groupoid 1 =MkGroupoid 7 11 swap
    b8_12:Groupoid 1 =MkGroupoid 8 12 swap
    b9_10:Groupoid 1 =MkGroupoid 9 10 swap
    b9_13:Groupoid 1 =MkGroupoid 9 13 swap
    b10_11:Groupoid 1 =MkGroupoid 10 11 swap
    b10_14:Groupoid 1 =MkGroupoid 10 14 swap
    b11_12:Groupoid 1 =MkGroupoid 11 12 swap
    b11_15:Groupoid 1 =MkGroupoid 11 15 swap
    b12_16:Groupoid 1 =MkGroupoid 12 16 swap
    b13_14:Groupoid 1 =MkGroupoid 13 14 swap
    b14_15:Groupoid 1 =MkGroupoid 14 15 swap
    b15_16:Groupoid 1 =MkGroupoid 15 16 swap
  in
    the (Groupoid 0) (MkGroupoid 0 0 [b1_2,b1_5,b2_3,b2_6,b3_4,b3_7,b4_8,
                                      b5_6,b5_9,b6_7,b6_10,b7_8,b7_11,b8_12,
                                      b9_10,b9_13,b10_11,b10_14,b11_12,b11_15,b12_16,
                                      b13_14,b14_15,b15_16])

A first thought for how to embed simplicial sets in topological spaces might be to equate each simplex with an open set, unfortunately this won't work for the following reasons:

Each of the points is now a vector in its own dimension, these are [1,0] and [0,1] and they are the basis vectors.

The line is a straight line between these basis vectors, parameterised by t like this { (1-t)*[1,0]+t*[0,1] | t[0,1] }.