open import 1Lab.Prelude hiding (_β_ ; id ; _βͺ_ ; _β _)

open import Cat.Solver
open import Cat.Base

module Cat.Morphism {o h} (C : Precategory o h) where

open Precategory C public
private variable
a b c d : Ob
f : Hom a b


Morphismsπ

This module defines the three most important classes of morphisms that can be found in a category: monomorphisms, epimorphisms, and isomorphisms.

Monosπ

A morphism is said to be monic when it is left-cancellable. A monomorphism from to written is a monic morphism.

is-monic : Hom a b β Type _
is-monic {a = a} f = β {c} β (g h : Hom c a) β f β g β‘ f β h β g β‘ h

is-monic-is-prop : β {a b} (f : Hom a b) β is-prop (is-monic f)
is-monic-is-prop f x y i {c} g h p = Hom-set _ _ _ _ (x g h p) (y g h p) i

record _βͺ_ (a b : Ob) : Type (o β h) where
field
mor   : Hom a b
monic : is-monic mor

open _βͺ_ public


Conversely, a morphism is said to be epic when it is right-cancellable. An epimorphism from to written is an epic morphism.

Episπ

is-epic : Hom a b β Type _
is-epic {b = b} f = β {c} β (g h : Hom b c) β g β f β‘ h β f β g β‘ h

is-epic-is-prop : β {a b} (f : Hom a b) β is-prop (is-epic f)
is-epic-is-prop f x y i {c} g h p = Hom-set _ _ _ _ (x g h p) (y g h p) i

record _β _ (a b : Ob) : Type (o β h) where
field
mor  : Hom a b
epic : is-epic mor

open _β _ public


The identity morphism is monic and epic.

id-monic : β {a} β is-monic (id {a})
id-monic g h p = sym (idl _) Β·Β· p Β·Β· idl _

id-epic : β {a} β is-epic (id {a})
id-epic g h p = sym (idr _) Β·Β· p Β·Β· idr _


Both monos and epis are closed under composition.

monic-β
: β {a b c} {f : Hom b c} {g : Hom a b}
β is-monic f
β is-monic g
β is-monic (f β g)
monic-β fm gm a b Ξ± = gm _ _ (fm _ _ (assoc _ _ _ Β·Β· Ξ± Β·Β· sym (assoc _ _ _)))

epic-β
: β {a b c} {f : Hom b c} {g : Hom a b}
β is-epic f
β is-epic g
β is-epic (f β g)
epic-β fe ge a b Ξ± = fe _ _ (ge _ _ (sym (assoc _ _ _) Β·Β· Ξ± Β·Β· (assoc _ _ _)))

_βMono_ : β {a b c} β b βͺ c β a βͺ b β a βͺ c
(f βMono g) .mor = f .mor β g .mor
(f βMono g) .monic = monic-β (f .monic) (g .monic)

_βEpi_ : β {a b c} β b β  c β a β  b β a β  c
(f βEpi g) .mor = f .mor β g .mor
(f βEpi g) .epic = epic-β (f .epic) (g .epic)


If is monic, then must also be monic.

monic-cancell
: β {a b c} {f : Hom b c} {g : Hom a b}
β is-monic (f β g)
β is-monic g
monic-cancell {f = f} fg-monic h h' p = fg-monic h h' $sym (assoc _ _ _) Β·Β· ap (f β_) p Β·Β· assoc _ _ _  Dually, if is epic, then must also be epic. epic-cancelr : β {a b c} {f : Hom b c} {g : Hom a b} β is-epic (f β g) β is-epic f epic-cancelr {g = g} fg-epic h h' p = fg-epic h h'$
assoc _ _ _ Β·Β· ap (_β g) p Β·Β· sym (assoc _ _ _)


Postcomposition with a mono is an embedding.

monic-postcomp-embedding
: β {a b c} {f : Hom b c}
β is-monic f
β is-embedding {A = Hom a b} (f β_)
monic-postcomp-embedding monic =
injectiveβis-embedding (Hom-set _ _) _ (monic _ _)


Likewise, precomposition with an epi is an embedding.

epic-precomp-embedding
: β {a b c} {f : Hom a b}
β is-epic f
β is-embedding {A = Hom b c} (_β f)
epic-precomp-embedding epic =
injectiveβis-embedding (Hom-set _ _) _ (epic _ _)


Sectionsπ

