Coalgebras of polynomial endofunctors

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-03.
Last modified on 2025-10-31.

module trees.coalgebras-polynomial-endofunctors where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import trees.polynomial-endofunctors

Idea

Coalgebras for a polynomial endofunctor P are types X equipped with a function X → P(X).

Definitions

module _
  {l1 l2 : Level} (l : Level) (P : polynomial-endofunctor l1 l2)
  where

  coalgebra-polynomial-endofunctor : UU (l1 ⊔ l2 ⊔ lsuc l)
  coalgebra-polynomial-endofunctor =
    Σ (UU l) (λ X → X → type-polynomial-endofunctor P X)

module _
  {l1 l2 l3 : Level} {P : polynomial-endofunctor l1 l2}
  (X : coalgebra-polynomial-endofunctor l3 P)
  where

  type-coalgebra-polynomial-endofunctor : UU l3
  type-coalgebra-polynomial-endofunctor = pr1 X

  structure-coalgebra-polynomial-endofunctor :
    type-coalgebra-polynomial-endofunctor →
    type-polynomial-endofunctor P type-coalgebra-polynomial-endofunctor
  structure-coalgebra-polynomial-endofunctor = pr2 X

  shape-coalgebra-polynomial-endofunctor :
    type-coalgebra-polynomial-endofunctor → shape-polynomial-endofunctor P
  shape-coalgebra-polynomial-endofunctor x =
    pr1 (structure-coalgebra-polynomial-endofunctor x)

  component-coalgebra-polynomial-endofunctor :
    (x : type-coalgebra-polynomial-endofunctor) →
    position-polynomial-endofunctor P
      ( shape-coalgebra-polynomial-endofunctor x) →
    type-coalgebra-polynomial-endofunctor
  component-coalgebra-polynomial-endofunctor x =
    pr2 (structure-coalgebra-polynomial-endofunctor x)

Recent changes