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

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 AA to BB, written Aโ†ชBA \hookrightarrow B, 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 AA to BB, written Aโ† BA \twoheadrightarrow B, 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 fโˆ˜gf \circ g is monic, then gg 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 fโˆ˜gf \circ g is epic, then ff 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 s:Bโ†’As : B \to A is a section of another morphism r:Aโ†’Br : A \to B when rโ‹…s=idr \cdot s = id. The intuition for this name is that ss picks out a cross-section of aa from bb. For instance, rr 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 ff has a section, then ff 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 r:Aโ†’Br : A \to B is a retract of another morphism s:Bโ†’As : B \to A when rโ‹…s=idr \cdot s = id. 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 ff has a retract, then ff 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      โˆŽ

Isos๐Ÿ”—

Maps f:Aโ†’Bf : A \to B and g:Bโ†’Ag : B \to A are inverses when we have fโˆ˜gf \circ g and gโˆ˜fg \circ f both equal to the identity. A map f:Aโ†’Bf : A \to B is invertible (or is an isomorphism) when there exists a gg for which ff and gg are inverses. An isomorphism Aโ‰…BA \cong B is a choice of map Aโ†’BA \to B, 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 f:Aโ†’Bf : A \to B with two inverses g:Bโ†’Ag : B \to A and h:Bโ†’Ah : B \to A, then not only are g=hg = h 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-โˆ˜ : {f : Hom a b} {fโปยน : Hom b a} {g : Hom b c} {gโปยน : Hom c b}
           โ†’ Inverses f fโปยน โ†’ Inverses g gโปยน โ†’ Inverses (g โˆ˜ f) (fโปยน โˆ˜ gโปยน)
Inverses-โˆ˜ {f = f} {fโปยน} {g} {gโปยน} finv ginv = record { invl = l ; invr = r } where
  module finv = Inverses finv
  module ginv = Inverses ginv

  abstract
    l : (g โˆ˜ f) โˆ˜ fโปยน โˆ˜ gโปยน โ‰ก id
    l = (g โˆ˜ f) โˆ˜ fโปยน โˆ˜ gโปยน โ‰กโŸจ cat! C โŸฉโ‰ก
        g โˆ˜ (f โˆ˜ fโปยน) โˆ˜ gโปยน โ‰กโŸจ (ฮป i โ†’ g โˆ˜ finv.invl i โˆ˜ gโปยน) โŸฉโ‰ก
        g โˆ˜ id โˆ˜ gโปยน        โ‰กโŸจ cat! C โŸฉโ‰ก
        g โˆ˜ gโปยน             โ‰กโŸจ ginv.invl โŸฉโ‰ก
        id                  โˆŽ

    r : (fโปยน โˆ˜ gโปยน) โˆ˜ g โˆ˜ f โ‰ก id
    r = (fโปยน โˆ˜ gโปยน) โˆ˜ g โˆ˜ f โ‰กโŸจ cat! C โŸฉโ‰ก
        fโปยน โˆ˜ (gโปยน โˆ˜ g) โˆ˜ f โ‰กโŸจ (ฮป i โ†’ fโปยน โˆ˜ ginv.invr i โˆ˜ f) โŸฉโ‰ก
        fโปยน โˆ˜ id โˆ˜ f        โ‰กโŸจ cat! C โŸฉโ‰ก
        fโปยน โˆ˜ f             โ‰กโŸจ finv.invr โŸฉโ‰ก
        id                  โˆŽ

_โˆ˜Iso_ : a โ‰… b โ†’ b โ‰… c โ†’ a โ‰… c
(f โˆ˜Iso g) .to = g .to โˆ˜ f .to
(f โˆ˜Iso g) .from = f .from โˆ˜ g .from
(f โˆ˜Iso g) .inverses = Inverses-โˆ˜ (f .inverses) (g .inverses)

infixr 40 _โˆ˜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-โˆ˜ g-inv.inverses f-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

instance
  H-Level-is-invertible : โˆ€ {f : Hom a b} {n} โ†’ H-Level (is-invertible f) (suc n)
  H-Level-is-invertible = prop-instance is-invertible-is-prop

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 }

โ‰…-is-set : is-set (a โ‰… b)
โ‰…-is-set x y p q = s where
  open _โ‰…_
  open Inverses

  s : p โ‰ก q
  s i j .to = Hom-set _ _ (x .to) (y .to) (ap to p) (ap to q) i j
  s i j .from = Hom-set _ _ (x .from) (y .from) (ap from p) (ap from q) i j
  s i j .inverses =
    is-propโ†’squarep
      (ฮป i j โ†’ Inverses-are-prop {f = Hom-set _ _ (x .to) (y .to) (ap to p) (ap to q) i j}
                                 {g = Hom-set _ _ (x .from) (y .from) (ap from p) (ap from q) i j})
      (ฮป i โ†’ x .inverses) (ฮป i โ†’ p i .inverses) (ฮป i โ†’ q i .inverses) (ฮป i โ†’ y .inverses) i j

instance
  H-Level-โ‰… : โˆ€ {a b} {n} โ†’ H-Level (a โ‰… b) (suc (suc n))
  H-Level-โ‰… = basic-instance 2 โ‰…-is-set

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 = f} {g = 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 = f Isoโปยน} {g = 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

โ†ช-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

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

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 ff is a monic retract, then ff 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

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 ff is invertible, then both pre and post-composition with ff 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