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' ℓ')
  where

private
  module ℬ = Cat.Morphism ℬ
  module ℬ^op = Cat.Morphism (ℬ ^op)
  module ℰ = Cat.Displayed.Morphism ℰ
  module ℰ^op = Cat.Displayed.Morphism (ℰ ^total-op)

  open Displayed ℰ
  open Cat.Morphism.Duality ℬ
  open Cat.Displayed.Reasoning ℰ

  open Cat.Displayed.Morphism

private variable
  a b c d : ℬ.Ob
  f g : ℬ.Hom a b
  a' b' c' d' : Ob[ a ]
  f' g' : Hom[ f ] a' b'

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.

co-mono[]→epi[]
  : ∀ {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

epi[]→co-mono[]
  : ∀ {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

co-epi[]→mono[]
  : ∀ {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

mono[]→co-epi[]
  : ∀ {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.

weak-mono→weak-co-epi
  : ∀ {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

weak-co-epi→weak-mono
  : ∀ {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

weak-epi→weak-co-mono
  : ∀ {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

weak-co-mono→weak-epi
  : ∀ {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.

co-section[]→retract[]
  : ∀ {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' =
  ℰ^op.is-section' f

retract[]→co-section[]
  : ∀ {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

co-retract[]→section[]
  : ∀ {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' =
  ℰ^op.is-retract' f

section[]→co-retract[]
  : ∀ {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.

vertical-co-section→vertical-retract
  : ℰ^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[] (ℰ^op.is-section' f)

vertical-retract→vertical-co-section
  : ℰ.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)

vertical-co-retract→vertical-section
  : ℰ^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[] (ℰ^op.is-retract' f)

vertical-section→vertical-co-retract
  : ℰ.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.

co-inverses[]→inverses[]
  : {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

inverses[]→co-inverses[]
  : {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

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

invertible[]→co-invertible[]
  : {i : ℬ.is-invertible f}
  → ℰ.is-invertible[ i ] f'
  → ℰ^op.is-invertible[ 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)

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

iso[]→co-iso[]
  : {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.

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

vertical-invertible→vertical-co-invertible
  : ℰ.is-invertible↓ f' → ℰ^op.is-invertible↓ f'
vertical-invertible→vertical-co-invertible f =
  ℰ^op.make-invertible↓
    (ℰ.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 =
  ℰ.make-vertical-iso
    (ℰ^op.to' 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 =
  ℰ^op.make-vertical-iso
    (ℰ.to' f)
    (ℰ.from' f)
    (cast[] (ℰ.invr' f))
    (cast[] (ℰ.invl' f))