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

module 1Lab.Path.Reasoning where


# Reasoning combinators for path spacesπ

private variable
β : Level
A : Type β
x y : A
p p' q q' r r' s s' t u v : x β‘ y

β-filler''
: β {β} {A : Type β} {x y z : A} (p : x β‘ y) (q : y β‘ z)
β Square refl (sym p) q (p β q)
β-filler'' {x = x} {y} {z} p q i j =
hcomp (β i β¨ ~ j) Ξ» where
k (i = i0) β p (~ j)
k (i = i1) β q (j β§ k)
k (j = i0) β y
k (k = i0) β p (i β¨ ~ j)

pasteP
: β {β} {A : Type β} {w w' x x' y y' z z' : A}
{p p' q q' r r' s s'}
{Ξ± Ξ² Ξ³ Ξ΄}
β Square Ξ± p p' Ξ²
β Square Ξ± q q' Ξ³
β Square Ξ² r r' Ξ΄
β Square Ξ³ s s' Ξ΄
β Square {a00 = w}  {x}  {y}  {z}  p  q  r  s
β Square {a00 = w'} {x'} {y'} {z'} p' q' r' s'
pasteP top left right bottom square i j = hcomp (β i β¨ β j) Ξ» where
k (i = i0) β left k j
k (i = i1) β right k j
k (j = i0) β top k i
k (j = i1) β bottom k i
k (k = i0) β square i j

paste
: p β‘ p' β q β‘ q' β r β‘ r' β s β‘ s'
β Square p q r s
β Square p' q' r' s'
paste p q r s = pasteP p q r s


## 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 opaque
β-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

β-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


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