Reasoning combinators for path spaces🔗

We often find ourselves in situations where we have an equality involving the composition of 2 morphisms, but the association is a bit off. These combinators aim to address that situation.

module _ (pq≡s : p ∙ q ≡ s) where
  ∙-pulll : p ∙ q ∙ r ≡ s ∙ r
  ∙-pulll {r = r} = ∙-assoc p q r ∙ ap (_∙ r) pq≡s

  double-left : p ∙∙ q ∙∙ r ≡ s ∙ r
  double-left {r = r} = double-composite p q r ∙ ∙-pulll

  ∙-pullr : (r ∙ p) ∙ q ≡ r ∙ s
  ∙-pullr {r = r} = sym (∙-assoc r p q) ∙ ap (r ∙_) pq≡s

  ∙-swapl : q ≡ sym p ∙ s
  ∙-swapl = ∙-introl (∙-invl p) ∙ ∙-pullr

  ∙-swapr : p ≡ s ∙ sym q
  ∙-swapr = ∙-intror (∙-invr q) ∙ ∙-pulll

module _ (s≡pq : s ≡ p ∙ q) where
  ∙-pushl : s ∙ r ≡ p ∙ q ∙ r
  ∙-pushl = sym (∙-pulll (sym s≡pq))

  ∙-pushr : r ∙ s ≡ (r ∙ p) ∙ q
  ∙-pushr = sym (∙-pullr (sym s≡pq))

  ∙→square : Square refl p s q
  ∙→square = ∙-filler p q ▷ sym s≡pq

  ∙→square' : Square (sym p) q s refl
  ∙→square' = ∙-filler' p q ▷ sym s≡pq

  ∙→square'' : Square (sym p) refl s q
  ∙→square'' = transpose (∙-filler'' p q) ▷ sym s≡pq

module _ (pq≡rs : p ∙ q ≡ r ∙ s) where
  ∙-extendl : p ∙ (q ∙ t) ≡ r ∙ (s ∙ t)
  ∙-extendl {t = t} = ∙-assoc _ _ _ ∙∙ ap (_∙ t) pq≡rs ∙∙ sym (∙-assoc _ _ _)

  ∙-extendr : (t ∙ p) ∙ q ≡ (t ∙ r) ∙ s
  ∙-extendr {t = t} = sym (∙-assoc _ _ _) ∙∙ ap (t ∙_) pq≡rs ∙∙ ∙-assoc _ _ _

∙∙-stack : (sym p' ∙∙ (sym p ∙∙ q ∙∙ r) ∙∙ r') ≡ (sym (p ∙ p') ∙∙ q ∙∙ (r ∙ r'))
∙∙-stack = ∙∙-unique' (∙∙-filler _ _ _ ∙₂ ∙∙-filler _ _ _)

∙∙-chain : (sym p ∙∙ q ∙∙ r) ∙ (sym r ∙∙ q' ∙∙ s) ≡ sym p ∙∙ (q ∙ q') ∙∙ s
∙∙-chain {p = p} {q = q} {r = r} {q' = q'} {s = s} = sym (∙-unique _ square) where
  square : Square refl (sym p ∙∙ q ∙∙ r) (sym p ∙∙ (q ∙ q') ∙∙ s) (sym r ∙∙ q' ∙∙ s)
  square i j = hcomp (~ j ∨ (j ∧ (i ∨ ~ i))) λ where
    k (k = i0) → ∙-filler q q' i j
    k (j = i0) → p k
    k (j = i1) (i = i0) → r k
    k (j = i1) (i = i1) → s k

∙∙-∙-assoc : p ∙∙ q ∙∙ (r ∙ s) ≡ (p ∙∙ q ∙∙ r) ∙ s
∙∙-∙-assoc {p = p} {q = q} {r = r} {s = s} = sym (∙∙-unique' square) where
  square : Square (sym p) q ((p ∙∙ q ∙∙ r) ∙ s) (r ∙ s)
  square i j = hcomp (~ i ∨ ~ j ∨ (i ∧ j)) λ where
    k (k = i0) → ∙∙-filler p q r i j
    k (i = i0) → q j
    k (j = i0) → p (~ i)
    k (i = i1) (j = i1) → s k

∙∙-introl
  : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : x ≡ z)
  → p ≡ q ∙∙ sym q ∙∙ p
∙∙-introl p q i j = hcomp (∂ j ∨ ~ i) λ where
  k (k = i0) → q (~ j ∧ i)
  k (i = i0) → p (k ∧ j)
  k (j = i0) → q (~ k ∧ i)
  k (j = i1) → p k

∙∙-intror
  : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z)
  → p ≡ p ∙∙ q ∙∙ sym q
