module Cat.Diagram.Duals {o h} (C : Precategory o h) where

Dualities of diagrams🔗

Following Hu and Carette, we’ve opted to have different concrete definitions for diagrams and their opposites. In particular, we have the following pairs of “redundant” definitions:

For all four of the above pairs, we have that one in CC is the other in CopC^{\mathrm{op}}. We prove these correspondences here:


import Cat.Diagram.Product (C ^op) as Co-prod
import Cat.Diagram.Coproduct C as Coprod

  :  {A B P} {i1 : C.Hom A P} {i2 : C.Hom B P} i1 i2 i1 i2
is-co-product→is-coproduct isp =
    { [_,_]      = isp.⟨_,_⟩
    ; in₀∘factor = isp.π₁∘factor
    ; in₁∘factor = isp.π₂∘factor
    ; unique     = isp.unique
  where module isp = isp

  :  {A B P} {i1 : C.Hom A P} {i2 : C.Hom B P} i1 i2 i1 i2
is-coproduct→is-co-product iscop =
    { ⟨_,_⟩     = iscop.[_,_]
    ; π₁∘factor = iscop.in₀∘factor
    ; π₂∘factor = iscop.in₁∘factor
    ; unique    = iscop.unique
  where module iscop = iscop


import Cat.Diagram.Equaliser (C ^op) as Co-equ
import Cat.Diagram.Coequaliser C as Coequ

  :  {A B E} {f g : C.Hom A B} {coeq : C.Hom B E} f g coeq f g coeq
is-co-equaliser→is-coequaliser eq =
    { coequal    = eq.equal
    ; universal  = eq.universal
    ; factors    = eq.factors
    ; unique     = eq.unique
  where module eq = eq

  :  {A B E} {f g : C.Hom A B} {coeq : C.Hom B E} f g coeq f g coeq
is-coequaliser→is-co-equaliser coeq =
    { equal     = coeq.coequal
    ; universal = coeq.universal
    ; factors   = coeq.factors
    ; unique    = coeq.unique
  where module coeq = coeq


import Cat.Diagram.Terminal (C ^op) as Coterm
import Cat.Diagram.Initial C as Init
open Coterm.Terminal
open Init.Initial

  :  {A} A A
is-coterminal→is-initial x = x

  :  {A} A A
is-initial→is-coterminal x = x

Coterminal→Initial : Coterm.Terminal  Init.Initial
Coterminal→Initial term .bot = term .top
Coterminal→Initial term .has⊥ = is-coterminal→is-initial (term .has⊤)

Initial→Coterminal : Init.Initial  Coterm.Terminal
Initial→Coterminal init .top = init .bot
Initial→Coterminal init .has⊤ = is-initial→is-coterminal (init .has⊥)


import Cat.Diagram.Pullback (C ^op) as Co-pull
import Cat.Diagram.Pushout C as Push

  :  {P X Y Z} {p1 : C.Hom X P} {f : C.Hom Z X} {p2 : C.Hom Y P} {g : C.Hom Z Y} p1 f p2 g f p1 g p2
is-co-pullback→is-pushout pb =
    { square = pb.square
    ; universal = pb.universal
    ; i₁∘universal = pb.p₁∘universal
    ; i₂∘universal = pb.p₂∘universal
    ; unique = pb.unique
  where module pb = pb

  :  {P X Y Z} {p1 : C.Hom X P} {f : C.Hom Z X} {p2 : C.Hom Y P} {g : C.Hom Z Y} f p1 g p2 p1 f p2 g
is-pushout→is-co-pullback po =
    { square      = po.square
    ; universal    = po.universal
    ; p₁∘universal = po.i₁∘universal
    ; p₂∘universal = po.i₂∘universal
    ; unique      = po.unique
  where module po = po


open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Colimit.Cocone
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Limit.Cone

module _ {o } {J : Precategory o } {F : Functor J C} where
  open Functor F renaming (op to F^op)

  open Cocone-hom
  open Cone-hom
  open Cocone
  open Cone

  Co-cone→Cocone : Cone F^op  Cocone F
  Co-cone→Cocone cone .coapex = cone .apex
  Co-cone→Cocone cone .ψ = cone .ψ
  Co-cone→Cocone cone .commutes = cone .commutes

  Cocone→Co-cone : Cocone F  Cone F^op
  Cocone→Co-cone cone .apex     = cone .coapex
  Cocone→Co-cone cone .ψ        = cone .ψ
  Cocone→Co-cone cone .commutes = cone .commutes

  Cocone→Co-cone→Cocone :  K  Co-cone→Cocone (Cocone→Co-cone K)  K
  Cocone→Co-cone→Cocone K i .coapex = K .coapex
  Cocone→Co-cone→Cocone K i .ψ = K .ψ
  Cocone→Co-cone→Cocone K i .commutes = K .commutes

  Co-cone→Cocone→Co-cone :  K  Cocone→Co-cone (Co-cone→Cocone K)  K
  Co-cone→Cocone→Co-cone K i .apex = K .apex
  Co-cone→Cocone→Co-cone K i .ψ = K .ψ
  Co-cone→Cocone→Co-cone K i .commutes = K .commutes

    :  {x y}
     Cone-hom F^op y x
     Cocone-hom F (Co-cone→Cocone x) (Co-cone→Cocone y)
  Co-cone-hom→Cocone-hom ch .hom = ch .hom
  Co-cone-hom→Cocone-hom ch .commutes o = ch .commutes o

    :  {x y}
     Cocone-hom F x y
     Cone-hom F^op (Cocone→Co-cone y) (Cocone→Co-cone x)
  Cocone-hom→Co-cone-hom ch .hom = ch .hom
  Cocone-hom→Co-cone-hom ch .commutes = ch .commutes


Limits and colimits are defined via Kan extensions, so it’s reasonable to expect that duality of Kan extensions would apply to (co)limits. Unfortunately, proof assistants: (co)limits are extensions of !F, but duality of Kan extensions inserts an extra Functor.op. We could work around this, but it’s easier to just do the proofs by hand.

    : Colimit F  Limit F^op
  Colimit→Co-limit colim = to-limit (to-is-limit ml) where
    module colim = Colimit colim
    open make-is-limit

    ml : make-is-limit F^op colim.coapex
    ml .ψ = colim.ψ
    ml .commutes = colim.commutes
    ml .universal eta p = colim.universal eta p
    ml .factors eta p = colim.factors eta p
    ml .unique eta p other q = colim.unique eta p other q

    : Limit F^op  Colimit F
  Co-limit→Colimit lim = to-colimit (to-is-colimit mc) where
    module lim = Limit lim
    open make-is-colimit

    mc : make-is-colimit F lim.apex
    mc .ψ = lim.ψ
    mc .commutes = lim.commutes
    mc .universal eta p = lim.universal eta p
    mc .factors eta p = lim.factors eta p
    mc .unique eta p other q = lim.unique eta p other q