open import 1Lab.Path hiding (_β_)
open import 1Lab.Type

module 1Lab.Path.Groupoid where

_ = Path
_ = hfill
_ = ap-refl
_ = ap-β
_ = ap-sym


# Types are groupoidsπ

The Path types equip every Type with the structure of an . The higher structure of a type begins with its inhabitants (the 0-cells); Then, there are the paths between inhabitants - these are inhabitants of the type Path A x y, which are the 1-cells in A. Then, we can consider the inhabitants of Path (Path A x y) p q, which are homotopies between paths.

This construction iterates forever - and, at every stage, we have that the in A are the 0-cells of some other type (e.g.: The 1-cells of A are the 0-cells of Path A ...). Furthermore, this structure is weak: The laws, e.g.Β associativity of composition, only hold up to a homotopy. These laws satisfy their own laws β again using associativity as an example, the associator satisfies the pentagon identity.

These laws can be proved in two ways: Using path induction, or directly with a cubical argument. Here, we do both.

## Book-styleπ

This is the approach taken in the HoTT book. We fix a type, and some variables of that type, and some paths between variables of that type, so that each definition doesnβt start with 12 parameters.

module WithJ where
private variable
β : Level
A : Type β
w x y z : A


First, we (re)define the operations using J. These will be closer to the structure given in the book.

  _β_ : x β‘ y β y β‘ z β x β‘ z
_β_ {x = x} {y} {z} = J (Ξ» y _ β y β‘ z β x β‘ z) (Ξ» x β x)


First we define path composition. Then, we can prove that the identity path - refl - acts as an identity for path composition.

  β-idr : (p : x β‘ y) β p β refl β‘ p
β-idr {x = x} {y = y} p =
J (Ξ» _ p β p β refl β‘ p)
(happly (J-refl (Ξ» y _ β y β‘ y β x β‘ y) (Ξ» x β x)) _)
p


This isnβt as straightforward as it would be in βBook HoTTβ because - remember - J doesnβt compute definitionally, only up to the path J-refl. Now the other identity law:

  β-idl : (p : y β‘ z) β refl β p β‘ p
β-idl {y = y} {z = z} p = happly (J-refl (Ξ» y _ β y β‘ z β y β‘ z) (Ξ» x β x)) p


This case we get for less since itβs essentially the computation rule for J.

  β-assoc : (p : w β‘ x) (q : x β‘ y) (r : y β‘ z)
β p β (q β r) β‘ (p β q) β r
β-assoc {w = w} {x = x} {y = y} {z = z} p q r =
J (Ξ» x p β (q : x β‘ y) (r : y β‘ z) β p β (q β r) β‘ (p β q) β r) lemma p q r
where
lemma : (q : w β‘ y) (r : y β‘ z)
β (refl β (q β r)) β‘ ((refl β q) β r)
lemma q r =
(refl β (q β r)) β‘β¨ β-idl (q β r) β©β‘
q β r            β‘β¨ sym (ap (Ξ» e β e β r) (β-idl q)) β©β‘
(refl β q) β r   β


The associativity rule is trickier to prove, since we do inductive where the motive is a dependent product. What weβre doing can be summarised using words: By induction, it suffices to assume p is refl. Then, what we want to show is (refl β (q β r)) β‘ ((refl β q) β r). But both of those compute to q β r, so we are done. This computation isnβt automatic - itβs expressed by the lemma.

This expresses that the paths behave like morphisms in a category. For a groupoid, we also need inverses and cancellation:

  inv : x β‘ y β y β‘ x
inv {x = x} = J (Ξ» y _ β y β‘ x) refl


The operation which assigns inverses has to be involutive, which follows from two computations.

  inv-inv : (p : x β‘ y) β inv (inv p) β‘ p
inv-inv {x = x} =
J (Ξ» y p β inv (inv p) β‘ p)
(ap inv (J-refl (Ξ» y _ β y β‘ x) refl) β J-refl (Ξ» y _ β y β‘ x) refl)


And we have to prove that composing with an inverse gives the reflexivity path.

  β-invr : (p : x β‘ y) β p β inv p β‘ refl
β-invr {x = x} = J (Ξ» y p β p β inv p β‘ refl)
(β-idl (inv refl) β J-refl (Ξ» y _ β y β‘ x) refl)

β-invl : (p : x β‘ y) β inv p β p β‘ refl
β-invl {x = x} = J (Ξ» y p β inv p β p β‘ refl)
(β-idr (inv refl) β J-refl (Ξ» y _ β y β‘ x) refl)


## Cubicallyπ

Now we do the same using hfill instead of path induction.

module _ where
private variable
β : Level
A B : Type β
w x y z : A
a b c d : A

open 1Lab.Path

  β-fillerβ : β {β} {A : Type β} {x y z : A} (q : x β‘ y) (r : y β‘ z)
β Square q (q β r) r refl
β-fillerβ q r k i = hcomp (k β¨ β i) Ξ» where
l (l = i0) β q (i β¨ k)
l (k = i1) β r (l β§ i)
l (i = i0) β q k
l (i = i1) β r l


The left and right identity laws follow directly from the two fillers for the composition operation.

  β-idr : (p : x β‘ y) β p β refl β‘ p
β-idr p = sym (β-filler p refl)