A morphism is a section of another morphism when The intuition for this name is that picks out a cross-section of from For instance, could map animals to their species; a section of this map would have to pick out a canonical representative of each species from the set of all animals.

_section-of_ : (s : Hom b a) (r : Hom a b) β Type _
s section-of r = r β s β‘ id

section-of-is-prop
: β {s : Hom b a} {r : Hom a b}
β is-prop (s section-of r)
section-of-is-prop = Hom-set _ _ _ _

record has-section (r : Hom a b) : Type h where
constructor make-section
field
section : Hom b a
is-section : section section-of r

open has-section public

id-has-section : β {a} β has-section (id {a})
id-has-section .section = id
id-has-section .is-section = idl _

section-of-β
: β {a b c} {f : Hom c b} {g : Hom b c} {h : Hom b a} {i : Hom a b}
β f section-of g β h section-of i
β (h β f) section-of (g β i)
section-of-β {f = f} {g = g} {h = h} {i = i} fg-sect hi-sect =
(g β i) β h β f β‘β¨ cat! C β©β‘
g β (i β h) β f β‘β¨ ap (Ξ» Ο β g β Ο β f) hi-sect β©β‘
g β id β f      β‘β¨ ap (g β_) (idl _) β©β‘
g β f           β‘β¨ fg-sect β©β‘
id β

section-β
: β {a b c} {f : Hom b c} {g : Hom a b}
β has-section f β has-section g β has-section (f β g)
section-β f-sect g-sect .section = g-sect .section β f-sect .section
section-β {f = f} {g = g} f-sect g-sect .is-section =
section-of-β (f-sect .is-section) (g-sect .is-section)


If has a section, then is epic.

has-sectionβepic
: β {a b} {f : Hom a b}
β has-section f
β is-epic f
has-sectionβepic {f = f} f-sect g h p =
g                         β‘Λβ¨ idr _ β©β‘Λ
g β id                    β‘Λβ¨ ap (g β_) (f-sect .is-section) β©β‘Λ
g β f β f-sect .section   β‘β¨ assoc _ _ _ β©β‘
(g β f) β f-sect .section β‘β¨ ap (_β f-sect .section) p β©β‘
(h β f) β f-sect .section β‘Λβ¨ assoc _ _ _ β©β‘Λ
h β f β f-sect .section   β‘β¨ ap (h β_) (f-sect .is-section) β©β‘
h β id                    β‘β¨ idr _ β©β‘
h β


Retractsπ

A morphism is a retract of another morphism when Note that this is the same equation involved in the definition of a section; retracts and sections always come in pairs. If sections solve a sort of βcuration problemβ where we are asked to pick out canonical representatives, then retracts solve a sort of βclassification problemβ.

_retract-of_ : (r : Hom a b) (s : Hom b a) β Type _
r retract-of s = r β s β‘ id

retract-of-is-prop
: β {s : Hom b a} {r : Hom a b}
β is-prop (r retract-of s)
retract-of-is-prop = Hom-set _ _ _ _

record has-retract (s : Hom b a) : Type h where
constructor make-retract
field
retract : Hom a b
is-retract : retract retract-of s

open has-retract public

id-has-retract : β {a} β has-retract (id {a})
id-has-retract .retract = id
id-has-retract .is-retract = idl _

retract-of-β
: β {a b c} {f : Hom c b} {g : Hom b c} {h : Hom b a} {i : Hom a b}
β f retract-of g β h retract-of i
β (h β f) retract-of (g β i)
retract-of-β fg-ret hi-ret = section-of-β hi-ret fg-ret

retract-β
: β {a b c} {f : Hom b c} {g : Hom a b}
β has-retract f β has-retract g
β has-retract (f β g)
retract-β f-ret g-ret .retract = g-ret .retract β f-ret .retract
retract-β f-ret g-ret .is-retract =
retract-of-β (f-ret .is-retract) (g-ret .is-retract)


If has a retract, then is monic.

has-retractβmonic
: β {a b} {f : Hom a b}
β has-retract f
β is-monic f
has-retractβmonic {f = f} f-ret g h p =
g                        β‘Λβ¨ idl _ β©β‘Λ
id β g                   β‘Λβ¨ ap (_β g) (f-ret .is-retract) β©β‘Λ
(f-ret .retract β f) β g β‘Λβ¨ assoc _ _ _ β©β‘Λ
f-ret .retract β (f β g) β‘β¨ ap (f-ret .retract β_) p β©β‘
f-ret .retract β f β h   β‘β¨ assoc _ _ _ β©β‘
(f-ret .retract β f) β h β‘β¨ ap (_β h) (f-ret .is-retract) β©β‘
id β h                   β‘β¨ idl _ β©β‘
h                        β


