Definitions: Mathlib.AlgebraicTopology, part 2 of 4

Assume that the composition of the homomorphism of $f$ and the homomorphism of $g$ is equal to the homomorphism of $h_{1}$. Then $\mathrm{SSet\_\_Truncated\_\_Edge\_\_CompStruct\_\_ofHomotopyCategory\_u2082\_Fac}$ applied to $\mathrm{fac}$ is an element of $\operatorname{CompStruct}$ applied to $f$, $g$ and $h_{1}$.

Let $s$ be an element of $\operatorname{CompStruct}$ applied to $f$, $g$ and $h_{1}$. Let $\mathrm{s'}$ be an element of $\operatorname{CompStruct}$ applied to $\mathrm{f'}$, $\mathrm{g'}$ and $\mathrm{h'}$. Let $\mathrm{hf}$ be a homotopy of $f$ and $\mathrm{f'}$. Let $\mathrm{hg}$ be a homotopy of $g$ and $\mathrm{g'}$. Then $\operatorname{unique}$ applied to $s$, $\mathrm{s'}$, $\mathrm{hf}$ and $\mathrm{hg}$ is a homotopy of $h_{1}$ and $\mathrm{h'}$ defined as the associator of the composition identity of $g$ and the associator of the homotopy of $\mathrm{hg}$ and the associator of the identity composition of $\mathrm{g'}$ and $\mathrm{s'}$.

homotopy of f and g (from the name)

Let $f$ and $g$ be edges of $x$ and $x_{1}$. Then a homotopy of $f$ and $g$ is an element of the function that maps $f$ and $g$ to $\operatorname{CompStruct}$ applied to $f$, the identity of $x_{1}$ and $g$.

the homotopy of h1 (from the name)

Let $h_{1}$ be a homotopy of $f$ and $g$. Then the homotopy of $h_{1}$ is a homotopy of $f$ and $g$ defined as the associator of the composition identity of $f$ and $h_{1}$.

the identity of f (from the name)

Let $f$ be an edge of $x$ and $x_{1}$. Then the identity of $f$ is a homotopy of $f$ and $f$ defined as the composition identity of $f$.

the inverse of h1 (from the name)

Let $h_{1}$ be a homotopy of $f$ and $g$. Then the inverse of $h_{1}$ is a homotopy of $g$ and $f$ defined as the associator of the identity composition of the identity of $x_{1}$ and the composition identity of $f$.

the composition of x2 and x3 (from the name)

Let $x_{2}$ be a homotopy of $f$ and $g$. Let $x_{3}$ be a homotopy of $g$ and $h_{1}$. Then the composition of $x_{2}$ and $x_{3}$ is a homotopy of $f$ and $h_{1}$ defined as the associator of the identity composition identity of $x_{1}$ and $x_{3}$.

homotopy of f and g (from the name)

Let $f$ and $g$ be edges of $x$ and $x_{1}$. Then a homotopy of $f$ and $g$ is an element of the function that maps $f$ and $g$ to $\operatorname{CompStruct}$ applied to the identity of $x$, $f$ and $g$.

the homotopy of h1 (from the name)

Let $h_{1}$ be a homotopy of $f$ and $g$. Then the homotopy of $h_{1}$ is a homotopy of $f$ and $g$ defined as the associator of the composition identity of $f$ and $h_{1}$.

the identity of f (from the name)

Let $f$ be an edge of $x$ and $x_{1}$. Then the identity of $f$ is a homotopy of $f$ and $f$ defined as the identity composition of $f$.

the inverse of h1 (from the name)

Let $h_{1}$ be a homotopy of $f$ and $g$. Then the inverse of $h_{1}$ is a homotopy of $g$ and $f$ defined as the associator of $h_{1}$ and the identity composition of $f$.

the composition of x2 and x3 (from the name)

Let $x_{2}$ be a homotopy of $f$ and $g$. Let $x_{3}$ be a homotopy of $g$ and $h_{1}$. Then the composition of $x_{2}$ and $x_{3}$ is a homotopy of $f$ and $h_{1}$ defined as the associator of $x_{2}$ and $x_{3}$.

the associator of x11 and h1 (from the name)

Let $x_{10}$ be an element of $\operatorname{CompStruct}$ applied to $x_{4}$, $x_{5}$ and $x_{7}$. Let $x_{11}$ be an element of $\operatorname{CompStruct}$ applied to $x_{5}$, $x_{6}$ and $x_{8}$. Let $h_{1}$ be an element of $\operatorname{CompStruct}$ applied to $x_{4}$, $x_{8}$ and $x_{9}$. Then the associator of $x_{11}$ and $h_{1}$ is an element of $\operatorname{CompStruct}$ applied to $x_{7}$, $x_{6}$ and $x_{9}$ defined as $\operatorname{some}$ applied to $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_fill31}$ applied to $x_{10}$, $x_{11}$ and $h_{1}$.

the associator of x11 and h1 (from the name)

Let $x_{10}$ be an element of $\operatorname{CompStruct}$ applied to $x_{4}$, $x_{5}$ and $x_{7}$. Let $x_{11}$ be an element of $\operatorname{CompStruct}$ applied to $x_{5}$, $x_{6}$ and $x_{8}$. Let $h_{1}$ be an element of $\operatorname{CompStruct}$ applied to $x_{7}$, $x_{6}$ and $x_{9}$. Then the associator of $x_{11}$ and $h_{1}$ is an element of $\operatorname{CompStruct}$ applied to $x_{4}$, $x_{8}$ and $x_{9}$ defined as $\operatorname{some}$ applied to $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_fill32}$ applied to $x_{10}$, $x_{11}$ and $h_{1}$.

the composition of f and g (from the name)

Let $f$ be an edge of $x$ and $x_{1}$. Let $g$ be an edge of $x_{1}$ and $x_{2}$. Then the composition of $f$ and $g$ is an edge of $x$ and $x_{2}$ defined as $\operatorname{fst}$ applied to $\operatorname{some}$ applied to $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_fill21}$ applied to $f$ and $g$.

Let $f$ be an edge of $x$ and $x_{1}$. Let $g$ be an edge of $x_{1}$ and $x_{2}$. Then $\operatorname{compStruct}$ applied to $f$ and $g$ is an element of $\operatorname{CompStruct}$ applied to $f$, $g$ and the composition of $f$ and $g$ defined as $\operatorname{snd}$ applied to $\operatorname{some}$ applied to $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_fill21}$ applied to $f$ and $g$.

f is homotopic to g (from the name)

Let $f$ and $g$ be edges of $x$ and $x_{1}$. Then $f$ is homotopic to $g$, if $\mathrm{Nonempty}$ holds for the set of homotopies of $f$ and $g$.

f is homotopic to g (from the name)

Let $f$ and $g$ be edges of $x$ and $x_{1}$. Then $f$ is homotopic to $g$, if $\mathrm{Nonempty}$ holds for the set of homotopies of $f$ and $g$.

homotopy category of X (from the name)

Let $X$ be an element of $\operatorname{Truncated}$ applied to $2$. Then the homotopy categories of $X$ are a basic type.

homomorphism of x and y (from the name)

Let $x$ and $y$ be homotopy categories of $X$. Then a homomorphism of $x$ and $y$ is an element of the function that maps $x$ and $y$ to $\mathrm{Quotient}$ applied to $\operatorname{instSetoidEdge}$ applied to $\mathrm{SSet\_\_Truncated\_\_HomotopyCategory\_u2082\_\_\_pt}$ applied to $x$ and $\mathrm{SSet\_\_Truncated\_\_HomotopyCategory\_u2082\_\_\_pt}$ applied to $y$.

Let $\mathrm{obj}$ be a function from elements of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_\_proof\_1}$ to elements of $D$. Let $\mathrm{map}$ be a function from elements $x_{9}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_\_proof\_1}$ and elements $y$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_\_proof\_1}$ and edges of $x_{9}$ and $y$ to homomorphisms of $\mathrm{obj}$ applied to $x_{9}$ and $\mathrm{obj}$ applied to $y$ such that for all elements $x_{8}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_\_proof\_1}$, $\mathrm{map}$ applied to $x_{8}$, $x_{8}$ and the identity of $x_{8}$ is equal to the identity morphism of $\mathrm{obj}$ applied to $x_{8}$ and for all elements $x_{1}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_\_proof\_1}$, for all elements $x_{2}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_\_proof\_1}$, for all elements $x_{3}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_\_proof\_1}$, for all edges $x_{4}$ of $x_{1}$ and $x_{2}$, for all edges $x_{5}$ of $x_{2}$ and $x_{3}$, for all edges $x_{6}$ of $x_{1}$ and $x_{3}$, for all elements $x_{7}$ of $\operatorname{CompStruct}$ applied to $x_{4}$, $x_{5}$ and $x_{6}$, the composition of $\mathrm{map}$ applied to $x_{1}$, $x_{2}$ and $x_{4}$ and $\mathrm{map}$ applied to $x_{2}$, $x_{3}$ and $x_{5}$ is equal to $\mathrm{map}$ applied to $x_{1}$, $x_{3}$ and $x_{6}$. Then $\mathrm{SSet\_\_Truncated\_\_HomotopyCategory\_u2082\_\_\_desc}$ applied to $\mathrm{obj}$, $x_{9}$, $y$, $\mathrm{map}$, $\mathrm{map\_id}$ and $\mathrm{map\_comp}$ is a functor of the set of homotopy categories of $X$ and $D$.

the homomorphism of f (from the name)

Let $f$ be an edge of $x$ and $x_{1}$. Then the homomorphism of $f$ is a homomorphism of $\mathrm{SSet\_\_Truncated\_\_HomotopyCategory\_u2082\_\_\_mk}$ applied to $x$ and $\mathrm{SSet\_\_Truncated\_\_HomotopyCategory\_u2082\_\_\_mk}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{instSetoidEdge}$ applied to $\mathrm{SSet\_\_Truncated\_\_HomotopyCategory\_u2082\_\_\_pt}$ applied to $\mathrm{SSet\_\_Truncated\_\_HomotopyCategory\_u2082\_\_\_mk}$ applied to $x$ and $\mathrm{SSet\_\_Truncated\_\_HomotopyCategory\_u2082\_\_\_pt}$ applied to $\mathrm{SSet\_\_Truncated\_\_HomotopyCategory\_u2082\_\_\_mk}$ applied to $x_{1}$ and $f$.

Let $\mathrm{self}$ be a homotopy category of $X$. Then $\mathrm{SSet\_\_Truncated\_\_HomotopyCategory\_u2082\_\_\_pt}$ applied to $\mathrm{self}$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_Truncated\_\_Quasicategory\_u2082\_\_\_\_proof\_1}$ defined as $\mathrm{SSet\_\_Truncated\_\_HomotopyCategory\_u2082\_\_\_proj0}$ applied to $\mathrm{self}$.

X is a quasicategory (from the name)

Let $X$ be an element of $\operatorname{Truncated}$ applied to $2$. Then we can say that $X$ is a quasicategory.

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Let $x_{3}$ be a set. Then the elements of $\operatorname{ReedyStructure}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ are a basic type.

