Named Opetopic Sets

Example

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
from opetopy.NamedOpetope import Point, Shift
from opetopy.NamedOpetopicSet import Glue, Repr, Sum

alpha = Shift(Shift(Point("a"), "f"), "α")
g = Shift(Point("c"), "g")
h = Shift(Point("b"), "h")
unglued = Sum(Sum(Repr(alpha), Repr(g)), Repr(h))
example = Glue(Glue(Glue(Glue(Glue(unglued,
                                   "a",
                                   "c"),
                              "b",
                              "tf"),
                         "b",
                         "tg"),
                    "a",
                    "th"),
               "g",
               "tα")

print(example.eval())
print()
print(example.toTex())

Documentation

Module author: Cédric HT

class opetopy.NamedOpetopicSet.Glue(p: opetopy.NamedOpetopicSet.RuleInstance, a: str, b: str)[source]

A class representing an instance of the glue rule in a proof tree.

__init__(p: opetopy.NamedOpetopicSet.RuleInstance, a: str, b: str) → None[source]

Initialize self. See help(type(self)) for accurate signature.

__repr__() → str[source]

Return repr(self).

__str__() → str[source]

Return str(self).

_toTex() → str[source]

Converts the proof tree in TeX code. This method should not be called directly, use NamedOpetope.RuleInstance.toTex() instead.

eval() → opetopy.NamedOpetope.OCMT[source]

Evaluates this instance of graft by first evaluating its premises, and then applying NamedOpetope.graft() at variable self.a on the resulting sequents.

class opetopy.NamedOpetopicSet.Repr(p: opetopy.NamedOpetope.RuleInstance)[source]

A class representing an instance of the repr rule in a proof tree.

__init__(p: opetopy.NamedOpetope.RuleInstance) → None[source]

Initialize self. See help(type(self)) for accurate signature.

__repr__() → str[source]

Return repr(self).

__str__() → str[source]

Return str(self).

_toTex() → str[source]

Converts the proof tree in TeX code. This method should not be called directly, use NamedOpetope.RuleInstance.toTex() instead.

eval() → opetopy.NamedOpetope.OCMT[source]

Pure virtual method evaluating a proof tree and returning the final conclusion sequent, or raising an exception if the proof is invalid.

class opetopy.NamedOpetopicSet.RuleInstance[source]

A rule instance of system \(\textbf{OptSet${}^!$}\).

eval() → opetopy.NamedOpetope.OCMT[source]

Pure virtual method evaluating a proof tree and returning the final conclusion sequent, or raising an exception if the proof is invalid.

class opetopy.NamedOpetopicSet.Sum(p1: opetopy.NamedOpetopicSet.RuleInstance, p2: opetopy.NamedOpetopicSet.RuleInstance)[source]

A class representing an instance of the sum rule in a proof tree.

__init__(p1: opetopy.NamedOpetopicSet.RuleInstance, p2: opetopy.NamedOpetopicSet.RuleInstance) → None[source]

Creates an instance of the graft rule at variable a, and plugs proof tree p1 on the first premise, and p2 on the second.

See:NamedOpetope.graft().
__repr__() → str[source]

Return repr(self).

__str__() → str[source]

Return str(self).

_toTex() → str[source]

Converts the proof tree in TeX code. This method should not be called directly, use NamedOpetope.RuleInstance.toTex() instead.

eval() → opetopy.NamedOpetope.OCMT[source]

Pure virtual method evaluating a proof tree and returning the final conclusion sequent, or raising an exception if the proof is invalid.

class opetopy.NamedOpetopicSet.Zero[source]

A class representing an instance of the zero rule in a proof tree.

_toTex() → str[source]

Converts the proof tree in TeX code. This method should not be called directly, use NamedOpetope.RuleInstance.toTex() instead.

eval() → opetopy.NamedOpetope.OCMT[source]

Pure virtual method evaluating a proof tree and returning the final conclusion sequent, or raising an exception if the proof is invalid.

opetopy.NamedOpetopicSet.glue(ocmt: opetopy.NamedOpetope.OCMT, aName: str, bName: str) → opetopy.NamedOpetope.OCMT[source]

The \(\textbf{OptSet${}^!$}\) \(\texttt{glue}\) rule.

opetopy.NamedOpetopicSet.repres(seq: opetopy.NamedOpetope.Sequent) → opetopy.NamedOpetope.OCMT[source]

The \(\textbf{OptSet${}^!$}\) \(\texttt{repr}\) rule.

opetopy.NamedOpetopicSet.sum(ocmt1: opetopy.NamedOpetope.OCMT, ocmt2: opetopy.NamedOpetope.OCMT) → opetopy.NamedOpetope.OCMT[source]

The \(\textbf{OptSet${}^!$}\) \(\texttt{sum}\) rule.

opetopy.NamedOpetopicSet.zero() → opetopy.NamedOpetope.OCMT[source]

The \(\textbf{OptSet${}^!$}\) \(\texttt{zero}\) rule.