A section that is also epic is a retract.

section-of+epicβretract-of
: β {a b} {s : Hom b a} {r : Hom a b}
β s section-of r
β is-epic s
β s retract-of r
section-of+epicβretract-of {s = s} {r = r} sect epic =
epic (s β r) id $(s β r) β s β‘Λβ¨ assoc s r s β©β‘Λ s β (r β s) β‘β¨ ap (s β_) sect β©β‘ s β id β‘β¨ idr _ β©β‘ s β‘Λβ¨ idl _ β©β‘Λ id β s β  Dually, a retract that is also monic is a section. retract-of+monicβsection-of : β {a b} {s : Hom b a} {r : Hom a b} β r retract-of s β is-monic r β r section-of s retract-of+monicβsection-of {s = s} {r = r} ret monic = monic (s β r) id$
r β s β r   β‘β¨ assoc r s r β©β‘
(r β s) β r β‘β¨ ap (_β r) ret β©β‘
id β r      β‘β¨ idl _ β©β‘
r           β‘Λβ¨ idr _ β©β‘Λ
r β id      β

has-retract+epicβhas-section
: β {a b} {f : Hom a b}
β has-retract f
β is-epic f
β has-section f
has-retract+epicβhas-section ret epic .section = ret .retract
has-retract+epicβhas-section ret epic .is-section =
section-of+epicβretract-of (ret .is-retract) epic

has-section+monicβhas-retract
: β {a b} {f : Hom a b}
β has-section f
β is-monic f
β has-retract f
has-section+monicβhas-retract sect monic .retract = sect .section
has-section+monicβhas-retract sect monic .is-retract =
retract-of+monicβsection-of (sect .is-section) monic


Isosπ

Maps and are inverses when we have and both equal to the identity. A map is invertible (or is an isomorphism) when there exists a for which and are inverses. An isomorphism is a choice of map together with a specified inverse.

record Inverses (f : Hom a b) (g : Hom b a) : Type h where
field
invl : f β g β‘ id
invr : g β f β‘ id

open Inverses

record is-invertible (f : Hom a b) : Type h where
field
inv : Hom b a
inverses : Inverses f inv

open Inverses inverses public

op : is-invertible inv
op .inv = f
op .inverses .Inverses.invl = invr inverses
op .inverses .Inverses.invr = invl inverses

record _β_ (a b : Ob) : Type h where
field
to       : Hom a b
from     : Hom b a
inverses : Inverses to from

open Inverses inverses public

open _β_ public


A given map is invertible in at most one way: If you have with two inverses and then not only are equal, but the witnesses of these equalities are irrelevant.

Inverses-are-prop : β {f : Hom a b} {g : Hom b a} β is-prop (Inverses f g)
Inverses-are-prop x y i .Inverses.invl = Hom-set _ _ _ _ (x .invl) (y .invl) i
Inverses-are-prop x y i .Inverses.invr = Hom-set _ _ _ _ (x .invr) (y .invr) i

is-invertible-is-prop : β {f : Hom a b} β is-prop (is-invertible f)
is-invertible-is-prop {a = a} {b = b} {f = f} g h = p where
module g = is-invertible g
module h = is-invertible h

gβ‘h : g.inv β‘ h.inv
gβ‘h =
g.inv             β‘β¨ sym (idr _) β apβ _β_ refl (sym h.invl) β©β‘
g.inv β f β h.inv β‘β¨ assoc _ _ _ Β·Β· apβ _β_ g.invr refl Β·Β· idl _ β©β‘
h.inv             β

p : g β‘ h
p i .is-invertible.inv = gβ‘h i
p i .is-invertible.inverses =
is-propβpathp (Ξ» i β Inverses-are-prop {g = gβ‘h i}) g.inverses h.inverses i


We note that the identity morphism is always iso, and that isos compose:

id-invertible : β {a} β is-invertible (id {a})
id-invertible .is-invertible.inv = id
id-invertible .is-invertible.inverses .invl = idl id
id-invertible .is-invertible.inverses .invr = idl id

