opetopy¶
Introduction¶
This project is the Python implementation of the opetope derivation systems presented in [CHM19] and some other work in progress.
The opetopy module is decomposed as follow:
| Module | Syntactical construct | Derivation system |
|---|---|---|
NamedOpetope |
Named opetopes | \(\textbf{Opt${}^!$}\) |
NamedOpetopicSet |
Named opetopic sets | \(\textbf{OptSet${}^!$}\) |
UnnamedOpetope |
Unnamed opetopes | \(\textbf{Opt${}^?$}\) |
UnnamedOpetopicSet |
Unnamed opetopic sets | \(\textbf{OptSet${}^?$}\) |
UnnamedOpetopicCategory |
Unnamed opetopic categories | \(\textbf{OptCat${}^?$}\) |
Each implement the following:
- the syntactic constructs required to describe opetopes / opetopic sets and their sequents;
- the derivation rules of the relevant system;
- wrappers of those rules to describe proof trees.
| Derivation system | Rule | Implementation | Proof tree node |
|---|---|---|---|
| \(\textbf{Opt${}^!$}\) | \(\texttt{point}\) | NamedOpetope.point() |
NamedOpetope.Point |
| \(\texttt{degen}\) | NamedOpetope.degen() |
NamedOpetope.Degen |
|
| \(\texttt{degen-shift}\) | NamedOpetope.degenshift() |
NamedOpetope.DegenShift |
|
| \(\texttt{shift}\) | NamedOpetope.shift() |
NamedOpetope.Shift |
|
| \(\texttt{graft}\) | NamedOpetope.graft() |
NamedOpetope.Graft |
|
| \(\textbf{OptSet${}^!$}\) | \(\texttt{repr}\) | NamedOpetopicSet.repres() |
NamedOpetopicSet.Repr |
| \(\texttt{zero}\) | NamedOpetopicSet.zero() |
NamedOpetopicSet.Zero |
|
| \(\texttt{sum}\) | NamedOpetopicSet.sum() |
NamedOpetopicSet.Sum |
|
| \(\texttt{glue}\) | NamedOpetopicSet.glue() |
NamedOpetopicSet.Glue |
|
| \(\textbf{OptSet${}^!_m$}\) | \(\texttt{point}\) | NamedOpetopicSetM.point() |
NamedOpetopicSetM.Point |
| \(\texttt{degen}\) | NamedOpetopicSetM.degen() |
NamedOpetopicSetM.Degen |
|
| \(\texttt{pd}\) | NamedOpetopicSetM.pd() |
NamedOpetopicSetM.Pd |
|
| \(\texttt{graft}\) | NamedOpetopicSetM.graft() |
NamedOpetopicSetM.Graft |
|
| \(\texttt{shift}\) | NamedOpetopicSetM.shift() |
NamedOpetopicSetM.Shift |
|
| \(\texttt{zero}\) | NamedOpetopicSetM.zero() |
NamedOpetopicSetM.Zero |
|
| \(\texttt{sum}\) | NamedOpetopicSetM.sum() |
NamedOpetopicSetM.Sum |
|
| \(\texttt{glue}\) | NamedOpetopicSetM.glue() |
NamedOpetopicSetM.Glue |
|
| \(\textbf{Opt${}^?$}\) | \(\texttt{point}\) | UnnamedOpetope.point() |
UnnamedOpetope.Point |
| \(\texttt{degen}\) | UnnamedOpetope.degen() |
UnnamedOpetope.Degen |
|
| \(\texttt{shift}\) | UnnamedOpetope.shift() |
UnnamedOpetope.Shift |
|
| \(\texttt{graft}\) | UnnamedOpetope.graft() |
UnnamedOpetope.Graft |
|
| \(\textbf{OptSet${}^?$}\) | \(\texttt{point}\) | UnnamedOpetopicSet.point() |
UnnamedOpetopicSet.Point |
| \(\texttt{degen}\) | UnnamedOpetopicSet.degen() |
UnnamedOpetopicSet.Degen |
|
| \(\texttt{graft}\) | UnnamedOpetopicSet.graft() |
UnnamedOpetopicSet.Graft |
|
| \(\texttt{shift}\) | UnnamedOpetopicSet.shift() |
UnnamedOpetopicSet.Shift |
|
| \(\textbf{OptCat${}^?$}\) | \(\texttt{tfill}\) | UnnamedOpetopicCategory.tfill() |
UnnamedOpetopicCategory.TFill |
| \(\texttt{tuniv}\) | UnnamedOpetopicCategory.tuniv() |
UnnamedOpetopicCategory.TUniv |
|
| \(\texttt{suniv}\) | UnnamedOpetopicCategory.suniv() |
UnnamedOpetopicCategory.SUniv |
|
| \(\texttt{tclose}\) | UnnamedOpetopicCategory.tclose() |
UnnamedOpetopicCategory.TClose |
Usage¶
Derivations and proof trees¶
A derivation / proof tree in any of those system can then be written as a Python expression. If it evaluates without raising any exception, it is considered valid.
For example, in system \(\textbf{Opt${}^?$}\), the unique \(1\)-opetope has the following expression:
from UnnamedOpetope import *
shift(point())
which indeed evaluates without raising exceptions.
The preferred way to construct proof trees is to use the proof tree node classes
(see table above), who act as instances of those rules. They behave as their
function counterparts, taking proof trees instead of sequents as constructor
arguments. Then, a proof tree can be evaluated with the eval() method. For
instance, the proof tree described above is written as:
from UnnamedOpetope import *
proof = Shift(Point())
and evaluated as:
proof.eval()
which again evaluates without raising exceptions.
Exporting to \(\TeX\)¶
opetopy’s main classes can be translated to \(\TeX\) code using
method toTeX(). Here is the minimal template to compile the returned code
\documentclass{article}
\usepackage{amsmath}
\usepackage{bussproofs}
\usepackage{fdsymbol}
\usepackage{MnSymbol}
\newcommand{\degenopetope}[1]{\left\lbrace \!\! \opetope{#1} \right.}
\newcommand{\opetope}[1]{\left\lbrace \begin{matrix*}[l] #1 \end{matrix*} \right.}
\newcommand{\optOne}{\filledsquare}
\newcommand{\optZero}{\filledlozenge}
\newcommand{\sep}{\leftarrow}
\begin{document}
Your code here.
\end{document}
Documentation¶
| [CHM19] | Pierre-Louis Curien, Cédric Ho Thanh, and Samuel Mimram. Syntactic approaches to opetopes. arXiv:1903.05848 |