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'' : Hom x y
f g 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 _ (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 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           ∎


## 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}
→ a ∘Iso b ≡ c
→ a ≡ c ∘Iso (b Iso⁻¹)
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} → a ∘Iso b ≡ c → b ≡ (a Iso⁻¹) ∘Iso c 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}
→ a ∘Iso b ≡ c
→ a ∘Iso e ≡ d ∘Iso g
→ b ∘Iso f ≡ e ∘Iso h
→ c ∘Iso f ≡ d ∘Iso i
→ g ∘Iso h ≡ 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 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