id-iso : a β a
id-iso .to = id
id-iso .from = id
id-iso .inverses .invl = idl id
id-iso .inverses .invr = idl id

Isomorphism = _β_

Inverses-β : {a b c : Ob} {f : Hom b c} {fβ»ΒΉ : Hom c b} {g : Hom a b} {gβ»ΒΉ : Hom b a}
β Inverses f fβ»ΒΉ β Inverses g gβ»ΒΉ β Inverses (f β g) (gβ»ΒΉ β fβ»ΒΉ)
Inverses-β {f = f} {fβ»ΒΉ} {g} {gβ»ΒΉ} finv ginv = record { invl = l ; invr = r } where
module finv = Inverses finv
module ginv = Inverses ginv

abstract
l : (f β g) β gβ»ΒΉ β fβ»ΒΉ β‘ id
l = (f β g) β gβ»ΒΉ β fβ»ΒΉ β‘β¨ cat! C β©β‘
f β (g β gβ»ΒΉ) β fβ»ΒΉ β‘β¨ (Ξ» i β f β ginv.invl i β fβ»ΒΉ) β©β‘
f β id β fβ»ΒΉ        β‘β¨ cat! C β©β‘
f β fβ»ΒΉ             β‘β¨ finv.invl β©β‘
id                  β

r : (gβ»ΒΉ β fβ»ΒΉ) β f β g β‘ id
r = (gβ»ΒΉ β fβ»ΒΉ) β f β g β‘β¨ cat! C β©β‘
gβ»ΒΉ β (fβ»ΒΉ β f) β g β‘β¨ (Ξ» i β gβ»ΒΉ β finv.invr i β g) β©β‘
gβ»ΒΉ β id β g        β‘β¨ cat! C β©β‘
gβ»ΒΉ β g             β‘β¨ ginv.invr β©β‘
id                  β

_βIso_ : β {a b c : Ob} β b β c β a β b β a β c
(f βIso g) .to = f .to β g .to
(f βIso g) .from = g .from β f .from
(f βIso g) .inverses = Inverses-β (f .inverses) (g .inverses)

_βIso_ : β {a b c : Ob} β a β b β b β c β a β c
f βIso g = g βIso f

infixr 40 _βIso_ _βIso_
infixr 41 _Isoβ»ΒΉ

invertible-β
: β {f : Hom b c} {g : Hom a b}
β is-invertible f β is-invertible g
β is-invertible (f β g)
invertible-β f-inv g-inv = record
{ inv = g-inv.inv β f-inv.inv
; inverses = Inverses-β f-inv.inverses g-inv.inverses
}
where
module f-inv = is-invertible f-inv
module g-inv = is-invertible g-inv

_invertibleβ»ΒΉ
: β {f : Hom a b} β (f-inv : is-invertible f)
β is-invertible (is-invertible.inv f-inv)
_invertibleβ»ΒΉ {f = f} f-inv .is-invertible.inv = f
_invertibleβ»ΒΉ f-inv .is-invertible.inverses .invl =
is-invertible.invr f-inv
_invertibleβ»ΒΉ f-inv .is-invertible.inverses .invr =
is-invertible.invl f-inv

_Isoβ»ΒΉ : a β b β b β a
(f Isoβ»ΒΉ) .to = f .from
(f Isoβ»ΒΉ) .from = f .to
(f Isoβ»ΒΉ) .inverses .invl = f .inverses .invr
(f Isoβ»ΒΉ) .inverses .invr = f .inverses .invl

make-inverses : {f : Hom a b} {g : Hom b a} β f β g β‘ id β g β f β‘ id β Inverses f g
make-inverses p q .invl = p
make-inverses p q .invr = q

make-invertible : {f : Hom a b} β (g : Hom b a) β f β g β‘ id β g β f β‘ id β is-invertible f
make-invertible g p q .is-invertible.inv = g
make-invertible g p q .is-invertible.inverses .invl = p
make-invertible g p q .is-invertible.inverses .invr = q

make-iso : (f : Hom a b) (g : Hom b a) β f β g β‘ id β g β f β‘ id β a β b
make-iso f g p q ._β_.to = f
make-iso f g p q ._β_.from = g
make-iso f g p q ._β_.inverses .Inverses.invl = p
make-iso f g p q ._β_.inverses .Inverses.invr = q

