open import Cat.Functor.Naturality.Reflection
open import Cat.Diagram.Coproduct.Indexed
open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Product.Indexed
open import Cat.Diagram.Colimit.Cocone
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Coequaliser
open import Cat.Functor.Kan.Duality
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Limit.Cone
open import Cat.Functor.Kan.Unique
open import Cat.Functor.Naturality
open import Cat.Diagram.Coproduct
open import Cat.Diagram.Equaliser
open import Cat.Functor.Coherence
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Functor.Constant
open import Cat.Functor.Kan.Base
open import Cat.Diagram.Initial
open import Cat.Diagram.Product
open import Cat.Diagram.Pushout
open import Cat.Prelude
open import Cat.Base

import Cat.Functor.Reasoning
import Cat.Reasoning

module Cat.Diagram.Duals where

private
  variable
    o' ā„“' : Level
    Idx : Type ā„“'
module _ {o ā„“} {C : Precategory o ā„“} where
  private
    module C = Cat.Reasoning C
    variable
      S : C.Ob

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

Indexed Co/productsšŸ”—

  is-indexed-co-productā†’is-indexed-coproduct
    : āˆ€ {F : Idx ā†’ C.Ob} {Ī¹ : āˆ€ i ā†’ C.Hom (F i) S} ā†’ is-indexed-product (C ^op) F Ī¹
    ā†’ is-indexed-coproduct C F Ī¹
  is-indexed-co-productā†’is-indexed-coproduct prod =
    record { is-indexed-product prod renaming (tuple to match) }

  is-indexed-coproductā†’is-indexed-co-product
    : āˆ€ {F : Idx ā†’ C.Ob} {Ī¹ : āˆ€ i ā†’ C.Hom (F i) S} ā†’ is-indexed-coproduct C F Ī¹
    ā†’ is-indexed-product (C ^op) F Ī¹
  is-indexed-coproductā†’is-indexed-co-product coprod =
    record { is-indexed-coproduct coprod renaming (match to tuple) }

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-terminalā†’is-coinitial
    : āˆ€ {A} ā†’ is-terminal C A ā†’ is-initial (C ^op) A
  is-terminalā†’is-coinitial x = x

  is-initialā†’is-coterminal
    : āˆ€ {A} ā†’ is-initial C A ā†’ is-terminal (C ^op) A
  is-initialā†’is-coterminal x = x

  is-coinitialā†’is-terminal
    : āˆ€ {A} ā†’ is-initial (C ^op) A ā†’ is-terminal C A
  is-coinitialā†’is-terminal 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āŠ¤)

  Terminalā†’Coinitial : Terminal C ā†’ Initial (C ^op)
  Terminalā†’Coinitial term .bot = term .top
  Terminalā†’Coinitial term .hasāŠ„ = is-terminalā†’is-coinitial (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āŠ„)

  Coinitialā†’terminal : Initial (C ^op) ā†’ Terminal C
  Coinitialā†’terminal init .top = init .bot
  Coinitialā†’terminal init .hasāŠ¤ = is-coinitialā†’is-terminal (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)
    private module F = Cat.Functor.Reasoning F

    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 .map = ch .map
    Co-cone-homā†’Cocone-hom ch .com o = ch .com 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 = record { Cocone-hom ch }

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

module _ {o ā„“} {C : Precategory o ā„“} where
  co-is-completeā†’is-cocomplete : is-complete o' ā„“' (C ^op) ā†’ is-cocomplete o' ā„“' C
  co-is-completeā†’is-cocomplete co-complete F = Co-limitā†’Colimit $
    co-complete $ Functor.op F

  is-cocompleteā†’co-is-complete : is-cocomplete o' ā„“' (C ^op) ā†’ is-complete o' ā„“' C
  is-cocompleteā†’co-is-complete cocomplete F = to-limit (to-is-limit ml) where
    dual = Colimitā†’Co-limit $ cocomplete $ Functor.op F
    ml : make-is-limit F $ Limit.apex dual
    ml = record { Limit dual }