the degree of self and x7 (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{ReedyStructure}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$. Let $x_{7}$ be an element of $C$. Then the degree of $\mathrm{self}$ and $x_{7}$ is an element of $x_{3}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{7}$.

the degree of r and f (from the docstring)

Let $r$ be an element of $\operatorname{ReedyStructure}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$. Let $f$ be a homomorphism of $X$ and $Y$. Then the degree of $r$ and $f$ is an element of $x_{3}$ defined as the degree of $r$ and $\operatorname{Z}$ applied to the map factorization data of $r$ and $f$.

the map factorization data of r and f (from the name)

Let $r$ be an element of $\operatorname{ReedyStructure}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map factorization data of $r$ and $f$ is a map factorization data of $x_{2}$ and $f$ defined as $\operatorname{default}$.

the opposite of r (from the docstring)

Let $r$ be an element of $\operatorname{ReedyStructure}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$. Then the opposite of $r$ is an element of $\operatorname{ReedyStructure}$ applied to the opposite of $x_{2}$, the opposite of $x_{1}$ and $x_{3}$.

$\operatorname{reedyStructure}$ is an element of $\operatorname{ReedyStructure}$ applied to the epimorphism of the set of simplex categories, the monomorphism of the set of simplex categories and $\Natural$.

Let $g$ be a function from elements $a$ of $x_{1}$ to homomorphisms of $A$ applied to $a$ and $B$ applied to $a$. Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the elements of $\operatorname{AttachCells}$ applied to $a$, $g$ and $f$ are a basic type.

the inclusion of c and i (from the docstring)

Let $c$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Let $i$ be an inclusion of $c$. Then the inclusion of $c$ and $i$ is a homomorphism of $B$ applied to the projection of $c$ and $i$ and $x_{3}$ defined as the composition of the injection of the cofan of $c$ and $i$ and $\mathrm{HomotopicalAlgebra\_\_AttachCells\_\_g\_u2082\_}$ applied to $c$.

the cofan of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Then the cofan of $\mathrm{self}$ is a cofan of the function that maps $i$ to $A$ applied to the projection of $\mathrm{self}$ and $i$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the cofan of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Then the cofan of $\mathrm{self}$ is a cofan of the function that maps $i$ to $B$ applied to the projection of $\mathrm{self}$ and $i$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Then $\mathrm{HomotopicalAlgebra\_\_AttachCells\_\_g\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to the cofan of $\mathrm{self}$ and $x_{2}$ defined as $\operatorname{proj8}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Then $\mathrm{HomotopicalAlgebra\_\_AttachCells\_\_g\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to the cofan of $\mathrm{self}$ and $x_{3}$ defined as $\operatorname{proj9}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Then $\mathrm{HomotopicalAlgebra\_\_AttachCells\_\_isColimit\_u2081\_}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to the cofan of $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Then $\mathrm{HomotopicalAlgebra\_\_AttachCells\_\_isColimit\_u2082\_}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to the cofan of $\mathrm{self}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Then $\operatorname{m}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to the cofan of $\mathrm{self}$ and $\operatorname{pt}$ applied to the cofan of $\mathrm{self}$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$.

Let $c$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Let $e$ be an isomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $\mathrm{f'}$. Then $\operatorname{ofArrowIso}$ applied to $c$ and $e$ is an element of $\operatorname{AttachCells}$ applied to $g$ and $\mathrm{f'}$.

the reindexing of c and e (from the name)

Let $c$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Let $e$ be an equivalence from $x_{4}$ to the set of inclusions of $c$. Then the reindexing of $c$ and $e$ is an element of $\operatorname{AttachCells}$ applied to $g$ and $f$.

the reindexing cell type of ha and i (from the name)

Let $c$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Let $\mathrm{g'}$ be a function from elements $\mathrm{i'}$ of $x_{4}$ to homomorphisms of $\mathrm{A'}$ applied to $\mathrm{i'}$ and $\mathrm{B'}$ applied to $\mathrm{i'}$. Let $a$ be a function from elements of $x_{1}$ to elements of $x_{4}$. Let $\mathrm{ha}$ be a function from elements $i$ of $x_{1}$ to isomorphisms of $\operatorname{mk}$ applied to $g$ applied to $i$ and $\operatorname{mk}$ applied to $\mathrm{g'}$ applied to $a$ applied to $i$. Then the reindexing cell type of $\mathrm{g'}$ and $a$ is an element of $\operatorname{AttachCells}$ applied to $\mathrm{g'}$ and $f$.

inclusion of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Then an inclusion of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

the projection of self and x4 (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{AttachCells}$ applied to $g$ and $f$. Let $x_{4}$ be an inclusion of $\mathrm{self}$. Then the projection of $\mathrm{self}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{4}$.

relative cell complex of basicCell and j (from the name)

Let $\mathrm{basicCell}$ be a function from elements $j$ of $J$ and elements $i$ of $x_{4}$ applied to $j$ to homomorphisms of $A$ applied to $j$ and $i$ and $B$ applied to $j$ and $i$. Let $f$ be a homomorphism of $X$ and $Y$. Then the relative cell complexes of $j$ and $i$ are a basic type.

cell of c (from the name)

Let $c$ be a relative cell complex of $\mathrm{basicCell}$ and $f$. Then the cells of $c$ are a basic type.

Let $x_{5}$ be a cell of $c$. Then $\operatorname{i}$ applied to $x_{5}$ is an element of $x_{4}$ applied to $\operatorname{j}$ applied to $x_{5}$ defined as the projection of $\operatorname{attachCells}$ applied to $c$, $\operatorname{j}$ applied to $x_{5}$ and $\operatorname{hj}$ applied to $x_{5}$ and $\operatorname{k}$ applied to $x_{5}$.

Let $\mathrm{self}$ be a cell of $c$. Then $\operatorname{j}$ applied to $\mathrm{self}$ is an element of $J$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a cell of $c$. Then $\operatorname{k}$ applied to $\mathrm{self}$ is an inclusion of $\operatorname{attachCells}$ applied to $c$, $\operatorname{j}$ applied to $\mathrm{self}$ and $\operatorname{hj}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the inclusion of x5 (from the docstring)

Let $x_{5}$ be a cell of $c$. Then the inclusion of $x_{5}$ is a homomorphism of $B$ applied to $\operatorname{j}$ applied to $x_{5}$ and $\operatorname{i}$ applied to $x_{5}$ and $Y$ defined as the composition of the inclusion of $\operatorname{attachCells}$ applied to $c$, $\operatorname{j}$ applied to $x_{5}$ and $\operatorname{hj}$ applied to $x_{5}$ and $\operatorname{k}$ applied to $x_{5}$ and the component of the inclusion of $\operatorname{toTransfiniteCompositionOfShape}$ applied to $c$ and the successor of $\operatorname{j}$ applied to $x_{5}$.

Let $\mathrm{self}$ be a relative cell complex of $\mathrm{basicCell}$ and $f$. Let $j$ be an element of $J$ such that $j$ is not a maximum. Then $\operatorname{attachCells}$ applied to $\mathrm{self}$, $j$ and $\mathrm{hj}$ is an element of $\operatorname{AttachCells}$ applied to $\mathrm{basicCell}$ applied to $j$ and the map of $\operatorname{F}$ applied to $\operatorname{toTransfiniteCompositionOfShape}$ applied to $\mathrm{self}$ and the homomorphism of $\mathrm{Order\_\_le\_succ}$ applied to $j$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $j$ and $\mathrm{hj}$.

the transfinite composition of g and i (from the name)

Let $g$ be a function from elements $i$ of $x_{4}$ to homomorphisms of $A$ applied to $i$ and $B$ applied to $i$. Let $c$ be a relative cell complex of the function that maps $x_{5}$ to $g$ and $f$. Then the transfinite composition of $i$ and $g$ is a transfinite composition of shape of $J$ and $f$.

the transfinite composition of c and hc (from the name)

Let $c$ be a relative cell complex of $\mathrm{basicCell}$ and $f$ such that for all cells $s$ of $c$, $I$ holds for $A$ applied to $\operatorname{j}$ applied to $s$ and $\operatorname{i}$ applied to $s$, $B$ applied to $\operatorname{j}$ applied to $s$ and $\operatorname{i}$ applied to $s$ and $\mathrm{basicCell}$ applied to $\operatorname{j}$ applied to $s$ and $\operatorname{i}$ applied to $s$. Then the transfinite composition of $c$ and $\mathrm{hc}$ is a transfinite composition of shape of $J$ and $f$.

augmented simplex category (from the name)

An augmented simplex category is an element of $\operatorname{WithInitial}$ applied to the set of simplex categories.

the equivalence augmented cosimplicial object (from the name)

The equivalence augmented cosimplicial object is an equivalence of the set of functors of the set of augmented simplex categories and $C$ and $\operatorname{Augmented}$ applied to $C$ defined as the equivalence comma.

$\operatorname{equivAugmentedCosimplicialObjectFunctorCompDropIso}$ is an isomorphism of the composition of the functor of the equivalence augmented cosimplicial object and $\operatorname{drop}$ and the action of the left whiskering of the set of augmented simplex categories and $C$ and the inclusion defined as the identity of the composition of the functor of the equivalence augmented cosimplicial object and $\operatorname{drop}$.

the equivalence augmented cosimplicial object functor composition point isomorphism (from the name)

The equivalence augmented cosimplicial object functor composition point isomorphism is an isomorphism of the composition of the functor of the equivalence augmented cosimplicial object and the point of the augmentation and the action of the evaluation of the set of augmented simplex categories and $C$ and the star defined as the identity of the composition of the functor of the equivalence augmented cosimplicial object and the point of the augmentation.

the equivalence augmented cosimplicial object functor composition to arrow isomorphism (from the name)

The equivalence augmented cosimplicial object functor composition to arrow isomorphism is an isomorphism of the composition of the functor of the equivalence augmented cosimplicial object and the arrow and the composition of the functor of the set of augmented simplex categories and $C$ and the action of the evaluation of the set of arrows of the set of augmented simplex categories and the set of arrows of $C$ and $\operatorname{mk}$ applied to $\operatorname{homTo}$ applied to $\operatorname{mk}$ applied to $0$ defined as the identity of the composition of the functor of the equivalence augmented cosimplicial object and the arrow.

the equivalence augmented simplicial object (from the name)

The equivalence augmented simplicial object is an equivalence of the set of functors of the set of opposites of the set of augmented simplex categories and $C$ and $\operatorname{Augmented}$ applied to $C$ defined as the composition of the left congruence of the opposite category of the set of simplex categories and the equivalence comma.

$\operatorname{equivAugmentedSimplicialObjectFunctorCompDropIso}$ is an isomorphism of the composition of the functor of the equivalence augmented simplicial object and $\operatorname{drop}$ and the action of the left whiskering of the set of opposites of the set of augmented simplex categories and $C$ and the opposite of the inclusion defined as the identity of the composition of the functor of the equivalence augmented simplicial object and $\operatorname{drop}$.

the equivalence augmented simplicial object functor composition point isomorphism (from the name)

The equivalence augmented simplicial object functor composition point isomorphism is an isomorphism of the composition of the functor of the equivalence augmented simplicial object and the point of the augmentation and the action of the evaluation of the set of opposites of the set of augmented simplex categories and $C$ and $\operatorname{op}$ applied to the star defined as the identity of the composition of the functor of the equivalence augmented simplicial object and the point of the augmentation.

the equivalence augmented simplicial object functor composition to arrow isomorphism (from the name)

The equivalence augmented simplicial object functor composition to arrow isomorphism is an isomorphism of the composition of the functor of the equivalence augmented simplicial object and the arrow and the composition of the functor of the set of opposites of the set of augmented simplex categories and $C$ and the action of the evaluation of the set of arrows of the set of opposites of the set of augmented simplex categories and the set of arrows of $C$ and $\operatorname{mk}$ applied to the opposite in $\operatorname{homTo}$ applied to $\operatorname{mk}$ applied to $0$ defined as the identity of the composition of the functor of the equivalence augmented simplicial object and the arrow.

the inclusion (from the name)

The inclusion is a functor of the set of simplex categories and the set of augmented simplex categories defined as the inclusion.

the associator of y and z (from the name)

Let $x$, $y$ and $z$ be augmented simplex categories. Then the associator of $y$ and $z$ is an isomorphism of the tensor object of the tensor object of $x$ and $y$ and $z$ and the tensor object of $x$ and the tensor object of $y$ and $z$.

the left injection of x and y (from the name)

Let $x$ and $y$ be augmented simplex categories. Then the left injection of $x$ and $y$ is a homomorphism of $x$ and the tensor object of $x$ and $y$ defined as the composition of the inverse of the right unitor of $x$ and the left whisker of $x$ and $\operatorname{to}$ applied to $\operatorname{starInitial}$ and $y$.

the left injection of x and y (from the name)

Let $x$ and $y$ be simplex categories. Then the left injection of $x$ and $y$ is a homomorphism of $x$ and $\operatorname{tensorObjOf}$ applied to $x$ and $y$ defined as $\operatorname{down}$ applied to the left injection of $\operatorname{of}$ applied to $x$ and $\operatorname{of}$ applied to $y$.

the right injection of x and y (from the name)

Let $x$ and $y$ be augmented simplex categories. Then the right injection of $x$ and $y$ is a homomorphism of $y$ and the tensor object of $x$ and $y$ defined as the composition of the inverse of the left unitor of $y$ and the right whisker of $\operatorname{to}$ applied to $\operatorname{starInitial}$ and $x$ and $y$.

the right injection of x and y (from the name)

Let $x$ and $y$ be simplex categories. Then the right injection of $x$ and $y$ is a homomorphism of $y$ and $\operatorname{tensorObjOf}$ applied to $x$ and $y$ defined as $\operatorname{down}$ applied to the right injection of $\operatorname{of}$ applied to $x$ and $\operatorname{of}$ applied to $y$.

the left unitor isomorphism for the monoidal structure in x (from the docstring)

Let $x$ be an augmented simplex category. Then the left unitor isomorphism for the monoidal structure in $x$ is an isomorphism of the tensor object of the tensor unit and $x$ and $x$.

the right unitor isomorphism for the monoidal structure in x (from the docstring)

Let $x$ be an augmented simplex category. Then the right unitor isomorphism for the monoidal structure in $x$ is an isomorphism of the tensor object of $x$ and the tensor unit and $x$.

the tensor homomorphism of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $x$ and $x_{1}$. Let $x_{5}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the tensor homomorphism of $x_{4}$ and $x_{5}$ is a homomorphism of the tensor object of $x$ and $x_{2}$ and the tensor object of $x_{1}$ and $x_{3}$.

the tensor homomorphism of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $x$ and $x_{1}$. Let $x_{5}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the tensor homomorphism of $x_{4}$ and $x_{5}$ is a homomorphism of $\operatorname{tensorObjOf}$ applied to $x$ and $x_{2}$ and $\operatorname{tensorObjOf}$ applied to $x_{1}$ and $x_{3}$.

the tensor object of m and n (from the name)

Let $m$ and $n$ be augmented simplex categories. Then the tensor object of $m$ and $n$ is an augmented simplex category.

the tensor unit (from the name)

The tensor unit is an augmented simplex category defined as the star.

the constant of y and i (from the name)

Let $x$ and $y$ be simplex categories. Let $i$ be an element of $\mathrm{Fin}$ applied to the sum of the length in $y$ and $1$. Then the constant of $y$ and $i$ is a homomorphism of $x$ and $y$.

the diagonal of n (from the name)

Let $n$ be a natural number. Then the diagonal of $n$ is a homomorphism of $\operatorname{mk}$ applied to $1$ and $\operatorname{mk}$ applied to $n$.

the factor of f and j (from the name)

Let $f$ be a homomorphism of $\operatorname{mk}$ applied to $m$ and $\operatorname{mk}$ applied to $n + 1$. Let $j$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then the factor of $f$ and $j$ is a homomorphism of $\operatorname{mk}$ applied to $m$ and $\operatorname{mk}$ applied to $n$ defined as the composition of $f$ and $\mathrm{SimplexCategory\_\_\_u3c3\_}$ applied to $\operatorname{predAbove}$ applied to $0$ and $j$.

the interval edge of j and l (from the name)

Let $j$ and $l$ be natural numbers such that $j + l \leq n$. Then the interval edge of $j$ and $l$ is a homomorphism of $\operatorname{mk}$ applied to $1$ and $\operatorname{mk}$ applied to $n$.

$\operatorname{isTerminalZero}$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{mk}$ applied to $0$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{mk}$ applied to $0$.

the homomorphism of f (from the name)

Let $f$ be an order homomorphism of $\mathrm{Fin}$ applied to $n + 1$ and $\mathrm{Fin}$ applied to $m + 1$. Then the homomorphism of $f$ is a homomorphism of $\operatorname{mk}$ applied to $n$ and $\operatorname{mk}$ applied to $m$ defined as $\operatorname{mk}$ applied to $f$.

Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $n + 1$ such that $i \leq j$. Then $\operatorname{mkOfLe}$ applied to $i$, $j$ and $h$ is a homomorphism of $\operatorname{mk}$ applied to $1$ and $\operatorname{mk}$ applied to $n$.

Let $i$, $j$ and $k$ be elements of $\mathrm{Fin}$ applied to $n + 1$ such that $i \leq j \leq k$. Then $\operatorname{mkOfLeComp}$ applied to $i$, $j$, $k$, $h$ and $h_{1}$ is a homomorphism of $\operatorname{mk}$ applied to $2$ and $\operatorname{mk}$ applied to $n$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then $\operatorname{mkOfSucc}$ applied to $i$ is a homomorphism of $\operatorname{mk}$ applied to $1$ and $\operatorname{mk}$ applied to $n$.

the order isomorphism of e (from the name)

Let $e$ be an isomorphism of $x$ and $y$. Then the order isomorphism of $e$ is an order isomorphism of $\mathrm{Fin}$ applied to the sum of the length in $x$ and $1$ and $\mathrm{Fin}$ applied to the sum of the length in $y$ and $1$.

the skeletal equivalence (from the name)

The skeletal equivalence is an equivalence of the set of simplex categories and the set of nonempty finite linear orders defined as $\operatorname{asEquivalence}$ applied to the skeletal functor.

the skeletal functor (from the name)

The skeletal functor is a functor of the set of simplex categories and the set of nonempty finite linear orders.

Let $j$ and $l$ be natural numbers such that $j + l \leq n$. Then $\operatorname{subinterval}$ applied to $j$, $l$ and $\mathrm{hjl}$ is a homomorphism of $\operatorname{mk}$ applied to $l$ and $\operatorname{mk}$ applied to $n$.

the category (from the name)

The category is a functor of the set of simplex categories and the set of categories defined as the composition of the skeletal functor and the composition of the forgetful functor of the set of nonempty finite linear orders and the set of linear orders and the composition of the forgetful functor of the set of linear orders and $\mathrm{Lat}$ and the composition of the forgetful functor of $\mathrm{Lat}$ and the set of part orders and the composition of the forgetful functor of the set of part orders and $\mathrm{Preord}$ and $\mathrm{preordToCat}$.

the part order (from the name)

The part order is a functor of the set of simplex categories and the set of part orders defined as the composition of the skeletal functor and the composition of the forgetful functor of the set of nonempty finite linear orders and the set of finite part orders and the composition of the forgetful functor of the set of finite part orders and the set of part orders and the lift functor.

the top isomorphism zero (from the name)

The top isomorphism zero is an isomorphism of $\operatorname{terminal}$ applied to the set of simplex categories and $\operatorname{mk}$ applied to $0$ defined as $\operatorname{terminalIsoIsTerminal}$ applied to $\operatorname{isTerminalZero}$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then $\mathrm{SimplexCategory\_\_\_u3b4\_}$ applied to $i$ is a homomorphism of $\operatorname{mk}$ applied to $n$ and $\operatorname{mk}$ applied to $n + 1$ defined as the homomorphism of the order homomorphism of the successor above order embedding of $i$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\mathrm{SimplexCategory\_\_\_u3c3\_}$ applied to $i$ is a homomorphism of $\operatorname{mk}$ applied to $n + 1$ and $\operatorname{mk}$ applied to $n$ defined as the homomorphism of the predecessor above order homomorphism of $i$.

simplex category (from the name)

The simplex categories are a basic type.

homomorphism of a and b (from the name)

Let $a$ and $b$ be simplex categories. Then a homomorphism of $a$ and $b$ is an element of the function that maps $a$ and $b$ to the set of order homomorphisms of $\mathrm{Fin}$ applied to the sum of the length in $a$ and $1$ and $\mathrm{Fin}$ applied to the sum of the length in $b$ and $1$.

the composition of f and g (from the name)

Let $f$ be a homomorphism of $b$ and $c$. Let $g$ be a homomorphism of $a$ and $b$. Then the composition of $f$ and $g$ is a homomorphism of $a$ and $c$ defined as $\operatorname{mk}$ applied to the composition of the order homomorphism of $f$ and the order homomorphism of $g$.

the identity of a (from the name)

Let $a$ be a simplex category. Then the identity of $a$ is a homomorphism of $a$ and $a$ defined as $\operatorname{mk}$ applied to the identity function.

Let $f$ be an order homomorphism of $\mathrm{Fin}$ applied to the sum of the length in $a$ and $1$ and $\mathrm{Fin}$ applied to the sum of the length in $b$ and $1$. Then $\operatorname{mk}$ applied to $f$ is a homomorphism of $a$ and $b$ defined as $f$.

the order homomorphism of f (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Then the order homomorphism of $f$ is an order homomorphism of $\mathrm{Fin}$ applied to the sum of the length in $a$ and $1$ and $\mathrm{Fin}$ applied to the sum of the length in $b$ and $1$ defined as $f$.

Let $n$ be a natural number. Then an element of $\operatorname{Truncated}$ applied to $n$ is an element of the function that maps $n$ to the set of full subcategories of the function that maps $a$ to the proposition that the length in $a$ is less than or equal to $n$.

the trace of f (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Assume that $\mathrm{autoParam}$ holds for the proposition that the length in $a$ is less than or equal to $n$ and $\mathrm{SimplexCategory\_\_Truncated\_\_Hom\_\_tr\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the length in $b$ is less than or equal to $n$ and $\mathrm{SimplexCategory\_\_Truncated\_\_Hom\_\_tr\_\_\_auto\_3}$. Then the trace of $f$ is a homomorphism of $\operatorname{mk}$ applied to $a$ and $\mathrm{ha}$ and $\operatorname{mk}$ applied to $b$ and $\mathrm{hb}$ defined as the homomorphism of $f$.

the inclusion of n (from the docstring)

Let $n$ and $m$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (n , m)$ and $\mathrm{SimplexCategory\_\_Truncated\_\_incl\_\_\_auto\_1}$. Then the inclusion of $n$ is a functor of $\operatorname{Truncated}$ applied to $n$ and $\operatorname{Truncated}$ applied to $m$.

the inclusion composition inclusion of h (from the name)

Assume that $n \leq m$. Then the inclusion composition inclusion of $h$ is an isomorphism of the composition of the inclusion of $n$ and the inclusion of $m$ and the inclusion of $n$.

the inclusion of n (from the name)

Let $n$ be a natural number. Then the inclusion of $n$ is a functor of $\operatorname{Truncated}$ applied to $n$ and the set of simplex categories defined as the inclusion of the function that maps $a$ to the proposition that the length in $a$ is less than or equal to $n$.

Let $n$ be a natural number. Then $\operatorname{fullyFaithful}$ applied to $n$ is an element of $\operatorname{FullyFaithful}$ applied to the opposite of the inclusion of $n$ defined as $\operatorname{ofFullyFaithful}$ applied to the opposite of the inclusion of $n$.

the notation (from the name)

the homomorphism equivalence functor (from the name)

The homomorphism equivalence functor is an equivalence from the set of homomorphisms of $a$ and $b$ to the set of functors of $\mathrm{Fin}$ applied to the sum of the length in $a$ and $1$ and $\mathrm{Fin}$ applied to the sum of the length in $b$ and $1$ defined as the composition of the homomorphism equivalence order homomorphism and the equivalence functor.

the homomorphism equivalence order homomorphism (from the name)

The homomorphism equivalence order homomorphism is an equivalence from the set of homomorphisms of $a$ and $b$ to the set of order homomorphisms of $\mathrm{Fin}$ applied to the sum of the length in $a$ and $1$ and $\mathrm{Fin}$ applied to the sum of the length in $b$ and $1$.

the length in self (from the docstring)

Let $\mathrm{self}$ be a simplex category. Then the length in $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $i$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (n + i , m)$ and $\mathrm{SimplexCategory\_\_\_u3b4\_\_u2080\_Iter\_\_\_auto\_1}$. Then $\mathrm{SimplexCategory\_\_\_u3b4\_\_u2080\_Iter}$ applied to $i$ and $\mathrm{hi}$ is a homomorphism of $\operatorname{mk}$ applied to $n$ and $\operatorname{mk}$ applied to $m$.

Let $i$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (n + i , m)$ and $\mathrm{SimplexCategory\_\_\_u3c3\_\_u2080\_Iter\_\_\_auto\_1}$. Then $\mathrm{SimplexCategory\_\_\_u3c3\_\_u2080\_Iter}$ applied to $i$ and $\mathrm{hi}$ is a homomorphism of $\operatorname{mk}$ applied to $m$ and $\operatorname{mk}$ applied to $n$.

free simplex quiver (from the name)

A free simplex quiver is a natural number.

homomorphism of x and x1 (from the name)

Let $x$ and $x_{1}$ be free simplex quivers. Then the homomorphisms of $x$ and $x_{1}$ are a basic type.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from natural numbers $n$ and elements $i$ of $\mathrm{Fin}$ applied to $n + 2$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $n$, $\operatorname{mk}$ applied to $n + 1$ and $\mathrm{FreeSimplexQuiver\_\_Hom\_\_\_u3b4\_}$ applied to $i$ and $\mathrm{PULift}$ applied to the set of functions from natural numbers $n_{1}$ and elements $i_{1}$ of $\mathrm{Fin}$ applied to $n_{1} + 1$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $n_{1} + 1$, $\operatorname{mk}$ applied to $n_{1}$ and $\mathrm{FreeSimplexQuiver\_\_Hom\_\_\_u3c3\_}$ applied to $i_{1}$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then $\mathrm{FreeSimplexQuiver\_\_Hom\_\_\_u3b4\_}$ applied to $i$ is a homomorphism of $\operatorname{mk}$ applied to $n$ and $\operatorname{mk}$ applied to $n + 1$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\mathrm{FreeSimplexQuiver\_\_Hom\_\_\_u3c3\_}$ applied to $i$ is a homomorphism of $\operatorname{mk}$ applied to $n + 1$ and $\operatorname{mk}$ applied to $n$.

the homomorphism relation (from the name)

The homomorphism relation is a homomorphism relation of the set of paths of the set of free simplex quivers.

Let $x$ be a free simplex quiver. Then $\operatorname{len}$ applied to $x$ is a natural number defined as $x$.

Let $n$ be a natural number. Then $\operatorname{mk}$ applied to $n$ is a free simplex quiver defined as $n$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then $\mathrm{FreeSimplexQuiver\_\_\_u3b4\_}$ applied to $i$ is a homomorphism of $\operatorname{mk}$ applied to $n$ and $\operatorname{mk}$ applied to $n + 1$ defined as $\mathrm{FreeSimplexQuiver\_\_Hom\_\_\_u3b4\_}$ applied to $i$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\mathrm{FreeSimplexQuiver\_\_\_u3c3\_}$ applied to $i$ is a homomorphism of $\operatorname{mk}$ applied to $n + 1$ and $\operatorname{mk}$ applied to $n$ defined as $\mathrm{FreeSimplexQuiver\_\_Hom\_\_\_u3c3\_}$ applied to $i$.

simplex category generator relation (from the name)

A simplex category generator relation is a quotient of the homomorphism relation.

the degeneracy (from the name)

The degeneracy is a morphism property of the set of simplex category generator relations.

the face (from the name)

The face is a morphism property of the set of simplex category generator relations.

the generator (from the name)

The generator is a morphism property of the set of simplex category generator relations defined as the maximum of the face and the degeneracy.

the length of x (from the docstring)

Let $x$ be a simplex category generator relation. Then the length of $x$ is a natural number.

Let $n$ be a natural number. Then $\operatorname{mk}$ applied to $n$ is a simplex category generator relation defined as $\operatorname{mk}$ applied to the object of $\operatorname{of}$ applied to the set of free simplex quivers and $n$.

the simplex category (from the name)

The simplex category is a functor of the set of simplex category generator relations and the set of simplex categories.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then $\mathrm{SimplexCategoryGenRel\_\_\_u3b4\_}$ applied to $i$ is a homomorphism of $\operatorname{mk}$ applied to $n$ and $\operatorname{mk}$ applied to $n + 1$ defined as the map of the functor of the homomorphism relation and the map of $\operatorname{of}$ applied to the set of free simplex quivers and $\mathrm{FreeSimplexQuiver\_\_Hom\_\_\_u3b4\_}$ applied to $i$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\mathrm{SimplexCategoryGenRel\_\_\_u3c3\_}$ applied to $i$ is a homomorphism of $\operatorname{mk}$ applied to $n + 1$ and $\operatorname{mk}$ applied to $n$ defined as the map of the functor of the homomorphism relation and the map of $\operatorname{of}$ applied to the set of free simplex quivers and $\mathrm{FreeSimplexQuiver\_\_Hom\_\_\_u3c3\_}$ applied to $i$.

the split epimorphism of i (from the name)

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the split epimorphism of $i$ is a split epimorphism of $\mathrm{SimplexCategoryGenRel\_\_\_u3c3\_}$ applied to $i$ defined as $\operatorname{mk}$ applied to $\mathrm{SimplexCategoryGenRel\_\_\_u3b4\_}$ applied to $\operatorname{castSucc}$ applied to $i$ and $\mathrm{SimplexCategoryGenRel\_\_\_u3b4\_\_comp\_\_u3c3\_\_self}$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then $\mathrm{SimplexCategoryGenRel\_\_splitMono\_u3b4\_}$ applied to $i$ is a split monomorphism of $\mathrm{SimplexCategoryGenRel\_\_\_u3b4\_}$ applied to $i$.

Let $m$ be a natural number. Let $L$ be a list of natural numbers. Then we can say that $\operatorname{IsAdmissible}$ holds for $m$ and $L$.

Assume that $\operatorname{IsAdmissible}$ holds for $m$ and $L$. Then we can say that $\operatorname{below}$ holds for $t$.

Assume that $\operatorname{IsAdmissible}$ holds for $m$ and $L$. Let $k$ be a natural number such that $k < \operatorname{length} (L)$. Then $\operatorname{getElemAsFin}$ applied to $\mathrm{hl}$, $k$ and $\mathrm{hK}$ is an element of $\mathrm{Fin}$ applied to $m + k + 1$.

the head of hl (from the docstring)

Assume that $\operatorname{IsAdmissible}$ holds for $m$ and $\operatorname{cons}$ applied to $a$ and $L$. Then the head of $\mathrm{hl}$ is an element of $\mathrm{Fin}$ applied to $m + 1$.

the simplicial evaluation of L and x (from the name)

Let $L$ be a list of natural numbers. Let $x$ be a natural number. Then the simplicial evaluation of $L$ and $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $L$ and $\mathrm{SimplexCategoryGenRel\_\_simplicialEval\_u3c3\_\_\_\_f}$ applied to $x$.

Let $a$ be a natural number. Let $x$ be a list of natural numbers. Then $\operatorname{simplicialInsert}$ applied to $a$ and $x$ is a list of natural numbers defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{SimplexCategoryGenRel\_\_simplicialInsert\_\_\_f}$ and $a$.

the standard of L and h (from the name)

Let $L$ be a list of natural numbers such that $x_{1} + \operatorname{length} (L)= x$. Then the standard of $L$ and $h$ is a homomorphism of $\operatorname{mk}$ applied to $x$ and $\operatorname{mk}$ applied to $x_{1}$ defined as $\operatorname{brecOn}$ applied to $L$, $\mathrm{SimplexCategoryGenRel\_\_standard\_u3c3\_\_\_\_f}$, $x_{1}$ and $h$.

$\operatorname{rev}$ is a functor of the set of simplex categories and the set of simplex categories.

$\operatorname{revCompRevIso}$ is an isomorphism of the composition of $\operatorname{rev}$ and $\operatorname{rev}$ and the identity of the set of simplex categories.

$\operatorname{revEquivalence}$ is an equivalence of the set of simplex categories and the set of simplex categories.

semi simplex category (from the name)

The semi simplex categories are a basic type.

homomorphism of n and m (from the name)

Let $n$ and $m$ be semi simplex categories. Then a homomorphism of $n$ and $m$ is an element of the function that maps $n$ and $m$ to the set of order embeddings of $\mathrm{Fin}$ applied to the sum of the length in $n$ and $1$ and $\mathrm{Fin}$ applied to the sum of the length in $m$ and $1$.

the homomorphism equivalence (from the name)

The homomorphism equivalence is an equivalence from the set of homomorphisms of $n$ and $m$ to the set of order embeddings of $\mathrm{Fin}$ applied to the sum of the length in $n$ and $1$ and $\mathrm{Fin}$ applied to the sum of the length in $m$ and $1$ defined as the identity of the set of homomorphisms of $n$ and $m$.

the homomorphism of f (from the name)

Let $f$ be a homomorphism of the action of the simplex category and $n$ and the action of the simplex category and $m$. Then the homomorphism of $f$ is a homomorphism of $n$ and $m$.

the length in self (from the docstring)

Let $\mathrm{self}$ be a semi simplex category. Then the length in $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the simplex category (from the name)

The simplex category is a functor of the set of semi simplex categories and the set of simplex categories.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then $\mathrm{SimplexCategory\_\_toMk\_u2081\_}$ applied to $i$ is a homomorphism of $\operatorname{mk}$ applied to $n$ and $\operatorname{mk}$ applied to $1$.

the equivalence (from the name)

The equivalence is an equivalence from $\mathrm{Fin}$ applied to $n + 2$ to the set of homomorphisms of $\operatorname{mk}$ applied to $n$ and $\operatorname{mk}$ applied to $1$ defined as the equivalence of $\mathrm{SimplexCategory\_\_toMk\_u2081\_}$ and $\mathrm{SimplexCategory\_\_toMk\_u2081\_\_bijective}$.

Let $m$ be a natural number. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Assume that $\mathrm{autoParam}$ holds for the proposition that the length in $\operatorname{mk}$ applied to $n$ is less than or equal to $m$ and $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the length in $\operatorname{mk}$ applied to $n + 1$ is less than or equal to $m$ and $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_\_\_auto\_3}$. Then $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_}$ applied to $m$, $i$, $\mathrm{hn}$ and $\mathrm{hn'}$ is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $n$ and $\mathrm{hn}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $n + 1$ and $\mathrm{hn'}$ defined as the trace of $\mathrm{SimplexCategory\_\_\_u3b4\_}$ applied to $i$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Assume that $\mathrm{autoParam}$ holds for the proposition that the length in $\operatorname{mk}$ applied to $n$ is less than or equal to $2$ and $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the length in $\operatorname{mk}$ applied to $n + 1$ is less than or equal to $2$ and $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_\_\_\_auto\_3}$. Then $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $i$, $\mathrm{hn}$ and $\mathrm{hn'}$ is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $n$ and $\mathrm{hn}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $n + 1$ and $\mathrm{hn'}$ defined as $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_}$ applied to $2$, $i$, $\mathrm{hn}$ and $\mathrm{hn'}$.

Let $m$ be a natural number. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Assume that $\mathrm{autoParam}$ holds for the proposition that the length in $\operatorname{mk}$ applied to $n + 1$ is less than or equal to $m$ and $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3c3\_\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the length in $\operatorname{mk}$ applied to $n$ is less than or equal to $m$ and $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3c3\_\_\_\_auto\_3}$. Then $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3c3\_}$ applied to $m$, $i$, $\mathrm{hn}$ and $\mathrm{hn'}$ is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $n + 1$ and $\mathrm{hn}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $n$ and $\mathrm{hn'}$ defined as the trace of $\mathrm{SimplexCategory\_\_\_u3c3\_}$ applied to $i$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Assume that $\mathrm{autoParam}$ holds for the proposition that the length in $\operatorname{mk}$ applied to $n + 1$ is less than or equal to $2$ and $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3c3\_\_u2082\_\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the length in $\operatorname{mk}$ applied to $n$ is less than or equal to $2$ and $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3c3\_\_u2082\_\_\_\_auto\_3}$. Then $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3c3\_\_u2082\_}$ applied to $i$, $\mathrm{hn}$ and $\mathrm{hn'}$ is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $n + 1$ and $\mathrm{hn}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $n$ and $\mathrm{hn'}$ defined as $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3c3\_}$ applied to $2$, $i$, $\mathrm{hn}$ and $\mathrm{hn'}$.

simplicial category of C (from the name)

Let $C$ be a set. Then a simplicial category of $C$ is an element of the function that maps $C$ to $\operatorname{EnrichedOrdinaryCategory}$ applied to the set of sets and $C$.

the homomorphism equivalence of K and L (from the name)

Let $K$ and $L$ be elements of $C$. Then the homomorphism equivalence of $K$ and $L$ is an equivalence from the set of homomorphisms of $K$ and $L$ to the action of the homomorphism of $K$ and $L$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ defined as the composition of the homomorphism equivalence of the set of sets and the unit homomorphism equivalence of the homomorphism of $K$ and $L$.

the homomorphism of K and L (from the name)

Let $K$ and $L$ be elements of $C$. Then the homomorphism of $K$ and $L$ is a set defined as the homomorphism of $K$ and $L$.

the homomorphism composition of L and M (from the name)

Let $K$, $L$ and $M$ be elements of $C$. Then the homomorphism composition of $L$ and $M$ is a homomorphism of the tensor object of the homomorphism of $K$ and $L$ and the homomorphism of $L$ and $M$ and the homomorphism of $K$ and $M$ defined as the composition of $L$ and $M$.

the homomorphism functor of C (from the name)

Let $C$ be a set. Then the homomorphism functor of $C$ is a functor of the set of opposites of $C$ and the set of functors of $C$ and the set of sets defined as the homomorphism functor of the set of sets and $C$.

abstract simplicial complex of x (from the name)

Let $x$ be a set. Then the abstract simplicial complexes of $x$ are a basic type.

abstract simplicial complex of x (from the name)

Let $x$ be a set. Then the abstract simplicial complexes of $x$ are a basic type.

the additive singleton of x and K (from the name)

Let $x$ be a set. Let $K$ be an abstract simplicial complex of $x$. Then the additive singleton of $x$ and $K$ is an abstract simplicial complex of $x$.

the face of self (from the name)

Let $\mathrm{self}$ be an abstract simplicial complex of $x$. Then the face of $\mathrm{self}$ is an element of the power set of the set of finite sets of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the map of K and f (from the name)

Let $K$ be an abstract simplicial complex of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $K$ and $f$ is an abstract simplicial complex of $x_{1}$.

the abstract simplicial complex of K (from the name)

Let $x$ be a set. Let $K$ be an abstract simplicial complex of $x$ such that for all elements $v$ of $x$, $\operatorname{singleton}$ applied to $v$ is an element of the face of $K$. Then the abstract simplicial complex of $K$ is an abstract simplicial complex of $x$ defined as $\operatorname{mk}$ applied to $K$ and $h$.

the simplicial nerve of C (from the docstring)

Let $C$ be a set. Then the simplicial nerve of $C$ is a set.

simplicial thickening of J (from the name)

Let $J$ be a set. Then the simplicial thickenings of $J$ are a basic type.

path of i and j (from the name)

Let $i$ and $j$ be elements of $J$. Then the paths of $i$ and $j$ are a basic type.

Let $\mathrm{self}$ be a path of $i$ and $j$. Then $\operatorname{I}$ applied to $\mathrm{self}$ is an element of $\wp J$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a simplicial thickening of $J$. Then $\operatorname{as}$ applied to $\mathrm{self}$ is an element of $J$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the composition functor of j and k (from the name)

Let $i$, $j$ and $k$ be simplicial thickenings of $J$. Then the composition functor of $j$ and $k$ is a functor of $\mathrm{Prod}$ applied to the set of homomorphisms of $i$ and $j$ and the set of homomorphisms of $j$ and $k$ and the set of homomorphisms of $i$ and $k$.

the functor of f (from the name)

Let $f$ be an order homomorphism of $J$ and $K$. Then the functor of $f$ is an enriched functor of the set of simplicial thickenings of $J$ and the set of simplicial thickenings of $K$.

cosimplicial object of C (from the name)

Let $C$ be a set. Then a cosimplicial object of $C$ is an element of the function that maps $C$ to the set of functors of the set of simplex categories and $C$.

Let $C$ be a set. Then an element of $\operatorname{Augmented}$ applied to $C$ is an element of the function that maps $C$ to the set of commas of the constant cosimplicial object of $C$ and the identity of the set of cosimplicial objects of $C$.

the constant augmented cosimplicial object functor (from the docstring)

The constant augmented cosimplicial object functor is a functor of $C$ and $\operatorname{Augmented}$ applied to $C$.

$\operatorname{drop}$ is a functor of $\operatorname{Augmented}$ applied to $C$ and the set of cosimplicial objects of $C$ defined as the second component of the constant cosimplicial object of $C$ and the identity of the set of cosimplicial objects of $C$.

the left opposite of X (from the name)

Let $X$ be an element of $\operatorname{Augmented}$ applied to the set of opposites of $C$. Then the left opposite of $X$ is an element of $\operatorname{Augmented}$ applied to $C$ defined as $\operatorname{mk}$ applied to the left opposite of the right subobject of $X$, the opposite of the left subobject of $X$ and the left opposite of the homomorphism of $X$.

the left opposite right opposite isomorphism of X (from the name)

Let $X$ be an element of $\operatorname{Augmented}$ applied to the set of opposites of $C$. Then the left opposite right opposite isomorphism of $X$ is an isomorphism of the right opposite of the left opposite of $X$ and $X$.

the point of the augmentation (from the docstring)

The point of the augmentation is a functor of $\operatorname{Augmented}$ applied to $C$ and $C$ defined as the first component of the constant cosimplicial object of $C$ and the identity of the set of cosimplicial objects of $C$.

the arrow (from the name)

The arrow is a functor of $\operatorname{Augmented}$ applied to $C$ and the set of arrows of $C$.

the whiskering of C and D (from the name)

Let $C$ and $D$ be sets. Then the whiskering of $C$ and $D$ is a functor of the set of functors of $C$ and $D$ and the set of functors of $\operatorname{Augmented}$ applied to $C$ and $\operatorname{Augmented}$ applied to $D$.

the whiskering object of F (from the name)

Let $C$ and $D$ be sets. Let $F$ be a functor of $C$ and $D$. Then the whiskering object of $F$ is a functor of $\operatorname{Augmented}$ applied to $C$ and $\operatorname{Augmented}$ applied to $D$.

Let $C$ be a set. Let $n$ be a natural number. Then an element of $\operatorname{Truncated}$ applied to $C$ and $n$ is an element of the function that maps $C$ and $n$ to the set of functors of $\operatorname{Truncated}$ applied to $n$ and $C$.

the notation (from the name)

the truncation of n and m (from the name)

Let $C$ be a set. Let $n$ and $m$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (m , n)$ and $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_Truncated\_\_trunc\_\_\_auto\_1}$. Then the truncation of $n$ and $m$ is a functor of $\operatorname{Truncated}$ applied to $C$ and $n$ and $\operatorname{Truncated}$ applied to $C$ and $m$.

