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))