This repository contains the formalisation of (most of) the results presented in my PhD thesis. There are two developments: the first one concerns the type-theoretical definition of opetopes (Chapter 1), while the second one concerns opetopic types and their applications (Chapters 2 and 3). Each project comes with the agda source code and a html version thereof. They depend on the agda HoTT library.
These two projects are based on Eric Finster's work: