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.
-
-
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.
-
-
class
opetopy.NamedOpetopicSet.
RuleInstance
[source]¶ A rule instance of system \(\textbf{OptSet${}^!$}\).
-
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 variablea
, and plugs proof treep1
on the first premise, andp2
on the second.See: NamedOpetope.graft()
.
-
-
class
opetopy.NamedOpetopicSet.
Zero
[source]¶ A class representing an instance of the
zero
rule in a proof tree.
-
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.