This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Full binary trees

module trees.full-binary-trees where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.empty-types
open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types

Idea

A full binary tree is a finite directed tree in which every non-leaf node has a specified left branch and a specified right branch. More precisely, a full binary tree consists of a root, a left full binary subtree and a right full binary subtree.

Definitions

Full binary trees

data full-binary-tree : UU lzero where
  leaf-full-binary-tree : full-binary-tree
  join-full-binary-tree : (s t : full-binary-tree) → full-binary-tree