the whiskering of C and D (from the name)

Let $C$ and $D$ be sets. Then the whiskering of $C$ and $D$ is a functor of the set of functors of $C$ and $D$ and the set of functors of $\operatorname{Truncated}$ applied to $C$ and $n$ and $\operatorname{Truncated}$ applied to $D$ and $n$ defined as the right whiskering of $C$ and $D$.

Let $X$ be a cosimplicial object of $C$. Let $x_{1}$ be an element of $C$. Let $f$ be a homomorphism of $x_{1}$ and the action of $X$ and $\operatorname{mk}$ applied to $0$ such that for all simplex categories $i$, for all homomorphisms $x_{2}$ and $x_{3}$ of $\operatorname{mk}$ applied to $0$ and $i$, the composition of $f$ and the map of $X$ and $x_{2}$ is equal to the composition of $f$ and the map of $X$ and $x_{3}$. Then $\operatorname{augment}$ applied to $X$, $x_{1}$, $f$ and $w$ is an element of $\operatorname{Augmented}$ applied to $C$.

Let $X$ be a cosimplicial object of $C$. Let $\mathrm{hT}$ be an element of $\operatorname{IsInitial}$ applied to $T$. Then $\operatorname{augmentOfIsInitial}$ applied to $X$ and $\mathrm{hT}$ is an element of $\operatorname{Augmented}$ applied to $C$.

