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

module 1Lab.Path.Groupoid where


# Types are Groupoidsπ

The Path types equip every Type with the structure of an $\infty$-groupoid. 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 $n$-cells 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.

  β-id-r : (p : x β‘ y) β p β refl β‘ p
β-id-r {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:

  β-id-l : (p : y β‘ z) β refl β p β‘ p
β-id-l {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)) β‘β¨ β-id-l (q β r) β©β‘
q β r            β‘β¨ sym (ap (Ξ» e β e β r) (β-id-l 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.

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

β-inv-r : (p : x β‘ y) β inv p β p β‘ refl
β-inv-r {x = x} = J (Ξ» y p β inv p β p β‘ refl)
(β-id-r (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

open 1Lab.Path


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

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

β-id-l : (p : x β‘ y) β refl β p β‘ p
β-id-l 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!

  β-inv-r : β {x y : A} (p : x β‘ y) β p β sym p β‘ refl
β-inv-r {x = x} p i j =
hcomp (Ξ» l β Ξ» { (j = i0) β x
; (j = i1) β p (~ l β§ ~ i)
; (i = i1) β x
})
(p (j β§ ~ 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!

  β-inv-l : (p : x β‘ y) β sym p β p β‘ refl
β-inv-l p = β-inv-r (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 and ap-sym in the 1Lab.Path module.

There, a proof that functions preserve path composition wasnβt included, because it needs hcomp to be defined. We fill a cube where the left face is defined to be ap f (p β q) (thatβs the (i = i0) face in the hcomp below), and the remaining structure of the proof mimics the definition of _β_, so that we indeed get ap f p β ap f q as the right face.

  ap-comp-path : (f : A β B) {x y z : A} (p : x β‘ y) (q : y β‘ z)
β ap f (p β q) β‘ ap f p β ap f q
ap-comp-path f {x} p q i j =
hcomp (Ξ» k β Ξ» { (i = i0) β f (β-filler p q k j)
; (j = i0) β f x
; (j = i1) β f (q k)
})
(f (p j))


### Convenient helpersπ

Since a lot of Homotopy Type Theory is dealing with paths, this section introduces useful helpers for dealing with $n$-ary compositions. For instance, we know that $p^{-1} β p β q$ is $q$, but this involves more than a handful of intermediate steps:

  β-cancel-l : {x y z : A} (p : x β‘ y) (q : y β‘ z)
β (sym p β p β q) β‘ q
β-cancel-l p q =
sym p β p β q   β‘β¨ β-assoc _ _ _ β©β‘
(sym p β p) β q β‘β¨ apβ _β_ (β-inv-l p) refl β©β‘
refl β q        β‘β¨ β-id-l q β©β‘
q               β

β-cancel'-l : {x y z : A} (p : x β‘ y) (q r : y β‘ z)
β p β q β‘ p β r β q β‘ r
β-cancel'-l = J (Ξ» y p β (q r : y β‘ _) β p β q β‘ p β r β q β‘ r)
(Ξ» q r proof β sym (β-id-l q) Β·Β· proof Β·Β· β-id-l r)

β-cancel'-r : {x y z : A} (p : y β‘ z) (q r : x β‘ y)
β q β p β‘ r β p β q β‘ r
β-cancel'-r = J (Ξ» y p β (q r : _ β‘ _) β q β p β‘ r β p β q β‘ r)
(Ξ» q r proof β sym (β-id-r q) Β·Β· proof Β·Β· β-id-r r)


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

A useful fact is that if $H$ is a homotopy f ~ id, then we can βinvertβ it as such:

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)
homotopy-invert {f = f} H {x = x} =
sym (
ap f (H x)                     β‘β¨ sym (β-id-r _) β©β‘
ap f (H x) β refl              β‘β¨ apβ _β_ refl (sym (β-inv-r _)) β©β‘
ap f (H x) β H x β sym (H x)   β‘β¨ β-assoc _ _ _ β©β‘
(ap f (H x) β H x) β sym (H x) β‘β¨ apβ _β_ (sym (homotopy-natural H _)) refl β©β‘
(H (f x) β H x) β sym (H x)    β‘β¨ sym (β-assoc _ _ _) β©β‘
H (f x) β H x β sym (H x)      β‘β¨ apβ _β_ refl (β-inv-r _) β©β‘
H (f x) β refl                 β‘β¨ β-id-r _ β©β‘
H (f x)                        β
)