Diagrammatric observational type theory

<! --- LETTERS ---> $$ \newcommand{\lR}{\mathbb{R}} $$ $$ \newcommand{\lZ}{\mathbb{Z}} $$ $$ \newcommand{\lN}{\mathbb{N}} $$ $$ \newcommand{\lI}{\mathbb{I}} $$ $$ \newcommand{\II}{\mathbb{I}} $$ $$ \newcommand{\bI}{\mathbf{I}} $$ $$ \newcommand{\bC}{\mathbf{C}} $$ $$ \newcommand{\bD}{\mathbf{D}} $$ $$ \newcommand{\bE}{\mathbf{E}} $$ $$ \newcommand{\bF}{\mathbf{F}} $$ $$ \newcommand{\iI}{\mathsf{I}} $$ $$ \newcommand{\iA}{\mathsf{A}} $$ $$ \newcommand{\iB}{\mathsf{B}} $$ $$ \newcommand{\iC}{\mathsf{C}} $$ $$ \newcommand{\iD}{\mathsf{D}} $$ $$ \newcommand{\iE}{\mathsf{E}} $$ $$ \newcommand{\iF}{\mathsf{F}} $$ $$ \newcommand{\iM}{\mathsf{M}} $$ <! --- SYMBOLS ---> $$ \newcommand{\eps}{\epsilon} $$ $$ \newcommand{\SetCat}{\mathrm{Set}} $$ $$ \newcommand{\Bool}{\mathrm{Bool}} $$ $$ \newcommand{\Pos}{\mathrm{Pos}} $$ $$ \newcommand{\lbl}{\mathsf{lbl}} $$ $$ \newcommand{\subdiv}{\mathsf{sd}} $$ $$ \newcommand{\Hom}{\mathrm{Hom}} $$ $$ \newcommand{\Fun}{\mathrm{Fun}} $$ $$ \newcommand{\Psh}{\mathrm{PSh}} $$ <! --- OPERATORS ---> $$ \newcommand{\dim}{\mathrm{dim}} $$ $$ \newcommand{\id}{\mathrm{id}} $$ $$ \newcommand{\src}{\partial^-} $$ $$ \newcommand{\tgt}{\partial^+} $$ $$ \newcommand{\und}[1]{\underline{#1}} $$ $$ \newcommand{\abs}[1]{\left|{#1}\right|} $$ $$ \newcommand{\op}{^{\mathrm{op}}} $$ $$ \newcommand{\inv}{^{-1}} $$ <! --- CATEGORIES, FUNCTORS AND CONSTRUCTIONS ---> $$ \newcommand{\ttr}[1]{\mathfrak{T}^{#1}} $$ $$ \newcommand{\lttr}[2]{\mathfrak{T}^{#1}{(#2)}} $$ $$ \newcommand{\truss}[1]{\mathsf{T}\!\mathsf{rs}_{#1}} $$ $$ \newcommand{\sctruss}[1]{\bar{\mathsf{T}}\!\mathsf{rs}_{#1}} $$ $$ \newcommand{\rotruss}[1]{\mathring{\mathsf{T}}\!\mathsf{rs}_{#1}} $$ $$\newcommand{\trussbun}[1]{\mathsf{TrsBun}_{#1}} $$ $$ \newcommand{\trusslbl}[1]{\mathsf{Lbl}\mathsf{T}\!\mathsf{rs}_{#1}} $$ $$ \newcommand{\blcat}[1]{\mathsf{B}\mathsf{lk}_{#1}} $$ $$ \newcommand{\blset}[1]{\mathsf{Blk}\mathsf{Set}_{#1}} $$ $$ \newcommand{\fcl}[2]{\chi^{#1}_{#2}} $$ $$ \newcommand{\Entr}{\mathsf{Entr}} $$ $$ \newcommand{\Exit}{\mathsf{Exit}} $$ <! --- ARROWS AND RELATIONS ---> $$ \newcommand{\fleq}{\preceq} $$ $$ \newcommand{\fles}{\prec} $$ $$ \newcommand{\xto}[1]{\xrightarrow{#1}} $$ $$ \newcommand{\xot}[1]{\xleftarrow{#1}} $$ $$ \newcommand{\ot}{\leftarrow} $$ $$ \newcommand{\toot}{\leftrightarrow} $$ $$ \newcommand{\imp}{\Rightarrow} $$ $$ \newcommand{\iff}{\Leftrightarrow} $$ $$ \newcommand{\iso}{\cong} $$ $$ \newcommand{\into}{\hookrightarrow} $$ $$ \newcommand{\proto}{\longrightarrow\mkern{-2.8ex}{\raisebox{.3ex}{$\tiny\vert$}}\mkern{2.5ex}} $$ <! --- DIAGRAM ARROWS ---> <! ---... should replace \rlap by \mathrlap, see KaTeX doc ---> $$ \newcommand{\ra}[1]{\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} $$ $$ \newcommand{\la}[1]{\xleftarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} $$ $$ \newcommand{\da}[1]{\downarrow\raisebox{.5ex}{\rlap{$\scriptstyle#1$}}} $$ $$ \newcommand{\dra}[1]{\raisebox{.2ex}{\llap{$\scriptstyle#1$}}\kern-.5ex\searrow}} $$ $$ \newcommand{\dla}[1]{\swarrow\kern-1ex\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$ $$ \newcommand{\ua}[1]{\uparrow\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$ $$ \newcommand{\ura}[1]{\raisebox{.2ex}{\llap{$\scriptstyle#1$}\kern-.5ex\nearrow}} $$ $$ \newcommand{\ula}[1]{\nwarrow\kern-1ex\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$

Abstract. Diagrammatic type theory takes a novel approach to working with higher directed inductive types. This does a way with complication of inductive types to unveil a (the) deeper mystery of canonical isotopies.

Context

When I wrote nine short stories about diagrammatic higher categories I struggled a bit in the last story (the vaguest of them all) when trying to express what I wanted from my diagrammatic type theory. It seems to me that observational type theory takes a perspective that fruitfully resolves some of these struggles. Maybe someone can make this more precise? (Put differently, is their something to be gained in combining the adjective “observational” and “diagrammatic”?)

The basic principle

Inductive types are great. In full generality, this means directed higher inductive types, which are still not well understood.

One obvious reason for studying directed higher type theory (especially when $n = \infty$ in the above) is generality: $(\infty,\infty)$-categories are among the most general higher categorical structures. Concretely this offers the following conceptual advantages.

• Universe types can retain their higher directed structure. type universe

  Universe types are (small) ‘internal’ reflections of the category of all types of our type theory, but without sufficient higher structure in the theory, this reflection process must forget structure present in the external category (for instance, the category of sets can only contain a ‘set of sets’ as an object which does not remember functions; similarly, the universe type in homotopy type theory must forget about maps between types that are not equivalences).

• Dependent function types become ‘just’ function types. In the presence of higher directed structure, equipped with a universe type $\mathcal{U}$ and unit type $\mathbf{1}$, dependent function types $\Pi_{x : A} F(x)$, for $F$ a type family $F : A \to \mathcal{U}$, can be understood in terms of ‘just’ function types, namely, as $\mathsf{Fun}{\mathsf{Fun}(A,\mathcal{U})}(\mathrm{const}{\mathbf{1}}, F)$ (where $\mathrm{const}_{\mathbf{1}} : A \to \mathcal{U}$ is the constant functor with image $\mathbf{1}$).

• Inductive types become substantially more expressive. Inductive types with dependent constructors can also be expressed in terms of non-dependent constructors: for instance, for $F$ a type family $F : A \to \mathcal{U}$, the dependent pair type $\Sigma_{x : A} F(x)$ can be introduced with a single constructor $\mathrm{in} : F \to \mathrm{const}{\Sigma{x : A} F(x)}$ (which is a map in the function type $\mathsf{Fun}(A, \mathcal{U})$ and should thus be thought of as a natural transformation between functors). Moreover, there is the topic of higher inductive types; a useful example of a ‘true’ directed higher inductive type is the poset type $(\mathbb{N},\leq)$ with constructors \(0 : \mathbf{1} \to \mathbb{N}\) \(\mathsf{succ} : \mathbb{N} \to \mathbb{N}\) \(\mathsf{less} : \mathrm{id}_{\mathbb{N}} \to \mathsf{succ}\)

• Formalization of (higher) categorical semantics. On a more practical side, access to higher directed structure could allow us to formalize the categorical semantics of other types theories, such as homotopy type theory.

The basic problem, solution, and problem

A key problem in working with higher inductive types is that they are “small types”, and correctly defining their higher compositional structure (i.e., categorical composition) usually uses “big machinery”.

But, as we’ve previously discussed, diagrammatic categories (or more precisely, diagrammatic computads) solve this problem. So … you should be able to build a cool higher directed type theory with them?

There’s only one difficulty (here, I see us in a situation of debugging our human approach to mathematics: we solve one problem to uncover a deeper one): canonicity. In order to make our type theory “compute” (i.e., fully resolve terms into expressions of generators) we must be able to guaranteee that isotopies (i.e., diagrammatic coherences) decompose (at least non-constructively) into finite, classifiable, generators.

This reduces to the classification of isotopies that we previously discussed, and thus deeply entangles (ha!) the isotopy classification problem with canonicity of diagrammatic type theory.

(PS)

(But: even in the absence of canonicity, you could likely go ahead an formulate a higher directed observational type theory … in which things are “true until disproven” :D)