inversesβinvertible : β {f : Hom a b} {g : Hom b a} β Inverses f g β is-invertible f
inversesβinvertible x .is-invertible.inv = _
inversesβinvertible x .is-invertible.inverses = x

invertibleβiso : (f : Hom a b) β is-invertible f β a β b
invertibleβiso f x =
record
{ to       = f
; from     = x .is-invertible.inv
; inverses = x .is-invertible.inverses
}

is-invertible-inverse
: {f : Hom a b} (g : is-invertible f) β is-invertible (g .is-invertible.inv)
is-invertible-inverse g =
record { inv = _ ; inverses = record { invl = invr g ; invr = invl g } }
where open Inverses (g .is-invertible.inverses)

isoβinvertible : (i : a β b) β is-invertible (i ._β_.to)
isoβinvertible i = record { inv = i ._β_.from ; inverses = i ._β_.inverses }

private
β-pathp-internal
: (p : a β‘ c) (q : b β‘ d)
β {f : a β b} {g : c β d}
β PathP (Ξ» i β Hom (p i) (q i)) (f ._β_.to) (g ._β_.to)
β PathP (Ξ» i β Hom (q i) (p i)) (f ._β_.from) (g ._β_.from)
β PathP (Ξ» i β p i β q i) f g
β-pathp-internal p q r s i .to = r i
β-pathp-internal p q r s i .from = s i
β-pathp-internal p q {f} {g} r s i .inverses =
is-propβpathp (Ξ» j β Inverses-are-prop {f = r j} {g = s j})
(f .inverses) (g .inverses) i

abstract
inverse-unique
: {x y : Ob} (p : x β‘ y) {b d : Ob} (q : b β‘ d) (f : x β b) (g : y β d)
β PathP (Ξ» i β Hom (p i) (q i)) (f .to) (g .to)
β PathP (Ξ» i β Hom (q i) (p i)) (f .from) (g .from)
inverse-unique =
J' (Ξ» a c p β β {b d} (q : b β‘ d) (f : a β b) (g : c β d)
β PathP (Ξ» i β Hom (p i) (q i)) (f .to) (g .to)
β PathP (Ξ» i β Hom (q i) (p i)) (f .from) (g .from))
Ξ» x β J' (Ξ» b d q β (f : x β b) (g : x β d)
β PathP (Ξ» i β Hom x (q i)) (f .to) (g .to)
β PathP (Ξ» i β Hom (q i) x) (f .from) (g .from))
Ξ» y f g p β
f .from                     β‘Λβ¨ ap (f .from β_) (g .invl) β idr _ β©β‘Λ
f .from β g .to β g .from   β‘β¨ assoc _ _ _ β©β‘
(f .from β g .to) β g .from β‘β¨ ap (_β g .from) (ap (f .from β_) (sym p) β f .invr) β idl _ β©β‘
g .from                     β

β-pathp
: (p : a β‘ c) (q : b β‘ d) {f : a β b} {g : c β d}
β PathP (Ξ» i β Hom (p i) (q i)) (f ._β_.to) (g ._β_.to)
β PathP (Ξ» i β p i β q i) f g
β-pathp p q {f = f} {g = g} r = β-pathp-internal p q r (inverse-unique p q f g r)

β-pathp-from
: (p : a β‘ c) (q : b β‘ d) {f : a β b} {g : c β d}
β PathP (Ξ» i β Hom (q i) (p i)) (f ._β_.from) (g ._β_.from)
β PathP (Ξ» i β p i β q i) f g
β-pathp-from p q {f = f} {g = g} r = β-pathp-internal p q (inverse-unique q p (f Isoβ»ΒΉ) (g Isoβ»ΒΉ) r) r

β-path : {f g : a β b} β f ._β_.to β‘ g ._β_.to β f β‘ g
β-path = β-pathp refl refl

β-path-from : {f g : a β b} β f ._β_.from β‘ g ._β_.from β f β‘ g
β-path-from = β-pathp-from refl refl

β-is-contr : (β {a b} β is-contr (Hom a b)) β is-contr (a β b)
β-is-contr hom-contr .centre =
make-iso (hom-contr .centre) (hom-contr .centre)
(is-contrβis-prop hom-contr _ _)
(is-contrβis-prop hom-contr _ _)
β-is-contr hom-contr .paths f = β-path (hom-contr .paths (f .to))

