Unnamed Opetopic Sets

Examples

The arrow

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
from opetopy.UnnamedOpetopicSet import Graft, pastingDiagram, Point, \
    RuleInstance, Shift
from opetopy.UnnamedOpetope import address, Arrow

ar = Point(None, "a")  # type: RuleInstance
ar = Point(ar, "b")
ar = Graft(
    ar, pastingDiagram(
        Arrow(),
        {
            address([], 0): "a"
        }))
ar = Shift(ar, "b", "f")

print(ar.eval())
print()
print(ar.toTex())

A classic, maximally folded

We start by deriving in \(\textbf{Opt${}^?$}\) (see UnnamedOpetope) the opetope \(\omega = \mathsf{Y}_{\mathbf{2}} \circ_{[[*]]} \mathsf{Y}_{\mathbf{2}}\) describing the shape of the maximal cell \(A\). We then proceed to derive the opetopic set in \(\textbf{OptSet${}^?$}\).

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
from opetopy.UnnamedOpetopicSet import Graft, pastingDiagram, Point, \
    RuleInstance, Shift
from opetopy.UnnamedOpetope import address, Arrow, OpetopicInteger, \
    OpetopicTree
from opetopy.UnnamedOpetope import Graft as OptGraft
from opetopy.UnnamedOpetope import Shift as OptShift

# Derivation of ω
omega = OptGraft(
    OptShift(OpetopicInteger(2)),
    OpetopicInteger(2),
    address([['*']]))

# Faster way:
# >>> omega = OpetopicTree([None, [None, None]])

# Derivation of a
classic = Point(None, "a")  # type: RuleInstance

# Derivation of f
classic = Graft(
    classic,
    pastingDiagram(
        Arrow(),
        {
            address([], 0): "a"
        }))
classic = Shift(classic, "a", "f")

# Derivation of α
classic = Graft(
    classic,
    pastingDiagram(
        OpetopicInteger(2),
        {
            address([], 1): "f",
            address(['*']): "f"
        }))
classic = Shift(classic, "f", "α")

# Derivation of β
classic = Graft(
    classic,
    pastingDiagram(
        OpetopicInteger(3),
        {
            address([], 1): "f",
            address(['*']): "f",
            address(['*', '*']): "f"
        }))
classic = Shift(classic, "f", "β")

# Derivation of A
classic = Graft(
    classic,
    pastingDiagram(
        omega,
        {
            address([], 2): "α",
            address([['*']]): "α"
        }))
classic = Shift(classic, "β", "A")

print(classic.eval())
print()
print(classic.toTex())

Documentation

Module author: Cédric HT

class opetopy.UnnamedOpetopicSet.Context[source]

A context is a set of tyings (see UnnamedOpetopicSet.Typing).

__add__(typing: opetopy.UnnamedOpetopicSet.Typing) → opetopy.UnnamedOpetopicSet.Context[source]

Adds a variable typing to a deep copy of the context context, if the typed variable isn’t already typed in the context.

__contains__(var) → bool[source]

Tests wether the variable var is typed in this context.

__getitem__(name: str) → opetopy.UnnamedOpetopicSet.Typing[source]

Returns typing whose variable name is name.

__next_in_mro__

alias of builtins.object

__repr__() → str[source]

Return repr(self).

__str__() → str[source]

Return str(self).

_gorg

alias of Context

source(name: str, addr: opetopy.UnnamedOpetope.Address) → str[source]

Returns the source at address addr of the variable whose name is name.

target(name: str) → str[source]

Returns the target of the variable whose name is name.

variableNames() → List[str][source]

Return a list containing all variable names typed in this context.

class opetopy.UnnamedOpetopicSet.Degen(p: opetopy.UnnamedOpetopicSet.RuleInstance, name: str)[source]

A class representing an instance of the \(\texttt{degen}\) rule in a proof tree.

