Named Opetopic Sets, mixed approach

Example

from opetopy.NamedOpetopicSetM import Glue, Pd, Point, RuleInstance, Shift, Sum

p1 = Shift(Pd(Point("a"), "a"), "f")
p1 = Shift(Pd(p1, "a"), "g")

p2 = Shift(Pd(Point("b"), "b"), "h")

example = Sum(p1, p2)  # type: RuleInstance
example = Glue(example, "b", "tf")
example = Glue(example, "b", "tg")
example = Shift(Pd(example, "f"), "ɑ")
example = Glue(example, "b", "ttɑ")
example = Glue(example, "g", "tɑ")
example = Glue(example, "a", "th")

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

Documentation

Module author: Cédric HT

class opetopy.NamedOpetopicSetM.Degen(p: opetopy.NamedOpetopicSetM.RuleInstance, name: str)

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

__init__(p: opetopy.NamedOpetopicSetM.RuleInstance, name: str) → None

Creates an instance of the degen rule and plugs proof tree p on the unique premise.

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.Sequent

Evaluates this instance of degen by first evaluating its premiss, and then applying NamedOpetopicSetM.degen() on the resulting sequent.

class opetopy.NamedOpetopicSetM.DegenShift(p: opetopy.NamedOpetopicSetM.RuleInstance, dname: str, fname: str)

A convenient class chaining an instance of the degen rule with an instance of the shift rule.

__init__(p: opetopy.NamedOpetopicSetM.RuleInstance, dname: str, fname: str) → None

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

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.OCMT

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

class opetopy.NamedOpetopicSetM.Glue(p: opetopy.NamedOpetopicSetM.RuleInstance, a: str, b: str)

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

__init__(p: opetopy.NamedOpetopicSetM.RuleInstance, a: str, b: str) → None

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

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.OCMT

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

class opetopy.NamedOpetopicSetM.Graft(p1: opetopy.NamedOpetopicSetM.RuleInstance, p2: opetopy.NamedOpetopicSetM.RuleInstance, a: str)

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

__init__(p1: opetopy.NamedOpetopicSetM.RuleInstance, p2: opetopy.NamedOpetopicSetM.RuleInstance, a: str) → None

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:NamedOpetopicSetM.graft().

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.Sequent

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

class opetopy.NamedOpetopicSetM.Pd(p: opetopy.NamedOpetopicSetM.RuleInstance, name: str)

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

__init__(p: opetopy.NamedOpetopicSetM.RuleInstance, name: str) → None

Creates an instance of the pd rule and plugs proof tree p on the unique premise.

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.Sequent

Evaluates this instance of degen by first evaluating its premiss, and then applying NamedOpetopicSetM.pd() on the resulting sequent.

class opetopy.NamedOpetopicSetM.Point(name: str)

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

__init__(name: str) → None

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

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.OCMT

Evaluates the proof tree, in this cases returns the point sequent by calling NamedOpetopicSetM.point().

class opetopy.NamedOpetopicSetM.RuleInstance

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

eval() → opetopy.NamedOpetope.OCMT

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

class opetopy.NamedOpetopicSetM.Shift(p: opetopy.NamedOpetopicSetM.RuleInstance, name: str)

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

__init__(p: opetopy.NamedOpetopicSetM.RuleInstance, name: str) → None

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

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.OCMT

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

class opetopy.NamedOpetopicSetM.Sum(p1: opetopy.NamedOpetopicSetM.RuleInstance, p2: opetopy.NamedOpetopicSetM.RuleInstance)

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

__init__(p1: opetopy.NamedOpetopicSetM.RuleInstance, p2: opetopy.NamedOpetopicSetM.RuleInstance) → None

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

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.OCMT

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

class opetopy.NamedOpetopicSetM.Zero

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

_toTex() → str

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

eval() → opetopy.NamedOpetope.OCMT

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

opetopy.NamedOpetopicSetM.degen(ocmt: opetopy.NamedOpetope.OCMT, name: str) → opetopy.NamedOpetope.Sequent

The \(\textbf{OptSet${}^!_m$}\) \(\texttt{degen}\) rule. Introduces the degenerate pasting diagram on a given variable.

opetopy.NamedOpetopicSetM.glue(ocmt: opetopy.NamedOpetope.OCMT, aName: str, bName: str) → opetopy.NamedOpetope.OCMT

The \(\textbf{OptSet${}^!_m$}\) \(\texttt{glue}\) rule, which is the same as system \(\textbf{OptSet${}^!$}\)’s \(\texttt{glue}\) rule.

opetopy.NamedOpetopicSetM.graft(seqt: opetopy.NamedOpetope.Sequent, seqx: opetopy.NamedOpetope.Sequent, name: str) → opetopy.NamedOpetope.Sequent

The \(\textbf{OptSet${}^!_m$}\) \(\texttt{graft}\) rule, which is the same as system \(\textbf{Opt${}^!$}\)’s \(\texttt{graft}\) rule.

opetopy.NamedOpetopicSetM.pd(ocmt: opetopy.NamedOpetope.OCMT, name: str) → opetopy.NamedOpetope.Sequent

The \(\textbf{OptSet${}^!_m$}\) \(\texttt{pd}\) rule. Introduces the trivial non degenerate pasting diagram on a given variable.

opetopy.NamedOpetopicSetM.point(name: str) → opetopy.NamedOpetope.OCMT

The \(\textbf{OptSet${}^!_m$}\) \(\texttt{point}\) rule. Introduces a \(0\)-variable with name x.

opetopy.NamedOpetopicSetM.shift(seq: opetopy.NamedOpetope.Sequent, name: str) → opetopy.NamedOpetope.OCMT

The \(\textbf{OptSet${}^!_m$}\) \(\texttt{shift}\) rule. Takes a sequent seq typing a term t and introduces a new variable x having t as \(1\)-source.

opetopy.NamedOpetopicSetM.sum(ocmt1: opetopy.NamedOpetope.OCMT, ocmt2: opetopy.NamedOpetope.OCMT) → opetopy.NamedOpetope.OCMT

The \(\textbf{OptSet${}^!_m$}\) \(\texttt{sum}\) rule, which is the same as system \(\textbf{OptSet${}^!$}\)’s \(\texttt{sum}\) rule.

opetopy.NamedOpetopicSetM.zero() → opetopy.NamedOpetope.OCMT

The \(\textbf{OptSet${}^!_m$}\) \(\texttt{zero}\) rule, which is the same as system \(\textbf{Opt${}^!$}\)’s \(\texttt{zero}\) rule.