Planar binary trees

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-05-06.
Last modified on 2024-04-13.

module trees.planar-binary-trees where
open import foundation.booleans
open import foundation.empty-types
open import foundation.function-types
open import foundation.universe-levels

open import trees.w-types


A planar binary tree is a binary tree in which the branchings are labeled by the booleans. The idea is that at any branching point in a planar binary tree, we know which branch goes to the left and which branch goes to the right.

Planar binary trees are commonly called binary trees, but in univalent mathematics it makes sense to recognize that the branching points in a binary tree should not record which branch goes left and which branch goes right.


The inductive definition of the type of planar binary trees

data Planar-Bin-Tree : UU lzero where
  root-PBT : Planar-Bin-Tree
  join-PBT : (x y : Planar-Bin-Tree)  Planar-Bin-Tree

The definition of the type of planar binary trees as a W-type

PBT-𝕎 : UU lzero
PBT-𝕎 = 𝕎 bool P
  P : bool  UU lzero
  P true = bool
  P false = empty

root-PBT-𝕎 : PBT-𝕎
root-PBT-𝕎 = constant-𝕎 false id

join-PBT-𝕎 : (x y : PBT-𝕎)  PBT-𝕎
join-PBT-𝕎 x y = tree-𝕎 true α
  α : bool  PBT-𝕎
  α true = x
  α false = y

Recent changes