Opetopic categories: unnamed approach

This part of opetopy implements finite opetopic categories as defined in [Baez1998] and [Finster].

[Baez1998]Baez, John C. and Dolan, James. Higher-dimensional algebra III: \(n\)-categories and the algebra of opetopes.
[Finster]Eric Finster. http://opetopic.net .

Examples

Filler of target horn

In this simple example, we use the target filling of a pasting diagram of shape \(\mathbf{2}\), effectively composing arrow cells \(f\) and \(g\). The result is the arrow \(h\), and the compositor is \(\alpha\).

 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
from opetopy.UnnamedOpetope import address, Arrow, OpetopicInteger
from opetopy.UnnamedOpetopicSet import Graft, pastingDiagram, Point, \
    RuleInstance, Shift
from opetopy.UnnamedOpetopicCategory import TFill

# Derive points
proof = Point(None, ["a", "b", "c"])  # type: RuleInstance

# Derive f
proof = Graft(
    proof, pastingDiagram(
        Arrow(),
        {
            address('*'): "a"
        }))
proof = Shift(proof, "b", "f")

# Derive g
proof = Graft(
    proof, pastingDiagram(
        Arrow(),
        {
            address('*'): "b"
        }))
proof = Shift(proof, "c", "g")

# Derive the composition cells
proof = Graft(
    proof, pastingDiagram(
        OpetopicInteger(2),
        {
            address([], 1): "g",
            address(['*']): "f"
        }))
proof = TFill(proof, "h", "α")

print(proof.eval())

Target universal property

In this example, we have two cells of shape \(\mathbf{0}\):

  • \(\delta\), degenerate at \(a\) with target \(f\), constructed via rules \(\texttt{degen}\) and \(\texttt{fill}\) of system \(\textbf{OptSet${}^?$}\);
  • \(\gamma\), constructed by filling the empty pasting diagram at \(a\), with universal target \(g\).

We then apply the target universal property of \(\gamma\) over \(\delta\) to get a factorization cell \(\xi\) and a filler \(A\).

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

# Derive a cell degenerate at point a
proof = Point(None, "a")  # type: RuleInstance
proof = Graft(proof, pastingDiagram(Arrow(), {address('*'): "a"}))
proof = Shift(proof, "a", "f")
proof = Degen(proof, "a")
proof = Shift(proof, "f", "δ")

# Fill the empty pasting diagram at a
proof = Degen(proof, "a")
proof = TFill(proof, "g", "γ")

# Apply the target universal property of γ
proof = TUniv(proof, "γ", "δ", "ξ", "A")

print(proof.eval())

Source universal property

This example is a continuation of that presented in Filler of target horn. We derive the following additional cells:

  • \(i\), parallel to \(h\) (the composition of arrows \(f\) and \(g\));
  • \(\beta\), from the \(fg\) horn to \(i\).

We then apply the target universal property of \(\alpha\) over \(\beta\) to obtain a factorization \(\xi : h \longrightarrow i\) and a filler \(A\). We do it again, with a new factorization \(\zeta\) and filler \(B\). Finally, we apply the source univerality of \(A\) over \(B\) to obtain a factorization \(C : \zeta \longrightarrow \xi\).

This hints that any two factorization in the application of the target universality of the composition \(h\) over \(i\) are homotopic, and in fact, equivalent.

 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
67
68
import sys
sys.path.insert(0, "../")

from opetopy.UnnamedOpetope import address, Arrow, OpetopicInteger
from opetopy.UnnamedOpetopicSet import Graft, pastingDiagram, Point, \
    RuleInstance, Shift
from opetopy.UnnamedOpetopicCategory import TUniv, SUniv, TFill

# Derive points
proof = Point(None, ["a", "b", "c"])  # type: RuleInstance

# Derive f
proof = Graft(
    proof, pastingDiagram(
        Arrow(),
        {
            address('*'): "a"
        }))
proof = Shift(proof, "b", "f")

# Derive g
proof = Graft(
    proof, pastingDiagram(
        Arrow(),
        {
            address('*'): "b"
        }))
proof = Shift(proof, "c", "g")

# Derive the composition cells
proof = Graft(
    proof, pastingDiagram(
        OpetopicInteger(2),
        {
            address([], 1): "g",
            address(['*']): "f"
        }))
proof = TFill(proof, "h", "α")

# Derive i, parallel to h
proof = Graft(
    proof, pastingDiagram(
        Arrow(),
        {
            address('*'): "a"
        }))
proof = Shift(proof, "c", "i")

# Derive β
proof = Graft(
    proof, pastingDiagram(
        OpetopicInteger(2),
        {
            address([], 1): "g",
            address(['*']): "f"
        }))
proof = Shift(proof, "i", "β")

# Apply target universality of α over β
proof = TUniv(proof, "α", "β", "ξ", "A")

# Again
proof = TUniv(proof, "α", "β", "ζ", "B")

# Apply source universality of A over B
proof = SUniv(proof, "A", "B", address([], 2), "C", "Ψ")

print(proof.eval())

Target universal closure

In this example, we derive two target universal arrows \(f\) and \(g\), and their composition \(h\). We then apply the target universal closure property to prove that \(h\) is target universal.

 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
from opetopy.UnnamedOpetope import address, Arrow, OpetopicInteger
from opetopy.UnnamedOpetopicSet import Graft, pastingDiagram, Point, \
    RuleInstance
from opetopy.UnnamedOpetopicCategory import TClose, TFill

proof = Point(None, "a")  # type: RuleInstance

