module 1Lab.Path.Reasoning whereReasoning 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)
β Triangle (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 sIdentity 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 β-elimrReassocationsπ
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 β-cancelsrNotationπ
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