module 1Lab.Path.Groupoid where

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

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: Other than the lemma ap-βˆ™, preservation of reflexivity and of inverses is definitional.

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:

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)