# Derive a target universal arrow f of source a
proof = Graft(proof, pastingDiagram(Arrow(), {address('*'): "a"}))
proof = TFill(proof, "b", "f")

# Derive a target universal arrow g of source b
proof = Graft(proof, pastingDiagram(Arrow(), {address('*'): "b"}))
proof = TFill(proof, "c", "g")

# Compose f and g
proof = Graft(
    proof, pastingDiagram(
        OpetopicInteger(2),
        {
            address([], 1): "g",
            address(['*']): "f"
        }))
proof = TFill(proof, "h", "α")

# Apply target universality closure
proof = TClose(proof, "α")

print(proof.eval())

Documentation

Module author: Cédric HT

class opetopy.UnnamedOpetopicCategory.SUniv(p: opetopy.UnnamedOpetopicSet.RuleInstance, suCellName: str, cellName: str, addr: opetopy.UnnamedOpetope.Address, factorizationName: str, fillerName: str)[source]

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

__init__(p: opetopy.UnnamedOpetopicSet.RuleInstance, suCellName: str, cellName: str, addr: opetopy.UnnamedOpetope.Address, factorizationName: str, fillerName: 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]

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

class opetopy.UnnamedOpetopicCategory.TClose(p: opetopy.UnnamedOpetopicSet.RuleInstance, tuCell: str)[source]

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

__init__(p: opetopy.UnnamedOpetopicSet.RuleInstance, tuCell: 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]

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

class opetopy.UnnamedOpetopicCategory.TFill(p: opetopy.UnnamedOpetopicSet.RuleInstance, targetName: str, fillerName: str)[source]

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

__init__(p: opetopy.UnnamedOpetopicSet.RuleInstance, targetName: str, fillerName: 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]

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

class opetopy.UnnamedOpetopicCategory.TUniv(p: opetopy.UnnamedOpetopicSet.RuleInstance, tuCell: str, cell: str, factorizationName: str, fillerName: str)[source]

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

__init__(p: opetopy.UnnamedOpetopicSet.RuleInstance, tuCell: str, cell: str, factorizationName: str, fillerName: 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]

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

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

Similar to UnnamedOpetopicSet.Type except information about the universality of faces is also stored/

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

Inits the type as in UnnamedOpetopicSet.Type.__init__, and sets all faces (sources and target) as non universal.

__repr__() → str[source]

Return repr(self).

__str__() → str[source]

Return str(self).

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

Tells wether this type is source universal at source address addr.

isTargetUniversal() → bool[source]

Tells wether this type is target universal.

opetopy.UnnamedOpetopicCategory.isSourceUniversal(t: opetopy.UnnamedOpetopicSet.Type, addr: opetopy.UnnamedOpetope.Address) → bool[source]

This convenient function allows to know if an instance of UnnamedOpetopicSet.Type is source universal at a given address, regardless of wether or not it is an actual instance of UnnamedOpetopicCategory.Type.

opetopy.UnnamedOpetopicCategory.isTargetUniversal(t: opetopy.UnnamedOpetopicSet.Type) → bool[source]

This convenient function allows to know if an instance of UnnamedOpetopicSet.Type is target universal, regardless of wether or not it is an actual instance of UnnamedOpetopicCategory.Type.

opetopy.UnnamedOpetopicCategory.suniv(seq: opetopy.UnnamedOpetopicSet.Sequent, suCellName: str, cellName: str, addr: opetopy.UnnamedOpetope.Address, factorizationName: str, fillerName: str) → opetopy.UnnamedOpetopicSet.Sequent[source]

From

  • an address \([p]\) (argument addr);
  • a cell \(\alpha : \forall_{[p]} \mathbf{P} \longrightarrow u\) (with name suCellName);
  • a cell \(\beta : \mathbf{P'} \longrightarrow u\) (with name cellName), where \(\mathbf{P'}\) is \(\mathbf{P}\) except at address \([p]\) where it is \(s\);

applies the source universal property of \(\alpha\) at \([p]\) over \(\beta\), thus creating

  • a factorization cell \(\xi : s \longrightarrow \mathsf{s}_{[p]} \mathbf{P}\);
  • a filler \(A\), target universal, and source universal at \(\xi\), i.e. at address \([[p]]\).
opetopy.UnnamedOpetopicCategory.tclose(seq: opetopy.UnnamedOpetopicSet.Sequent, tuCell: str) → opetopy.UnnamedOpetopicSet.Sequent[source]

From a target universal cell \(A : \mathbf{P} \longrightarrow \forall u\) such that all its faces are target universal but one, turns that one target universal as well.

opetopy.UnnamedOpetopicCategory.tfill(seq: opetopy.UnnamedOpetopicSet.Sequent, targetName: str, fillerName: str) → opetopy.UnnamedOpetopicSet.Sequent[source]

This function takes a UnnamedOpetopicSet.Sequent, (recall that the context of a sequent derivable in \(\textbf{OptSet${}^?$}\) is a finite opetopic set) typing a pasting diagram \(\mathbf{P}\), and solves the Kan filler problem by adding

  • a new cell \(t\) with name targetName;
  • a new cell \(\alpha : \mathbf{P} \longrightarrow t\) with name fillerName.
opetopy.UnnamedOpetopicCategory.tuniv(seq: opetopy.UnnamedOpetopicSet.Sequent, tuCell: str, cell: str, factorizationName: str, fillerName: str) → opetopy.UnnamedOpetopicSet.Sequent[source]

From a target universal cell \(\alpha : \mathbf{P} \longrightarrow t\) (whose name is tuCell), and another cell \(\beta : \mathbf{P} \longrightarrow u\), creates the universal factorization.