the constant cosimplicial object of C (from the docstring)

Let $C$ be a set. Then the constant cosimplicial object of $C$ is a functor of $C$ and the set of cosimplicial objects of $C$ defined as the constant of the set of simplex categories.

Let $X$ be a cosimplicial object of $C$. Assume that $n = m$. Then $\operatorname{eqToIso}$ applied to $X$ and $h$ is an isomorphism of the action of $X$ and $\operatorname{mk}$ applied to $n$ and the action of $X$ and $\operatorname{mk}$ applied to $m$.

the truncation of n (from the name)

Let $n$ be a natural number. Then the truncation of $n$ is a functor of the set of cosimplicial objects of $C$ and $\operatorname{Truncated}$ applied to $C$ and $n$ defined as the action of the left whiskering of the set of simplex categories and $C$ and the inclusion of $n$.

the truncation composition truncation of h (from the name)

Assume that $m \leq n$. Then the truncation composition truncation of $h$ is an isomorphism of the composition of the truncation of $n$ and the truncation of $n$ and $m$ and the truncation of $m$.

the whiskering of C and D (from the name)

Let $C$ and $D$ be sets. Then the whiskering of $C$ and $D$ is a functor of the set of functors of $C$ and $D$ and the set of functors of the set of cosimplicial objects of $C$ and the set of cosimplicial objects of $D$ defined as the right whiskering of $C$ and $D$.