β-is-prop : (β {a b} β is-prop (Hom a b)) β is-prop (a β b)
β-is-prop hom-prop f g = β-path (hom-prop (f .to) (g .to))

βͺ-pathp
: {a : I β Ob} {b : I β Ob} {f : a i0 βͺ b i0} {g : a i1 βͺ b i1}
β PathP (Ξ» i β Hom (a i) (b i)) (f .mor) (g .mor)
β PathP (Ξ» i β a i βͺ b i) f g
βͺ-pathp {a = a} {b} {f} {g} pa = go where
go : PathP (Ξ» i β a i βͺ b i) f g
go i .mor = pa i
go i .monic {c = c} =
is-propβpathp
(Ξ» i β Ξ -is-hlevel {A = Hom c (a i)} 1
Ξ» g β Ξ -is-hlevel {A = Hom c (a i)} 1
Ξ» h β fun-is-hlevel {A = pa i β g β‘ pa i β h} 1
(Hom-set c (a i) g h))
(f .monic)
(g .monic)
i

β -pathp
: {a : I β Ob} {b : I β Ob} {f : a i0 β  b i0} {g : a i1 β  b i1}
β PathP (Ξ» i β Hom (a i) (b i)) (f .mor) (g .mor)
β PathP (Ξ» i β a i β  b i) f g
β -pathp {a = a} {b} {f} {g} pa = go where
go : PathP (Ξ» i β a i β  b i) f g
go i .mor = pa i
go i .epic {c = c} =
is-propβpathp
(Ξ» i β Ξ -is-hlevel {A = Hom (b i) c} 1
Ξ» g β Ξ -is-hlevel {A = Hom (b i) c} 1
Ξ» h β fun-is-hlevel {A = g β pa i β‘ h β pa i} 1
(Hom-set (b i) c g h))
(f .epic)
(g .epic)
i


Isomorphisms enjoy a 2-out-of-3 property: if any 2 of and are isomorphisms, then so is the third.

inverses-cancell
: β {f : Hom b c} {g : Hom a b} {gβ»ΒΉ : Hom b a} {fgβ»ΒΉ : Hom c a}
β Inverses g gβ»ΒΉ β Inverses (f β g) fgβ»ΒΉ
β Inverses f (g β fgβ»ΒΉ)

inverses-cancelr
: β {f : Hom b c} {fβ»ΒΉ : Hom c b} {g : Hom a b} {fgβ»ΒΉ : Hom c a}
β Inverses f fβ»ΒΉ β Inverses (f β g) fgβ»ΒΉ
β Inverses g (fgβ»ΒΉ β f)

invertible-cancell
: β {f : Hom b c} {g : Hom a b}
β is-invertible g β is-invertible (f β g)
β is-invertible f

invertible-cancelr
: β {f : Hom b c} {g : Hom a b}
β is-invertible f β is-invertible (f β g)
β is-invertible g

We are early into our bootstrapping process for category theory, so the proofs of these lemmas are quite low-level, and thus omitted.
inverses-cancell g-inv fg-inv .invl =
assoc _ _ _ β fg-inv .invl
inverses-cancell g-inv fg-inv .invr =
sym (idr _)
β apβ _β_ refl (sym (g-inv .invl))
β assoc _ _ _
β apβ _β_
(sym (assoc _ _ _)
β sym (assoc _ _ _)
β apβ _β_ refl (fg-inv .invr)
β idr _)
refl
β g-inv .invl

inverses-cancelr f-inv fg-inv .invl =
sym (idl _)
β apβ _β_ (sym (f-inv .invr)) refl
β sym (assoc _ _ _)
β apβ _β_ refl
(assoc _ _ _
β assoc _ _ _
β apβ _β_ (fg-inv .invl) refl
β idl _)
β f-inv .invr
inverses-cancelr f-inv fg-inv .invr =
sym (assoc _ _ _) β fg-inv .invr

invertible-cancell g-inv fg-inv =
inversesβinvertible $inverses-cancell (g-inv .is-invertible.inverses) (fg-inv .is-invertible.inverses) invertible-cancelr f-inv fg-inv = inversesβinvertible$
inverses-cancelr
(f-inv .is-invertible.inverses)
(fg-inv .is-invertible.inverses)


We also note that invertible morphisms are both epic and monic.

