\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{opetopic type theory}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{higher_category_theory}{}\paragraph*{{Higher category theory}}\label{higher_category_theory}

[[!include higher category theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{related_entries}{Related entries}\dotfill \pageref*{related_entries} \linebreak
\noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

\emph{Opetopic type theory} (\hyperlink{Finster12}{Finster 12}) is a higher dimensional [[directed homotopy type theory|directed]] [[homotopy type theory|homotopy]] [[type theory]] for [[omega-categories]], i.e. of [[infinity-categories]] in the full sense of [[(infinity,infinity)-categories]]. Specifically it realizes the higher-dimensional [[horn]]-filler conditions in the definition of [[opetopic omega-categories]] \href{opetopic+omega-category#DefinitionByPalm}{due to Palm} as [[inference rules]] of [[term introduction]] for a higher-dimensional kind of [[formal logic]] (but it presently ignores the saturation condition on the thin cells).

Where in [[homotopy type theory]] there is an [[identity type]] of any type axiomatizing the [[infinity-groupoid]] structure of that type in, effectively, the style of a [[globular omega-groupoid]], in opetopic type theory there is axiomatized instead a type of [[k-morphisms]] for all $k$ in the [[geometric shape for higher structures|shape]] of [[opetopes]].

Hence given a base type $\mathbf{B}\mathcal{U}$ -- and a priori there is just one, to be thought of as the categorically delooped [[type universe]], see below -- a type is thus effectively identified with the shape of an [[opetope]] and thought of as the type of [[k-morphisms]] in $\mathbf{B}\mathcal{U}$, the only other data being a possible marking that identifies it as just the sub-type of $k$-[[equivalences]] of the given opetopic shape.

The only [[natural deduction|deduction rule]] is opetopic [[type formation]] and a [[term introduction]] rule which expresses the evident [[Kan complex|Kan filler-like]] condition saying that if a term of given opetopic shape is an outer [[horn]] (here: a ``nook'') of $k$-cells, then a $k$-dimensional filler term is deduced, and if an outer or inner [[horn]] has a boundary by equivalences then a filler term marked as an equivalence is deduced.

Due to the genuinely [[infinity-category|omega-categorical]] nature of the setup, it makes sense to think of the (a priori) unique base type $\mathbf{B}\mathcal{U}$ as the categorical [[delooping]] of a [[type universe]] $\mathcal{U}^\times$ being a [[monoidal (infinity,n)-category]] [[omega-category]], and hence of the 1-[[endomorphisms]] (hence the terms of shape the [[interval category|directed interval]] $(\mathbf{B}\mathcal{U}\to \mathbf{B}\mathcal{U})$ ) as being the [[types]] in that universe. Composition of 1-morphism hence implies a [[type formation]] for [[multiplicative conjunction]]-types in a directed kind of [[linear homotopy type theory]].

Introducing an [[axiom]] to this system just means postulating terms of (the type of) the shape of prescribed [[opetopes]]. For example:

\begin{itemize}%
\item \textbf{$n$-trunction} -- For the language inside an [[(infinity,n)-category]] one demands that all [[k-morphisms]] for $k \geq n+1$ are marked as [[equivalences]];


\item \textbf{$k$-adjoints} -- To axiomatize that two $k$-morphism are [[left adjoint]] and [[right adjoint]] to each other, respectively, one postulates the existence of $k+1$-morphisms serving as [[unit of an adjunction]] and [[counit of an adjunction]] and of a [[3-morphism]] marked as [[equivalence]] which axiomatizes the [[zig-zag identities]].



\end{itemize}
Imposing $n$-trunction and adjoints for all [[k-morphisms]] for $0 \leq k \leq n$ therefore axiomatizes the language for a [[free construction|free]] [[(infinity,n)-category with adjoints]] on a single object. Categorical looping (which is immediate and primitive in the system, as above) hence gives the [[free construction|free]] [[(infinity,n)-category with duals]] on a single object.

This is the structure to which the [[cobordism hypothesis]] applies. Of course the proof of the cobordism hypothesis is not formulated in opetopic type theory and one would have to show that the language it is formulated in is suitably equivalent to that of opetopic type theory, but inspection in low dimension shows that the [[higher dimensional traces]] that opetopic type theory produces are of just the right kind.

\hypertarget{related_entries}{}\subsection*{{Related entries}}\label{related_entries}

[[!include proof assistants and formalization projects -- list]]

\hypertarget{References}{}\subsection*{{References}}\label{References}

Opetopic type theory is due to

\begin{itemize}%
\item [[Eric Finster]], \emph{Type Theory and the Opetopes}, talk at \href{http://www.mimuw.edu.pl/~zawado/SemTK/OSTKA.html}{Polish Seminar on Category Theory and its Applications, June 2012} (\href{http://sma.epfl.ch/~finster/opetope/types-and-opetopes.pdf}{pdf})

\end{itemize}
It [[syntax|syntactically]] implements the definition of [[opetopic omega-category]] due to

\begin{itemize}%
\item [[Thorsten Palm]], \ldots{}

\end{itemize}
by interpreting the higher-dimensional [[horn]]-filler conditions given there as [[inference rules]].

(\hyperlink{Palm}{Palm} shows that any opetopic set satisfying these filler conditions satisfies the property of [[Michael Makkai]]`s definition of a opetopic set that qualifies as an [[opetopic omega-category]]. The converse is presently unknown.)

The higher dimensional [[string diagram]]-notation used here for opetopes was introduced (as ``zoom complexes'' in section 1.1) in

\begin{itemize}%
\item [[Joachim Kock]], [[André Joyal]], [[Michael Batanin]], [[Jean-François Mascari]], \emph{Polynomial functors and opetopes} (\href{http://arxiv.org/abs/0706.1033}{arXiv:0706.1033})

\end{itemize}
Animated exposition of this higher-dimensional string-diagram notation is in

\begin{itemize}%
\item [[Eric Finster]], \emph{Opetopic Diagrams 1 - Basics} (\href{http://www.youtube.com/watch?v=OANwLohwJqk}{video})


\item [[Eric Finster]], \emph{Opetopic Diagrams 2 - Geometry} (\href{http://www.youtube.com/watch?v=E7OvuA1jRKM}{video})



\end{itemize}
A computer [[proof assistant]] for working with opetopic type theory is

\begin{itemize}%
\item [[Eric Finster]], \emph{Orchard} (\href{https://github.com/ericfinster/orchard}{GitHub repository})


\item [[Eric Finster]], \emph{\href{http://sma.epfl.ch/~finster/opetope/opetope.html}{Opetope!}} (online opetopic type theory system)



\end{itemize}
A video tutorial for Orchard is

\begin{itemize}%
\item [[Eric Finster]], \emph{Orchard 1 - Introduction} (\href{http://www.youtube.com/watch?v=sEVJJCwohW0&list=PLWAw3zSOqFVKZ-LzAq4hQaKIVj8zjtfCs}{video})


\item [[Eric Finster]], \emph{Orchard 2 - Modifying the shape} (\href{http://www.youtube.com/watch?v=sEVJJCwohW0&list=PLWAw3zSOqFVKZ-LzAq4hQaKIVj8zjtfCs}{video})


\item [[Eric Finster]], \emph{Orchard 3 - Composition and associativity} (\href{http://www.youtube.com/watch?v=Vxnf_3Bxj2o&index=5&list=PLWAw3zSOqFVKZ-LzAq4hQaKIVj8zjtfCs}{video})


\item [[Eric Finster]], \emph{Orchard 4 - Identities and invertibility} (\href{http://www.youtube.com/watch?v=DRFjUSaNexQ&list=PLWAw3zSOqFVKZ-LzAq4hQaKIVj8zjtfCs&index=6}{video})



\end{itemize}
Apparently Orchard is discontinued in favour of an online version of similar functionality:

\begin{itemize}%
\item [[Eric Finster]], \emph{Opetopic} (\href{https://github.com/ericfinster/opetopic}{GitHub repository}) (\href{http://opetopic.net/}{Website})

\end{itemize}
Something like an implementation of aspects of opetopic type theory \emph{within} [[homotopy type theory]] is described in

\begin{itemize}%
\item [[Eric Finster]], \emph{[[homotopytypetheory:Eric Finster, Towards Higher Universal Algebra in Type Theory|Towards Higher Universal Algebra in Type Theory]]}, \href{https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html}{Homotopy Type Theory Electronic Seminar} 2018 (\href{https://www.youtube.com/watch?v=hlCVHVtAlqQ}{recording}, [[Agda]] \href{https://github.com/ericfinster/higher-alg}{code})

\end{itemize}


\end{document}