Let $X$ be a cosimplicial object of $C$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $X$ and $i$ is a homomorphism of the action of $X$ and $\operatorname{mk}$ applied to $n$ and the action of $X$ and $\operatorname{mk}$ applied to $n + 1$ defined as the map of $X$ and $\mathrm{SimplexCategory\_\_\_u3b4\_}$ applied to $i$.

Let $X$ be a cosimplicial object of $C$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3c3\_}$ applied to $X$ and $i$ is a homomorphism of the action of $X$ and $\operatorname{mk}$ applied to $n + 1$ and the action of $X$ and $\operatorname{mk}$ applied to $n$ defined as the map of $X$ and $\mathrm{SimplexCategory\_\_\_u3c3\_}$ applied to $i$.

simplicial object of C (from the name)

Let $C$ be a set. Then a simplicial object of $C$ is an element of the function that maps $C$ to the set of functors of the set of opposites of the set of simplex categories and $C$.

Let $C$ be a set. Then an element of $\operatorname{Augmented}$ applied to $C$ is an element of the function that maps $C$ to the set of commas of the identity of the set of simplicial objects of $C$ and the constant simplicial object of $C$.

the constant augmented simplicial object functor (from the docstring)

The constant augmented simplicial object functor is a functor of $C$ and $\operatorname{Augmented}$ applied to $C$.

$\operatorname{drop}$ is a functor of $\operatorname{Augmented}$ applied to $C$ and the set of simplicial objects of $C$ defined as the first component of the identity of the set of simplicial objects of $C$ and the constant simplicial object of $C$.

the point of the augmentation (from the docstring)

The point of the augmentation is a functor of $\operatorname{Augmented}$ applied to $C$ and $C$ defined as the second component of the identity of the set of simplicial objects of $C$ and the constant simplicial object of $C$.

the right opposite of X (from the name)

Let $X$ be an element of $\operatorname{Augmented}$ applied to $C$. Then the right opposite of $X$ is an element of $\operatorname{Augmented}$ applied to the set of opposites of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to the right subobject of $X$, the right opposite of the left subobject of $X$ and the right opposite of the homomorphism of $X$.

the right opposite left opposite isomorphism of X (from the name)

Let $X$ be an element of $\operatorname{Augmented}$ applied to $C$. Then the right opposite left opposite isomorphism of $X$ is an isomorphism of the left opposite of the right opposite of $X$ and $X$.

the arrow (from the name)

The arrow is a functor of $\operatorname{Augmented}$ applied to $C$ and the set of arrows of $C$.

the whiskering of C and D (from the name)

Let $C$ and $D$ be sets. Then the whiskering of $C$ and $D$ is a functor of the set of functors of $C$ and $D$ and the set of functors of $\operatorname{Augmented}$ applied to $C$ and $\operatorname{Augmented}$ applied to $D$.

the whiskering object of F (from the name)

Let $C$ and $D$ be sets. Let $F$ be a functor of $C$ and $D$. Then the whiskering object of $F$ is a functor of $\operatorname{Augmented}$ applied to $C$ and $\operatorname{Augmented}$ applied to $D$.

Let $C$ be a set. Let $n$ be a natural number. Then an element of $\operatorname{Truncated}$ applied to $C$ and $n$ is an element of the function that maps $C$ and $n$ to the set of functors of the set of opposites of $\operatorname{Truncated}$ applied to $n$ and $C$.

Let $n$ be a natural number. Then $\operatorname{cosk}$ applied to $n$ is a functor of $\operatorname{Truncated}$ applied to $C$ and $n$ and the set of simplicial objects of $C$ defined as $\operatorname{ran}$ applied to the opposite of the inclusion of $n$.

Let $n$ be a natural number. Then $\operatorname{fullyFaithful}$ applied to $n$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{cosk}$ applied to $n$ defined as $\operatorname{fullyFaithfulROfIsIsoCounit}$ applied to $\operatorname{coskAdj}$ applied to $n$.

the notation (from the name)

Let $n$ be a natural number. Then $\operatorname{sk}$ applied to $n$ is a functor of $\operatorname{Truncated}$ applied to $C$ and $n$ and the set of simplicial objects of $C$ defined as $\operatorname{lan}$ applied to the opposite of the inclusion of $n$.

Let $n$ be a natural number. Then $\operatorname{fullyFaithful}$ applied to $n$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{sk}$ applied to $n$ defined as $\operatorname{fullyFaithfulLOfIsIsoUnit}$ applied to $\operatorname{skAdj}$ applied to $n$.

the truncation of n and m (from the name)

Let $C$ be a set. Let $n$ and $m$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (m , n)$ and $\mathrm{CategoryTheory\_\_SimplicialObject\_\_Truncated\_\_trunc\_\_\_auto\_1}$. Then the truncation of $n$ and $m$ is a functor of $\operatorname{Truncated}$ applied to $C$ and $n$ and $\operatorname{Truncated}$ applied to $C$ and $m$.

the whiskering of C and D (from the name)

Let $C$ and $D$ be sets. Then the whiskering of $C$ and $D$ is a functor of the set of functors of $C$ and $D$ and the set of functors of $\operatorname{Truncated}$ applied to $C$ and $n$ and $\operatorname{Truncated}$ applied to $D$ and $n$ defined as the right whiskering of $C$ and $D$.

Let $X$ be a simplicial object of $C$. Let $x_{1}$ be an element of $C$. Let $f$ be a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and $x_{1}$ such that for all simplex categories $i$, for all homomorphisms $x_{2}$ and $x_{3}$ of $\operatorname{mk}$ applied to $0$ and $i$, the composition of the map of $X$ and the opposite in $x_{2}$ and $f$ is equal to the composition of the map of $X$ and the opposite in $x_{3}$ and $f$. Then $\operatorname{augment}$ applied to $X$, $x_{1}$, $f$ and $w$ is an element of $\operatorname{Augmented}$ applied to $C$.

Let $X$ be a simplicial object of $C$. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then $\operatorname{augmentOfIsTerminal}$ applied to $X$ and $\mathrm{hT}$ is an element of $\operatorname{Augmented}$ applied to $C$.

the constant simplicial object of C (from the docstring)

Let $C$ be a set. Then the constant simplicial object of $C$ is a functor of $C$ and the set of simplicial objects of $C$ defined as the constant of the set of opposites of the set of simplex categories.

Let $n$ be a natural number. Then $\operatorname{cosk}$ applied to $n$ is a functor of the set of simplicial objects of $C$ and the set of simplicial objects of $C$ defined as the composition of the truncation of $n$ and $\operatorname{cosk}$ applied to $n$.

Let $n$ be a natural number. Then $\operatorname{coskAdj}$ applied to $n$ is an adjunction of the truncation of $n$ and $\operatorname{cosk}$ applied to $n$ defined as $\operatorname{ranAdjunction}$ applied to the opposite of the inclusion of $n$ and $C$.

the diagonal of X (from the docstring)

Let $X$ be a simplicial object of $C$. Then the diagonal of $X$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$ defined as the map of $X$ and the opposite in the diagonal of $n$.

Let $X$ be a simplicial object of $C$. Assume that $n = m$. Then $\operatorname{eqToIso}$ applied to $X$ and $h$ is an isomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $m$.

Let $n$ be a natural number. Then $\operatorname{sk}$ applied to $n$ is a functor of the set of simplicial objects of $C$ and the set of simplicial objects of $C$ defined as the composition of the truncation of $n$ and $\operatorname{sk}$ applied to $n$.

Let $n$ be a natural number. Then $\operatorname{skAdj}$ applied to $n$ is an adjunction of $\operatorname{sk}$ applied to $n$ and the truncation of $n$ defined as $\operatorname{lanAdjunction}$ applied to the opposite of the inclusion of $n$ and $C$.

the truncation of n (from the name)

Let $n$ be a natural number. Then the truncation of $n$ is a functor of the set of simplicial objects of $C$ and $\operatorname{Truncated}$ applied to $C$ and $n$ defined as the action of the left whiskering of the set of opposites of the set of simplex categories and $C$ and the opposite of the inclusion of $n$.

the truncation composition truncation of h (from the name)

Assume that $m \leq n$. Then the truncation composition truncation of $h$ is an isomorphism of the composition of the truncation of $n$ and the truncation of $n$ and $m$ and the truncation of $m$.

the whiskering of C and D (from the name)

Let $C$ and $D$ be sets. Then the whiskering of $C$ and $D$ is a functor of the set of functors of $C$ and $D$ and the set of functors of the set of simplicial objects of $C$ and the set of simplicial objects of $D$ defined as the right whiskering of $C$ and $D$.

Let $X$ be a simplicial object of $C$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_}$ applied to $X$ and $i$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n + 1$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ defined as the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_\_u3b4\_}$ applied to $i$.

Let $X$ be a simplicial object of $C$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3c3\_}$ applied to $X$ and $i$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n + 1$ defined as the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_\_u3c3\_}$ applied to $i$.

the cosimplicial simplicial equivalence of C (from the name)

Let $C$ be a set. Then the cosimplicial simplicial equivalence of $C$ is an equivalence of the set of opposites of the set of cosimplicial objects of $C$ and the set of simplicial objects of the set of opposites of $C$ defined as the opposite opposite equivalence of the set of simplex categories and $C$.

Let $C$ be a set. Then $\operatorname{cosimplicialToSimplicialAugmented}$ applied to $C$ is a functor of $\operatorname{Augmented}$ applied to the set of opposites of $C$ and the set of opposites of $\operatorname{Augmented}$ applied to $C$.

the simplicial cosimplicial augmented equivalence of C (from the name)

Let $C$ be a set. Then the simplicial cosimplicial augmented equivalence of $C$ is an equivalence of the set of opposites of $\operatorname{Augmented}$ applied to $C$ and $\operatorname{Augmented}$ applied to the set of opposites of $C$.

the simplicial cosimplicial equivalence of C (from the name)

Let $C$ be a set. Then the simplicial cosimplicial equivalence of $C$ is an equivalence of the set of opposites of the set of simplicial objects of $C$ and the set of cosimplicial objects of the set of opposites of $C$ defined as the left opposite right opposite equivalence of the set of simplex categories and $C$.

Let $C$ be a set. Then $\operatorname{simplicialToCosimplicialAugmented}$ applied to $C$ is a functor of the set of opposites of $\operatorname{Augmented}$ applied to $C$ and $\operatorname{Augmented}$ applied to the set of opposites of $C$.

the homomorphism of p and q (from the name)

Let $H$ be a homotopy of $f$ and $g$. Let $p$ and $q$ be natural numbers. Then the homomorphism of $p$ and $q$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $p$ and the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $q$.

the chain homotopy of H (from the name)

Let $H$ be a homotopy of $f$ and $g$. Then the chain homotopy of $H$ is a homotopy of the map of the alternating face map complex of $C$ and $f$ and the map of the alternating face map complex of $C$ and $g$.

Let $X$ be a simplicial object of $C$. Let $n$ be a natural number. Then we can say that $\operatorname{IsCoskeletal}$ holds for $X$ and $n$.

Let $X$ be a simplicial object of $C$. Let $n$ be a natural number. Then $\operatorname{isUniversalOfIsRightKanExtension}$ applied to $X$ and $n$ is an element of $\operatorname{IsUniversal}$ applied to the right extension inclusion of $X$ and $n$ defined as $\operatorname{isUniversalOfIsRightKanExtension}$ applied to $X$ and the identity morphism of the composition of the opposite of the inclusion of $n$ and $X$.

the right extension inclusion of X and n (from the name)

Let $X$ be a simplicial object of $C$. Let $n$ be a natural number. Then the right extension inclusion of $X$ and $n$ is a right extension of the opposite of the inclusion of $n$ and the composition of the opposite of the inclusion of $n$ and $X$ defined as $\operatorname{mk}$ applied to $X$ and the identity morphism of the composition of the opposite of the inclusion of $n$ and $X$.

the canonical isomorphism of X and n (from the docstring)

Let $X$ be a simplicial object of $C$. Let $n$ be a natural number. Then the canonical isomorphism of $X$ and $n$ is an isomorphism of $X$ and the action of $\operatorname{cosk}$ applied to $n$ and $X$ defined as $\operatorname{asIso}$ applied to the component of the unit of $\operatorname{coskAdj}$ applied to $n$ and $X$.

