open import Cat.Diagram.Colimit.Cocone
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Limit.Cone
open import Cat.Diagram.Coproduct
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Initial
open import Cat.Diagram.Product
open import Cat.Diagram.Pushout
open import Cat.Prelude

module Cat.Diagram.Duals where

module _ {o ā„“} {C : Precategory o ā„“} where
  private module C = Precategory C

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