module Cat.Functor.Kan.Duality where

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.

  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 (Functor.op 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 (Functor.op G) (co-unit→counit eta)
    ran .σ {M = M} α = op (lan.σ α') where
      unquoteDecl α' = dualise-into α'
        (Functor.op F => Functor.op M F∘ Functor.op p)
        α

    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} α = op (lan.σ α') where
      unquoteDecl α' = dualise-into α'
        (Functor.op F => Functor.op M F∘ Functor.op p)
        α
    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
      unquoteDecl α' = dualise-into α' (Functor.op M F∘ p => F) α
      unquoteDecl σ' = dualise-into σ' (Functor.op Ext => M) (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     = Functor.op (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 (Functor.op 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 (Functor.op G) (counit→co-unit eps)
    lan .σ {M = M} β = op (ran.σ β') where
      unquoteDecl β' = dualise-into β'
        (Functor.op M F∘ Functor.op p => Functor.op F)
        β
    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} β = op (ran.σ β') where
      unquoteDecl β' = dualise-into β'
        (Functor.op M F∘ Functor.op p => Functor.op F)
        β
    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
      unquoteDecl β' = dualise-into β' (F => Functor.op M F∘ p) β
      unquoteDecl σ' = dualise-into σ' (M => Functor.op G) (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 = Functor.op (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)