Trees

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2023-01-26.
Last modified on 2024-04-17.

{-# OPTIONS --guardedness #-}

Files in the trees module

module trees where

open import trees.algebras-polynomial-endofunctors public
open import trees.bases-directed-trees public
open import trees.bases-enriched-directed-trees public
open import trees.binary-w-types public
open import trees.bounded-multisets public
open import trees.coalgebra-of-directed-trees public
open import trees.coalgebra-of-enriched-directed-trees public
open import trees.coalgebras-polynomial-endofunctors public
open import trees.combinator-directed-trees public
open import trees.combinator-enriched-directed-trees public
open import trees.directed-trees public
open import trees.elementhood-relation-coalgebras-polynomial-endofunctors public
open import trees.elementhood-relation-w-types public
open import trees.empty-multisets public
open import trees.enriched-directed-trees public
open import trees.equivalences-directed-trees public
open import trees.equivalences-enriched-directed-trees public
open import trees.extensional-w-types public
open import trees.fibers-directed-trees public
open import trees.fibers-enriched-directed-trees public
open import trees.full-binary-trees public
open import trees.functoriality-combinator-directed-trees public
open import trees.functoriality-fiber-directed-tree public
open import trees.functoriality-w-types public
open import trees.hereditary-w-types public
open import trees.indexed-w-types public
open import trees.induction-w-types public
open import trees.inequality-w-types public
open import trees.lower-types-w-types public
open import trees.morphisms-algebras-polynomial-endofunctors public
open import trees.morphisms-coalgebras-polynomial-endofunctors public
open import trees.morphisms-directed-trees public
open import trees.morphisms-enriched-directed-trees public
open import trees.multiset-indexed-dependent-products-of-types public
open import trees.multisets public
open import trees.planar-binary-trees public
open import trees.plane-trees public
open import trees.polynomial-endofunctors public
open import trees.raising-universe-levels-directed-trees public
open import trees.ranks-of-elements-w-types public
open import trees.rooted-morphisms-directed-trees public
open import trees.rooted-morphisms-enriched-directed-trees public
open import trees.rooted-quasitrees public
open import trees.rooted-undirected-trees public
open import trees.small-multisets public
open import trees.submultisets public
open import trees.transitive-multisets public
open import trees.underlying-trees-elements-coalgebras-polynomial-endofunctors public
open import trees.underlying-trees-of-elements-of-w-types public
open import trees.undirected-trees public
open import trees.universal-multiset public
open import trees.universal-tree public
open import trees.w-type-of-natural-numbers public
open import trees.w-type-of-propositions public
open import trees.w-types public

Recent changes