Let $X$ be a simplicial object of $C$. Let $i$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (n + i , m)$ and $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_\_u2080\_Iter\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_\_u2080\_Iter}$ applied to $X$, $i$ and $\mathrm{hi}$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $m$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ defined as the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_\_u3b4\_\_u2080\_Iter}$ applied to $i$ and $\mathrm{hi}$.

Let $X$ be a simplicial object of $C$. Let $i$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (n + i , m)$ and $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3c3\_\_u2080\_Iter\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3c3\_\_u2080\_Iter}$ applied to $X$, $i$ and $\mathrm{hi}$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $m$ defined as the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_\_u3c3\_\_u2080\_Iter}$ applied to $i$ and $\mathrm{hi}$.

homotopy of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the homotopies of $f$ and $g$ are a basic type.

Let $\mathrm{self}$ be a homotopy of $f$ and $g$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{h}$ applied to $\mathrm{self}$ and $i$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n + 1$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

the postcomposition of H and p (from the name)

Let $H$ be a homotopy of $f$ and $g$. Let $p$ be a homomorphism of $Y$ and $\mathrm{Y'}$. Then the postcomposition of $H$ and $p$ is a homotopy of the composition of $f$ and $p$ and the composition of $g$ and $p$.

the precomposition of H and p (from the name)

Let $H$ be a homotopy of $f$ and $g$. Let $p$ be a homomorphism of $\mathrm{X'}$ and $X$. Then the precomposition of $H$ and $p$ is a homotopy of the composition of $p$ and $f$ and the composition of $p$ and $g$.

the identity of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the identity of $f$ is a homotopy of $f$ and $f$.

the right whisker of H and F (from the name)

Let $H$ be a homotopy of $f$ and $g$. Let $F$ be a functor of $C$ and $D$. Then the right whisker of $H$ and $F$ is a homotopy of the map of the action of the whiskering of $C$ and $D$ and $F$ and $f$ and the map of the action of the whiskering of $C$ and $D$ and $F$ and $g$.

$\operatorname{II}$ is a cosimplicial object of the set of opposites of the set of simplex categories.

the opposite equivalence (from the name)

The opposite equivalence is an equivalence of the set of simplicial objects of $C$ and the set of simplicial objects of $C$.

the opposite functor (from the name)

The opposite functor is a functor of the set of simplicial objects of $C$ and the set of simplicial objects of $C$ defined as the action of the left whiskering of the set of opposites of the set of simplex categories and $C$ and the opposite of $\operatorname{rev}$.

the functor (from the docstring)

The functor is an isomorphism of the composition of the opposite functor and the opposite functor and the identity of the set of simplicial objects of $C$ defined as the composition of the inverse of the whiskering left object composition isomorphism of the opposite of $\operatorname{rev}$ and the opposite of $\operatorname{rev}$ and the composition of the map isomorphism of the left whiskering of the set of opposites of the set of simplex categories and $C$ and the composition of the inverse of the opposite composition of $\operatorname{rev}$ and $\operatorname{rev}$ and the composition of the map isomorphism of the opposite homomorphism of the set of simplex categories and the set of simplex categories and the opposite isomorphism of the inverse of $\operatorname{revCompRevIso}$ and the opposite identity of the set of simplex categories and the whiskering left object identity isomorphism.

the isomorphism (from the docstring)

The isomorphism is an isomorphism of the action of the action of the opposite functor and $X$ and $n$ and the action of $X$ and $n$ defined as the identity of the action of the action of the opposite functor and $X$ and $n$.

split of C (from the name)

Let $C$ be a set. Then the splits of $C$ are a basic type.

homomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be splits of $C$. Then the homomorphisms of $x_{1}$ and $x_{2}$ are a basic type.

Let $\mathrm{self}$ be a homomorphism of $x_{1}$ and $x_{2}$. Then $\operatorname{F}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{X}$ applied to $x_{1}$ and $\operatorname{X}$ applied to $x_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $n$ be a natural number. Then $\operatorname{f}$ applied to $\mathrm{self}$ and $n$ is a homomorphism of $\operatorname{N}$ applied to $\operatorname{s}$ applied to $x_{1}$ and $n$ and $\operatorname{N}$ applied to $\operatorname{s}$ applied to $x_{2}$ and $n$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $n$.

Let $\mathrm{self}$ be a split of $C$. Then $\operatorname{X}$ applied to $\mathrm{self}$ is a simplicial object of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the evaluation of C and n (from the name)

Let $C$ be a set. Let $n$ be a natural number. Then the evaluation of $C$ and $n$ is a functor of the set of splits of $C$ and $C$.

Let $C$ be a set. Then $\operatorname{forget}$ applied to $C$ is a functor of the set of splits of $C$ and the set of simplicial objects of $C$.

Let $s$ be a splitting of $X$. Then $\operatorname{mk'}$ applied to $s$ is a split of $C$ defined as $\operatorname{mk}$ applied to $X$ and $s$.

the natural transformation cofan injection of C and A (from the name)

Let $C$ be a set. Let $A$ be an index set of $x_{1}$. Then the natural transformation cofan injection of $C$ and $A$ is a homomorphism of the evaluation of $C$ and the length in the opposite of $\operatorname{fst}$ applied to $A$ and the composition of $\operatorname{forget}$ applied to $C$ and the action of the evaluation of the set of opposites of the set of simplex categories and $C$ and $x_{1}$.

Let $\mathrm{self}$ be a split of $C$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is a splitting of $\operatorname{X}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

splitting of X (from the name)

Let $X$ be a simplicial object of $C$. Then the splittings of $X$ are a basic type.

index set of x (from the name)

Let $x$ be an opposite of the set of simplex categories. Then an index set of $x$ is an element of the function that maps $x$ to $\Sigma$ applied to the function that maps $x_{1}$ to $\SubtypeSet {x_{2}}{\operatorname{Epi} (x_{2})}$.

Let $A$ be an index set of $x$. Then $\operatorname{EqId}$ holds for $A$, if $A$ is equal to the identity of $x$.

Let $A$ be an index set of $x$. Then $\operatorname{e}$ applied to $A$ is a homomorphism of the opposite of $x$ and the opposite of $\operatorname{fst}$ applied to $A$ defined as $\operatorname{snd}$ applied to $A$.

the epimorphism composition of A and p (from the name)

Let $A$ be an index set of $x$. Let $p$ be a homomorphism of $x$ and $x_{1}$. Then the epimorphism composition of $A$ and $p$ is an index set of $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{fst}$ applied to $A$ and the composition of the opposite of $p$ and $\operatorname{e}$ applied to $A$.

the identity of x (from the name)

Let $x$ be an opposite of the set of simplex categories. Then the identity of $x$ is an index set of $x$ defined as $\operatorname{mk}$ applied to $x$ and the identity morphism of the opposite of $x$.

Let $f$ be a homomorphism of $x$ and $x_{1}$. Then $\operatorname{mk}$ applied to $f$ is an index set of $\operatorname{op}$ applied to $x$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $x_{1}$ and $f$.

Let $A$ be an index set of $x$. Let $x_{2}$ be a homomorphism of $x$ and $x_{1}$. Then $\operatorname{pull}$ applied to $A$ and $x_{2}$ is an index set of $x_{1}$ defined as $\operatorname{mk}$ applied to the map from the source to the image of the composition of the opposite of $x_{2}$ and $\operatorname{e}$ applied to $A$.

Let $\mathrm{self}$ be a splitting of $X$. Let $x_{1}$ be a natural number. Then $\operatorname{N}$ applied to $\mathrm{self}$ and $x_{1}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

the cofan of s and x1 (from the name)

Let $s$ be a splitting of $X$. Let $x_{1}$ be an opposite of the set of simplex categories. Then the cofan of $s$ and $x_{1}$ is a cofan of $\operatorname{summand}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to the action of $X$ and $x_{1}$ and the function that maps $A$ to the composition of the inclusion of $s$ and the length in the opposite of $\operatorname{fst}$ applied to $A$ and the map of $X$ and the opposite in $\operatorname{e}$ applied to $A$.

the cofan of x1 and n (from the name)

Let $N$ be a function from natural numbers to elements of $C$. Let $X$ be a simplicial object of $C$. Let $x_{1}$ be a function from natural numbers $n$ to homomorphisms of $N$ applied to $n$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$. Let $x_{2}$ be an opposite of the set of simplex categories. Then the cofan of $n$ and $x_{1}$ is a cofan of $\operatorname{summand}$ applied to $x_{2}$ defined as the function that maps $x_{2}$ to $\operatorname{mk}$ applied to the action of $X$ and $x_{1}$, the function that maps $A$ to the composition of $n$ applied to the length in the opposite of $\operatorname{fst}$ applied to $A$ and the map of $X$ and the opposite in $\operatorname{e}$ applied to $A$ and $x_{2}$.

Let $s$ be a splitting of $X$. Let $x_{1}$ be an opposite of the set of simplex categories. Let $F$ be a function from index sets $A$ of $x_{1}$ to homomorphisms of $\operatorname{N}$ applied to $s$ and the length in the opposite of $\operatorname{fst}$ applied to $A$ and $Z$. Then $\operatorname{desc}$ applied to $s$, $x_{1}$, $A$ and $F$ is a homomorphism of the action of $X$ and $x_{1}$ and $Z$ defined as the function that maps $F$ to $\operatorname{desc}$ applied to $\operatorname{isColimit}$ applied to $s$ and $x_{1}$, $A$ and $F$.

Let $s$ be a splitting of $X$. Let $x_{1}$ be an opposite of the set of simplex categories. Then $\operatorname{isColimit}$ applied to $s$ and $x_{1}$ is an element of $\operatorname{IsColimit}$ applied to the cofan of $s$ and $x_{1}$ defined as $\operatorname{isColimit'}$ applied to $s$ and $x_{1}$.

Let $\mathrm{self}$ be a splitting of $X$. Let $x_{1}$ be an opposite of the set of simplex categories. Then $\operatorname{isColimit'}$ applied to $\mathrm{self}$ and $x_{1}$ is an element of $\operatorname{IsColimit}$ applied to the cofan of $\mathrm{CategoryTheory\_\_SimplicialObject\_\_Splitting\_\_\_u3b9\_}$ applied to $\mathrm{self}$ and $x_{1}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{1}$.

the map of s and F (from the name)

Let $s$ be a splitting of $X$. Let $F$ be a functor of $C$ and $D$. Then the map of $s$ and $F$ is a splitting of the composition of $X$ and $F$.

the splitting of s and e (from the name)

Let $s$ be a splitting of $X$. Let $e$ be an isomorphism of $X$ and $Y$. Then the splitting of $s$ and $e$ is a splitting of $Y$.

the summand of x and A (from the name)

Let $N$ be a function from natural numbers to elements of $C$. Let $x$ be an opposite of the set of simplex categories. Let $A$ be an index set of $x$. Then the summand of $x$ and $A$ is an element of $C$ defined as $N$ applied to the length in the opposite of $\operatorname{fst}$ applied to $A$.

the inclusion of self and n (from the name)

Let $\mathrm{self}$ be a splitting of $X$. Let $n$ be a natural number. Then the inclusion of $\mathrm{self}$ and $n$ is a homomorphism of $\operatorname{N}$ applied to $\mathrm{self}$ and $n$ and the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $n$.

Let $s$ be a splitting of $X$. Let $f$ be a homomorphism of $X$ and $Y$. Let $n$ be a natural number. Then $\mathrm{CategoryTheory\_\_SimplicialObject\_\_Splitting\_\_\_u3c6\_}$ applied to $s$, $f$ and $n$ is a homomorphism of $\operatorname{N}$ applied to $s$ and $n$ and the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ defined as the composition of the inclusion of $s$ and $n$ and the component of $f$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$.

the anodyne extension (from the name)

The anodyne extension is a morphism property of the set of sets defined as $\operatorname{llp}$ applied to the fibration of the set of sets.

the strong anodyne extension (from the name)

The strong anodyne extension is a morphism property of the set of sets defined as the function that maps $x$, $x_{1}$ and $f$ to the proposition that $f$ is a monomorphism and there exists a pairing $P$ of the range of $f$ such that $P$ is regular.

the inner anodyne extension (from the name)

The inner anodyne extension is a morphism property of the set of sets defined as $\operatorname{llp}$ applied to the inner fibration.

the strong inner anodyne extension (from the name)

The strong inner anodyne extension is a morphism property of the set of sets defined as the function that maps $x$, $x_{1}$ and $f$ to the proposition that $f$ is a monomorphism and there exists a pairing $P$ of the range of $f$ such that there exists an element $h$ of $\operatorname{IsRegular}$ applied to $P$ such that $P$ is inner.

Let $x$ and $y$ be elements of $\operatorname{S}$ applied to $X$. Then $\operatorname{IsUniquelyCodimOneFace}$ holds for $x$ and $y$, if the dimension of the simplex of $y$ is equal to the sum of the dimension of the simplex of $x$ and $1$ and $\mathrm{ExistsUnique}$ holds for the function that maps $f$ to the proposition that $f$ is a monomorphism and $\operatorname{hom}$ applied to the map of $X$ and the opposite in $f$ and the simplex of $y$ is equal to the simplex of $x$.

the index of hxy and hd (from the name)

Assume that $\operatorname{IsUniquelyCodimOneFace}$ holds for $x$ and $y$. Assume that the dimension of the simplex of $x$ is equal to $d$. Then the index of $\mathrm{hxy}$ and $\mathrm{hd}$ is an element of $\mathrm{Fin}$ applied to $d + 2$.

the opposite of P (from the name)

Let $P$ be a pairing of $A$. Then the opposite of $P$ is a pairing of the opposite of $A$.

pairing of A (from the name)

Let $A$ be a subcomplex of $X$. Then the pairings of $A$ are a basic type.

Let $P$ be a pairing of $A$. Let $x$ and $y$ be elements of $\operatorname{II}$ applied to $P$. Then $\operatorname{AncestralRel}$ holds for $P$, $x$ and $y$, if $x \neq y$ and $x < \operatorname{p} (P , y)$.

Let $\mathrm{self}$ be a pairing of $A$. Then $\operatorname{I}$ applied to $\mathrm{self}$ is an element of $\wp \operatorname{N} (A)$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a pairing of $A$. Then $\operatorname{II}$ applied to $\mathrm{self}$ is an element of $\wp \operatorname{N} (A)$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

P is inner (from the name)

Let $P$ be a pairing of $A$. Then we can say that $P$ is inner.

P is proper (from the name)

Let $P$ be a pairing of $A$. Then we can say that $P$ is proper.

P is regular (from the name)

Let $P$ be a pairing of $A$. Then we can say that $P$ is regular.

the pairing of P and e (from the name)

Let $P$ be a pairing of $A$. Let $e$ be an isomorphism of $Y$ and $X$ such that the preimage of $A$ and the homomorphism of $e$ is equal to $B$. Then the pairing of $P$ and $e$ is a pairing of $B$.

Let $\mathrm{self}$ be a pairing of $A$. Then $\operatorname{p}$ applied to $\mathrm{self}$ is an equivalence from the set of elements of $\operatorname{II}$ applied to $\mathrm{self}$ to the set of elements of $\operatorname{I}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

the pairing of P (from the name)

Let $P$ be a pairing of $A$. Then the pairing of $P$ is a pairing of $A$.

pairing of A (from the name)

Let $A$ be a subcomplex of $X$. Then the pairings of $A$ are a basic type.

Let $h$ be a pairing of $A$. Let $s$ and $t$ be inclusions of $h$. Then $\operatorname{AncestralRel}$ holds for $h$, $s$ and $t$, if $s \neq t$ and the type of $h$ and $s$ is less than the type of $h$ and $t$.

Let $h$ be a pairing of $A$. Then $\operatorname{I}$ applied to $h$ is an element of $\wp \operatorname{N} (A)$ defined as the range of $\mathrm{SSet\_\_Subcomplex\_\_PairingCore\_\_type\_u2081\_}$ applied to $h$.

Let $h$ be a pairing of $A$. Then $\operatorname{II}$ applied to $h$ is an element of $\wp \operatorname{N} (A)$ defined as the range of $\mathrm{SSet\_\_Subcomplex\_\_PairingCore\_\_type\_u2082\_}$ applied to $h$.

h is inner (from the name)

Let $h$ be a pairing of $A$. Then we can say that $h$ is inner.

h is proper (from the name)

Let $h$ be a pairing of $A$. Then we can say that $h$ is proper.

h is regular (from the name)

Let $h$ be a pairing of $A$. Then we can say that $h$ is regular.

the dimension of self and s (from the name)

Let $\mathrm{self}$ be a pairing of $A$. Let $s$ be an inclusion of $\mathrm{self}$. Then the dimension of $\mathrm{self}$ and $s$ is a natural number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $s$.

the equivalence of h (from the name)

Let $h$ be a pairing of $A$. Then the equivalence of $h$ is an equivalence from the set of inclusions of $h$ to the set of elements of $\operatorname{I}$ applied to $h$ defined as the equivalence of $\mathrm{SSet\_\_Subcomplex\_\_PairingCore\_\_type\_u2081\_}$ applied to $h$ and $\mathrm{SSet\_\_Subcomplex\_\_PairingCore\_\_injective\_type\_u2081\_}$ applied to $h$.

Let $h$ be a pairing of $A$. Then $\operatorname{equivII}$ applied to $h$ is an equivalence from the set of inclusions of $h$ to the set of elements of $\operatorname{II}$ applied to $h$ defined as the equivalence of $\mathrm{SSet\_\_Subcomplex\_\_PairingCore\_\_type\_u2082\_}$ applied to $h$ and $\mathrm{SSet\_\_Subcomplex\_\_PairingCore\_\_injective\_type\_u2082\_}$ applied to $h$.

the index of self and s (from the name)

Let $\mathrm{self}$ be a pairing of $A$. Let $s$ be an inclusion of $\mathrm{self}$. Then the index of $\mathrm{self}$ and $s$ is an element of $\mathrm{Fin}$ applied to the sum of the dimension of $\mathrm{self}$ and $s$ and $2$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $s$.

the pairing of h (from the name)

Let $h$ be a pairing of $A$. Then the pairing of $h$ is a pairing of $A$.

the simplex of self and s (from the name)

Let $\mathrm{self}$ be a pairing of $A$. Let $s$ be an inclusion of $\mathrm{self}$. Then the simplex of $\mathrm{self}$ and $s$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to the sum of the dimension of $\mathrm{self}$ and $s$ and $1$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $s$.

the type of h and s (from the name)

Let $h$ be a pairing of $A$. Let $s$ be an inclusion of $h$. Then the type of $h$ and $s$ is an element of $\operatorname{N}$ applied to $A$ defined as $\operatorname{mk}$ applied to the simplex of $h$ and $s$, $\mathrm{SSet\_\_Subcomplex\_\_PairingCore\_\_nonDegenerate\_u2081\_}$ applied to $h$ and $s$ and $\mathrm{SSet\_\_Subcomplex\_\_PairingCore\_\_notMem\_u2081\_}$ applied to $h$ and $s$.

the type of h and s (from the name)

Let $h$ be a pairing of $A$. Let $s$ be an inclusion of $h$. Then the type of $h$ and $s$ is an element of $\operatorname{N}$ applied to $A$ defined as $\operatorname{mk}$ applied to $\operatorname{hom}$ applied to $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_}$ applied to $X$ and the index of $h$ and $s$ and the simplex of $h$ and $s$, $\mathrm{SSet\_\_Subcomplex\_\_PairingCore\_\_nonDegenerate\_u2082\_}$ applied to $h$ and $s$ and $\mathrm{SSet\_\_Subcomplex\_\_PairingCore\_\_notMem\_u2082\_}$ applied to $h$ and $s$.

inclusion of self (from the name)

Let $\mathrm{self}$ be a pairing of $A$. Then an inclusion of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

rank function of P and x (from the name)

Let $P$ be a pairing of $A$. Let $x$ be a set. Then the rank functions of $P$ and $x$ are a basic type.

the rank function of self and x2 (from the docstring)

Let $\mathrm{self}$ be a rank function of $P$ and $x$. Let $x_{2}$ be an element of $\operatorname{II}$ applied to $P$. Then the rank function of $\mathrm{self}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

the weak rank function of P and f (from the name)

Let $P$ be a pairing of $A$. Let $x$ be a set. Let $f$ be a rank function of $P$ and $x$. Then the weak rank function of $P$ and $f$ is a weak rank function of $P$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{rank}$ applied to $f$ and the function that maps $x_{2}$, $x_{3}$, $h$ and $h_{1}$ to $\operatorname{lt}$ applied to $f$ and $h$.

weak rank function of P and x (from the name)

Let $P$ be a pairing of $A$. Let $x$ be a set. Then the weak rank functions of $P$ and $x$ are a basic type.

the rank of self and x2 (from the name)

Let $\mathrm{self}$ be a weak rank function of $P$ and $x$. Let $x_{2}$ be an element of $\operatorname{II}$ applied to $P$. Then the rank of $\mathrm{self}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

rank function of h and x (from the name)

Let $h$ be a pairing of $A$. Let $x$ be a set. Then the rank functions of $h$ and $x$ are a basic type.

the rank function of self and x2 (from the docstring)

Let $\mathrm{self}$ be a rank function of $h$ and $x$. Let $x_{2}$ be an inclusion of $h$. Then the rank function of $\mathrm{self}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

weak rank function of h and x (from the name)

Let $h$ be a pairing of $A$. Let $x$ be a set. Then the weak rank functions of $h$ and $x$ are a basic type.

the rank of self and x2 (from the name)

Let $\mathrm{self}$ be a weak rank function of $h$ and $x$. Let $x_{2}$ be an inclusion of $h$. Then the rank of $\mathrm{self}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

the rank function equivalence of h and x (from the name)

Let $h$ be a pairing of $A$. Let $x$ be a set. Then the rank function equivalence of $h$ and $x$ is an equivalence from the set of rank functions of $h$ and $x$ to the set of rank functions of the pairing of $h$ and $x$.

the weak rank function equivalence of h and x (from the name)

Let $h$ be a pairing of $A$. Let $x$ be a set. Then the weak rank function equivalence of $h$ and $x$ is an equivalence from the set of weak rank functions of $h$ and $x$ to the set of weak rank functions of the pairing of $h$ and $x$.

the rank of P and x (from the name)

Let $P$ be a pairing of $A$. Let $x$ be an element of $\operatorname{II}$ applied to $P$. Then the rank of $P$ and $x$ is a natural number.

the rank function of P (from the name)

Let $P$ be a pairing of $A$. Then the rank function of $P$ is a rank function of $P$ and $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{rank}$ applied to $P$ and the function that maps $x$ and $x_{1}$ to $\mathrm{SSet\_\_Subcomplex\_\_Pairing\_\_rank\_lt}$.

cell of f and i (from the name)

Let $f$ be a rank function of $P$ and $x$. Let $i$ be an element of $x$. Then the cells of $f$ and $i$ are a basic type.

the dimension of c (from the docstring)

Let $c$ be a cell of $f$ and $i$. Then the dimension of $c$ is a natural number defined as the dimension of the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to $\operatorname{s}$ applied to $c$.

the horn in the standard simplex corresponding to a cell of c (from the docstring)

Let $c$ be a cell of $f$ and $i$. Then the horn in the standard simplex corresponding to a cell of $c$ is a subcomplex of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to the sum of the dimension of $c$ and $1$ defined as the horn of the sum of the dimension of $c$ and $1$ and the index of $c$.

the index of c (from the name)

Let $c$ be a cell of $f$ and $i$. Then the index of $c$ is an element of $\mathrm{Fin}$ applied to the sum of the dimension of $c$ and $2$.

the map of c (from the name)

Let $c$ be a cell of $f$ and $i$. Then the map of $c$ is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to the sum of the dimension of $c$ and $1$ and $X$.

the map horn of f and c (from the name)

Let $f$ be a rank function of $P$ and $x$. Let $c$ be a cell of $f$ and $j$. Then the map horn of $f$ and $c$ is a homomorphism of the underlying simplicial set of the horn in the standard simplex corresponding to a cell of $c$ and the underlying simplicial set of the filtration of $f$ and $j$.

the map to successor of c (from the name)

Let $c$ be a cell of $f$ and $j$. Then the map to successor of $c$ is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to the sum of the dimension of $c$ and $1$ and the underlying simplicial set of the filtration of $f$ and the successor of $j$.

Let $\mathrm{self}$ be a cell of $f$ and $i$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is an element of $\operatorname{II}$ applied to $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the type of f and c (from the name)

Let $f$ be a rank function of $P$ and $x$. Let $c$ be a cell of $f$ and $j$. Then the type of $f$ and $c$ is an element of $\operatorname{N}$ applied to the range of $\operatorname{m}$ applied to $f$ and $j$.

the type of f and c (from the name)

Let $f$ be a rank function of $P$ and $x$. Let $c$ be a cell of $f$ and $j$. Then the type of $f$ and $c$ is an element of $\operatorname{N}$ applied to the range of $\operatorname{m}$ applied to $f$ and $j$.

the inclusion sigma horn of c (from the name)

Let $c$ be a cell of $f$ and $j$. Then the inclusion sigma horn of $c$ is a homomorphism of the underlying simplicial set of the horn in the standard simplex corresponding to a cell of $c$ and the sigma horn of $f$ and $j$ defined as the inclusion of the function that maps $c_{1}$ to the underlying simplicial set of the horn in the standard simplex corresponding to a cell of $c_{1}$ and $c$.

Let $c$ be a cell of $f$ and $j$. Then $\mathrm{SSet\_\_Subcomplex\_\_Pairing\_\_RankFunction\_\_Cell\_\_\_u3b9\_SigmaStdSimplex}$ applied to $c$ is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to the sum of the dimension of $c$ and $1$ and $\operatorname{sigmaStdSimplex}$ applied to $f$ and $j$ defined as the inclusion of the function that maps $c_{1}$ to the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to the sum of the dimension of $c_{1}$ and $1$ and $c$.

Let $f$ be a rank function of $P$ and $x$. Let $j$ be an element of $x$. Then $\operatorname{b}$ applied to $f$ and $j$ is a homomorphism of $\operatorname{sigmaStdSimplex}$ applied to $f$ and $j$ and the underlying simplicial set of the filtration of $f$ and the successor of $j$ defined as $\operatorname{desc}$ applied to the function that maps $c$ to the map to successor of $c$.

Let $f$ be a rank function of $P$ and $x$. Let $i$ be an element of $x$. Let $c$ be a cell of $f$ and $i$. Then $\operatorname{basicCell}$ applied to $f$, $i$ and $c$ is a homomorphism of the underlying simplicial set of the horn in the standard simplex corresponding to a cell of $c$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to the sum of the dimension of $c$ and $1$ defined as the inclusion of the horn in the standard simplex corresponding to a cell of $c$.

the filtration of f and i (from the docstring)

Let $f$ be a rank function of $P$ and $x$. Let $i$ be an element of $x$. Then the filtration of $f$ and $i$ is a subcomplex of $X$ defined as the maximum of $A$ and the supremum of the function that maps $j$ to the supremum of the function that maps $h$ to the supremum of the function that maps $c$ to the subcomplex generated by a simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to $\operatorname{p}$ applied to $P$ and $\operatorname{s}$ applied to $c$.

Let $f$ be a rank function of $P$ and $x$. Let $j$ be an element of $x$. Then $\operatorname{m}$ applied to $f$ and $j$ is a homomorphism of the sigma horn of $f$ and $j$ and $\operatorname{sigmaStdSimplex}$ applied to $f$ and $j$ defined as the map of $\operatorname{basicCell}$ applied to $f$ and $j$.

the map of f and x3 (from the name)

Let $f$ be a rank function of $P$ and $x$. Let $x_{3}$ be an element of $\operatorname{N}$ applied to the range of $\operatorname{m}$ applied to $f$ and $j$. Then the map of $f$ and $x_{3}$ is an element of $\operatorname{S}$ applied to $X$ defined as $\operatorname{mk}$ applied to $\operatorname{hom}$ applied to the component of $\operatorname{b}$ applied to $f$ and $j$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to the dimension of the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to $x_{3}$ and the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to $x_{3}$.

the relative cell complex of f (from the name)

Let $f$ be a rank function of $P$ and $x$. Then the relative cell complex of $f$ is a relative cell complex of $\operatorname{basicCell}$ applied to $f$ and the inclusion of $A$.

the sigma horn of f and j (from the name)

Let $f$ be a rank function of $P$ and $x$. Let $j$ be an element of $x$. Then the sigma horn of $f$ and $j$ is a set defined as the sigma object of the function that maps $c$ to the underlying simplicial set of the horn in the standard simplex corresponding to a cell of $c$.

Let $f$ be a rank function of $P$ and $x$. Let $j$ be an element of $x$. Then $\operatorname{sigmaStdSimplex}$ applied to $f$ and $j$ is a set defined as the sigma object of the function that maps $i$ to the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to the sum of the dimension of $i$ and $1$.

Let $f$ be a rank function of $P$ and $x$. Let $j$ be an element of $x$. Then $\operatorname{t}$ applied to $f$ and $j$ is a homomorphism of the sigma horn of $f$ and $j$ and the underlying simplicial set of the filtration of $f$ and $j$ defined as $\operatorname{desc}$ applied to the function that maps $c$ to the map horn of $f$ and $c$.

the pairing of k and n (from the name)

Let $k$ be an element of $\mathrm{Fin}$ applied to $m + 2$. Let $n$ be a natural number. Then the pairing of $k$ and $n$ is a pairing of the union product of the horn of $m + 1$ and $k$ and the boundary of $n$.

the pairing of k and n (from the name)

Let $k$ be an element of $\mathrm{Fin}$ applied to $m + 1$. Let $n$ be a natural number. Then the pairing of $k$ and $n$ is a pairing of the union product of the horn of $m + 1$ and $\operatorname{castSucc}$ applied to $k$ and the boundary of $n$.

Let $x$ be an element of $\operatorname{N}$ applied to the union product of the horn of $m + 1$ and $\operatorname{castSucc}$ applied to $k$ and the boundary of $n$ such that the dimension of the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to $x$ is equal to $d$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $d + 1$. Then $\operatorname{IsIndex}$ holds for $x$, $\mathrm{hd}$ and $x_{1}$, if $\operatorname{cases}$ holds for the proposition that we have a contradiction, the function that maps $l$ to the proposition that $\operatorname{fst}$ applied to the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to the cast of $x$ and $\mathrm{hd}$ and $\operatorname{castSucc}$ applied to $l$ is equal to $\operatorname{castSucc}$ applied to $k$, $\operatorname{fst}$ applied to the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to the cast of $x$ and $\mathrm{hd}$ and $\operatorname{succ}$ applied to $l$ is equal to $\operatorname{succ}$ applied to $k$ and $\operatorname{snd}$ applied to the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to the cast of $x$ and $\mathrm{hd}$ and $\operatorname{succ}$ applied to $l$ is equal to $\operatorname{snd}$ applied to the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to the cast of $x$ and $\mathrm{hd}$ and $\operatorname{castSucc}$ applied to $l$ and $x_{1}$.

the type of h (from the name)

Assume that $\operatorname{IsIndex}$ holds for $x$, $\mathrm{hd}$ and $\operatorname{succ}$ applied to $i$. Then the type of $h$ is a type of $k$ and $n$ defined as $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_Type\_u2081\_\_\_mk}$ applied to $x$, $d$, $\mathrm{hd}$, $i$ and $h$.

Assume that $\operatorname{IsIndex}$ holds for $x$, $\mathrm{hd}$ and $\operatorname{succ}$ applied to $l$. Then $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_IsIndex\_\_\_u3b4\_}$ applied to $\mathrm{hl}$ is an element of $\operatorname{N}$ applied to the union product of the horn of $m + 1$ and $\operatorname{castSucc}$ applied to $k$ and the boundary of $n$.

x is a type (from the name)

Let $x$ be an element of $\operatorname{N}$ applied to the union product of the horn of $m + 1$ and $\operatorname{castSucc}$ applied to $k$ and the boundary of $n$. Then $x$ is a type, if for all natural numbers $d$, for all elements $\mathrm{hd}$ of $\mathrm{Proof}$ applied to the proposition that the dimension of the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to $x$ is equal to $d$, for all elements $l$ of $\mathrm{Fin}$ applied to $d + 1$, it is not the case that $\operatorname{IsIndex}$ holds for $x$, $\mathrm{hd}$ and $l$.

the simplex of hx and hd (from the name)

Assume that $x$ is a type. Assume that the dimension of the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to $x$ is equal to $d$. Then the simplex of $\mathrm{hx}$ and $\mathrm{hd}$ is an element of the action of the tensor object of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $m + 1$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $d + 1$.

the type of hx and hd (from the name)

Assume that $x$ is a type. Assume that the dimension of the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to $x$ is equal to $d$. Then the type of $\mathrm{hx}$ and $\mathrm{hd}$ is a type of $k$ and $n$.

type of k and n (from the name)

Let $k$ be an element of $\mathrm{Fin}$ applied to $m + 1$. Let $n$ be a natural number. Then the types of $k$ and $n$ are a basic type.

Let $\mathrm{self}$ be a type of $k$ and $n$. Then $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_Type\_u2081\_\_\_d}$ applied to $\mathrm{self}$ is a natural number defined as $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_Type\_u2081\_\_\_proj1}$ applied to $\mathrm{self}$.

