Indexed W-types
Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.
Created on 2023-01-26.
Last modified on 2023-05-16.
module trees.indexed-w-types where
Imports
open import foundation.universe-levels
Idea
Indexed W-types are a generalization of ordinary W-types using indexed containers. The main idea is that indexed W-types are initial algebras for the polynomial endofunctor
(X : I → UU) ↦ Σ (a : A i), Π (b : B i a), X (f i a b),
where f : Π (i : I), Π (a : A i), B i a → I
is a reindexing function.
data i𝕎 {l1 l2 l3 : Level} (I : UU l1) (A : I → UU l2) (B : (i : I) → A i → UU l3) (f : (i : I) (x : A i) → B i x → I) (i : I) : UU (l2 ⊔ l3) where tree-i𝕎 : (x : A i) (α : (y : B i x) → i𝕎 I A B f (f i x y)) → i𝕎 I A B f i
Recent changes
- 2023-05-16. Fredrik Bakke. Swap from
md
totext
code blocks (#622). - 2023-05-03. Egbert Rijke. Enriched directed trees and elements of W-types (#561).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).
- 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).