open import Cat.Diagram.Comonad
open import Cat.Displayed.Total
open import Cat.Functor.Adjoint
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Reasoning

open Total-hom
open Functor
open _=>_
open _⊣_

module Cat.Instances.Coalgebras where

Coalgebras over a comonad🔗

A coalgebra for a comonad $W:\mathcal{C}\to \mathcal{C}$ is a pair of an object $A:\mathcal{C}$ and morphism $\alpha :A\to W(A)$ that satisfy the dual axioms of a monad algebra.

module _ {o ℓ} {C : Precategory o ℓ} {W : Functor C C} (cm : Comonad-on W) where
  open Cat.Reasoning C
  private module W = Comonad-on cm
  open W

  record Coalgebra-on (A : Ob) : Type (o ⊔ ℓ) where
    no-eta-equality

    field
      ρ        : Hom A (W₀ A)
      ρ-counit : W.ε A ∘ ρ ≡ id
      ρ-comult : W₁ ρ ∘ ρ ≡ δ A ∘ ρ

This definition is rather abstract, but has a nice intuition in terms of computational processes. First, recall that a monad $M$ can be thought of as a categorical representation of an abstract syntax tree for some algebraic theory, with the unit $\eta :A\to M(A)$ serving as the inclusion of “variables” into syntax trees, and the join $\mu :M(M(A))\to M(A)$ encoding substitution. From this perspective, a monad algebra $\alpha :M(A)\to A$ describes how to evaluate syntax trees that contain variables of type $A\text{.}$ In other words, a monad $M$ describes some class of inert computations that requires an environment to be evaluated, and a monad algebra describes the objects of $\mathcal{C}$ that can function as environments¹.

Dually, a comonad $W$ can be interpreted as an inert environment that is waiting for a computation to perform, with the counit $\epsilon :W(A)\to A$ discarding the environment, and the comultiplication map $\delta :W(A)\to W(W(A))$ reifying the environment as a value². Similarly, a comonad coalgebra $\rho :A\to W(A)$ describes the objects of $\mathcal{C}$ that can function as computations. More explicitly, the map $\rho :A\to W(A)$ can be thought of as a way of taking an $A$ and situating it in an environment $W(A)\text{;}$ the counit compatibility $\epsilon \circ \rho =\mathrm{id}$ ensures that the underlying $A$ does not change when we include it in an environment, and the comultiplication condition $W(\rho )\circ \rho =\delta \circ \rho$ ensures that the environments reified by $\delta$ align with those produced by $\rho \text{.}$

  open Coalgebra-on
  module _ where
    open Displayed

The Eilenberg-Moore category of a comonad🔗

If we view a comonad $W$ as a specification of an environment, and a comonad coalgebra as a computational process that produces environments, then a homomorphism of $W\text{-coalgebras}$ $(A,\alpha )\to (B,\beta )$ ought to be a map $f:A\to B$ that allows us to “simulate” the computation $\alpha$ via $\beta \text{.}$ We can neatly formalize this intuition by requiring that the following square commute:

    is-coalgebra-hom : ∀ {x y} (h : Hom x y) → Coalgebra-on x → Coalgebra-on y → Type _
    is-coalgebra-hom f α β = W₁ f ∘ α .ρ ≡ β .ρ ∘ f

We can then assemble $W\text{-coalgebras}$ and their homomorphisms into a displayed category over $\mathcal{C}\text{:}$ the type of displayed objects over some $A$ consists of all possible $W\text{-coalgebra}$ structures on $A\text{,}$ and the type of morphisms over $\mathcal{C}(A,B)$ are proofs that $f$ is a $W\text{-coalgebra}$ homomorphism.

    Coalgebras-over : Displayed C (o ⊔ ℓ) ℓ
    Coalgebras-over .Ob[_]            = Coalgebra-on
    Coalgebras-over .Hom[_]           = is-coalgebra-hom
    Coalgebras-over .Hom[_]-set f α β = hlevel 

    Coalgebras-over .id'      = eliml W-id ∙ intror refl
    Coalgebras-over ._∘'_ p q = pushl (W-∘ _ _) ·· ap (W₁ _ ∘_) q ·· extendl p

    Coalgebras-over .idr' f'         = prop!
    Coalgebras-over .idl' f'         = prop!
    Coalgebras-over .assoc' f' g' h' = prop!

The total category of this displayed category is referred to as the Eilenberg Moore category of $W\text{.}$

  Coalgebras : Precategory (o ⊔ ℓ) ℓ
  Coalgebras = ∫ Coalgebras-over

  module Coalgebras = Cat.Reasoning Coalgebras

module _ {o ℓ} {C : Precategory o ℓ} {F : Functor C C} {W : Comonad-on F} where instance
  Extensional-coalgebra-hom
    : ∀ {ℓr} {x y} ⦃ _ : Extensional (C .Precategory.Hom (x .fst) (y .fst)) ℓr ⦄
    → Extensional (Coalgebras.Hom W x y) ℓr
  Extensional-coalgebra-hom ⦃ e ⦄ = injection→extensional! (λ p → total-hom-path (Coalgebras-over W) p prop!) e

module _ {o ℓ} {C : Precategory o ℓ} {F : Functor C C} (W : Comonad-on F) where
  open Cat.Reasoning C
  private module W = Comonad-on W
  open Coalgebra-on
  open W

Cofree coalgebras🔗

Recall that for a monad $M:\mathcal{C}\to \mathcal{C}\text{,}$ the forgetful functor ${\mathcal{C}}^M\to \mathcal{C}$ from the Eilenberg-Moore category has a left adjoint that sends an object $A:\mathcal{C}$ to the free algebra $(M(A),\mu )\text{.}$ We can completely dualize this construction to comonads, which gives us cofree coalgebras.

  Cofree-coalgebra : Ob → Coalgebras.Ob W
  Cofree-coalgebra A .fst = W₀ A
  Cofree-coalgebra A .snd .ρ = δ _
  Cofree-coalgebra A .snd .ρ-counit = δ-idr
  Cofree-coalgebra A .snd .ρ-comult = δ-assoc

  Cofree : Functor C (Coalgebras W)
  Cofree .F₀ = Cofree-coalgebra

  Cofree .F₁ h .hom       = W₁ h
  Cofree .F₁ h .preserves = sym (comult.is-natural _ _ h)

  Cofree .F-id    = ext W-id
  Cofree .F-∘ f g = ext (W-∘ _ _)

However, there is a slight twist: instead of obtaining a left adjoint to the forgetful functor, we get a right adjoint!

  Forget⊣Cofree : πᶠ (Coalgebras-over W) ⊣ Cofree
  Forget⊣Cofree .unit .η (x , α) .hom       = α .ρ
  Forget⊣Cofree .unit .η (x , α) .preserves = α .ρ-comult
  Forget⊣Cofree .unit .is-natural x y f = ext (sym (f .preserves))

  Forget⊣Cofree .counit .η x              = W.ε x
  Forget⊣Cofree .counit .is-natural x y f = W.counit.is-natural _ _ _

  Forget⊣Cofree .zig {A , α} = α .ρ-counit
  Forget⊣Cofree .zag         = ext δ-idl

  to-cofree-hom
    : ∀ {X Y} → Hom (X .fst) Y → Coalgebras.Hom W X (Cofree-coalgebra Y)
  to-cofree-hom f = L-adjunct Forget⊣Cofree f