__init__(p: opetopy.UnnamedOpetopicSet.RuleInstance, name: 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 UnnamedOpetopicSet.RuleInstance.toTex() instead.

eval() → opetopy.UnnamedOpetopicSet.Sequent[source]

Evaluates the proof tree.

class opetopy.UnnamedOpetopicSet.Graft(p: opetopy.UnnamedOpetopicSet.RuleInstance, pd: opetopy.UnnamedOpetopicSet.PastingDiagram)[source]

A class representing an instance of the \(\texttt{graft}\) rule in a proof tree.

__init__(p: opetopy.UnnamedOpetopicSet.RuleInstance, pd: opetopy.UnnamedOpetopicSet.PastingDiagram) → 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 UnnamedOpetopicSet.RuleInstance.toTex() instead.

eval() → opetopy.UnnamedOpetopicSet.Sequent[source]

Evaluates the proof tree.

class opetopy.UnnamedOpetopicSet.PastingDiagram[source]

A pasting diagram consist in a shape \(\omega\) (UnnamedOpetope.Preopetope) and

  • if \(\omega\) is not degenerate, a mapping \(f : \omega^\bullet \longrightarrow \mathbb{V}\) such that \(f (\mathsf{s}_{[p]} \omega)^\natural = f([p])^\natural\), where \(\mathbb{V}\) is the set of variable (UnnamedOpetopicSet.Variable); this case is implemented in UnnamedOpetopicSet.NonDegeneratePastingDiagram;
  • if \(\omega\) is degenerate, say \(\omega = \{\{\phi\), a variable of shape \(\phi\); this case is implemented in UnnamedOpetopicSet.DegeneratePastingDiagram.
__eq__(other) → bool[source]

Return self==value.

__getitem__(addr: opetopy.UnnamedOpetope.Address) → str[source]

Returns the source variable at addr of a non degenerate pasting diagram.

__ne__(other) → bool[source]

Return self!=value.

__repr__() → str[source]

Return repr(self).

__str__() → str[source]

Return str(self).

__weakref__

list of weak references to the object (if defined)

degeneracyVariable() → str[source]

Returns the degeneracy variable, or raises an exception if the pasting diagram is not degenerate.

static degeneratePastingDiagram(shapeProof: opetopy.UnnamedOpetope.RuleInstance, degeneracy: str) → opetopy.UnnamedOpetopicSet.PastingDiagram[source]

Creates a degenerate pasting diagram.

static nonDegeneratePastingDiagram(shapeProof: opetopy.UnnamedOpetope.RuleInstance, nodes: Dict[opetopy.UnnamedOpetope.Address, str]) → opetopy.UnnamedOpetopicSet.PastingDiagram[source]

Creates a non degenerate pasting diagram.

static point()[source]

Creates the trivial pasting diagram with shape the point

shape

Returns the actual shape (UnnamedOpetope.Preopetope) of the pasting diagram, from the proof tree (UnnamedOpetope.RuleInstance) that was provided at its creation.

shapeTarget() → opetopy.UnnamedOpetope.Preopetope[source]

Returns the shape target (UnnamedOpetope.Preopetope) of the pasting diagram, from the proof tree (UnnamedOpetope.RuleInstance) that was provided at its creation.

source(addr: opetopy.UnnamedOpetope.Address) → str[source]

Returns the variable name at address addr, or raises an exception if the pasting diagram is degenerate

class opetopy.UnnamedOpetopicSet.Point(p: Optional[opetopy.UnnamedOpetopicSet.RuleInstance], name: Union[str, List[str]])[source]

A class representing an instance of the \(\texttt{point}\) rule in a proof tree.

__init__(p: Optional[opetopy.UnnamedOpetopicSet.RuleInstance], name: Union[str, List[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 UnnamedOpetopicSet.RuleInstance.toTex() instead.

eval() → opetopy.UnnamedOpetopicSet.Sequent[source]

Evaluates the proof tree.

class opetopy.UnnamedOpetopicSet.RuleInstance[source]

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

eval() → opetopy.UnnamedOpetopicSet.Sequent[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.UnnamedOpetopicSet.Sequent[source]

A sequent is composed of

  • a context (UnnamedOpetopicSet.Context);
  • optionally, a pasting diagram (UnnamedOpetopicSet.PastingDiagram).
__getitem__(name: str) → opetopy.UnnamedOpetopicSet.Variable[source]

Returns the variable in the sequent’s context whose name is name. Note that unlike UnnamedOpetopicSet.Context.__getitem__(), this function returns a UnnamedOpetopicSet.Variable (and not a UnnamedOpetopicSet.Typing)

__init__() → None[source]

Creates a sequent with an empty context, and no pasting diagram.

__repr__() → str[source]

Return repr(self).

__str__() → str[source]

Return str(self).

__weakref__

list of weak references to the object (if defined)

class opetopy.UnnamedOpetopicSet.Shift(p: opetopy.UnnamedOpetopicSet.RuleInstance, targetName: str, name: str)[source]

A class representing an instance of the \(\texttt{shift}\) rule in a proof tree.

__init__(p: opetopy.UnnamedOpetopicSet.RuleInstance, targetName: str, name: 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 UnnamedOpetopicSet.RuleInstance.toTex() instead.

eval() → opetopy.UnnamedOpetopicSet.Sequent[source]

Evaluates the proof tree.

class opetopy.UnnamedOpetopicSet.Type(source: opetopy.UnnamedOpetopicSet.PastingDiagram, target: Optional[opetopy.UnnamedOpetopicSet.Variable])[source]

A type consist in

  • a source pasting diagram (UnnamedOpetopicSet.PastingDiagram), say \(\mathbf{P}\),
  • a target variable (UnnamedOpetopicSet.Variable), say \(x\),

such that \(\mathsf{t} \mathbf{P}^\natural = x^\natural\)

__eq__(other) → bool[source]

Return self==value.

__init__(source: opetopy.UnnamedOpetopicSet.PastingDiagram, target: Optional[opetopy.UnnamedOpetopicSet.Variable]) → None[source]

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

__ne__(other) → bool[source]

Return self!=value.

__repr__() → str[source]

Return repr(self).

__str__() → str[source]

Return str(self).

__weakref__

list of weak references to the object (if defined)

class opetopy.UnnamedOpetopicSet.Typing(variable: opetopy.UnnamedOpetopicSet.Variable, type: opetopy.UnnamedOpetopicSet.Type)[source]

A typing consists in

  • a variable UnnamedOpetopicSet.Variable, say \(v\),
  • a type UnnamedOpetopicSet.Type, say \(\mathbf{P} \longrightarrow t\)

such that \(x^\natural = \mathbf{P}^\natural\).

__init__(variable: opetopy.UnnamedOpetopicSet.Variable, type: opetopy.UnnamedOpetopicSet.Type) → None[source]

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

__repr__() → str[source]

Return repr(self).

__str__() → str[source]

Return str(self).

__weakref__

list of weak references to the object (if defined)

class opetopy.UnnamedOpetopicSet.Variable(name: str, shapeProof: opetopy.UnnamedOpetope.RuleInstance)[source]

A variable is just a string representing its name, annotated by an opetope (UnnamedOpetope.Preopetope) representing its shape. To construct a variable, however, not only does the shape need to be specified, but its whole proof tree.

__eq__(other) → bool[source]

Tests syntactic equality between two variables. Two variables are equal if they have the same name and the same shape.

__init__(name: str, shapeProof: opetopy.UnnamedOpetope.RuleInstance) → None[source]

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

__ne__(other) → bool[source]

Return self!=value.

__repr__() → str[source]

Return repr(self).

__str__() → str[source]

Return str(self).

__weakref__

list of weak references to the object (if defined)

shape

Returns the actual shape (UnnamedOpetope.Preopetope) of the variable, from the proof tree (UnnamedOpetope.RuleInstance) that was provided at its creation.

shapeTarget() → opetopy.UnnamedOpetope.Preopetope[source]

Returns the shape target (UnnamedOpetope.Preopetope) of the variable, from the proof tree (UnnamedOpetope.RuleInstance) that was provided at its creation.

toTex() → str[source]

Returns the string representation of the variable, which is really just the variable name.

opetopy.UnnamedOpetopicSet.degen(seq: opetopy.UnnamedOpetopicSet.Sequent, name: str) → opetopy.UnnamedOpetopicSet.Sequent[source]

The \(\textbf{OptSet${}^?$}\) \(\texttt{degen}\) rule.

opetopy.UnnamedOpetopicSet.graft(seq: opetopy.UnnamedOpetopicSet.Sequent, pd: opetopy.UnnamedOpetopicSet.PastingDiagram) → opetopy.UnnamedOpetopicSet.Sequent[source]

The \(\textbf{OptSet${}^?$}\) \(\texttt{graft}\) rule.

opetopy.UnnamedOpetopicSet.pastingDiagram(shapeProof: opetopy.UnnamedOpetope.RuleInstance, args: Union[Dict[opetopy.UnnamedOpetope.Address, str], str]) → opetopy.UnnamedOpetopicSet.PastingDiagram[source]

Convenient function that regroups UnnamedOpetopicSet.PastingDiagram.degeneratePastingDiagram() and UnnamedOpetopicSet.PastingDiagram.nonDegeneratePastingDiagram(). It calls either depending on the shape opetope.

opetopy.UnnamedOpetopicSet.point(seq: opetopy.UnnamedOpetopicSet.Sequent, name: Union[str, List[str]]) → opetopy.UnnamedOpetopicSet.Sequent[source]

The \(\textbf{OptSet${}^?$}\) \(\texttt{point}\) rule.

  • If argument name is a str, creates a new point with that name (this is just the \(\texttt{point}\));
  • if it is a list of str, then creates as many points.
opetopy.UnnamedOpetopicSet.shift(seq: opetopy.UnnamedOpetopicSet.Sequent, targetName: str, name: str) → opetopy.UnnamedOpetopicSet.Sequent[source]

The \(\textbf{OptSet${}^?$}\) \(\texttt{shift}\) rule.