invertibleβmonic : is-invertible f β is-monic f
invertibleβmonic {f = f} invert g h p =
g             β‘Λβ¨ idl g β©β‘Λ
id β g        β‘Λβ¨ ap (_β g) (is-invertible.invr invert) β©β‘Λ
(inv β f) β g β‘Λβ¨ assoc inv f g β©β‘Λ
inv β (f β g) β‘β¨ ap (inv β_) p β©β‘
inv β (f β h) β‘β¨ assoc inv f h β©β‘
(inv β f) β h β‘β¨ ap (_β h) (is-invertible.invr invert) β©β‘
id β h        β‘β¨ idl h β©β‘
h β
where
open is-invertible invert

invertibleβepic : is-invertible f β is-epic f
invertibleβepic {f = f} invert g h p =
g             β‘Λβ¨ idr g β©β‘Λ
g β id        β‘Λβ¨ ap (g β_) (is-invertible.invl invert) β©β‘Λ
g β (f β inv) β‘β¨ assoc g f inv β©β‘
(g β f) β inv β‘β¨ ap (_β inv) p β©β‘
(h β f) β inv β‘Λβ¨ assoc h f inv β©β‘Λ
h β (f β inv) β‘β¨ ap (h  β_) (is-invertible.invl invert) β©β‘
h β id        β‘β¨ idr h β©β‘
h β
where
open is-invertible invert

isoβmonic : (f : a β b) β is-monic (f .to)
isoβmonic f = invertibleβmonic (isoβinvertible f)

isoβepic : (f : a β b) β is-epic (f .to)
isoβepic f = invertibleβepic (isoβinvertible f)


Furthermore, isomorphisms also yield section/retraction pairs.

inversesβto-has-section
: β {f : Hom a b} {g : Hom b a}
β Inverses f g β has-section f
inversesβto-has-section {g = g} inv .section = g
inversesβto-has-section inv .is-section = Inverses.invl inv

inversesβfrom-has-section
: β {f : Hom a b} {g : Hom b a}
β Inverses f g β has-section g
inversesβfrom-has-section {f = f} inv .section = f
inversesβfrom-has-section inv .is-section = Inverses.invr inv

inversesβto-has-retract
: β {f : Hom a b} {g : Hom b a}
β Inverses f g β has-retract f
inversesβto-has-retract {g = g} inv .retract = g
inversesβto-has-retract inv .is-retract = Inverses.invr inv

inversesβfrom-has-retract
: β {f : Hom a b} {g : Hom b a}
β Inverses f g β has-retract g
inversesβfrom-has-retract {f = f} inv .retract = f
inversesβfrom-has-retract inv .is-retract = Inverses.invl inv

invertibleβto-has-section : is-invertible f β has-section f
invertibleβto-has-section f-inv .section = is-invertible.inv f-inv
invertibleβto-has-section f-inv .is-section = is-invertible.invl f-inv

isoβto-has-section : (f : a β b) β has-section (f .to)
isoβto-has-section f .section = f .from
isoβto-has-section f .is-section = f .invl

isoβfrom-has-section : (f : a β b) β has-section (f .from)
isoβfrom-has-section f .section = f .to
isoβfrom-has-section f .is-section = f .invr

isoβto-has-retract : (f : a β b) β has-retract (f .to)
isoβto-has-retract f .retract = f .from
isoβto-has-retract f .is-retract = f .invr

isoβfrom-has-retract : (f : a β b) β has-retract (f .from)
isoβfrom-has-retract f .retract = f .to
isoβfrom-has-retract f .is-retract = f .invl


Using our lemmas about section/retraction pairs from before, we can show that if is a monic retract, then is an iso.

retract-of+monicβinverses
: β {a b} {s : Hom b a} {r : Hom a b}
β r retract-of s
β is-monic r
β Inverses r s
retract-of+monicβinverses ret monic .invl = ret
retract-of+monicβinverses ret monic .invr =
retract-of+monicβsection-of ret monic


We also have a dual result for sections and epis.

section-of+epicβinverses
: β {a b} {s : Hom b a} {r : Hom a b}
β s retract-of r
β is-epic r
β Inverses r s
section-of+epicβinverses sect epic .invl =
section-of+epicβretract-of sect epic
section-of+epicβinverses sect epic .invr = sect

has-retract+epicβinvertible
: β {a b} {f : Hom a b}
β has-retract f
β is-epic f
β is-invertible f
has-retract+epicβinvertible f-ret epic .is-invertible.inv =
f-ret .retract
has-retract+epicβinvertible f-ret epic .is-invertible.inverses =
section-of+epicβinverses (f-ret .is-retract) epic

