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.
-
-
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.
-
-
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.
-
-
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.
-
-
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.
-
-
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 ofUnnamedOpetopicCategory.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 ofUnnamedOpetopicCategory.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]]\).
- an address \([p]\) (argument
-
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
.
- a new cell \(t\) with name
-
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.