Examples.PolynomialFunctors

Polynomial-functor examples

This is the Examples.PolynomialFunctors module of the Agda Universal Algebra Library.

This subtree is illustrative. It develops a closed-universe encoding of polynomial functors and their least fixed points (W-types), using the polymorphic-list datatype as a worked example demonstrating the equivalence between the W-type encoding μ (L A) and the standard inductive definition. The content was relocated here under #306 from Legacy.Base.Categories.*; nothing in the canonical Setoid/, Classical/, or planned Cubical/ development depends on it.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Examples.PolynomialFunctors where

open import Examples.PolynomialFunctors.Functors public