∙∙-intror p q i j = hcomp (∂ j ∨ ~ i) λ where
  k (k = i0) → q (i ∧ j)
  k (i = i0) → p (j ∨ ~ k)
  k (j = i0) → p (~ k)
  k (j = i1) → q (~ k ∧ i)

module _ {p q : x ≡ y} where
  ∨-square : p ≡ q → Square p q refl refl
  ∨-square sq i j = hcomp (∂ i ∨ ∂ j) λ where
    k (k = i0) → p j
    k (i = i0) → sq k j
    k (i = i1) → p (j ∨ k)
    k (j = i0) → p (i ∧ k)
    k (j = i1) → y

  flatten-∨-square : Square p q refl refl → p ≡ q
  flatten-∨-square sq i j = hcomp (∂ i ∨ ∂ j) λ where
    k (k = i0) → sq j i
    k (i = i0) → p j
    k (i = i1) → q (j ∨ ~ k)
    k (j = i1) → y
    k (j = i0) → q (i ∧ ~ k)

  ∧-square : p ≡ q → Square refl refl p q
  ∧-square sq i j = hcomp (∂ i ∨ ∂ j) λ where
    k (k = i0) → p (i ∧ j)
    k (i = i0) → x
    k (i = i1) → p j
    k (j = i0) → x
    k (j = i1) → sq k i

  flatten-∧-square : Square refl refl p q → p ≡ q
  flatten-∧-square sq i j = hcomp (∂ i ∨ ∂ j) λ where
    k (k = i0) → sq j i
    k (i = i0) → p (j ∧ k)
    k (i = i1) → q j
    k (j = i0) → x
    k (j = i1) → p (i ∨ k)

Cancellation🔗

These lemmas do 2 things at once: rearrange parenthesis, and also remove things that are equal to id.

module _ (inv : p ∙ q ≡ refl) where abstract
  ∙-cancelsl : p ∙ (q ∙ r) ≡ r
  ∙-cancelsl = ∙-pulll inv ∙ ∙-idl _

  ∙-cancelsr : (r ∙ p) ∙ q ≡ r
  ∙-cancelsr = ∙-pullr inv ∙ ∙-idr _

  ∙-insertl : r ≡ p ∙ (q ∙ r)
  ∙-insertl = sym ∙-cancelsl

  ∙-insertr : r ≡ (r ∙ p) ∙ q
  ∙-insertr = sym ∙-cancelsr

Notation🔗

When doing equational reasoning, it’s often somewhat clumsy to have to write ap (f ∙_) p when proving that f ∙ g ≡ f ∙ h. To fix this, we steal some cute mixfix notation from agda-categories which allows us to write ≡⟨ refl⟩∙⟨ p ⟩ instead, which is much more aesthetically pleasing!

_⟩∙⟨_ : p ≡ q → r ≡ s → p ∙ r ≡ q ∙ s
_⟩∙⟨_ p q i = p i ∙ q i

refl⟩∙⟨_ : p ≡ q → r ∙ p ≡ r ∙ q
refl⟩∙⟨_ {r = r} p = ap (r ∙_) p

_⟩∙⟨refl : p ≡ q → p ∙ r ≡ q ∙ r
_⟩∙⟨refl {r = r} p = ap (_∙ r) p