open import Cat.Displayed.Total.Op
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Displayed.Morphism
import Cat.Morphism.Duality
import Cat.Morphism

module Cat.Displayed.Morphism.Duality
  {o  o′ ℓ′}
  { : Precategory o }
  ( : Displayed  o′ ℓ′)

Duality of Displayed Morphism Classes🔗

In this file we prove that morphism classes in a displayed category correspond to their duals in the total opposite displayed category. There is even less mathematical content here than the non-displayed case, just mountains of boilerplate.

We start by showing that displayed monos and epis are dual.

  :  {f : a ℬ^op.↪ b}
   a′ ℰ^op.↪[ f ] b′
   b′ ℰ.↠[ co-mono→epi f ] a′
co-mono[]→epi[] f .mor′ = ℰ^op.mor′ f
co-mono[]→epi[] f .epic′ = ℰ^op.monic′ f

  :  {f : b ℬ.↠ a}
   b′ ℰ.↠[ f ] a′
   a′ ℰ^op.↪[ epi→co-mono f ] b′
epi[]→co-mono[] f .mor′ = ℰ.mor′ f
epi[]→co-mono[] f .monic′ = ℰ.epic′ f

  :  {f : a ℬ^op.↠ b}
   a′ ℰ^op.↠[ f ] b′
   b′ ℰ.↪[ co-epi→mono f ] a′
co-epi[]→mono[] f .mor′ = ℰ^op.mor′ f
co-epi[]→mono[] f .monic′ = ℰ^op.epic′ f

  :  {f : b ℬ.↪ a}
   b′ ℰ.↪[ f ] a′
   a′ ℰ^op.↠[ mono→co-epi f ] b′
mono[]→co-epi[] f .mor′ = ℰ.mor′ f
mono[]→co-epi[] f .epic′ = ℰ.monic′ f

Next, we show the same for weak monos and weak epis.

  :  {f : ℬ.Hom b a}
   ℰ.weak-mono-over f b′ a′
   ℰ^op.weak-epi-over f a′ b′
weak-mono→weak-co-epi f .mor′ = ℰ.mor′ f
weak-mono→weak-co-epi f .weak-epic = ℰ.weak-monic f

  :  {f : ℬ.Hom b a}
   ℰ^op.weak-epi-over f a′ b′
   ℰ.weak-mono-over f b′ a′
weak-co-epi→weak-mono f .mor′ = ℰ^op.mor′ f
weak-co-epi→weak-mono f .weak-monic = ℰ^op.weak-epic f

  :  {f : ℬ.Hom b a}
   ℰ.weak-epi-over f b′ a′
   ℰ^op.weak-mono-over f a′ b′
weak-epi→weak-co-mono f .mor′ = ℰ.mor′ f
weak-epi→weak-co-mono f .weak-monic = ℰ.weak-epic f

  :  {f : ℬ.Hom b a}
   ℰ^op.weak-mono-over f a′ b′
   ℰ.weak-epi-over f b′ a′
weak-co-mono→weak-epi f .mor′ = ℰ^op.mor′ f
weak-co-mono→weak-epi f .weak-epic = ℰ^op.weak-monic f

Next, sections and retractions.

  :  {s : ℬ^op.has-section f}
   ℰ^op.has-section[ s ] f′
   ℰ.has-retract[ co-section→retract s ] f′
co-section[]→retract[] f .retract′ =
  ℰ^op.section′ f
co-section[]→retract[] f .is-retract′ =
  ℰ^′ f

  :  {r : ℬ.has-retract f}
   ℰ.has-retract[ r ] f′
   ℰ^op.has-section[ retract→co-section r ] f′
retract[]→co-section[] f .section′ =
  ℰ.retract′ f
retract[]→co-section[] f .is-section′ =
  ℰ.is-retract′ f

  :  {r : ℬ^op.has-retract f}
   ℰ^op.has-retract[ r ] f′
   ℰ.has-section[ co-retract→section r ] f′
co-retract[]→section[] f .section′ =
  ℰ^op.retract′ f
co-retract[]→section[] f .is-section′ =
  ℰ^′ f

  :  {s : ℬ.has-section f}
   ℰ.has-section[ s ] f′
   ℰ^op.has-retract[ section→co-retract s ] f′
section[]→co-retract[] f .retract′ =
  ℰ.section′ f
section[]→co-retract[] f .is-retract′ =
  ℰ.is-section′ f

We handle vertical sections and retract separately.

  : ℰ^op.has-section↓ f′
   ℰ.has-retract↓ f′
vertical-co-section→vertical-retract f .retract′ =
  ℰ^op.section′ f
vertical-co-section→vertical-retract f .is-retract′ =
  cast[] (ℰ^′ f)

  : ℰ.has-retract↓ f′
   ℰ^op.has-section↓ f′
