open import 1Lab.Path

open import Cat.Base

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π

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

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

introl : f β‘ a β f
introl = sym eliml

intror : f β‘ f β a
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 _ (abβ‘c : a β b β‘ c) where

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

pushl : c β f β‘ a β (b β f)
pushl = sym (pulll (sym cβ‘ab))

pushr : f β c β‘ (f β a) β b
pushr = sym (pullr (sym cβ‘ab))

module _ (p : f β h β‘ g β i) where
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

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


## 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
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β _β_

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