Lower types of elements in W-types
Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.
Created on 2023-01-26.
Last modified on 2024-04-11.
module trees.lower-types-w-types where
Imports
open import foundation.existential-quantification open import foundation.universe-levels open import trees.ranks-of-elements-w-types open import trees.w-types
Idea
We define by induction a type family over W A B
in a way that generalizes the
construction of the standard finite types over ℕ to arbitrary W-types.
Definition
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where data lower-𝕎 : 𝕎 A B → UU (l1 ⊔ l2) where lower-tree-𝕎 : {x : A} {f : B x → 𝕎 A B} → ((y : B x) → lower-𝕎 (f y)) → lower-𝕎 (tree-𝕎 x f) inclusion-lower-𝕎 : {x : 𝕎 A B} → lower-𝕎 x → 𝕎 A B inclusion-lower-𝕎 (lower-tree-𝕎 {a} {f} g) = tree-𝕎 a (λ y → inclusion-lower-𝕎 (g y)) upper-bound-rank-inclusion-lower-𝕎 : {x : 𝕎 A B} (y : lower-𝕎 x) → inclusion-lower-𝕎 y ≼-𝕎 x upper-bound-rank-inclusion-lower-𝕎 (lower-tree-𝕎 g) y = intro-exists y (upper-bound-rank-inclusion-lower-𝕎 (g y))
Recent changes
- 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).