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 nn-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-r : (p : x ≑ y) β†’ p βˆ™ inv p ≑ refl
  βˆ™-inv-r {x = x} = J (Ξ» y p β†’ p βˆ™ inv p ≑ refl)
                      (βˆ™-id-l (inv refl) βˆ™ J-refl (Ξ» y _ β†’ y ≑ x) refl)

  βˆ™-inv-l : (p : x ≑ y) β†’ inv p βˆ™ p ≑ refl
  βˆ™-inv-l {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 (βˆ‚ 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!

  βˆ™-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, ap-comp-path 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 nn-ary compositions. For instance, we know that pβˆ’1βˆ™pβˆ™qp^{-1} βˆ™ p βˆ™ q is qq, but this involves more than a handful of intermediate steps:

  βˆ™-cancel-l
    : βˆ€ {β„“} {A : Type β„“} {x y z : A} (p : x ≑ y) (q : y ≑ z)
    β†’ (sym p βˆ™ p βˆ™ q) ≑ q
  βˆ™-cancel-l {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

  βˆ™-cancel-r
    : βˆ€ {β„“} {A : Type β„“} {x y z : A} (p : x ≑ y) (q : z ≑ y)
    β†’ ((p βˆ™ sym q) βˆ™ q) ≑ p
  βˆ™-cancel-r {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 (βˆ™-cancel-l p q) Β·Β· ap (sym p βˆ™_) sq Β·Β· βˆ™-cancel-l 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 (βˆ™-cancel-r q (sym p))
    Β·Β· ap (_βˆ™ sym p) sq
    Β·Β· βˆ™-cancel-r r (sym p)

Groupoid structure of types (cont.)πŸ”—

A useful fact is that if HH 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)                        ∎
  )