Algebras for polynomial endofunctors

Content created by Fredrik Bakke and Egbert Rijke.

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

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

open import trees.polynomial-endofunctors

Idea

Given a polynomial endofunctor P, an algebra for P consists of a type X and a map P(X) → X.

Definitions

Algebras for polynomial endofunctors

algebra-polynomial-endofunctor :
  (l : Level) {l1 l2 : Level} →
  polynomial-endofunctor l1 l2 →
  UU (lsuc l ⊔ l1 ⊔ l2)
algebra-polynomial-endofunctor l P =
  Σ (UU l) (λ X → type-polynomial-endofunctor P X → X)

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

  type-algebra-polynomial-endofunctor :
    algebra-polynomial-endofunctor l P → UU l
  type-algebra-polynomial-endofunctor X = pr1 X

  structure-algebra-polynomial-endofunctor :
    (X : algebra-polynomial-endofunctor l P) →
    type-polynomial-endofunctor P (type-algebra-polynomial-endofunctor X) →
    type-algebra-polynomial-endofunctor X
  structure-algebra-polynomial-endofunctor X = pr2 X

Recent changes