Higher Dimensional Trees

Opetopes are a collection of polytopes which correspond to certain well-formed higher dimensional trees. It takes some work to make precise what one means by well-formed, so in this section, we will warm up with a simpler definition of what exactly is a higher dimensional tree, and we will use this to motivate the definition of opetopes to follow.

We begin by examining some low dimensional incarnations of trees. The data type definitions which follow are given in two forms, one using more or less standard naming conventions, and the other named in order to bring out the pattern we are trying to generalize.

A zero-dimensional tree is just a point. As we want to consider trees with nodes labeled in some type A, this means that the type constructor corresponding to zero-dimensional trees is the Id constructor, which is presented below.

data Id (A : Set) : Set where
  id : A -> Id A
	

data Tree0 (A : Set) : Set where
  pt0 : A -> Tree0 A
	

We can make a picture of an element of our type, say with A taken to be the natural numbers. As described, the identity constructor gives us just a single point of data.

Now consider the following two definitions of list.

data List (A : Set) : Set where
  nil : List A
  cons : A -> Id (List A) -> List A
	

data Tree1 (A : Set) : Set where
  leaf1 : Tree1 A
  node1 : A -> Tree0 (Tree1 A) 
            -> Tree1 A
	

The picture of a list is slightly more interesting.

Next, here are the definitions in dimension 2.

data Tree (A : Set) : Set where
  leaf : Tree A
  node : A -> List (Tree A) -> Tree A
	

data Tree2 (A : Set) : Set where
  leaf2 : Tree2 A
  node2 : A -> Tree1 (Tree2 A) 
            -> Tree2 A
	

A now we get to a traditional, two-dimensional tree.

Looking back at our definitions, we can see that we can immediately generalize our trees to all dimensions with the following indexed inductive type.

data Tree (A : Set) : N -> Set where
  pt : A -> Tree A 0
  leaf : {n : N} -> Tree A (S n)
  node : {n : N} -> A -> Tree (Tree A (S n)) n -> Tree A (S n)
	

Here is a picture of the three dimensional tree: