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