open import 1Lab.Path
open import 1Lab.Type hiding (id; _β_)

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.

private variable
u v w x y z : Ob
a a' a'' b b' b'' c c' c'' d d' d'' e : Hom x y
f g g' h h' i : Hom x y


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

idr2 : β {a b c} (f : Hom b c) (g : Hom a b) β f β g β id β‘ f β g
idr2 f g = ap (f β_) (idr g)

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

pull-inner : (f β a) β (b β g) β‘ f β c β g
pull-inner {f = f} = sym (assoc _ _ _) β ap (f β_) pulll

module _ (abcβ‘d : a β b β c β‘ d) where abstract
pulll3 : a β (b β (c β f)) β‘ d β f
pulll3 {f = f} =
a β b β c β f   β‘β¨ ap (a β_) (assoc _ _ _) β©β‘
a β (b β c) β f β‘β¨ assoc _ _ _ β©β‘
(a β b β c) β f β‘β¨ ap (_β f) abcβ‘d β©β‘
d β f           β

pullr3 : ((f β a) β b) β c β‘ f β d
pullr3 {f = f} =
((f β a) β b) β c β‘Λβ¨ assoc _ _ _ β©β‘Λ
(f β a) β b β c   β‘Λβ¨ assoc _ _ _ β©β‘Λ
f β a β b β c     β‘β¨ ap (f β_) abcβ‘d β©β‘
f β d β

module _ (abcdβ‘e : a β b β c β d β‘ e) where abstract
pulll4 : a β (b β (c β (d β f))) β‘ e β f
pulll4 {f = f} =
a β b β c β d β f β‘β¨ ap (Ξ» x β a β b β x) (assoc _ _ _) β©β‘
a β b β (c β d) β f β‘β¨ ap (a β_) (assoc _ _ _) β©β‘
a β (b β c β d) β f β‘β¨ assoc _ _ _ β©β‘
(a β b β c β d) β f β‘β¨ ap (_β f) abcdβ‘e β©β‘
e β f β

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 _ (dβ‘abc : d β‘ a β b β c) where abstract
pushl3 : d β f β‘ a β (b β (c β f))
pushl3 = sym (pulll3 (sym dβ‘abc))

pushr3 : f β d β‘ ((f β a) β b) β c
pushr3 = sym (pullr3 (sym dβ‘abc))

module _ (eβ‘abcd : e β‘ a β b β c β d) where abstract
pushl4 : e β f β‘ a β (b β (c β (d β f)))
pushl4 = sym (pulll4 (sym eβ‘abcd))

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

module _ (p : a β b β c β‘ d β f β g) where abstract
extendl3 : a β (b β (c β h)) β‘ d β (f β (g β h))
extendl3 = pulll3 p β sym (pulll3 refl)

extendr3 : ((h β a) β b) β c β‘ ((h β d) β f) β g
extendr3 = pullr3 p β sym (pullr3 refl)

module _ (p : a β b β c β d β‘ e β f β g β h) where abstract
extendl4 : a β b β c β d β i β‘ e β f β g β h β i
extendl4 = pulll4 p β sym (pulll4 refl)


We also define some useful combinators for performing repeated pulls/pushes.

abstract
centralize
: f β g β‘ a β b
β h β i β‘ c β d
β f β g β h β i β‘ a β (b β c) β d
centralize {f = f} {g = g} {a = a} {b = b} {h = h} {i = i} {c = c} {d = d} p q =
f β g β h β i   β‘β¨ pulll p β©β‘
(a β b) β h β i β‘β¨ pullr (pushr q) β©β‘
a β (b β c) β d β

centralizel
: f β g β‘ a β b
β f β g β h β i β‘ a β (b β h) β i
centralizel p = centralize p refl

centralizer
: h β i β‘ c β d
β f β g β h β i β‘ f β (g β c) β d
centralizer p = centralize refl p

