open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Reasoning

module Cat.Displayed.Morphism
  {o β„“ o' β„“'}
  {ℬ : Precategory o β„“}
  (β„° : Displayed ℬ o' β„“')
  where

open Cat.Displayed.Reasoning β„°
open Cat.Reasoning ℬ

private variable
  β„“i : Level
  Ix : Type β„“i
  a b c d : Ob
  aα΅’ bα΅’ cα΅’ : Ix β†’ Ob
  f g h : Hom a b
  a' b' c' : Ob[ a ]
  aα΅’'  bα΅’' cα΅’' : (ix : Ix) β†’ Ob[ bα΅’ ix ]
  f' g' h' : Hom[ f ] a' b'

Displayed morphismsπŸ”—

This module defines the displayed analogs of monomorphisms, epimorphisms, and isomorphisms.

MonosπŸ”—

Displayed monomorphisms have the the same left-cancellation properties as their non-displayed counterparts. However, they must be displayed over a monomorphism in the base.

is-monic[_]
  : βˆ€ {a' : Ob[ a ]} {b' : Ob[ b ]} {f : Hom a b}
  β†’ is-monic f β†’ Hom[ f ] a' b'
  β†’ Type _
is-monic[_] {a = a} {a' = a'} {f = f} mono f' =
  βˆ€ {c c'} {g h : Hom c a}
  β†’ (g' : Hom[ g ] c' a') (h' : Hom[ h ] c' a')
  β†’ (p : f ∘ g ≑ f ∘ h)
  β†’ f' ∘' g' ≑[ p ] f' ∘' h'
  β†’ g' ≑[ mono g h p ] h'

is-monic[]-is-prop
  : βˆ€ {a' : Ob[ a ]} {b' : Ob[ b ]} {f : Hom a b}
  β†’ (mono : is-monic f) β†’ (f' : Hom[ f ] a' b')
  β†’ is-prop (is-monic[ mono ] f')
is-monic[]-is-prop {a' = a'} mono f' mono[] mono[]' i {c' = c'} g' h' p p' =
  is-set→squarep (λ i j → Hom[ mono _ _ p j ]-set c' a')
    refl (mono[] g' h' p p') (mono[]' g' h' p p') refl i

record _β†ͺ[_]_
  {a b} (a' : Ob[ a ]) (f : a β†ͺ b) (b' : Ob[ b ])
  : Type (o βŠ” β„“ βŠ” o' βŠ” β„“')
  where
  no-eta-equality
  field
    mor' : Hom[ f .mor ] a' b'
    monic' : is-monic[ f .monic ] mor'

open _β†ͺ[_]_ public

Weak monosπŸ”—

When working in a displayed setting, we also have weaker versions of the morphism classes we are familiar with, wherein we can only left/right cancel morphisms that are displayed over the same morphism in the base. We denote these morphisms classes as β€œweak”.

is-weak-monic
  : βˆ€ {a' : Ob[ a ]} {b' : Ob[ b ]} {f : Hom a b}
  β†’ Hom[ f ] a' b'
  β†’ Type _
is-weak-monic {a = a} {a' = a'} {f = f} f' =
  βˆ€ {c c'} {g h : Hom c a}
  β†’ (g' : Hom[ g ] c' a') (h' : Hom[ h ] c' a')
  β†’ (p : g ≑ h)
  β†’ f' ∘' g' ≑[ ap (f ∘_) p ] f' ∘' h'
  β†’ g' ≑[ p ] h'

is-weak-monic-is-prop
  : βˆ€ {a' : Ob[ a ]} {b' : Ob[ b ]} {f : Hom a b}
  β†’ (f' : Hom[ f ] a' b')
  β†’ is-prop (is-weak-monic f')
is-weak-monic-is-prop f' = hlevel 1

record weak-mono-over
  {a b} (f : Hom a b) (a' : Ob[ a ]) (b' : Ob[ b ])
  : Type (o βŠ” β„“ βŠ” o' βŠ” β„“')
  where
  no-eta-equality
  field
    mor' : Hom[ f ] a' b'
    weak-monic : is-weak-monic mor'

open weak-mono-over public

Weak monomorphisms are closed under composition, and every displayed monomorphism is weakly monic.

∘-is-weak-monic
  : is-weak-monic f'
  β†’ is-weak-monic g'
  β†’ is-weak-monic (f' ∘' g')
∘-is-weak-monic {f' = f'} {g' = g'} f'-weak-monic g'-weak-monic h' k' p p' =
  g'-weak-monic h' k' p $
  f'-weak-monic (g' ∘' h') (g' ∘' k') (apβ‚‚ _∘_ refl p) $ begin[]
    f' ∘' g' ∘' h'   ≑[]⟨ assoc' f' g' h' βŸ©β‰‘[]
    (f' ∘' g') ∘' h' ≑[]⟨ p' βŸ©β‰‘[]
    (f' ∘' g') ∘' k' ≑[]˘⟨ assoc' f' g' k' βŸ©β‰‘[]˘
    f' ∘' g' ∘' k'   ∎[]

is-monic[]β†’is-weak-monic
  : {f-monic : is-monic f}
  β†’ is-monic[ f-monic ] f'
  β†’ is-weak-monic f'
is-monic[]β†’is-weak-monic f'-monic g' h' p p' =
  cast[] $ f'-monic g' h' (apβ‚‚ _∘_ refl p) p'

If is weakly monic, then so is 

weak-monic-cancell
  : is-weak-monic (f' ∘' g')
  β†’ is-weak-monic g'
weak-monic-cancell {f' = f'} {g' = g'} fg-weak-monic h' k' p p' =
  fg-weak-monic h' k' p (extendr' _ p')

Moreover, postcomposition with a weak monomorphism is an embedding. This suggests that weak monomorphisms are the β€œright” notion of monomorphisms in displayed categories.

weak-monic-postcomp-embedding
  : {f : Hom b c} {g : Hom a b}
  β†’ {f' : Hom[ f ] b' c'}
  β†’ is-weak-monic f'
  β†’ is-embedding {A = Hom[ g ] a' b'} (f' ∘'_)
weak-monic-postcomp-embedding {f' = f'} f'-weak-monic =
  injectiveβ†’is-embedding (hlevel 2) (f' ∘'_) Ξ» {g'} {h'} β†’ f'-weak-monic g' h' refl

Jointly weak monosπŸ”—

We can generalize the notion of weak monomorphisms to families of morphisms, which yields a displayed version of a jointly monic family.

A family of displayed morphisms is jointly monic if for all if for all 

is-jointly-weak-monic
  : {fα΅’ : (ix : Ix) β†’ Hom a (bα΅’ ix)}
  β†’ (fα΅’' : (ix : Ix) β†’ Hom[ fα΅’ ix ] a' (bα΅’' ix))
  β†’ Type _
is-jointly-weak-monic {a = a} {a' = a'} {fα΅’ = fα΅’} fα΅’' =
  βˆ€ {x x'} {g h : Hom x a}
  β†’ (g' : Hom[ g ] x' a') (h' : Hom[ h ] x' a')
  β†’ (p : g ≑ h)
  β†’ (βˆ€ ix β†’ fα΅’' ix ∘' g' ≑[ ap (fα΅’ ix ∘_) p ] fα΅’' ix ∘' h')
  β†’ g' ≑[ p ] h'

Jointly weak monic families are closed under precomposition with weak monos.

∘-is-jointly-weak-monic
  : {fα΅’ : (ix : Ix) β†’ Hom a (bα΅’ ix)}
  β†’ {fα΅’' : (ix : Ix) β†’ Hom[ fα΅’ ix ] a' (bα΅’' ix)}
  β†’ is-jointly-weak-monic fα΅’'
  β†’ is-weak-monic g'
  β†’ is-jointly-weak-monic (Ξ» ix β†’ fα΅’' ix ∘' g')
∘-is-jointly-weak-monic {g' = g'} {fᡒ' = fᡒ'} fᡒ'-joint-mono g'-joint-mono h' h'' p p' =
  g'-joint-mono h' h'' p $
  fα΅’'-joint-mono (g' ∘' h') (g' ∘' h'') (apβ‚‚ _∘_ refl p) Ξ» ix β†’ begin[]
    fα΅’' ix ∘' g' ∘' h'    ≑[]⟨ assoc' (fα΅’' ix) g' h' βŸ©β‰‘[]
    (fα΅’' ix ∘' g') ∘' h'  ≑[]⟨ p' ix βŸ©β‰‘[]
    (fα΅’' ix ∘' g') ∘' h'' ≑[]˘⟨ assoc' (fα΅’' ix) g' h'' βŸ©β‰‘[]˘
    fᡒ' ix ∘' g' ∘' h''   ∎[]

Similarly, if is a jointly weak monic family, then must be a weak mono.

jointly-weak-monic-cancell
  : {fα΅’ : (ix : Ix) β†’ Hom a (bα΅’ ix)}
  β†’ {fα΅’' : (ix : Ix) β†’ Hom[ fα΅’ ix ] a' (bα΅’' ix)}
  β†’ is-jointly-weak-monic (Ξ» ix β†’ fα΅’' ix ∘' g')
  β†’ is-weak-monic g'
jointly-weak-monic-cancell fα΅’'-joint-mono h' h'' p p' =
  fα΅’'-joint-mono h' h'' p Ξ» _ β†’ extendr' (apβ‚‚ _∘_ refl p) p'

EpisπŸ”—

Displayed epimorphisms are defined in a similar fashion.

is-epic[_]
  : βˆ€ {a' : Ob[ a ]} {b' : Ob[ b ]} {f : Hom a b}
  β†’ is-epic f β†’ Hom[ f ] a' b'
  β†’ Type _
is-epic[_] {b = b} {b' = b'} {f = f} epi f' =
  βˆ€ {c} {c'} {g h : Hom b c}
  β†’ (g' : Hom[ g ] b' c') (h' : Hom[ h ] b' c')
  β†’ (p : g ∘ f ≑ h ∘ f)
  β†’ g' ∘' f' ≑[ p ] h' ∘' f'
  β†’ g' ≑[ epi g h p ] h'

is-epic[]-is-prop
  : βˆ€ {a' : Ob[ a ]} {b' : Ob[ b ]} {f : Hom a b}
  β†’ (epi : is-epic f) β†’ (f' : Hom[ f ] a' b')
  β†’ is-prop (is-epic[ epi ] f')
is-epic[]-is-prop {b' = b'} epi f' epi[] epi[]' i {c' = c'} g' h' p p' =
  is-set→squarep (λ i j → Hom[ epi _ _ p j ]-set b' c')
    refl (epi[] g' h' p p') (epi[]' g' h' p p') refl i

record _β† [_]_
  {a b} (a' : Ob[ a ]) (f : a β†  b) (b' : Ob[ b ])
  : Type (o βŠ” β„“ βŠ” o' βŠ” β„“')
  where
  no-eta-equality
  field
    mor' : Hom[ f .mor ] a' b'
    epic' : is-epic[ f .epic ] mor'

open _β† [_]_ public

Weak episπŸ”—

We can define a weaker notion of epis that is dual to the definition of a weak mono.

is-weak-epic
  : βˆ€ {a' : Ob[ a ]} {b' : Ob[ b ]} {f : Hom a b}
  β†’ Hom[ f ] a' b'
  β†’ Type _
is-weak-epic {b = b} {b' = b'} {f = f} f' =
  βˆ€ {c c'} {g h : Hom b c}
  β†’ (g' : Hom[ g ] b' c') (h' : Hom[ h ] b' c')
  β†’ (p : g ≑ h)
  β†’ g' ∘' f' ≑[ ap (_∘ f) p ] h' ∘' f'
  β†’ g' ≑[ p ] h'

is-weak-epic-is-prop
  : βˆ€ {a' : Ob[ a ]} {b' : Ob[ b ]} {f : Hom a b}
  β†’ (f' : Hom[ f ] a' b')
  β†’ is-prop (is-weak-epic f')
is-weak-epic-is-prop f' = hlevel 1

record weak-epi-over
  {a b} (f : Hom a b) (a' : Ob[ a ]) (b' : Ob[ b ])
  : Type (o βŠ” β„“ βŠ” o' βŠ” β„“')
  where
  no-eta-equality
  field
    mor' : Hom[ f ] a' b'
    weak-epic : is-weak-epic mor'

open weak-epi-over public

SectionsπŸ”—

Following the same pattern as before, we define a notion of displayed sections.

_section-of[_]_
  : βˆ€ {x y} {s : Hom y x} {r : Hom x y}
  β†’ βˆ€ {x' y'} (s' : Hom[ s ] y' x') β†’ s section-of r β†’ (r' : Hom[ r ] x' y')
  β†’ Type _
s' section-of[ p ] r' = r' ∘' s' ≑[ p ] id'

record has-section[_]
  {x y x' y'} {r : Hom x y} (sect : has-section r) (r' : Hom[ r ] x' y')
  : Type β„“'
  where
  no-eta-equality
  field
    section' : Hom[ sect .section ] y' x'
    is-section' : section' section-of[ sect .is-section ] r'

open has-section[_] public

We also distinguish the sections that are displayed over the identity morphism; these are known as β€œvertical sections”.

_section-of↓_
  : βˆ€ {x} {x' x'' : Ob[ x ]} (s' : Hom[ id ] x'' x') β†’ (r : Hom[ id ] x' x'')
  β†’ Type _
s' section-of↓ r' = s' section-of[ idl id ] r'

has-section↓ : βˆ€ {x} {x' x'' : Ob[ x ]} (r' : Hom[ id ] x' x'') β†’ Type _
has-section↓ r' = has-section[ id-has-section ] r'

RetractsπŸ”—

We can do something similar for retracts.

_retract-of[_]_
  : βˆ€ {x y} {s : Hom y x} {r : Hom x y}
  β†’ βˆ€ {x' y'} (r' : Hom[ r ] x' y') β†’ r retract-of s β†’ (s' : Hom[ s ] y' x')
  β†’ Type _
r' retract-of[ p ] s' = r' ∘' s' ≑[ p ] id'


record has-retract[_]
  {x y x' y'} {s : Hom x y} (ret : has-retract s) (s' : Hom[ s ] x' y')
  : Type β„“'
  where
  no-eta-equality
  field
    retract' : Hom[ ret .retract ] y' x'
    is-retract' : retract' retract-of[ ret .is-retract ] s'

open has-retract[_] public

We also define vertical retracts in a similar manner as before.

_retract-of↓_
  : βˆ€ {x} {x' x'' : Ob[ x ]} (r' : Hom[ id ] x' x'') β†’ (s : Hom[ id ] x'' x')
  β†’ Type _
r' retract-of↓ s' = r' retract-of[ idl id ] s'

has-retract↓ : βˆ€ {x} {x' x'' : Ob[ x ]} (s' : Hom[ id ] x'' x') β†’ Type _
has-retract↓ s' = has-retract[ id-has-retract ] s'

IsosπŸ”—

Displayed isomorphisms must also be defined over isomorphisms in the base.

record Inverses[_]
  {a b a' b'} {f : Hom a b} {g : Hom b a}
  (inv : Inverses f g)
  (f' : Hom[ f ] a' b') (g' : Hom[ g ] b' a')
  : Type β„“'
  where
  no-eta-equality
  field
    invl' : f' ∘' g' ≑[ Inverses.invl inv ] id'
    invr' : g' ∘' f' ≑[ Inverses.invr inv ] id'

record is-invertible[_]
  {a b a' b'} {f : Hom a b}
  (f-inv : is-invertible f)
  (f' : Hom[ f ] a' b')
  : Type β„“'
  where
  no-eta-equality
  field
    inv' : Hom[ is-invertible.inv f-inv ] b' a'
    inverses' : Inverses[ is-invertible.inverses f-inv ] f' inv'

  open Inverses[_] inverses' public

record _β‰…[_]_
  {a b} (a' : Ob[ a ]) (i : a β‰… b) (b' : Ob[ b ])
  : Type β„“'
  where
  no-eta-equality
  field
    to' : Hom[ i .to ] a' b'
    from' : Hom[ i .from ] b' a'
    inverses' : Inverses[ i .inverses ] to' from'

  open Inverses[_] inverses' public

Isomorphism[_] : βˆ€ {a b} (i : a β‰… b) (a' : Ob[ a ]) (b' : Ob[ b ]) β†’ Type β„“'
Isomorphism[ i ] a' b' = a' β‰…[ i ] b'

open _β‰…[_]_ public
{-# INLINE _β‰…[_]_.constructor #-}

Since isomorphisms over the identity map will be of particular importance, we also define their own type: they are the vertical isomorphisms.

_≅↓_ : {x : Ob} (A B : Ob[ x ]) β†’ Type β„“'
_≅↓_ = _β‰…[ id-iso ]_

is-invertible↓ : {x : Ob} {x' x'' : Ob[ x ]} β†’ Hom[ id ] x' x'' β†’ Type _
is-invertible↓ = is-invertible[ id-invertible ]

make-invertible↓
  : βˆ€ {x} {x' x'' : Ob[ x ]} {f' : Hom[ id ] x' x''}
  β†’ (g' : Hom[ id ] x'' x')
  β†’ f' ∘' g' ≑[ idl _ ] id'
  β†’ g' ∘' f' ≑[ idl _ ] id'
  β†’ is-invertible↓ f'
make-invertible↓ g' p q .is-invertible[_].inv' = g'
make-invertible↓ g' p q .is-invertible[_].inverses' .Inverses[_].invl' = p
make-invertible↓ g' p q .is-invertible[_].inverses' .Inverses[_].invr' = q

Like their non-displayed counterparts, existence of displayed inverses is a proposition.

Inverses[]-are-prop
  : βˆ€ {a b a' b'} {f : Hom a b} {g : Hom b a}
  β†’ (inv : Inverses f g)
  β†’ (f' : Hom[ f ] a' b') (g' : Hom[ g ] b' a')
  β†’ is-prop (Inverses[ inv ] f' g')
Inverses[]-are-prop inv f' g' inv[] inv[]' i .Inverses[_].invl' =
  is-set→squarep (λ i j → Hom[ Inverses.invl inv j ]-set _ _)
    refl (Inverses[_].invl' inv[]) (Inverses[_].invl' inv[]') refl i
Inverses[]-are-prop inv f' g' inv[] inv[]' i .Inverses[_].invr' =
  is-set→squarep (λ i j → Hom[ Inverses.invr inv j ]-set _ _)
    refl (Inverses[_].invr' inv[]) (Inverses[_].invr' inv[]') refl i

is-invertible[]-is-prop
  : βˆ€ {a b a' b'} {f : Hom a b}
  β†’ (f-inv : is-invertible f)
  β†’ (f' : Hom[ f ] a' b')
  β†’ is-prop (is-invertible[ f-inv ] f')
is-invertible[]-is-prop inv f' p q = path where
  module inv = is-invertible inv
  module p = is-invertible[_] p
  module q = is-invertible[_] q

  inv≑inv' : p.inv' ≑ q.inv'
  inv≑inv' =
    p.inv'                           β‰‘βŸ¨ shiftr (insertr inv.invl) (insertr' _ q.invl') βŸ©β‰‘
    hom[] ((p.inv' ∘' f') ∘' q.inv') β‰‘βŸ¨ weave _ (eliml inv.invr) refl (eliml' _ p.invr') βŸ©β‰‘
    hom[] q.inv'                     β‰‘βŸ¨ liberate _ βŸ©β‰‘
    q.inv' ∎

  path : p ≑ q
  path i .is-invertible[_].inv' = inv≑inv' i
  path i .is-invertible[_].inverses' =
    is-propβ†’pathp (Ξ» i β†’ Inverses[]-are-prop inv.inverses f' (inv≑inv' i))
      p.inverses' q.inverses' i

make-iso[_]
  : βˆ€ {a b a' b'}
  β†’ (iso : a β‰… b)
  β†’ (f' : Hom[ iso .to ] a' b') (g' : Hom[ iso .from ] b' a')
  β†’ f' ∘' g' ≑[ iso .invl ] id'
  β†’ g' ∘' f' ≑[ iso .invr ] id'
  β†’ a' β‰…[ iso ] b'
{-# INLINE make-iso[_] #-}
make-iso[ inv ] f' g' p q = record { to' = f' ; from' = g' ; inverses' = record { invl' = p ; invr' = q }}

make-invertible[_]
  : βˆ€ {a b a' b'} {f : Hom a b} {f' : Hom[ f ] a' b'}
  β†’ (f-inv : is-invertible f)
  β†’ (f-inv' : Hom[ is-invertible.inv f-inv ] b' a')
  β†’ f' ∘' f-inv' ≑[ is-invertible.invl f-inv ] id'
  β†’ f-inv' ∘' f' ≑[ is-invertible.invr f-inv ] id'
  β†’ is-invertible[ f-inv ] f'
make-invertible[ f-inv ] f-inv' p q .is-invertible[_].inv' = f-inv'
make-invertible[ f-inv ] f-inv' p q .is-invertible[_].inverses' .Inverses[_].invl' = p
make-invertible[ f-inv ] f-inv' p q .is-invertible[_].inverses' .Inverses[_].invr' = q

make-vertical-iso
  : βˆ€ {x} {x' x'' : Ob[ x ]}
  β†’ (f' : Hom[ id ] x' x'') (g' : Hom[ id ] x'' x')
  β†’ f' ∘' g' ≑[ idl _ ] id'
  β†’ g' ∘' f' ≑[ idl _ ] id'
  β†’ x' ≅↓ x''
make-vertical-iso = make-iso[ id-iso ]

invertible[]β†’iso[]
  : βˆ€ {a b a' b'} {f : Hom a b} {f' : Hom[ f ] a' b'}
  β†’ {i : is-invertible f}
  β†’ is-invertible[ i ] f'
  → a' ≅[ invertible→iso f i ] b'
invertible[]β†’iso[] {f' = f'} i = make-iso[ _ ] f'
  (is-invertible[_].inv' i)
  (is-invertible[_].invl' i)
  (is-invertible[_].invr' i)

is-invertible[]-inverse
  : βˆ€ {x y x' y'} {f : Hom x y} {f-inv : is-invertible f}
    {f' : Hom[ f ] x' y'} (f'-inv : is-invertible[ f-inv ] f')
  β†’ is-invertible[ is-invertible-inverse f-inv ] (f'-inv .is-invertible[_].inv')
is-invertible[]-inverse f'-inv =
  record { inv' = _ ; inverses' = record { invl' = g'.invr' ; invr' = g'.invl' } }
  where module g' = Inverses[_] (f'-inv .is-invertible[_].inverses')

iso[]β†’invertible[]
  : βˆ€ {a b a' b'}
  β†’ {i : a β‰… b}
  β†’ (i' : a' β‰…[ i ] b')
  → is-invertible[ iso→invertible i ] (i' .to')
iso[]β†’invertible[] {i = i} i' =
  make-invertible[ (iso→invertible i) ] (i' .from') (i' .invl') (i' .invr')

β‰…[]-path
  : {x y : Ob} {A : Ob[ x ]} {B : Ob[ y ]} {f : x β‰… y}
    {p q : A β‰…[ f ] B}
  β†’ p .to' ≑ q .to'
  β†’ p ≑ q
β‰…[]-path {f = f} {p = p} {q = q} a = it where
  p' : PathP (λ i → is-invertible[ iso→invertible f ] (a i))
    (record { inv' = p .from' ; inverses' = p .inverses' })
    (record { inv' = q .from' ; inverses' = q .inverses' })
  p' = is-prop→pathp (λ i → is-invertible[]-is-prop _ (a i)) _ _

  it : p ≑ q
  it i .to'       = a i
  it i .from'     = p' i .is-invertible[_].inv'
  it i .inverses' = p' i .is-invertible[_].inverses'

instance
  Extensional-β‰…[]
    : βˆ€ {β„“r} {x y : Ob} {x' : Ob[ x ]} {y' : Ob[ y ]} {f : x β‰… y}
    β†’ ⦃ sa : Extensional (Hom[ f .to ] x' y') β„“r ⦄
    β†’ Extensional (x' β‰…[ f ] y') β„“r
  Extensional-β‰…[] ⦃ sa ⦄ = injectionβ†’extensional! β‰…[]-path sa

As in the non-displayed case, the identity isomorphism is always an iso. In fact, it is a vertical iso!

id-iso↓ : βˆ€ {x} {x' : Ob[ x ]} β†’ x' ≅↓ x'
id-iso↓ = make-iso[ id-iso ] id' id' (idl' id') (idl' id')

We take the opportunity to define the displayed counterpart to path→iso:

path[_]β†’iso[]
  : βˆ€ {a} {b} (p : a ≑ b) {a'} {b'} (q : PathP (Ξ» i β†’ Ob[ p i ]) a' b')
  → a' ≅[ path→iso p ] b'
path[ p ]β†’iso[] {a'} {b'} p' = transport
  (Ξ» i β†’ Isomorphism[ id=pathβ†’iso i ] a' (p' i)) id-iso↓
  where
    id=path→iso : PathP (λ i → _ ≅ p i) id-iso (path→iso p)
    id=path→iso = transport-filler (λ i → _ ≅ p i) id-iso

We also have that displayed isos compose

Inverses-∘'
  : βˆ€ {a b c f g f⁻¹ g⁻¹ finv ginv} {a : Ob[ a ]} {b : Ob[ b ]} {c : Ob[ c ]}
    {f' : Hom[ f ] a b} {f'⁻¹ : Hom[ f⁻¹ ] b a}
    {g' : Hom[ g ] b c} {g'⁻¹ : Hom[ g⁻¹ ] c b}
  β†’ Inverses[ finv ] f' f'⁻¹ β†’ Inverses[ ginv ] g' g'⁻¹
  β†’ Inverses[ Inverses-∘ ginv finv ] (g' ∘' f') (f'⁻¹ ∘' g'⁻¹)
Inverses-∘' {finv = finv} {ginv} {f' = f'} {f'⁻¹} {g'} {g'⁻¹} finv' ginv' = record
  { invl' = l' ; invr' = r' } where
    module gfinv = Inverses (Inverses-∘ ginv finv)
    module finv' = Inverses[_] finv'
    module ginv' = Inverses[_] ginv'

    l' : (g' ∘' f') ∘' f'⁻¹ ∘' g'⁻¹ ≑[ gfinv.invl ] id'
    l' = begin[]
      (g' ∘' f') ∘' f'⁻¹ ∘' g'⁻¹    ≑[]⟨ assoc' (g' ∘' f') f'⁻¹ g'⁻¹ βŸ©β‰‘[]
      ((g' ∘' f') ∘' f'⁻¹) ∘' g'⁻¹  ≑[]˘⟨ assoc' g' f' f'⁻¹ ⟩∘'⟨refl βŸ©β‰‘[]˘
      (g' ∘' (f' ∘' f'⁻¹)) ∘' g'⁻¹  ≑[]⟨ (refl⟩∘'⟨ finv'.invl') ⟩∘'⟨refl βŸ©β‰‘[]
      (g' ∘' id') ∘' g'⁻¹           ≑[]⟨ (idr' g') ⟩∘'⟨refl βŸ©β‰‘[]
      g' ∘' g'⁻¹                    ≑[]⟨ ginv'.invl' βŸ©β‰‘[]
      id'                           ∎[]

    r' : (f'⁻¹ ∘' g'⁻¹) ∘' g' ∘' f' ≑[ gfinv.invr ] id'
    r' = begin[]
      (f'⁻¹ ∘' g'⁻¹) ∘' g' ∘' f'    ≑[]⟨ assoc' (f'⁻¹ ∘' g'⁻¹) g' f' βŸ©β‰‘[]
      ((f'⁻¹ ∘' g'⁻¹) ∘' g') ∘' f'  ≑[]˘⟨ assoc' f'⁻¹ g'⁻¹ g' ⟩∘'⟨refl βŸ©β‰‘[]˘
      (f'⁻¹ ∘' (g'⁻¹ ∘' g')) ∘' f'  ≑[]⟨ (refl⟩∘'⟨ ginv'.invr') ⟩∘'⟨refl βŸ©β‰‘[]
      (f'⁻¹ ∘' id') ∘' f'           ≑[]⟨ (idr' f'⁻¹) ⟩∘'⟨refl βŸ©β‰‘[]
      f'⁻¹ ∘' f'                    ≑[]⟨ finv'.invr' βŸ©β‰‘[]
      id'                           ∎[]

_∘Iso'_
  : βˆ€ {a b c f g} {a' : Ob[ a ]} {b' : Ob[ b ]} {c' : Ob[ c ]}
  β†’ b' β‰…[ g ] c' β†’ a' β‰…[ f ] b' β†’ a' β‰…[ g ∘Iso f ] c'
(g' ∘Iso' f') .to' = g' .to' ∘' f' .to'
(g' ∘Iso' f') .from' = f' .from' ∘' g' .from'
(g' ∘Iso' f') .inverses' = Inverses-∘' (f' .inverses') (g' .inverses')

_Iso[]⁻¹
  : βˆ€ {a b a' b'} {i : a β‰… b}
  β†’ a' β‰…[ i ] b'
  β†’ b' β‰…[ i Iso⁻¹ ] a'
(i' Iso[]⁻¹) .to' = i' .from'
(i' Iso[]⁻¹) .from' = i' .to'
(i' Iso[]⁻¹) .inverses' .Inverses[_].invl' = i' .invr'
(i' Iso[]⁻¹) .inverses' .Inverses[_].invr' = i' .invl'

Isomorphisms are also instances of sections and retracts.

inverses[]β†’to-has-section[]
  : βˆ€ {f : Hom a b} {g : Hom b a}
  β†’ βˆ€ {a' b'} {f' : Hom[ f ] a' b'} {g' : Hom[ g ] b' a'}
  β†’ {inv : Inverses f g} β†’ Inverses[ inv ] f' g'
  → has-section[ inverses→to-has-section inv ] 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}
  β†’ βˆ€ {a' b'} {f' : Hom[ f ] a' b'} {g' : Hom[ g ] b' a'}
  β†’ {inv : Inverses f g} β†’ Inverses[ inv ] f' g'
  → has-section[ inverses→from-has-section inv ] 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}
  β†’ βˆ€ {a' b'} {f' : Hom[ f ] a' b'} {g' : Hom[ g ] b' a'}
  β†’ {inv : Inverses f g} β†’ Inverses[ inv ] f' g'
  → has-retract[ inverses→to-has-retract inv ] 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}
  β†’ βˆ€ {a' b'} {f' : Hom[ f ] a' b'} {g' : Hom[ g ] b' a'}
  β†’ {inv : Inverses f g} β†’ Inverses[ inv ] f' g'
  → has-retract[ inverses→from-has-retract inv ] g'
inverses[]β†’from-has-retract[] {f' = f'} inv' .retract' = f'
inverses[]β†’from-has-retract[] inv' .is-retract' = Inverses[_].invl' inv'

module _
  {f : Hom a b} {f' : Hom[ f ] a' b'}
  {f-inv : is-invertible f}
  (f'-inv : is-invertible[ f-inv ] f')
  where
  private module f' = is-invertible[_] f'-inv

  invertible[]→to-has-section[] : has-section[ invertible→to-has-section f-inv ] f'
  invertible[]β†’to-has-section[] .section' = f'.inv'
  invertible[]β†’to-has-section[] .is-section' = f'.invl'

  invertible[]→from-has-section[] : has-section[ invertible→from-has-section f-inv ] f'.inv'
  invertible[]β†’from-has-section[] .section' = f'
  invertible[]β†’from-has-section[] .is-section' = f'.invr'

  invertible[]→to-has-retract[] : has-retract[ invertible→to-has-retract f-inv ] f'
  invertible[]β†’to-has-retract[] .retract' = f'.inv'
  invertible[]β†’to-has-retract[] .is-retract' = f'.invr'

  invertible[]→from-has-retract[] : has-retract[ invertible→from-has-retract f-inv ] f'.inv'
  invertible[]β†’from-has-retract[] .retract' = f'
  invertible[]β†’from-has-retract[] .is-retract' = f'.invl'

  invertible[]→monic[] : is-monic[ invertible→monic f-inv ] f'
  invertible[]β†’monic[] g' h' p p' =
    cast[] $ introl[] _ f'.invr' βˆ™[] extendr[] _ p' βˆ™[] eliml[] _ f'.invr'


iso[]β†’to-has-section[]
  : {f : a β‰… b} β†’ (f' : a' β‰…[ f ] b')
  → has-section[ iso→to-has-section f ] (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} β†’ (f' : a' β‰…[ f ] b')
  → has-section[ iso→from-has-section f ] (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} β†’ (f' : a' β‰…[ f ] b')
  → has-retract[ iso→to-has-retract f ] (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} β†’ (f' : a' β‰…[ f ] b')
  → has-retract[ iso→from-has-retract f ] (f' .from')
iso[]β†’from-has-retract[] f' .retract' = f' .to'
iso[]β†’from-has-retract[] f' .is-retract' = f' .invl'

The following is a displayed counterpart to inverse-uniquβ‚€.

abstract
  inverse-uniqueβ‚€'
    : βˆ€ {x b} {f g : x β‰… b} {r : f .to ≑ g .to}
      {x' : Ob[ x ]} {b' : Ob[ b ]} (f' : x' β‰…[ f ] b') (g' : x' β‰…[ g ] b')
      (r' : f' .to' ≑[ r ] g' .to')
    β†’ f' .from' ≑[ inverse-uniqueβ‚€ f g r ] g' .from'
  inverse-uniqueβ‚€' f' g' r' = begin[]
    f' .from'                           ≑[]˘⟨ apd (Ξ» _ β†’ f' .from' ∘'_) (g' .invl') βˆ™[] idr' _ βŸ©β‰‘[]˘
    f' .from' ∘' g' .to' ∘' g' .from'   ≑[]⟨ assoc' (f' .from') (g' .to') (g' .from') βŸ©β‰‘[]
    (f' .from' ∘' g' .to') ∘' g' .from' ≑[]⟨ (apd (Ξ» _ β†’ _∘' g' .from') (apd (Ξ» _ β†’ f' .from' ∘'_) (symP r') βˆ™[] f' .invr')) βˆ™[] idl' _ βŸ©β‰‘[]
    g' .from'                           ∎[]

module _
  {f : Hom a b} {f' : Hom[ f ] a' b'}
  {f-section : has-section f}
  (f-section' : has-section[ f-section ] f')
  where abstract
  private
    module f = has-section f-section
    module f' = has-section[_] f-section'

  pre-section'
    : βˆ€ {h₁ : Hom b c} {hβ‚‚ : Hom a c}
    β†’ {p : h₁ ∘ f ≑ hβ‚‚} {q : h₁ ≑ hβ‚‚ ∘ f.section}
    β†’ {h₁' : Hom[ h₁ ] b' c'} {hβ‚‚' : Hom[ hβ‚‚ ] a' c'}
    β†’ h₁' ∘' f' ≑[ p ] hβ‚‚'
    β†’ h₁' ≑[ q ] hβ‚‚' ∘' f'.section'
  pre-section' {p = p} {q = q} {h₁' = h₁'} {hβ‚‚' = hβ‚‚'} p' =
    symP (rswizzle' (sym p) f.is-section (symP p') f'.is-section')

  pre-section[]
    : βˆ€ {h₁ : Hom b c} {hβ‚‚ : Hom a c}
    β†’ {p : h₁ ∘ f ≑ hβ‚‚}
    β†’ {h₁' : Hom[ h₁ ] b' c'} {hβ‚‚' : Hom[ hβ‚‚ ] a' c'}
    β†’ h₁' ∘' f' ≑[ p ] hβ‚‚'
    β†’ h₁' ≑[ pre-section f-section p ] hβ‚‚' ∘' f'.section'
  pre-section[] = pre-section'

  post-section'
    : βˆ€ {h₁ : Hom c b} {hβ‚‚ : Hom c a}
    β†’ {p : f.section ∘ h₁ ≑ hβ‚‚} {q : h₁ ≑ f ∘ hβ‚‚}
    β†’ {h₁' : Hom[ h₁ ] c' b'} {hβ‚‚' : Hom[ hβ‚‚ ] c' a'}
    β†’ f'.section' ∘' h₁' ≑[ p ] hβ‚‚'
    β†’ h₁' ≑[ q ] f' ∘' hβ‚‚'
  post-section' {p = p} {q = q} {h₁' = h₁'} {hβ‚‚' = hβ‚‚'} p' =
    symP (lswizzle' (sym p) f.is-section (symP p') f'.is-section')

  post-section[]
    : βˆ€ {h₁ : Hom c b} {hβ‚‚ : Hom c a}
    β†’ {p : f.section ∘ h₁ ≑ hβ‚‚}
    β†’ {h₁' : Hom[ h₁ ] c' b'} {hβ‚‚' : Hom[ hβ‚‚ ] c' a'}
    β†’ f'.section' ∘' h₁' ≑[ p ] hβ‚‚'
    β†’ h₁' ≑[ post-section f-section p ] f' ∘' hβ‚‚'
  post-section[] = post-section'