The universal polynomial endofunctor

Content created by Fredrik Bakke.

Created on 2025-10-31.
Last modified on 2025-10-31.

module trees.universal-polynomial-endofunctor where
Imports 
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.universe-levels

open import trees.polynomial-endofunctors

Idea

The universal polynomial endofunctor is the polynomial endofunctor whose type of shapes is the universe of types Type, and whose family of positions is the identity function.

Definition

universal-polynomial-endofunctor :
  (l : Level) → polynomial-endofunctor (lsuc l) l
universal-polynomial-endofunctor l = (UU l , id)

Recent changes