vertical-retract→vertical-co-section f .section′ =
  ℰ.retract′ f
vertical-retract→vertical-co-section f .is-section′ =
  cast[] (ℰ.is-retract′ f)

  : ℰ^op.has-retract↓ f′
   ℰ.has-section↓ f′
vertical-co-retract→vertical-section f .section′ =
  ℰ^op.retract′ f
vertical-co-retract→vertical-section f .is-section′ =
  cast[] (ℰ^′ f)

  : ℰ.has-section↓ f′
   ℰ^op.has-retract↓ f′
vertical-section→vertical-co-retract f .retract′ =
  ℰ.section′ f
vertical-section→vertical-co-retract f .is-retract′ =
  cast[] (ℰ.is-section′ f)

Now, on to self-duality for invertible morphisms.

  : {i : ℬ^op.Inverses f g}
   ℰ^op.Inverses[ i ] f′ g′
   ℰ.Inverses[ co-inverses→inverses i ] f′ g′
co-inverses[]→inverses[] i .Inverses[_].invl′ =
  ℰ^op.Inverses[_].invr′ i
co-inverses[]→inverses[] i .Inverses[_].invr′ =
  ℰ^op.Inverses[_].invl′ i

  : {i : ℬ.Inverses f g}
   ℰ.Inverses[ i ] f′ g′
   ℰ^op.Inverses[ inverses→co-inverses i ] f′ g′
inverses[]→co-inverses[] i .Inverses[_].invl′ =
  ℰ.Inverses[_].invr′ i
inverses[]→co-inverses[] i .Inverses[_].invr′ =
  ℰ.Inverses[_].invl′ i

  : {i : ℬ^ f}
   ℰ^[ i ] f′
   ℰ.is-invertible[ co-invertible→invertible i ] f′
co-invertible[]→invertible[] i .is-invertible[_].inv′ =
  ℰ^[_].inv′ i
co-invertible[]→invertible[] i .is-invertible[_].inverses′ =
  co-inverses[]→inverses[] (ℰ^[_].inverses′ i)

  : {i : ℬ.is-invertible f}
   ℰ.is-invertible[ i ] f′
   ℰ^[ invertible→co-invertible i ] f′
invertible[]→co-invertible[] i .is-invertible[_].inv′ =
  ℰ.is-invertible[_].inv′ i
invertible[]→co-invertible[] i .is-invertible[_].inverses′ =
  inverses[]→co-inverses[] (ℰ.is-invertible[_].inverses′ i)

  : {f : a ℬ^op.≅ b}
   a′ ℰ^op.≅[ f ] b′
   b′ ℰ.≅[ co-iso→iso f ] a′
co-iso[]→iso[] f .to′ =
  ℰ^′ f
co-iso[]→iso[] f .from′ =
  ℰ^op.from′ f
co-iso[]→iso[] f .inverses′ =
  co-inverses[]→inverses[] (ℰ^op.inverses′ f)

  : {f : b ℬ.≅ a}
   b′ ℰ.≅[ f ] a′
   a′ ℰ^op.≅[ iso→co-iso f ] b′
iso[]→co-iso[] f .to′ =
  ℰ.to′ f
iso[]→co-iso[] f .from′ =
  ℰ.from′ f
iso[]→co-iso[] f .inverses′ =
  inverses[]→co-inverses[] (ℰ.inverses′ f)

We handle the case of vertical isos separately, as the dual of the identity iso isn’t definitionally the identity iso.

  : ℰ^↓ f′  ℰ.is-invertible↓ f′
vertical-co-invertible→vertical-invertible f =
    (ℰ^[_].inv′ f)
    (cast[] (ℰ^[_].invr′ f))
    (cast[] (ℰ^[_].invl′ f))

  : ℰ.is-invertible↓ f′  ℰ^↓ f′
vertical-invertible→vertical-co-invertible f =
    (ℰ.is-invertible[_].inv′ f)
    (cast[] (ℰ.is-invertible[_].invr′ f))
    (cast[] (ℰ.is-invertible[_].invl′ f))

vertical-co-iso→vertical-iso : a′ ℰ^op.≅↓ b′  b′ ℰ.≅↓ a′
vertical-co-iso→vertical-iso f =
    (ℰ^′ f)
    (ℰ^op.from′ f)
    (cast[] (ℰ^op.invr′ f))
    (cast[] (ℰ^op.invl′ f))

vertical-iso→vertical-co-iso : a′ ℰ.≅↓ b′  b′ ℰ^op.≅↓ a′
vertical-iso→vertical-co-iso f =
    (ℰ.to′ f)
    (ℰ.from′ f)
    (cast[] (ℰ.invr′ f))
    (cast[] (ℰ.invl′ f))