# Planar binary trees

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-05-06.

module trees.planar-binary-trees where

Imports
open import foundation.booleans
open import foundation.empty-types
open import foundation.function-types
open import foundation.universe-levels

open import trees.w-types


## Idea

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.

## Definitions

### 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
where
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 α
where
α : bool → PBT-𝕎
α true = x
α false = y


## Properties

### The types Planar-Bin-Tree and PBT-𝕎 are equivalent

{-
Planar-Bin-Tree-PBT-𝕎 : PBT-𝕎 → Planar-Bin-Tree
Planar-Bin-Tree-PBT-𝕎 (tree-𝕎 true α) =
join-PBT
( Planar-Bin-Tree-PBT-𝕎 (α true))
( Planar-Bin-Tree-PBT-𝕎 (α false))
Planar-Bin-Tree-PBT-𝕎 (tree-𝕎 false α) = {!!}
-}