open import 1Lab.Path.Groupoid
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Path.Reasoning where

Reasoning combinators for path spaces🔗

Identity paths🔗

∙-id-comm : p ∙ refl ≡ refl ∙ p
∙-id-comm {p = p} i j =
  hcomp (∂ i ∨ ∂ j) λ where
    k (i = i0) → ∙-filler p refl k j
    k (i = i1) → ∙-filler'' refl p j k
    k (j = i0) → p i0
    k (j = i1) → p (~ i ∨ k)
    k (k = i0) → (p (~ i ∧ j))

module _ (p≡refl : p ≡ refl) where
  ∙-eliml : p ∙ q ≡ q
  ∙-eliml {q = q} = sym $ paste (ap sym p≡refl) refl refl refl (∙-filler' p q)

  ∙-elimr : q ∙ p ≡ q
  ∙-elimr {q = q} = sym $ paste refl refl refl p≡refl (∙-filler q p)

  ∙-introl : q ≡ p ∙ q
  ∙-introl = sym ∙-eliml

  ∙-intror : q ≡ q ∙ p
  ∙-intror = sym ∙-elimr

Reassocations🔗

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

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))

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 _ _ _

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
  ∙-cancell : p ∙ (q ∙ r) ≡ r
  ∙-cancell = ∙-pulll inv ∙ ∙-id-l _

  ∙-cancelr : (r ∙ p) ∙ q ≡ r
  ∙-cancelr = ∙-pullr inv ∙ ∙-id-r _

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

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

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 define 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