M types as limits

module m where

open import sum
open import equality
open import function
open import sets.nat
open import sets.unit
open import hott.level.core

module _ (A : Set)(B : A → Set) where
  F : Set → Set
  F X = Σ A λ a → B a → X

  map : {X Y : Set} → (X → Y) → F X → F Y
  map f (a , u) = a , f ∘' u

  W : ℕ → Set
  W 0 = ⊤
  W (suc n) = F (W n)

  hd : {n : ℕ} → W (suc n) → A
  hd (a , u) = a

  tl : {n : ℕ}(w : W (suc n)) → B (hd w) → W n
  tl (a , u) = u

  trunc : (n : ℕ) → W (suc n) → W n
  trunc zero w = tt
  trunc (suc n) (a , u) = a , λ b → trunc n (u b)

  record M : Set where
    constructor mk-m
    field
      f : (n : ℕ) → W n
      trunc-eq : (n : ℕ) → f n ≡ trunc n (f (suc n))

  open M using (trunc-eq) renaming (f to _!_)

  IsCoalg : Set → Set
  IsCoalg X = X → F X

  Coalg : Set₁
  Coalg = Σ Set IsCoalg

  IsMor : {X Y : Set} → IsCoalg X → IsCoalg Y → (X → Y) → Set
  IsMor {X}{Y} θ ψ f = (x : X) → ψ (f x) ≡ map f (θ x)

  Mor : Coalg → Coalg → Set
  Mor (X , θ) (Y , ψ) = Σ (X → Y) (IsMor θ ψ)

  eq-a : (m : M)(n : ℕ) → hd (m ! 1) ≡ hd (m ! suc n)
  eq-a m zero = refl
  eq-a m (suc n) = eq-a m n · ap proj₁ (trunc-eq m (suc n))

  out : IsCoalg M
  out m = a , λ b → mk-m (f' b) (p' b)
    where
      a : A
      a = hd (m ! 1)

      f' : B a → (n : ℕ) → W n
      f' b n = tl (m ! suc n) (subst B (eq-a m n) b)

      p' : (b : B a)(n : ℕ) → f' b n ≡ trunc n (f' b (suc n))
      p' b n = {!!}

  M* : Coalg
  M* = M , out

  out-terminal : (X : Coalg) → contr (Mor X M*)
  out-terminal = {!!}