module Cat.Diagram.Duals 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 is the other in We prove these correspondences here:

Co/products🔗

  is-co-product→is-coproduct
    :  {A B P} {i1 : C.Hom A P} {i2 : C.Hom B P}
     is-product (C ^op) i1 i2  is-coproduct C i1 i2
  is-co-product→is-coproduct isp =
    record
      { [_,_]      = isp.⟨_,_⟩
      ; []∘ι₁ = isp.π₁∘⟨⟩
      ; []∘ι₂ = isp.π₂∘⟨⟩
      ; unique     = isp.unique
      }
    where module isp = is-product isp

  is-coproduct→is-co-product
    :  {A B P} {i1 : C.Hom A P} {i2 : C.Hom B P}
     is-coproduct C i1 i2  is-product (C ^op) i1 i2
  is-coproduct→is-co-product iscop =
    record
      { ⟨_,_⟩     = iscop.[_,_]
      ; π₁∘⟨⟩ = iscop.[]∘ι₁
      ; π₂∘⟨⟩ = iscop.[]∘ι₂
      ; unique    = iscop.unique
      }
    where module iscop = is-coproduct iscop

Co/equalisers🔗

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

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

Initial/terminal🔗

  open Terminal
  open Initial

  is-coterminal→is-initial
    :  {A}  is-terminal (C ^op) A  is-initial C A
  is-coterminal→is-initial x = x

  is-initial→is-coterminal
    :  {A}  is-initial C A  is-terminal (C ^op) A
  is-initial→is-coterminal x = x

  Coterminal→Initial : Terminal (C ^op)  Initial C
  Coterminal→Initial term .bot = term .top
  Coterminal→Initial term .has⊥ = is-coterminal→is-initial (term .has⊤)

  Initial→Coterminal : Initial C  Terminal (C ^op)
  Initial→Coterminal init .top = init .bot
  Initial→Coterminal init .has⊤ = is-initial→is-coterminal (init .has⊥)

Pullback/pushout🔗

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

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

Co/cones🔗

  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

    Co-cone-hom→Cocone-hom
      :  {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

    Cocone-hom→Co-cone-hom
      :  {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

Co/limits🔗

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→Co-limit
      : 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 eps p = colim.universal eps p
      ml .factors eps p = colim.factors eps p
      ml .unique eps p other q = colim.unique eps p other q

    Co-limit→Colimit
      : 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