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