the index of self (from the name)

Let $\mathrm{self}$ be a type of $k$ and $n$. Then the index of $\mathrm{self}$ is an element of $\mathrm{Fin}$ applied to $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_Type\_u2081\_\_\_d} (\mathrm{self})+ 1$ defined as $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_Type\_u2081\_\_\_proj3}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a type of $k$ and $n$. Then $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_Type\_u2081\_\_\_x}$ applied to $\mathrm{self}$ is an element of $\operatorname{N}$ applied to the union product of the horn of $m + 1$ and $\operatorname{castSucc}$ applied to $k$ and the boundary of $n$ defined as $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_Type\_u2081\_\_\_proj0}$ applied to $\mathrm{self}$.

Let $s$ be a type of $k$ and $n$. Then $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_Type\_u2081\_\_\_\_u3b4\_}$ applied to $s$ is an element of $\operatorname{N}$ applied to the union product of the horn of $m + 1$ and $\operatorname{castSucc}$ applied to $k$ and the boundary of $n$ defined as $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_IsIndex\_\_\_u3b4\_}$ applied to $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_Type\_u2081\_\_\_isIndex}$ applied to $s$.

the finite set of x and hd (from the name)

Let $x$ be an element of $\operatorname{N}$ applied to the union product of the horn of $m + 1$ and $\operatorname{castSucc}$ applied to $k$ and the boundary of $n$ such that $\operatorname{dim} (\operatorname{toS} (\operatorname{toN} (x)))= d$. Then the finite set of $x$ and $\mathrm{hd}$ is a finite set of $\mathrm{Fin}$ applied to $d + 1$ defined as $\FinsetFilter {l}{(\EqtMACRoH {\operatorname{fst} (\operatorname{simplex} (\operatorname{toS} (\operatorname{toN} (\operatorname{cast} (x , \mathrm{hd})))), l)}{\operatorname{succ} (k)})}{\FinsetunivMACRoAC}$.

