open import Cat.Functor.Coherence
open import Cat.Functor.Kan.Base
open import Cat.Prelude
module Cat.Functor.Kan.Duality where
private
  variable
    o ā„“ : Level
    C C' D : Precategory o ā„“

Duality for Kan extensionsšŸ”—

Left Kan extensions are dual to right Kan extensions. This is straightforward enough to prove, but does involve some bureaucracy involving opposite categories.

module _ (p : Functor C C') (F : Functor C D) where
  open Ran
  open Lan
  open is-ran
  open is-lan
  open _=>_

  co-unitā†’counit
    : āˆ€ {G : Functor (C' ^op) (D ^op)}
    ā†’ Functor.op F => G Fāˆ˜ Functor.op p
    ā†’ unopF G Fāˆ˜ p => F
  co-unitā†’counit Ī± = record { opN Ī± }

  co-unitā†counit
    : āˆ€ {G : Functor C' D}
    ā†’ G Fāˆ˜ p => F
    ā†’ Functor.op F => Functor.op G Fāˆ˜ Functor.op p
  co-unitā†counit Ī± = record { opN Ī± }

  counitā†’co-unit
    : āˆ€ {G : Functor (C' ^op) (D ^op)}
    ā†’ G Fāˆ˜ Functor.op p => Functor.op F
    ā†’ F => unopF G Fāˆ˜ p
  counitā†’co-unit Ī± = record { opN Ī± }

  counitā†co-unit
    : āˆ€ {G : Functor C' D}
    ā†’ F => G Fāˆ˜ p
    ā†’ Functor.op G Fāˆ˜ Functor.op p => Functor.op F
  counitā†co-unit Ī± = record { opN Ī± }
  is-co-lan'ā†’is-ran
    : āˆ€ {G : Functor (C' ^op) (D ^op)} {eta : Functor.op F => G Fāˆ˜ Functor.op p}
    ā†’ is-lan (Functor.op p) (Functor.op F) G eta
    ā†’ is-ran p F (unopF G) (co-unitā†’counit eta)
  is-co-lan'ā†’is-ran {G = G} {eta = eta} is-lan = ran where
    module lan = is-lan is-lan

    ran : is-ran p F (unopF G) (co-unitā†’counit eta)
    ran .Ļƒ {M = M} Ī± = record { opN (lan.Ļƒ Ī±') } where
      Ī±' : Functor.op F => Functor.op M Fāˆ˜ Functor.op p
      Ī±' = record { opN Ī± }

    ran .Ļƒ-comm = ext (lan.Ļƒ-comm Ī·ā‚š_)
    ran .Ļƒ-uniq {M = M} {Ļƒ' = Ļƒ'} p = ext Ī» x ā†’
      lan.Ļƒ-uniq {Ļƒ' = dualise! Ļƒ'} (reext! p) Ī·ā‚š x
  -- This is identical to is-co-lan'ā†’is-ran, but we push the Functor.op
  -- into the is-lan, which is what you want when not dealing with Lan.
  is-co-lanā†’is-ran
    : {G : Functor C' D} {eps : G Fāˆ˜ p => F}
    ā†’ is-lan (Functor.op p) (Functor.op F) (Functor.op G) (co-unitā†counit eps)
    ā†’ is-ran p F G eps
  is-co-lanā†’is-ran {G = G} {eps} lan = ran where
    module lan = is-lan lan

    ran : is-ran p F G eps
    ran .Ļƒ {M = M} Ī± = record { opN (lan.Ļƒ Ī±') } where
      Ī±' : (Functor.op F => Functor.op M Fāˆ˜ Functor.op p)
      Ī±' = record { _=>_ (_=>_.op Ī±) }
    ran .Ļƒ-comm = ext (lan.Ļƒ-comm Ī·ā‚š_)
    ran .Ļƒ-uniq {M = M} {Ļƒ' = Ļƒ'} p = ext Ī» x ā†’
      lan.Ļƒ-uniq {Ļƒ' = dualise! Ļƒ'} (reext! p) Ī·ā‚š x

  is-ranā†’is-co-lan
    : āˆ€ {Ext : Functor C' D} {eta : Ext Fāˆ˜ p => F}
    ā†’ is-ran p F Ext eta
    ā†’ is-lan (Functor.op p) (Functor.op F) (Functor.op Ext) (co-unitā†counit eta)
  is-ranā†’is-co-lan {Ext = Ext} is-ran = lan where
    module ran = is-ran is-ran

    lan : is-lan (Functor.op p) (Functor.op F) (Functor.op Ext) _
    lan .Ļƒ {M = M} Ī± = Ļƒ' where
      Ī±' : (unopF M Fāˆ˜ p => F)
      Ī±' = record { opN Ī± }

      Ļƒ' : (Functor.op Ext => M)
      Ļƒ' = record { opN (ran.Ļƒ Ī±') }

    lan .Ļƒ-comm = ext (ran.Ļƒ-comm Ī·ā‚š_)
    lan .Ļƒ-uniq {M = M} {Ļƒ' = Ļƒ'} p = ext Ī» x ā†’
      ran.Ļƒ-uniq {Ļƒ' = dualise! Ļƒ'} (reext! p) Ī·ā‚š x

  Co-lanā†’Ran : Lan (Functor.op p) (Functor.op F) ā†’ Ran p F
  Co-lanā†’Ran lan .Ext     = unopF (lan .Ext)
  Co-lanā†’Ran lan .eps     = co-unitā†’counit (lan .eta)
  Co-lanā†’Ran lan .has-ran = is-co-lan'ā†’is-ran (lan .has-lan)

  Ranā†’Co-lan : Ran p F ā†’ Lan (Functor.op p) (Functor.op F)
  Ranā†’Co-lan ran .Ext = Functor.op (ran .Ext)
  Ranā†’Co-lan ran .eta = co-unitā†counit (ran .eps)
  Ranā†’Co-lan ran .has-lan = is-ranā†’is-co-lan (ran .has-ran)

  is-co-ran'ā†’is-lan
    : {G : Functor (C' ^op) (D ^op)} {eps : G Fāˆ˜ Functor.op p => Functor.op F}
    ā†’ is-ran (Functor.op p) (Functor.op F) G eps
    ā†’ is-lan p F (unopF G) (counitā†’co-unit eps)
  is-co-ran'ā†’is-lan {G = G} {eps} is-ran = lan where
    module ran = is-ran is-ran

    lan : is-lan p F (unopF G) (counitā†’co-unit eps)
    lan .Ļƒ {M = M} Ī² = record { opN (ran.Ļƒ Ī²') } where
      Ī²' : Functor.op M Fāˆ˜ Functor.op p => Functor.op F
      Ī²' = record { opN Ī² }
    lan .Ļƒ-comm = ext (ran.Ļƒ-comm Ī·ā‚š_)
    lan .Ļƒ-uniq {M = M} {Ļƒ' = Ļƒ'} p = ext Ī» x ā†’
      ran.Ļƒ-uniq {Ļƒ' = dualise! Ļƒ'} (reext! p) Ī·ā‚š x

  is-co-ranā†’is-lan
    : āˆ€ {G : Functor C' D} {eta}
    ā†’ is-ran (Functor.op p) (Functor.op F) (Functor.op G) (counitā†co-unit eta)
    ā†’ is-lan p F G eta
  is-co-ranā†’is-lan {G = G} {eta} is-ran = lan where
    module ran = is-ran is-ran

    lan : is-lan p F G eta
    lan .Ļƒ {M = M} Ī² = record { opN (ran.Ļƒ Ī²') } where
      Ī²' : Functor.op M Fāˆ˜ Functor.op p => Functor.op F
      Ī²' = record { opN Ī² }
    lan .Ļƒ-comm = ext (ran.Ļƒ-comm Ī·ā‚š_)
    lan .Ļƒ-uniq {M = M} {Ļƒ' = Ļƒ'} p = ext Ī» x ā†’
      ran.Ļƒ-uniq {Ļƒ' = dualise! Ļƒ'} (reext! p) Ī·ā‚š x

  is-lanā†’is-co-ran
    : āˆ€ {G : Functor C' D} {eps : F => G Fāˆ˜ p}
    ā†’ is-lan p F G eps
    ā†’ is-ran (Functor.op p) (Functor.op F) (Functor.op G) (counitā†co-unit eps)
  is-lanā†’is-co-ran {G = G} is-lan = ran where
    module lan = is-lan is-lan

    ran : is-ran (Functor.op p) (Functor.op F) (Functor.op G) _
    ran .Ļƒ {M = M} Ī² = Ļƒ' where
      Ī²' : F => unopF M Fāˆ˜ p
      Ī²' = record { opN Ī² }

      Ļƒ' : M => Functor.op G
      Ļƒ' = record { opN (lan.Ļƒ Ī²') }

    ran .Ļƒ-comm = ext (lan.Ļƒ-comm Ī·ā‚š_)
    ran .Ļƒ-uniq {M = M} {Ļƒ' = Ļƒ'} p = ext Ī» x ā†’
      lan.Ļƒ-uniq {Ļƒ' = dualise! Ļƒ'} (reext! p) Ī·ā‚š x

  Co-ranā†’Lan : Ran (Functor.op p) (Functor.op F) ā†’ Lan p F
  Co-ranā†’Lan ran .Ext = unopF (ran .Ext)
  Co-ranā†’Lan ran .eta = counitā†’co-unit (ran .eps)
  Co-ranā†’Lan ran .has-lan = is-co-ran'ā†’is-lan (ran .has-ran)

  Lanā†’Co-ran : Lan p F ā†’ Ran (Functor.op p) (Functor.op F)
  Lanā†’Co-ran lan .Ext = Functor.op (lan .Ext)
  Lanā†’Co-ran lan .eps = counitā†co-unit (lan .eta)
  Lanā†’Co-ran lan .has-ran = is-lanā†’is-co-ran (lan .has-lan)