Standard finite pruned trees

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

Created on 2022-03-07.
Last modified on 2023-03-13.

module univalent-combinatorics.standard-finite-pruned-trees where
open import elementary-number-theory.natural-numbers

open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types


A standard finite pruned tree of height n can be thought of as a standard finite tree in which each path from the root to a leaf has length n + 1.


data Pruned-Tree-Fin :   UU lzero where
  root-Pruned-Tree-Fin : Pruned-Tree-Fin zero-ℕ
  tree-Pruned-Tree-Fin :
    (n k : )  (Fin k  Pruned-Tree-Fin n)  Pruned-Tree-Fin (succ-ℕ n)

width-Pruned-Tree-Fin : (n : )  Pruned-Tree-Fin (succ-ℕ n)  
width-Pruned-Tree-Fin n (tree-Pruned-Tree-Fin .n k x) = k

Recent changes