the minimum of x and hd (from the name)

Let $x$ be an element of $\operatorname{N}$ applied to the union product of the horn of $m + 1$ and $\operatorname{castSucc}$ applied to $k$ and the boundary of $n$ such that the dimension of the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to $x$ is equal to $d$. Then the minimum of $x$ and $\mathrm{hd}$ is an element of $\mathrm{Fin}$ applied to $d + 1$ defined as the minimum of the finite set of $x$ and $\mathrm{hd}$ and $\mathrm{SSet\_\_prodStdSimplex\_\_pairingCore\_\_nonempty\_finset}$ applied to $x$ and $\mathrm{hd}$.

the weak rank function of k and n (from the name)

Let $k$ be an element of $\mathrm{Fin}$ applied to $m + 1$. Let $n$ be a natural number. Then the weak rank function of $k$ and $n$ is a weak rank function of the pairing of $k$ and $n$ and $\Natural$.

set (from the name)

A set is a simplicial object of the set of sets.

An element of $\operatorname{Augmented}$ is an element of $\operatorname{Augmented}$ applied to the set of sets.

Let $n$ be a natural number. Then an element of $\operatorname{Truncated}$ applied to $n$ is an element of the function that maps $n$ to $\operatorname{Truncated}$ applied to the set of sets and $n$.

Let $n$ be a natural number. Then $\operatorname{cosk}$ applied to $n$ is a functor of $\operatorname{Truncated}$ applied to $n$ and the set of sets defined as $\operatorname{cosk}$ applied to $n$.

Let $n$ be a natural number. Then $\operatorname{fullyFaithful}$ applied to $n$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{cosk}$ applied to $n$ defined as $\operatorname{fullyFaithful}$ applied to $n$.

Let $n$ be a natural number. Then $\operatorname{sk}$ applied to $n$ is a functor of $\operatorname{Truncated}$ applied to $n$ and the set of sets defined as $\operatorname{sk}$ applied to $n$.

Let $n$ be a natural number. Then $\operatorname{fullyFaithful}$ applied to $n$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{sk}$ applied to $n$ defined as $\operatorname{fullyFaithful}$ applied to $n$.

the truncation of n and m (from the name)

Let $n$ and $m$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (m , n)$ and $\mathrm{SSet\_\_Truncated\_\_trunc\_\_\_auto\_1}$. Then the truncation of $n$ and $m$ is a functor of $\operatorname{Truncated}$ applied to $n$ and $\operatorname{Truncated}$ applied to $m$.

the lift functor of k (from the name)

Let $k$ be a natural number. Then the lift functor of $k$ is a functor of $\operatorname{Truncated}$ applied to $k$ and $\operatorname{Truncated}$ applied to $k$ defined as the action of the right whiskering of the set of sets and the set of sets and the functor embedding.

the constant of y (from the name)

Let $y$ be an element of the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$. Then the constant of $y$ is a homomorphism of $X$ and $Y$.

Let $n$ be a natural number. Then $\operatorname{cosk}$ applied to $n$ is a functor of the set of sets and the set of sets defined as $\operatorname{cosk}$ applied to $n$.

Let $n$ be a natural number. Then $\operatorname{coskAdj}$ applied to $n$ is an adjunction of the truncation of $n$ and $\operatorname{cosk}$ applied to $n$ defined as $\operatorname{coskAdj}$ applied to $n$.

the evaluation (from the name)

The evaluation is a functor of the set of opposites of the set of simplex categories and the set of functors of the set of sets and the set of sets defined as the evaluation of the set of opposites of the set of simplex categories and the set of sets.

Let $n$ be a natural number. Then $\operatorname{sk}$ applied to $n$ is a functor of the set of sets and the set of sets defined as $\operatorname{sk}$ applied to $n$.

Let $n$ be a natural number. Then $\operatorname{skAdj}$ applied to $n$ is an adjunction of $\operatorname{sk}$ applied to $n$ and the truncation of $n$ defined as $\operatorname{skAdj}$ applied to $n$.

the truncation of n (from the name)

Let $n$ be a natural number. Then the truncation of $n$ is a functor of the set of sets and $\operatorname{Truncated}$ applied to $n$ defined as the truncation of $n$.

the truncation composition truncation of h (from the name)

Assume that $m \leq n$. Then the truncation composition truncation of $h$ is an isomorphism of the composition of the truncation of $n$ and the truncation of $n$ and $m$ and the truncation of $m$.

the lift functor (from the name)

The lift functor is a functor of the set of sets and the set of sets defined as the action of the whiskering of the set of sets and the set of sets and the functor embedding.

the boundary of n (from the docstring)

Let $n$ be a natural number. Then the boundary of $n$ is a subcomplex of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$.

the inclusion of i (from the docstring)

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the inclusion of $i$ is a homomorphism of the underlying simplicial set of the face of the complement of $\operatorname{singleton}$ applied to $i$ and the underlying simplicial set of the boundary of $n$ defined as the homomorphism of $\mathrm{SSet\_\_face\_singleton\_compl\_le\_boundary}$ applied to $i$.

the inclusion of i (from the name)

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then the inclusion of $i$ is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and the underlying simplicial set of the boundary of $n + 1$.

the lift of p and b (from the name)

Assume that $f$ is compatible. Let $p$ be a homomorphism of $X$ and $Y$. Let $b$ be a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n + 1$ and $Y$ such that for all elements $j$ of $\mathrm{Fin}$ applied to $n + 2$, for all elements $\mathrm{hj}$ of $\mathrm{Proof}$ applied to $\mathrm{Neq} (j , i)$, the composition of $f$ applied to $j$ and $\mathrm{hj}$ and $p$ is equal to the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $j$ and $b$. Then the lift of $p$ and $b$ is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n + 1$ and $X$ defined as $\operatorname{choose}$ applied to $\mathrm{SSet\_\_horn\_\_IsCompatible\_\_exists\_lift}$ applied to $\mathrm{hf}$, $p$, $b$ and $\mathrm{comm}$.

There is a morphism property of the set of sets. Proof. Let $n$ be arbitrary. By n. By SSet__boundary. By SSet__Subcomplex___u3b9_. By CategoryTheory__MorphismProperty__ofHoms.

There is a morphism property of the set of sets. Proof. Let $n$ be arbitrary. Let $i$ be arbitrary. By n. By 1. By plus. By i. By SSet__horn. By SSet__Subcomplex___u3b9_. By CategoryTheory__MorphismProperty__ofHoms. By iSup.