Short Intro to Opetopes

Seminar 2013-11-19

My goals:

1. form an intuition of opetopic sets
2. sketch a calculus of (string) diagrams
3. discuss the missing piece of cartesian closure
4. potential applications to Ωmega 2.0

Origin

Mid-1990'es by Baez and Dolan (metatree, opetope), published as arXiv:q-alg/9702014.

TQFTs arXiv:q-alg/9503002

Many People

Various researchers/groups contributed since, and similar concepts go by a multitude of names

• Multitopes – Hermida, Makkai
• Opetopes – Eugenia Cheng (e.g. arXiv:math/0304284)
• "positive-to-one computads" – Marek Zawadowski, arXiv:0708.2658
• Szawiel, Marek Zawadowski arXiv:1011.2374
• Joachim Kock, et al. arXiv:0706.1033

At IAS:

• Krzysztof Kapulkin
• Eric Finster

Higher-dimensional Trees

Polynomial functors and monads (iterated construction)

Zooms and Complexes

We define zooms as configurable 'tree transformers'.

Then we compose zooms to compexes, subject to boundary conditions.

Zoom definition

Input data: finite rooted (planar) trees (the nth dimension)

Freely decorate with disks, adhering to rules:

• disk must cut branch(es), but nothing else
• every disk must capture a subtree

Input-to-output translation

Just change the perspective!

Translate to tree in the (n+1)th dimension

Input		Output
branch	⊣
dot	⇒	(unit) branch
disk	⇒	dot

Special case: corolla

A corolla is a special zoom with just one dot in the left tree and no disks.

The output tree is thus a unit branch:

Assembling the complex

The trees have labelled branches and dots (without repetition)

Zooms can be joined when the trees match, forming a zoom complex.

Note: These complexes form a semicategory, as there are input trees not admitting an identity zoom (e.g. unit tree, most corollas).

Opetope

A zoom complex with dimensions

-2	-1	…	n+1
O	(.)		.

and a corolla appearing in the last dimension is called an opetope.

Opetopes are normally drawn starting with dimension 0.

• a 0-dimensional opetope is (isomorphic to) a natural number
• the zoom in dimension 1 has a planar tree input

You can construct opetopes interactively.

Inductive Datatypes

Finster gives data type + typechecker

But intrinsic definition of Zooms is possible.

Category of Opetopes

Similarly defined as the category of singular complexes ∆

• Morphisms are face maps (corresponding to each 'round-ish thing')

• Identity morphism (the top cell)

Pointers

To mark (e.g.) a dot in a tree we use trees that only have one unit branch

Composition

"pointer" tree to mark a unit branch

then graft

Substitution

Mark an n-ary node (or disk), swap it for an n-ary tree

Analogous to monadic bind.

Geometric Realization

As pasting diagrams.

As string diagrams (dual to the above).

Coherence conditions

Automatically "type-checked"

Deductions (following Finster)

Let's have a formal language whose 'terms' are pasting diagrams.

We (say) start out with a set of basic opetopes (axioms).

What are the deduction rules to create new ones?

N.B.: How deductions (proof trees) map to adjuctions in is nicely described here.

Empty rule

From any opetope one can derive an empty pasting diagram one dimension up.

See the corolla zoom. It only shows the highest-dimensional zoom, but that is ok as nothing below changes.

Paste rule

Given n pasting diagrams and a cell (corolla) with n branches

• such that the target cells of the pasting diagrams match the (input) branches
• then a bigger pasting diagram can be created

See pointer guided composition, which is the atomic operation underlying this rule.

Composite rule

Universal cell introduction

Universal cell elimination

Similar to the J-rule

Can we Obtain Cartesian Closure?

Tensor product on operads http://arxiv.org/pdf/math/0701293.pdf

Boardman-Vogt tensoring: http://arxiv.org/pdf/1302.3711.pdf

Operator categories: http://arxiv.org/pdf/1302.5756.pdf

Symmetric monoidal closed, yes, but cartesian?

• Gambino and Joyal: http://www1.maths.leeds.ac.uk/~pmtng/Research/Lectures/gambino-bmc.pdf

Excursion: Lambda Calculus

Several notations, e.g. λ (with μ), item notation (Kamareddine, Nederpelt)

let's come up with another one! (…see also Zena Ariola…)

(Binary) search tree

We start with a lambda term

Respecting scope we build a search tree and retrofit it with references

Kind for shapes

kind Sh = Ap Sh Sh | Lm Sh | Rf Ref
kind Ref = Up Ref | Stop | Left Ref | Right Ref | Down Ref

Abstraction / Binders

Key insight: Trees admit naturals

But we need deBruijn + extra sauce

References: Identification, gluing

• gluing an input on a (constructor) application ⟶ pattern matching
• … means: "application dot" here
• gluing inputs vanish from application dot
• n-ary application possible? semantics?

Beta-reduction

When a selected external branch is saturated by application, it completely dissolves, and the addressed binding station gets glued to the argument.

Depending on the intended reduction strategy the use references may be expanded (unsharing).

Internal Hom

(→) is binary type constructor

• profunctor (contra-/covariant)
• Klein bottle (orientation-reversing)

Strata in Ωmega

Singleton Types in Haskell

Kind promotion

data {- kind -} Nat = Z | S Nat

data Nat' :: Nat -> * where
  Z' :: Nat' Z
  S' :: Nat' n -> Nat' (S n)

Singleton Types in Ωmega

Kind definitions possible (at any level)

kind Nat = Z | S Nat

data Nat' :: Nat ~> * where
  Z' :: Nat' Z
  S' :: Nat' n -> Nat' (S n)

Level Polymorphism

data Nat :: level k . *k where
  Z :: Nat
  S :: Nat ~> Nat

Can we please have Curry-Howard back?

C-H lost as level-polymorphic type Nat above has no type parameter/index!

Idea: parametrize with the same thing, but from one level up...

Unfortunately this is not working out :-(

I tried:

For a few levels (each differently named) it can be made.

Next idea

parametrize on the left. Make access to parameter optional.

these all mean the same thing:

S Z :: Nat
S Z :: S Z ° Nat
S Z :: (S Z :: Nat) ° Nat
S Z :: (S Z :: S Z ° Nat) ° Nat

Ad infinitum, coinductively.

Programming in the Sky

Program in the (co)limit. Write a very simple data definition

data Nat = Z | S Nat

… but have the refinement structure available when wanting to state type-level propositions.

Conclusion

1. Opetopic calculus is rich and very interesting
2. It appears to be a solid basis for stratified type systems
3. Cartesian closure not completely understood yet

Questions?

Thanks for your attention!

Btw. I am looking for collaborators

1. to make these ideas precise
2. kick-start an initial implementation.