Coalgebras of the maybe monad

Content created by Fredrik Bakke.

Created on 2025-01-04.
Last modified on 2025-01-04.

module foundation.coalgebras-maybe where
Imports 
open import foundation.dependent-pair-types
open import foundation.maybe
open import foundation.universe-levels

open import trees.polynomial-endofunctors

Idea

A coalgebra is a type X equipped with a map

  X → Maybe X.

Definitions

Maybe-coalgebra structure on a type

coalgebra-structure-Maybe : {l : Level} → UU l → UU l
coalgebra-structure-Maybe X = X → Maybe X

Maybe-coalgebras

coalgebra-Maybe : (l : Level) → UU (lsuc l)
coalgebra-Maybe l = Σ (UU l) (coalgebra-structure-Maybe)

module _
  {l : Level} (X : coalgebra-Maybe l)
  where

  type-coalgebra-Maybe : UU l
  type-coalgebra-Maybe = pr1 X

  map-coalgebra-Maybe : type-coalgebra-Maybe → Maybe type-coalgebra-Maybe
  map-coalgebra-Maybe = pr2 X

Recent changes