open import Cat.Instances.Functor.Duality
open import Cat.Instances.Functor
open import Cat.Prelude

import Cat.Reasoning

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:

  • Products and coproducts
  • Pullbacks and pushouts
  • Equalisers and coequalisers
  • Terminal objects and initial objects

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

Co/products🔗

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

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

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

Co/equalisers🔗

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

is-co-equaliser→is-coequaliser
  :  {A B E} {f g : C.Hom A B} {coeq : C.Hom B E}
   Co-equ.is-equaliser f g coeq  Coequ.is-coequaliser f g coeq
is-co-equaliser→is-coequaliser eq =
  record
    { coequal    = eq.equal
    ; coequalise = eq.limiting
    ; universal  = eq.universal
    ; unique     = eq.unique
    }
  where module eq = Co-equ.is-equaliser eq

is-coequaliser→is-co-equaliser
  :  {A B E} {f g : C.Hom A B} {coeq : C.Hom B E}
   Coequ.is-coequaliser f g coeq  Co-equ.is-equaliser f g coeq
is-coequaliser→is-co-equaliser coeq =
  record
    { equal     = coeq.coequal
    ; limiting  = coeq.coequalise
    ; universal = coeq.universal
    ; unique    = coeq.unique
    }
  where module coeq = Coequ.is-coequaliser coeq

Initial/terminal🔗

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

is-initial→is-coterminal
  :  {A}  Coterm.is-terminal A  Init.is-initial A
is-initial→is-coterminal x = x

is-coterminal→is-initial
  :  {A}  Init.is-initial A  Coterm.is-terminal A
is-coterminal→is-initial x = x

Pullback/pushout🔗

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

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}
   Co-pull.is-pullback p1 f p2 g  Push.is-pushout f p1 g p2
is-co-pullback→is-pushout pb =
  record
    { square = pb.square
    ; colimiting = pb.limiting
    ; i₁∘colimiting = pb.p₁∘limiting
    ; i₂∘colimiting = pb.p₂∘limiting
    ; unique = pb.unique
    }
  where module pb = Co-pull.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}
   Push.is-pushout f p1 g p2  Co-pull.is-pullback p1 f p2 g
is-pushout→is-co-pullback po =
  record
    { square      = po.square
    ; limiting    = po.colimiting
    ; p₁∘limiting = po.i₁∘colimiting
    ; p₂∘limiting = po.i₂∘colimiting
    ; unique      = po.unique
    }
  where module po = Push.is-pushout po

Co/cones🔗

open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Terminal
open import Cat.Diagram.Initial

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 Terminal
  open Initial
  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🔗

  Colimit→Co-limit
    : Colimit F  Limit F^op
  Colimit→Co-limit colim = lim where
    lim : Limit F^op
    lim .top = Cocone→Co-cone (colim .bot)
    lim .has⊤ co-cone =
      retract→is-contr f g fg
        (colim .has⊥ (Co-cone→Cocone co-cone))
      where
        f : _  _
        f x = subst  e  Cone-hom F^op e _)
          (Co-cone→Cocone→Co-cone _)
          (Cocone-hom→Co-cone-hom x)

        g : _  _
        g x = subst  e  Cocone-hom F e _)
          (Cocone→Co-cone→Cocone _)
          (Co-cone-hom→Cocone-hom x)

        fg : is-left-inverse f g
        fg x = Cone-hom-path _ (transport-refl _  transport-refl _)

  Co-limit→Colimit
    : Limit F^op  Colimit F
  Co-limit→Colimit lim = colim where
    colim : Colimit F
    colim .bot = Co-cone→Cocone (lim .top)
    colim .has⊥ cocon =
      retract→is-contr f g fg
        (lim .has⊤ (Cocone→Co-cone cocon))
      where
        f : _  _
        f x = subst  e  Cocone-hom F _ e)
          (Cocone→Co-cone→Cocone _)
          (Co-cone-hom→Cocone-hom x)

        g : _  _
        g x = subst  e  Cone-hom F^op _ e)
          (Co-cone→Cocone→Co-cone _)
          (Cocone-hom→Co-cone-hom x)

        fg : is-left-inverse f g
        fg x = Cocone-hom-path _ (transport-refl _  transport-refl _)

module _ {o } {J : Precategory o } {F F′ : Functor J C} where
  private module JC = Cat.Reasoning Cat[ J , C ]

  Colimit-ap-iso : F JC.≅ F′  Colimit F  Colimit F′
  Colimit-ap-iso f cl =
    Co-limit→Colimit (Limit-ap-iso (op-natural-iso f) (Colimit→Co-limit cl))