has-section+monicβinvertible
: β {a b} {f : Hom a b}
β has-section f
β is-monic f
β is-invertible f
has-section+monicβinvertible f-sect monic .is-invertible.inv =
f-sect .section
has-section+monicβinvertible f-sect monic .is-invertible.inverses =
retract-of+monicβinverses (f-sect .is-section) monic


Hom-sets between isomorphic objects are equivalent. Crucially, this allows us to use univalence to transport properties between hom-sets.

isoβhom-equiv
: β {a a' b b'} β a β a' β b β b'
β Hom a b β Hom a' b'
isoβhom-equiv f g = IsoβEquiv $(Ξ» h β g .to β h β f .from) , iso (Ξ» h β g .from β h β f .to ) (Ξ» h β g .to β (g .from β h β f .to) β f .from β‘β¨ cat! C β©β‘ (g .to β g .from) β h β (f .to β f .from) β‘β¨ apβ (Ξ» l r β l β h β r) (g .invl) (f .invl) β©β‘ id β h β id β‘β¨ cat! C β©β‘ h β) (Ξ» h β g .from β (g .to β h β f .from) β f .to β‘β¨ cat! C β©β‘ (g .from β g .to) β h β (f .from β f .to) β‘β¨ apβ (Ξ» l r β l β h β r) (g .invr) (f .invr) β©β‘ id β h β id β‘β¨ cat! C β©β‘ h β)  -- Optimized versions of IsoβHom-equiv which yield nicer results -- if only one isomorphism is needed. dom-isoβhom-equiv : β {a a' b} β a β a' β Hom a b β Hom a' b dom-isoβhom-equiv f = IsoβEquiv$
(Ξ» h β h β f .from) ,
iso (Ξ» h β h β f .to )
(Ξ» h β
(h β f .to) β f .from β‘β¨ sym (assoc _ _ _) β©β‘
h β (f .to β f .from) β‘β¨ ap (h β_) (f .invl) β©β‘
h β id                β‘β¨ idr _ β©β‘
h β)
(Ξ» h β
(h β f .from) β f .to β‘β¨ sym (assoc _ _ _) β©β‘
h β (f .from β f .to) β‘β¨ ap (h β_) (f .invr) β©β‘
h β id                β‘β¨ idr _ β©β‘
h β)

cod-isoβHom-equiv
: β {a b b'} β b β b'
β Hom a b β Hom a b'
cod-isoβHom-equiv f = IsoβEquiv $(Ξ» h β f .to β h) , iso (Ξ» h β f .from β h) (Ξ» h β f .to β f .from β h β‘β¨ assoc _ _ _ β©β‘ (f .to β f .from) β h β‘β¨ ap (_β h) (f .invl) β©β‘ id β h β‘β¨ idl _ β©β‘ h β) (Ξ» h β f .from β f .to β h β‘β¨ assoc _ _ _ β©β‘ (f .from β f .to) β h β‘β¨ ap (_β h) (f .invr) β©β‘ id β h β‘β¨ idl _ β©β‘ h β)  If is invertible, then both pre and post-composition with are equivalences. invertible-precomp-equiv : β {a b c} {f : Hom a b} β is-invertible f β is-equiv {A = Hom b c} (_β f) invertible-precomp-equiv {f = f} f-inv = is-isoβis-equiv$
iso (Ξ» h β h β f-inv.inv)
(Ξ» h β sym (assoc _ _ _) Β·Β· ap (h β_) f-inv.invr Β·Β· idr h)
(Ξ» h β sym (assoc _ _ _) Β·Β· ap (h β_) f-inv.invl Β·Β· idr h)
where module f-inv = is-invertible f-inv

invertible-postcomp-equiv
: β {a b c} {f : Hom b c}
β is-invertible f
β is-equiv {A = Hom a b} (f β_)
invertible-postcomp-equiv {f = f} f-inv = is-isoβis-equiv \$
iso (Ξ» h β f-inv.inv β h)
(Ξ» h β assoc _ _ _ Β·Β· ap (_β h) f-inv.invl Β·Β· idl h)
(Ξ» h β assoc _ _ _ Β·Β· ap (_β h) f-inv.invr Β·Β· idl h)
where module f-inv = is-invertible f-inv