open import Cat.Diagram.Limit.Finite
open import Cat.Instances.Coalgebras
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Comonad
open import Cat.Diagram.Product
open import Cat.Displayed.Total
open import Cat.Functor.Adjoint
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning

module Cat.Instances.Coalgebras.Cartesian
  {o ℓ} {C : Precategory o ℓ} {F : Functor C C} (W : Comonad-on F)
  (fc : Finitely-complete C) (lex : is-lex F)
  where

open Finitely-complete fc
open Cat.Reasoning C
open is-lex lex

open Total-hom

open Coalgebra-on
open Comonad-on W

open is-pullback
open Pullback

private module W = Func F

Finite limits in categories of coalgebras🔗

If $(W, ε, δ)$ is an arbitrary comonad on a category $C,$ there’s not much we can say about general limits in the category of $W$ -coalgebras. Indeed, precisely dualising the case for categories of algebras over a monad, where limits are inherited from the base category but colimits are onerous, for $C_{W},$ colimits come easily but limits are onerous. However, if $W$ preserves a certain class of limits, then the forgetful functor $U : C_{W} \to C$ preserves and reflects those same limits.

module
  _ {(A , α') (B , β') (X , ξ') : Coalgebras.Ob W}
    (f : Coalgebras.Hom W (A , α') (X , ξ'))
    (g : Coalgebras.Hom W (B , β') (X , ξ'))
  where
  private
    module α = Coalgebra-on α'
    module β = Coalgebra-on β'
    module ξ = Coalgebra-on ξ'
    open α renaming (ρ to α) using ()
    open β renaming (ρ to β) using ()
    open ξ renaming (ρ to ξ) using ()

In this module, we’re interested in the specific case where $W$ is a left exact functor, i.e., it preserves finite limits. Accordingly, $C_{W}$ will have all finite limits, and they will be computed as in $C .$ The more general computation can be found in Cat.Instances.Coalgebras.Limits.

We start by showing that $U$ reflects pullbacks, since that’s what we’ll use to construct pullbacks in $C_{W} .$

  is-pullback-coalgebra
    : ∀ {(P , π) : Coalgebras.Ob W}
        {π₁ : Coalgebras.Hom W (P , π) (A , α')}
        {π₂ : Coalgebras.Hom W (P , π) (B , β')}
    → is-pullback C (π₁ .hom) (f .hom) (π₂ .hom) (g .hom)
    → is-pullback (Coalgebras W) π₁ f π₂ g
  is-pullback-coalgebra {P , π'} {π₁} {π₂} pb = pb' where

To be precise, we’re showing that, if a square

is sent by $U$ to a pullback in $C,$ it must already have been a pullback in $C_{W} .$

    module π = Coalgebra-on π'
    open π renaming (ρ to π) using ()
    pres = pres-pullback pb
    module p  = is-pullback pb
    module p' = is-pullback pres

    module
      _ {(Q , χ') : Coalgebras.Ob W}
        (p1 : Coalgebras.Hom W (Q , χ') (A , α'))
        (p2 : Coalgebras.Hom W (Q , χ') (B , β'))
        (wit : f .hom ∘ p1 .hom ≡ g .hom ∘ p2 .hom)
      where
      module χ = Coalgebra-on χ'
      open χ renaming (ρ to χ) using ()

Since $W$ preserves pullbacks, $W P$ is a pullback as well. If we are given a coalgebra $(Q, χ)$ together with a span of homomorphisms

(A, α) p_{1} (Q, χ) p_{2} (B, β)

satisfying $f p_{1} = g p_{2},$ hence also $W (f) \circ α p_{1} = W (g) \circ β p_{2},$ there is a unique factorisation

⟨ α p_{1}, β p_{2} ⟩ : Q \to W P,

which we can compose with the counit $ε$ to give a morphism $ν : Q \to P$ satisfying $π_{1} ν = p_{1}$ and $π_{2} ν = p_{2},$ as shown in the formalisation below.

      abstract
        wit' : W₁ (f .hom) ∘ α ∘ p1 .hom ≡ W₁ (g .hom) ∘ β ∘ p2 .hom
        wit' = W₁ (f .hom) ∘ α ∘ p1 .hom   ≡⟨ pulll (f .preserves) ⟩≡
               (ξ ∘ f .hom) ∘ p1 .hom      ≡⟨ pullr wit ⟩≡
               ξ ∘ g .hom ∘ p2 .hom        ≡⟨ extendl (sym (g .preserves)) ⟩≡
               W₁ (g .hom) ∘ β ∘ p2 .hom   ∎

      ν : Hom Q P
      ν = counit.ε _ ∘ p'.universal wit'

      abstract
        comm₁ : π₁ .hom ∘ ν ≡ p1 .hom
        comm₁ =
          π₁ .hom ∘ ν                                    ≡⟨ pulll (sym (counit.is-natural _ _ _)) ⟩≡
          (counit.ε _ ∘ W₁ (π₁ .hom)) ∘ p'.universal _  ≡⟨ pullr p'.p₁∘universal ⟩≡
          counit.ε _ ∘ α ∘ p1 .hom                       ≡⟨ cancell α.ρ-counit ⟩≡
          p1 .hom                                        ∎

Since equality of morphisms in $C_{W}$ is entirely tested downstairs in $C,$ if $ρ$ extends to a coalgebra homomorphism, then it is precisely the factorisation we’re seeking for the square to be a pullback in $C_{W} .$ That’s because, since it’s induced by the universal property of $P$ as a pullback, it automatically satisfies the commutativity and uniqueness requirements.

        comm₂ : π₂ .hom ∘ ν ≡ p2 .hom
        comm₂ = pulll (sym (counit.is-natural _ _ _))
             ·· pullr p'.p₂∘universal
             ·· cancell β.ρ-counit

It therefore remains to show that $W (ε ⟨ α p_{1}, β p_{2} ⟩) \circ χ$ is $π ε ⟨ α p_{1}, β p_{2} ⟩ .$ Since these are both maps into a pullback, namely $W P,$ we can do so componentwise. Therefore, we calculate

      step₁ : W₁ (π₁ .hom) ∘ W₁ ν ∘ χ ≡ α ∘ p1 .hom
      step₁ =
        W₁ (π₁ .hom) ∘ W₁ ν ∘ χ                    ≡⟨ pulll (W.weave (pulll (sym (counit.is-natural _ _ _)) ∙ pullr p'.p₁∘universal)) ⟩≡
        (W₁ (counit.ε _) ∘ W₁ (α ∘ p1 .hom)) ∘ χ   ≡⟨ pullr (ap₂ _∘_ (W-∘ _ _) refl ∙ pullr (p1 .preserves)) ⟩≡
        W₁ (counit.ε _) ∘ W₁ α ∘ α ∘ p1 .hom       ≡⟨ W.cancell α.ρ-counit ⟩≡
        α ∘ p1 .hom                                ∎

and

      step₂ : W₁ (π₁ .hom) ∘ π ∘ ν ≡ α ∘ p1 .hom
      step₂ = W₁ (π₁ .hom) ∘ π ∘ ν ≡⟨ pulll (π₁ .preserves) ⟩≡
              (α ∘ π₁ .hom) ∘ ν    ≡⟨ pullr comm₁ ⟩≡
              α ∘ p1 .hom          ∎

with very similar, but symmetric, proofs for the second projection — so $ν$ was indeed the map we were looking for!

      factor : Coalgebras.Hom W (Q , χ') (P , π')
      factor .hom       = ν
      factor .preserves = p'.unique₂ {p = wit'} step₁
        (  pulll (W.weave (pulll (sym (counit.is-natural _ _ _)) ∙ pullr p'.p₂∘universal))
        ·· pullr (ap₂ _∘_ (W-∘ _ _) refl ∙ pullr (p2 .preserves))
        ·· W.cancell β.ρ-counit)
        step₂
        (pulll (π₂ .preserves) ∙ pullr comm₂)

    pb' : is-pullback (Coalgebras W) π₁ f π₂ g
    pb' .square = ext p.square
    pb' .universal {p₁' = p₁'} {p₂'} x = factor p₁' p₂' (ap hom x)
    pb' .p₁∘universal {p₁' = p₁'} {p₂'} {p} = ext $ comm₁ p₁' p₂' (ap hom p)
    pb' .p₂∘universal {p₁' = p₁'} {p₂'} {p} = ext $ comm₂ p₁' p₂' (ap hom p)
    pb' .unique {p₁' = p₁'} {p₂'} {p} q r = ext $ p.unique₂
      {p = ap hom p} (ap hom q) (ap hom r)
      (comm₁ p₁' p₂' (ap hom p)) (comm₂ p₁' p₂' (ap hom p))

  Coalgebra-on-pullback
    : (p : Pullback C (f .hom) (g .hom))
    → Coalgebra-on W (Pullback.apex p)
  Coalgebra-on-pullback p = coalg where

    rem₁ = pres-pullback (p .has-is-pb)
    rem₂ = pres-pullback rem₁
    module p' = is-pullback rem₁
    module p = Pullback p

Suppose now that we have a pullback

and we want to equip $A \times_{X} B$ with a $W -coalgebra$ structure. We must come up with a map $A \times_{X} B \to W (A \times_{X} B),$ but since $W$ preserves pullbacks, it will suffice to come up with a map $A \times_{X} B \to W A \times_{W X} W B .$ Since that is a pullback, we can write such a map as $⟨ x, y ⟩$ given $x : A \times_{X} B \to W A$ and $y : A \times_{X} B \to W B,$ as long as we have $W (f) x = W (g) y .$

We define $x$ (resp. $y)$ to be the composite $A \times_{X} B p_{1} A α W A$ (resp. $p_{2},$ $β),$ and a short calculation shows that this indeed satisfies the aforementioned compatibility condition.

    abstract
      wit : W₁ (f .hom) ∘ α ∘ p.p₁ ≡ W₁ (g .hom) ∘ β ∘ p.p₂
      wit = W₁ (f .hom) ∘ α ∘ p.p₁  ≡⟨ pulll (f .preserves) ⟩≡
            (ξ ∘ f .hom) ∘ p.p₁     ≡⟨ pullr p.square ⟩≡
            ξ ∘ g .hom ∘ p.p₂       ≡⟨ extendl (sym (g .preserves)) ⟩≡
            W₁ (g .hom) ∘ β ∘ p.p₂  ∎

    coalg : Coalgebra-on W p.apex
    coalg .ρ = p'.universal wit

It remains to show that this factorisation is compatible with $W ’s$ counit and comultiplication. We start with the former: we must show that $ε ⟨ α p_{1}, β p_{2} ⟩$ is the identity. Since equality of maps into pullbacks is determined by their composition with the projections, it will suffice to show that

p_{1} ε ⟨ α p_{1}, β p_{2} ⟩

is $p_{1},$ and respectively for $p_{2},$ but we can calculate

p_{1} ε ⟨ α p_{1}, β p_{2} ⟩ = ε p_{1} ⟨ α p_{1}, β p_{2} ⟩ = ε α p_{1} = p_{1}

where the first step is by naturality, the second is computation, and the third is because $α$ is a $W -coalgebra.$ To show compatibility with the comultiplication, we perform a similar calculation: it will suffice to show that

WW (p_{1}) \circ W ⟨ α p_{1}, β p_{2} ⟩ \circ ⟨ α p_{1}, β p_{2} ⟩

and

WW (p_{1}) \circ δ \circ ⟨ α p_{1}, β p_{2} ⟩

are both $W (α) \circ α p_{1} .$ In the former case this is immediate, but in the latter case it requires naturality of $δ$ and compatibility of $α$ with the comultiplication:

= WW (p_{1}) \circ δ \circ ⟨ α p_{1}, β p_{2} ⟩ = δ \circ W (p_{1}) \circ ⟨ α p_{1}, β p_{2} ⟩ = δ \circ α p_{1} = W (α) \circ α p_{1} .

Since putting the above paragraphs together into an actual formalised proof is a bit annoying, it’s hidden in this <details> tag.

    coalg .ρ-counit =
      p.unique₂
        {p = pulll (sym (counit.is-natural _ _ _))
          ·· pullr wit
          ·· extendl (counit.is-natural _ _ _)}
        (pulll (sym (counit.is-natural _ _ _)) ∙ pullr p'.p₁∘universal)
        (pulll (sym (counit.is-natural _ _ _)) ∙ pullr p'.p₂∘universal)
        (idr _ ∙ sym (cancell α.ρ-counit))
        (idr _ ∙ sym (cancell β.ρ-counit))
    coalg .ρ-comult =
      is-pullback.unique₂ rem₂
        {p = W.extendl (f .preserves)
          ·· ap₂ _∘_ refl wit
          ·· W.extendl (sym (g .preserves))}
        (pulll (W.weave p'.p₁∘universal) ∙ pullr p'.p₁∘universal)
        (pulll (W.weave p'.p₂∘universal) ∙ pullr p'.p₂∘universal)
        (pulll (sym (comult.is-natural _ _ _)) ·· pullr p'.p₁∘universal ·· extendl (sym α.ρ-comult))
        (  pulll (sym (comult.is-natural _ _ _))
        ·· pullr p'.p₂∘universal
        ·· extendl (sym β.ρ-comult))

Pullback-coalgebra
  : {(A , α) (B , β) (X , ξ) : Coalgebras.Ob W}
    (f : Coalgebras.Hom W (A , α) (X , ξ))
    (g : Coalgebras.Hom W (B , β) (X , ξ))
  → Pullback (Coalgebras W) f g

Pullback-coalgebra f g = pb' where
  pb = pullbacks (f .hom) (g .hom)
  rem₁ = pres-pullback (pb .has-is-pb)

  pb' : Pullback (Coalgebras W) _ _
  pb' .apex .fst = _
  pb' .apex .snd = Coalgebra-on-pullback f g pb

  pb' .p₁ .hom       = Pullback.p₁ pb
  pb' .p₁ .preserves = rem₁ .p₁∘universal

  pb' .p₂ .hom       = Pullback.p₂ pb
  pb' .p₂ .preserves = rem₁ .p₂∘universal

  pb' .has-is-pb = is-pullback-coalgebra f g (pb .has-is-pb)

open Terminal

The case of the terminal object is infinitely simpler: since $W$ preserves the terminal object, we have $W ⊤ ≅ ⊤ .$ We equip it with its (necessarily unique) cofree coalgebra structure, and since there is an isomorphism

Hom_{C_{W}} ((A, α), W ⊤) ≅ Hom_{C} (A, ⊤)

the former is contractible if the latter is.

Terminal-coalgebra : Terminal (Coalgebras W)
Terminal-coalgebra .top = _
Terminal-coalgebra .has⊤ (A , α) = Equiv→is-hlevel 0
  (Equiv.inverse (_ , L-adjunct-is-equiv (Forget⊣Cofree W)))
  (terminal .has⊤ A)

Since we have a terminal object and pullbacks, we have arbitrary finite limits, too.

Coalgebras-finitely-complete : Finitely-complete (Coalgebras W)
Coalgebras-finitely-complete = with-pullbacks (Coalgebras W)
  Terminal-coalgebra
  Pullback-coalgebra