disperse
: f β g β‘ a β b
β h β i β‘ c β d
β f β (g β h) β i β‘ a β b β c β d
disperse {f = f} {g = g} {a = a} {b = b} {h = h} {i = i} {c = c} {d = d} p q =
f β (g β h) β i β‘β¨ pushr (pullr q) β©β‘
(f β g) β c β d β‘β¨ pushl p β©β‘
a β b β c β d β

dispersel
: f β g β‘ a β b
β f β (g β h) β i β‘ a β b β h β i
dispersel p = disperse p refl

disperser
: h β i β‘ c β d
β f β (g β h) β i β‘ f β g β c β d
disperser p = disperse refl p


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

module _ (inv : g β h β i β‘ id) where abstract
cancell3 : g β (h β (i β f)) β‘ f
cancell3 {f = f} = pulll3 inv β idl f

cancelr3 : ((f β g) β h) β i β‘ f
cancelr3 {f = f} = pullr3 inv β idr f

insertl3 : f β‘ g β (h β (i β f))
insertl3 = sym cancell3

insertr3 : f β‘ ((f β g) β h) β i
insertr3 = sym cancelr3


We also have combinators which combine expanding on one side with a cancellation on the other side:

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

rswizzle : g β‘ i β h β h β f β‘ id β g β f β‘ i
rswizzle {g = g} {i = i} {h = h} {f = f} p q =
g β f       β‘β¨ apβ _β_ p refl β©β‘
(i β h) β f β‘β¨ cancelr q β©β‘
i           β


The following βswizzleβ operation can be pictured as flipping a commutative square along an axis, provided the morphisms on that axis are invertible.

swizzle : f β g β‘ h β i β g β g' β‘ id β h' β h β‘ id β h' β f β‘ i β g'
swizzle {f = f} {g = g} {h = h} {i = i} {g' = g'} {h' = h'} p q r =
lswizzle (sym (assoc _ _ _ β rswizzle (sym p) q)) r


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


If we have a commuting triangle of isomorphisms, then we can flip one of the sides to obtain a new commuting triangle of isomorphisms.

Iso-swapr :
β {a : x β y} {b : y β z} {c : x β z}
β b βIso a β‘ c
β a β‘ b Isoβ»ΒΉ βIso c
Iso-swapr {a = a} {b = b} {c = c} p = β-path $a .to β‘β¨ introl (b .invr) β©β‘ (b .from β b .to) β a .to β‘β¨ pullr (ap to p) β©β‘ b .from β c .to β Iso-swapl : β {a : x β y} {b : y β z} {c : x β z} β b βIso a β‘ c β b β‘ c βIso a Isoβ»ΒΉ Iso-swapl {a = a} {b = b} {c = c} p = β -path$
b .to                   β‘β¨ intror (a .invl) β©β‘
b .to β a .to β a .from β‘β¨ pulll (ap to p) β©β‘
c .to β a .from         β


Assume we have a prism of isomorphisms, as in the following diagram:

If the top, front, left, and right faces all commute, then so does the bottom face.

Iso-prism : β {a : u β v} {b : v β w} {c : u β w}
β {d : u β x} {e : v β y} {f : w β z}
β {g : x β y} {h : y β z} {i : x β z}
β b βIso a β‘ c
β e βIso a β‘ g βIso d
β f βIso b β‘ h βIso e
β f βIso c β‘ i βIso d
β h βIso g β‘ i
Iso-prism {a = a} {b} {c} {d} {e} {f} {g} {h} {i} top left right front =
β-path \$
h .to β g .to                                           β‘β¨ apβ _β_ (ap to (Iso-swapl (sym right))) (ap to (Iso-swapl (sym left)) β sym (assoc _ _ _)) β©β‘
((f .to β b .to) β e .from) β (e .to β a .to β d .from) β‘β¨ cancel-inner (e .invr) β©β‘
(f .to β b .to) β (a .to β d .from)                     β‘β¨ pull-inner (ap to top) β©β‘
f .to β c .to β d .from                                 β‘β¨ assoc _ _ _ β sym (ap to (Iso-swapl (sym front))) β©β‘
i .to β


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

_β©ββ¨_ : f β‘ h β g β‘ i β f β g β‘ h β i