Horns #
This file introduce horns Λ[n, i]
.
horn n i
(or Λ[n, i]
) is the i
-th horn of the n
-th standard simplex, where i : n
.
It consists of all m
-simplices α
of Δ[n]
for which the union of {i}
and the range of α
is not all of n
(when viewing α
as monotone function m → n
).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The i
-th horn Λ[n, i]
of the standard n
-simplex
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion of the i
-th horn of the n
-th standard simplex into that standard simplex.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The (degenerate) subsimplex of Λ[n+2, i]
concentrated in vertex k
.
Instances For
Alternative constructor for the edge of Λ[n, i]
with endpoints a
and b
,
assuming 3 ≤ n
.
Instances For
The edge of Λ[n, i]
with endpoints j
and j+1
.
This constructor assumes 0 < i < n
,
which is the type of horn that occurs in the horn-filling condition of quasicategories.
Instances For
The triangle in the standard simplex with vertices k
, k+1
, and k+2
.
This constructor assumes 0 < i < n
,
which is the type of horn that occurs in the horn-filling condition of quasicategories.
Equations
Instances For
The j
th subface of the i
-th horn.
Equations
Instances For
Two morphisms from a horn are equal if they are equal on all suitable faces.