module Cat.Reasoning {o β} (C : Precategory o β) where open import Cat.Morphism C public
Reasoning Combinators for Categoriesπ
When doing category theory, we often have to perform many βtrivialβ algebraic manipulations like reassociation, insertion of identity morphisms, etc. On paper we can omit these steps, but Agda is a bit more picky! We could just do these steps in our proofs one after another, but this clutters things up. Instead, we provide a series of reasoning combinators to make writing (and reading) proofs easier.
Most of these helpers were taken from
agda-categories
.
Identity Morphismsπ
abstract id-comm : β {a b} {f : Hom a b} β f β id β‘ id β f id-comm {f = f} = idr f β sym (idl f) id-comm-sym : β {a b} {f : Hom a b} β id β f β‘ f β id id-comm-sym {f = f} = idl f β sym (idr f) module _ (aβ‘id : a β‘ id) where abstract eliml : a β f β‘ f eliml {f = f} = a β f β‘β¨ ap (_β f) aβ‘id β©β‘ id β f β‘β¨ idl f β©β‘ f β elimr : f β a β‘ f elimr {f = f} = f β a β‘β¨ ap (f β_) aβ‘id β©β‘ f β id β‘β¨ idr f β©β‘ f β elim-inner : f β a β h β‘ f β h elim-inner {f = f} = ap (f β_) eliml introl : f β‘ a β f introl = sym eliml intror : f β‘ f β a intror = sym elimr intro-inner : f β h β‘ f β a β h intro-inner {f = f} = ap (f β_) introl
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 _ (abβ‘c : a β b β‘ c) where abstract pulll : a β (b β f) β‘ c β f pulll {f = f} = a β b β f β‘β¨ assoc a b f β©β‘ (a β b) β f β‘β¨ ap (_β f) abβ‘c β©β‘ c β f β pullr : (f β a) β b β‘ f β c pullr {f = f} = (f β a) β b β‘Λβ¨ assoc f a b β©β‘Λ f β (a β b) β‘β¨ ap (f β_) abβ‘c β©β‘ f β c β module _ (cβ‘ab : c β‘ a β b) where abstract pushl : c β f β‘ a β (b β f) pushl = sym (pulll (sym cβ‘ab)) pushr : f β c β‘ (f β a) β b pushr = sym (pullr (sym cβ‘ab)) push-inner : f β c β g β‘ (f β a) β (b β g) push-inner {f = f} = ap (f β_) pushl β assoc _ _ _ module _ (p : f β h β‘ g β i) where abstract extendl : f β (h β b) β‘ g β (i β b) extendl {b = b} = f β (h β b) β‘β¨ assoc f h b β©β‘ (f β h) β b β‘β¨ ap (_β b) p β©β‘ (g β i) β b β‘Λβ¨ assoc g i b β©β‘Λ g β (i β b) β extendr : (a β f) β h β‘ (a β g) β i extendr {a = a} = (a β f) β h β‘Λβ¨ assoc a f h β©β‘Λ a β (f β h) β‘β¨ ap (a β_) p β©β‘ a β (g β i) β‘β¨ assoc a g i β©β‘ (a β g) β i β extend-inner : a β f β h β b β‘ a β g β i β b extend-inner {a = a} = ap (a β_) extendl
Cancellationπ
These lemmas do 2 things at once: rearrange parenthesis, and also
remove things that are equal to id
.
module _ (inv : h β i β‘ id) where abstract cancell : h β (i β f) β‘ f cancell {f = f} = h β (i β f) β‘β¨ pulll inv β©β‘ id β f β‘β¨ idl f β©β‘ f β cancelr : (f β h) β i β‘ f cancelr {f = f} = (f β h) β i β‘β¨ pullr inv β©β‘ f β id β‘β¨ idr f β©β‘ f β insertl : f β‘ h β (i β f) insertl = sym cancell insertr : f β‘ (f β h) β i insertr = sym cancelr cancel-inner : (f β h) β (i β g) β‘ f β g cancel-inner = pulll cancelr insert-inner : f β g β‘ (f β h) β (i β g) insert-inner = pushl insertr deleter : (f β g β h) β i β‘ f β g deleter = pullr cancelr deletel : h β (i β f) β g β‘ f β g deletel = pulll cancell
We also have a combinator which combines expanding on the right with a cancellation on the left:
lswizzle : g β‘ h β i β f β h β‘ id β f β g β‘ i lswizzle {g = g} {h = h} {i = i} {f = f} p q = f β g β‘β¨ apβ _β_ refl p β©β‘ f β h β i β‘β¨ cancell q β©β‘ i β
Isomorphismsπ
These lemmas are useful for proving that partial inverses to an isomorphism are unique. Thereβs a helper for proving uniqueness of left inverses, of right inverses, and for proving that any left inverse must match any right inverse.
module _ {y z} (f : y β z) where abstract open _β _ left-inv-unique : β {g h} β g β f .to β‘ id β h β f .to β‘ id β g β‘ h left-inv-unique {g = g} {h = h} p q = g β‘β¨ intror (f .invl) β©β‘ g β f .to β f .from β‘β¨ extendl (p β sym q) β©β‘ h β f .to β f .from β‘β¨ elimr (f .invl) β©β‘ h β left-right-inv-unique : β {g h} β g β f .to β‘ id β f .to β h β‘ id β g β‘ h left-right-inv-unique {g = g} {h = h} p q = g β‘β¨ intror (f .invl) β©β‘ g β f .to β f .from β‘β¨ cancell p β©β‘ f .from β‘β¨ intror q β©β‘ f .from β f .to β h β‘β¨ cancell (f .invr) β©β‘ h β right-inv-unique : β {g h} β f .to β g β‘ id β f .to β h β‘ id β g β‘ h right-inv-unique {g = g} {h} p q = g β‘β¨ introl (f .invr) β©β‘ (f .from β f .to) β g β‘β¨ pullr (p β sym q) β©β‘ f .from β f .to β h β‘β¨ cancell (f .invr) β©β‘ h β
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!
_β©ββ¨_ : f β‘ h β g β‘ i β f β g β‘ h β i _β©ββ¨_ = apβ _β_ infixr 40 _β©ββ¨_ reflβ©ββ¨_ : g β‘ h β f β g β‘ f β h reflβ©ββ¨_ {f = f} p = ap (f β_) p _β©ββ¨refl : f β‘ h β f β g β‘ h β g _β©ββ¨refl {g = g} p = ap (_β g) p