β-idl : (p : x β‘ y) β refl β p β‘ p
β-idl p = sym (β-filler' refl p)


For associativity, we use both:

  β-assoc : (p : w β‘ x) (q : x β‘ y) (r : y β‘ z)
β p β (q β r) β‘ (p β q) β r
β-assoc p q r i = β-filler p q i β β-filler' q r (~ i)


For cancellation, we need to sketch an open cube where the missing square expresses the equation weβre looking for. Thankfully, we only have to do this once!

  β-invr : β {x y : A} (p : x β‘ y) β p β sym p β‘ refl
β-invr {x = x} p i j = hcomp (β j β¨ i) Ξ» where
k (k = i0) β p (j β§ ~ i)
k (i = i1) β x
k (j = i0) β x
k (j = i1) β p (~ k β§ ~ i)


For the other direction, we use the fact that p is definitionally equal to sym (sym p). In that case, we show that sym p β sym (sym p) β‘ refl - which computes to the thing we want!

  β-invl : (p : x β‘ y) β sym p β p β‘ refl
β-invl p = β-invr (sym p)


In addition to the groupoid identities for paths in a type, it has been established that functions behave like functors: These are the lemmas ap-refl, ap-β and ap-sym in the 1Lab.Path module.

### Convenient helpersπ

Since a lot of Homotopy Type Theory is dealing with paths, this section introduces useful helpers for dealing with compositions. For instance, we know that is but this involves more than a handful of intermediate steps:

  β-cancell
: β {β} {A : Type β} {x y z : A} (p : x β‘ y) (q : y β‘ z)
β (sym p β p β q) β‘ q
β-cancell {y = y} p q i j = hcomp (β i β¨ β j) Ξ» where
k (k = i0) β p (i β¨ ~ j)
k (i = i0) β β-filler (sym p) (p β q) k j
k (i = i1) β q (j β§ k)
k (j = i0) β y
k (j = i1) β β-fillerβ p q i k

β-cancelr
: β {β} {A : Type β} {x y z : A} (p : x β‘ y) (q : z β‘ y)
β ((p β sym q) β q) β‘ p
β-cancelr {x = x} {y = y} q p = sym \$ β-unique _ Ξ» i j β
β-filler q (sym p) (~ i) j

commutesβsquare
: {p : w β‘ x} {q : w β‘ y} {s : x β‘ z} {r : y β‘ z}
β p β s β‘ q β r
β Square p q s r
commutesβsquare {p = p} {q} {s} {r} fill i j =
hcomp (β i β¨ β j) Ξ» where
k (k = i0) β fill j i
k (i = i0) β q (k β§ j)
k (i = i1) β s (~ k β¨ j)
k (j = i0) β β-filler p s (~ k) i
k (j = i1) β β-fillerβ q r k i

squareβcommutes
: {p : w β‘ x} {q : w β‘ y} {s : x β‘ z} {r : y β‘ z}
β Square p q s r β p β s β‘ q β r
squareβcommutes {p = p} {q} {s} {r} fill i j = hcomp (β i β¨ β j) Ξ» where
k (k = i0) β fill j i
k (i = i0) β β-filler p s k j
k (i = i1) β β-fillerβ q r (~ k) j
k (j = i0) β q (~ k β§ i)
k (j = i1) β s (k β¨ i)

β-cancel'-l : {x y z : A} (p : x β‘ y) (q r : y β‘ z)
β p β q β‘ p β r β q β‘ r
β-cancel'-l p q r sq = sym (β-cancell p q) Β·Β· ap (sym p β_) sq Β·Β· β-cancell p r

β-cancel'-r : {x y z : A} (p : y β‘ z) (q r : x β‘ y)
β q β p β‘ r β p β q β‘ r
β-cancel'-r p q r sq =
sym (β-cancelr q (sym p))
Β·Β· ap (_β sym p) sq
Β·Β· β-cancelr r (sym p)


While connections give us degenerate squares where two adjacent faces are some path and the other two are refl, it is sometimes also useful to have a degenerate square with two pairs of equal adjacent faces. We can build this using hcomp and more connections:

  double-connection
: (p : a β‘ b) (q : b β‘ c)
β Square p p q q
double-connection {b = b} p q i j = hcomp (β i β¨ β j) Ξ» where
k (k = i0) β b
k (i = i0) β p (j β¨ ~ k)
k (i = i1) β q (j β§ k)
k (j = i0) β p (i β¨ ~ k)
k (j = i1) β q (i β§ k)


This corresponds to the following diagram, which expresses the trivial equation

# Groupoid structure of types (cont.)π

A useful fact is that if is a homotopy then it βcommutes with β, in the following sense:

open 1Lab.Path

homotopy-invert
: β {a} {A : Type a} {f : A β A}
β (H : (x : A) β f x β‘ x) {x : A}
β H (f x) β‘ ap f (H x)


The proof proceeds entirely using itself, together with the De Morgan algebra structure on the interval.

homotopy-invert {f = f} H {x} i j = hcomp (β i β¨ β j) Ξ» where
k (k = i0) β H x       (j β§ i)
k (j = i0) β H (f x)   (~ k)
k (j = i1) β H x       (~ k β§ i)
k (i = i0) β H (f x)   (~ k β¨ j)
k (i = i1) β H (H x j) (~ k)