Definitions: Mathlib.AlgebraicTopology, part 4 of 4

the relative cell complex of X (from the name)

Let $X$ be a set. Then the relative cell complex of $X$ is a relative cell complex of the function that maps $n$ and $x$ to the inclusion of the boundary of $n$ and the inclusion of the bottom defined as the relative cell complex of the inclusion of the bottom.

the relative cell complex cell equivalence (from the name)

The relative cell complex cell equivalence is an equivalence from the set of cells of the relative cell complex of $X$ to $\operatorname{N}$ applied to $X$.

the relative cell complex of i (from the name)

Let $i$ be a homomorphism of $X$ and $Y$. Then the relative cell complex of $i$ is a relative cell complex of the function that maps $n$ and $x$ to the inclusion of the boundary of $n$ and $i$.

cell of i and d (from the name)

Let $i$ be a homomorphism of $X$ and $Y$. Let $d$ be a natural number. Then the cells of $i$ and $d$ are a basic type.

the map of c (from the name)

Let $c$ be a cell of $i$ and $d$. Then the map of $c$ is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $d$ and $Y$ defined as $\operatorname{symm}$ applied to the Yoneda equivalence and the simplex of $c$.

the simplex of self (from the name)

Let $\mathrm{self}$ be a cell of $i$ and $d$. Then the simplex of $\mathrm{self}$ is an element of the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $d$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the inclusion sigma boundary of c (from the name)

Let $c$ be a cell of $i$ and $d$. Then the inclusion sigma boundary of $c$ is a homomorphism of the underlying simplicial set of the boundary of $d$ and the sigma boundary of $i$ and $d$ defined as the inclusion of the function that maps $x$ to the underlying simplicial set of the boundary of $d$ and $c$.

Let $c$ be a cell of $i$ and $d$. Then $\mathrm{SSet\_\_relativeCellComplexOfMono\_\_Cell\_\_\_u3b9\_SigmaStdSimplex}$ applied to $c$ is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $d$ and $\operatorname{sigmaStdSimplex}$ applied to $i$ and $d$ defined as the inclusion of the function that maps $x$ to the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $d$ and $c$.

Let $i$ be a homomorphism of $X$ and $Y$. Let $d$ be a natural number. Then $\operatorname{b}$ applied to $i$ and $d$ is a homomorphism of $\operatorname{sigmaStdSimplex}$ applied to $i$ and $d$ and the underlying simplicial set of $\operatorname{skeletonOfMono}$ applied to $i$ and $d + 1$ defined as $\operatorname{desc}$ applied to the function that maps $c$ to the lift of the map of $c$ and $\mathrm{SSet\_\_relativeCellComplexOfMono\_\_Cell\_\_range\_map\_le}$ applied to $c$.

Let $i$ be a homomorphism of $X$ and $Y$. Let $d$ be a natural number. Then $\operatorname{l}$ applied to $i$ and $d$ is a homomorphism of the sigma boundary of $i$ and $d$ and $\operatorname{sigmaStdSimplex}$ applied to $i$ and $d$ defined as the map of the function that maps $x$ to the inclusion of the boundary of $d$.

Let $i$ be a homomorphism of $X$ and $Y$. Let $d$ be a natural number. Then $\operatorname{r}$ applied to $i$ and $d$ is a homomorphism of the underlying simplicial set of $\operatorname{skeletonOfMono}$ applied to $i$ and $d$ and the underlying simplicial set of $\operatorname{skeletonOfMono}$ applied to $i$ and $d + 1$.

the sigma boundary of i and d (from the name)

Let $i$ be a homomorphism of $X$ and $Y$. Let $d$ be a natural number. Then the sigma boundary of $i$ and $d$ is a set defined as the sigma object of the function that maps $x$ to the underlying simplicial set of the boundary of $d$.

Let $i$ be a homomorphism of $X$ and $Y$. Let $d$ be a natural number. Then $\operatorname{sigmaStdSimplex}$ applied to $i$ and $d$ is a set defined as the sigma object of the function that maps $x$ to the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $d$.

Let $i$ be a homomorphism of $X$ and $Y$. Let $d$ be a natural number. Then $\operatorname{t}$ applied to $i$ and $d$ is a homomorphism of the sigma boundary of $i$ and $d$ and the underlying simplicial set of $\operatorname{skeletonOfMono}$ applied to $i$ and $d$.

the skeleton of X (from the name)

Let $X$ be a set. Then the skeleton of $X$ is an order homomorphism of $\Natural$ and the set of subcomplexes of $X$.

the skeleton of i (from the docstring)

Let $i$ be a homomorphism of $X$ and $Y$. Then the skeleton of $i$ is an order homomorphism of $\Natural$ and the set of subcomplexes of $Y$.

the canonical splitting of X (from the docstring)

Let $X$ be a set. Then the canonical splitting of $X$ is a splitting of $X$.

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

$\operatorname{S1}$ is a set defined as the colimit of the parallel pair of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $0$ and $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $1$.

the simplex of x (from the name)

Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$. Then the simplex of $x$ is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and the underlying simplicial set of the subcomplex of $x$.

$\operatorname{stdSimplex}$ is a cosimplicial object of the set of sets defined as the lift Yoneda.

Let $x$ be an element of the action of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and $m$. Then $\operatorname{asOrderHom}$ applied to $x$ is an order homomorphism of $\mathrm{Fin}$ applied to the sum of the length in the opposite of $m$ and $1$ and $\mathrm{Fin}$ applied to $n + 1$ defined as the order homomorphism of $\operatorname{down}$ applied to $x$.

the constant of k and m (from the name)

Let $n$ be a natural number. Let $k$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $m$ be an opposite of the set of simplex categories. Then the constant of $k$ and $m$ is an element of the action of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and $m$ defined as the object of $\operatorname{const}$ applied to $\mathrm{Fin}$ applied to the sum of the length in the opposite of $m$ and $1$ and $k$.

the edge of a and b (from the name)

Let $n$ be a natural number. Let $a$ and $b$ be elements of $\mathrm{Fin}$ applied to $n + 1$ such that $a \leq b$. Then the edge of $a$ and $b$ is an element of the action of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$.

the face of S (from the name)

Let $S$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Then the face of $S$ is a subcomplex of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$.

the face pair complement isomorphism of i and j (from the name)

Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $n + 3$ such that $i < j$. Then the face pair complement isomorphism of $i$ and $j$ is an isomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and the underlying simplicial set of the face of the complement of $\operatorname{insert}$ applied to $i$ and $\operatorname{singleton}$ applied to $j$ defined as the isomorphism of $\operatorname{faceRepresentableBy}$ applied to the complement of $\operatorname{insert}$ applied to $i$ and $\operatorname{singleton}$ applied to $j$, $n$ and the finite order isomorphism pair complement of $i$ and $j$.

the face pair isomorphism of i and j (from the name)

Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $n + 1$ such that $i < j$. Then the face pair isomorphism of $i$ and $j$ is an isomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and the underlying simplicial set of the face of $\operatorname{insert}$ applied to $i$ and $\operatorname{singleton}$ applied to $j$ defined as the isomorphism of $\operatorname{faceRepresentableBy}$ applied to $\operatorname{insert}$ applied to $i$ and $\operatorname{singleton}$ applied to $j$, $1$ and the order isomorphism pair of $i$ and $j$.

Let $S$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Let $m$ be a natural number. Let $e$ be an order isomorphism of $\mathrm{Fin}$ applied to $m + 1$ and $\SubtypeSet {x}{(\MembershipmemMACRoT {S}{x})}$. Then $\operatorname{faceRepresentableBy}$ applied to $S$, $m$ and $e$ is an element of $\operatorname{RepresentableBy}$ applied to the underlying simplicial set of the face of $S$ and $\operatorname{mk}$ applied to $m$.

the face singleton complement isomorphism of i (from the name)

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then the face singleton complement isomorphism of $i$ is an isomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and the underlying simplicial set of the face of the complement of $\operatorname{singleton}$ applied to $i$ defined as the isomorphism of $\operatorname{faceRepresentableBy}$ applied to the complement of $\operatorname{singleton}$ applied to $i$, $n$ and the finite successor above order isomorphism finite set of $i$.

the face singleton isomorphism of i (from the name)

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the face singleton isomorphism of $i$ is an isomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $0$ and the underlying simplicial set of the face of $\operatorname{singleton}$ applied to $i$ defined as the isomorphism of $\operatorname{faceRepresentableBy}$ applied to $\operatorname{singleton}$ applied to $i$, $0$ and the order isomorphism singleton of $i$.

the finite order isomorphism pair complement of i and j (from the name)

Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $n + 2$ such that $i < j$. Then the finite order isomorphism pair complement of $i$ and $j$ is an order isomorphism of $\mathrm{Fin}$ applied to $n$ and $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{compl} (\operatorname{insert} (i , \operatorname{singleton} (j)))}{x})}$.

the finite successor above order isomorphism finite set of i (from the name)

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then the finite successor above order isomorphism finite set of $i$ is an order isomorphism of $\mathrm{Fin}$ applied to $n + 1$ and $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{compl} (\operatorname{singleton} (i))}{x})}$.

$\operatorname{fullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{stdSimplex}$ defined as $\operatorname{fullyFaithful}$ applied to the set of simplex categories.

the isomorphism nerve of n (from the name)

Let $n$ be a natural number. Then the isomorphism nerve of $n$ is an isomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and the nerve of $\mathrm{ULift}$ applied to $\mathrm{Fin}$ applied to $n + 1$.

the isomorphism of h (from the name)

Let $h$ be an element of $\operatorname{RepresentableBy}$ applied to $X$ and $\operatorname{mk}$ applied to $m$. Then the isomorphism of $h$ is an isomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $m$ and $X$.

the non degenerate equivalence (from the name)

The non degenerate equivalence is an equivalence from the set of elements of $\operatorname{nonDegenerate}$ applied to the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and $d$ to the set of order embeddings of $\mathrm{Fin}$ applied to $d + 1$ and $\mathrm{Fin}$ applied to $n + 1$.

the non degenerate equivalence (from the name)

The non degenerate equivalence is an equivalence from the set of elements of $\operatorname{nonDegenerate}$ applied to the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and $d$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $S$ to $\mathrm{Eq} (\FinsetcardMACRoM {S}, d + 1)$.

the object equivalence (from the name)

The object equivalence is an equivalence from the action of the action of $\operatorname{stdSimplex}$ and $n$ and $m$ to the set of homomorphisms of the opposite of $m$ and $n$ defined as the lift.

the object of f (from the name)

Let $f$ be an order homomorphism of $\mathrm{Fin}$ applied to the sum of the length in the opposite of $m$ and $1$ and $\mathrm{Fin}$ applied to the sum of the length in $n$ and $1$. Then the object of $f$ is an element of the action of the action of $\operatorname{stdSimplex}$ and $n$ and $m$ defined as $\operatorname{symm}$ applied to the object equivalence and $\operatorname{mk}$ applied to $f$.

the object equivalence (from the name)

The object equivalence is an equivalence from the action of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ to $\mathrm{Fin}$ applied to $n + 1$.

the opposite of n (from the docstring)

Let $n$ be a simplex category. Then the opposite of $n$ is an isomorphism of the opposite of the action of $\operatorname{stdSimplex}$ and $n$ and the action of $\operatorname{stdSimplex}$ and $n$.

the opposite object equivalence (from the name)

The opposite object equivalence is an equivalence from the action of the opposite of the action of $\operatorname{stdSimplex}$ and $n$ and $d$ to the action of the action of $\operatorname{stdSimplex}$ and $n$ and $d$ defined as the composition of the opposite object equivalence and the composition of the object equivalence and the composition of the equivalence of the functor of $\operatorname{revEquivalence}$ and the inverse of the object equivalence.

the order isomorphism of x (from the name)

Let $x$ be an element of $\operatorname{nonDegenerate}$ applied to the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and $d$. Then the order isomorphism of $x$ is an order isomorphism of $\mathrm{Fin}$ applied to $d + 1$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{nonDegenerateEquiv'} (x)}{x_{1}})}$.

the triangle of b and c (from the name)

Let $a$, $b$ and $c$ be elements of $\mathrm{Fin}$ applied to $n + 1$ such that $a \leq b \leq c$. Then the triangle of $b$ and $c$ is an element of the action of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $2$.

the Yoneda equivalence (from the name)

The Yoneda equivalence is an equivalence from the set of homomorphisms of the action of $\operatorname{stdSimplex}$ and $n$ and $X$ to the action of $X$ and $\operatorname{op}$ applied to $n$ defined as the lift Yoneda equivalence.

the object of i (from the name)

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then the object of $i$ is an element of the action of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$.

Let $C$ be a set. Then $\operatorname{strictSegal}$ applied to $C$ is an element of $\operatorname{StrictSegal}$ applied to the nerve of $C$.

Let $X$ be a set. Then we can say that $\operatorname{IsStrictSegal}$ holds for $X$.

Let $X$ be a set. Then the elements of $\operatorname{StrictSegal}$ applied to $X$ are a basic type.

Let $h$ be a function from natural numbers $n$ to elements of $\operatorname{StrictSegalCore}$ applied to $X$ and $n$. Then $\operatorname{ofCore}$ applied to $n$ and $h$ is an element of $\operatorname{StrictSegal}$ applied to $X$.

Let $X$ be a set. Then $\operatorname{ofIsStrictSegal}$ applied to $X$ is an element of $\operatorname{StrictSegal}$ applied to $X$.

the spine equivalence of sx and n (from the name)

Let $\mathrm{sx}$ be an element of $\operatorname{StrictSegal}$ applied to $X$. Let $n$ be a natural number. Then the spine equivalence of $\mathrm{sx}$ and $n$ is an equivalence from the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ to the set of paths of $X$ and $n$ defined as $\operatorname{mk}$ applied to $\operatorname{spine}$ applied to $n$, $\operatorname{spineToSimplex}$ applied to $\mathrm{sx}$, $\mathrm{SSet\_\_StrictSegal\_\_spineToSimplex\_spine\_apply}$ applied to $\mathrm{sx}$ and $\mathrm{SSet\_\_StrictSegal\_\_spine\_spineToSimplex\_apply}$ applied to $\mathrm{sx}$.

the spine to diagonal of sx and f (from the name)

Let $\mathrm{sx}$ be an element of $\operatorname{StrictSegal}$ applied to $X$. Let $f$ be a path of $X$ and $n$. Then the spine to diagonal of $\mathrm{sx}$ and $f$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$ defined as $\operatorname{hom}$ applied to the diagonal of $X$ and the spine to simplex of $\mathrm{sx}$ and $f$.

the spine to simplex of self and x (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{StrictSegal}$ applied to $X$. Let $x$ be a path of $X$ and $n$. Then the spine to simplex of $\mathrm{self}$ and $x$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

the truncation of sx and n (from the name)

Let $\mathrm{sx}$ be an element of $\operatorname{StrictSegal}$ applied to $X$. Let $n$ be a natural number. Then the truncation of $\mathrm{sx}$ and $n$ is an element of $\operatorname{StrictSegal}$ applied to the action of the truncation of $n + 1$ and $X$ defined as $\operatorname{mk}$ applied to the function that maps $x$ and $h$ to $\operatorname{spineToSimplex}$ applied to $\mathrm{sx}$, the function that maps $m$ and $h_{1}$ to $\mathrm{SSet\_\_StrictSegal\_\_spine\_spineToSimplex}$ applied to $\mathrm{sx}$ and $m$ and the function that maps $m_{1}$ and $h_{2}$ to $\mathrm{SSet\_\_StrictSegal\_\_spineToSimplex\_spine}$ applied to $\mathrm{sx}$ and $m_{1}$.

Let $X$ be a set. Let $n$ be a natural number. Then the elements of $\operatorname{StrictSegalCore}$ applied to $X$ and $n$ are a basic type.

Let $\mathrm{self}$ be an element of $\operatorname{StrictSegalCore}$ applied to $X$ and $n$. Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$. Let $s$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ such that $\operatorname{hom}$ applied to $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_}$ applied to $X$ and $0$ and $x$ is equal to $\operatorname{hom}$ applied to the map of $X$ and the opposite in the constant of $\operatorname{mk}$ applied to $n$ and $0$ and $s$. Then $\operatorname{concat}$ applied to $\mathrm{self}$, $x$, $s$ and $h$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n + 1$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x$, $s$ and $h$.

Let $X$ be an element of $\operatorname{Truncated}$ applied to $n + 1$. Then we can say that $\operatorname{IsStrictSegal}$ holds for $X$.

Let $X$ be an element of $\operatorname{Truncated}$ applied to $n + 1$. Then the elements of $\operatorname{StrictSegal}$ applied to $X$ are a basic type.

Let $X$ be an element of $\operatorname{Truncated}$ applied to $n + 1$. Then $\operatorname{ofIsStrictSegal}$ applied to $X$ is an element of $\operatorname{StrictSegal}$ applied to $X$.

the spine equivalence of sx and m (from the name)

Let $\mathrm{sx}$ be an element of $\operatorname{StrictSegal}$ applied to $X$. Let $m$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (m , n + 1)$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_StrictSegal\_\_0\_\_\_auto\_34}$. Then the spine equivalence of $\mathrm{sx}$ and $m$ is an equivalence from the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $m$ and $h$ to the set of paths of $X$ and $m$ defined as $\operatorname{mk}$ applied to $\operatorname{spine}$ applied to $m$, $\operatorname{spineToSimplex}$ applied to $m$, $\mathrm{SSet\_\_Truncated\_\_StrictSegal\_\_spineToSimplex\_spine\_apply}$ applied to $\mathrm{sx}$, $m$ and $h$ and $\mathrm{SSet\_\_Truncated\_\_StrictSegal\_\_spine\_spineToSimplex\_apply}$ applied to $\mathrm{sx}$, $m$ and $h$.

the spine to diagonal of m and x (from the name)

Let $\mathrm{sx}$ be an element of $\operatorname{StrictSegal}$ applied to $X$. Let $m$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (m , n + 1)$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_StrictSegal\_\_0\_\_\_auto\_42}$. Let $x$ be a path of $X$ and $m$. Then the spine to diagonal of $m$ and $x$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{SSet\_\_Truncated\_\_StrictSegal\_\_spineToDiagonal\_\_\_proof\_2}$ applied to $m$.

the spine to simplex of m and x (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{StrictSegal}$ applied to $X$. Let $m$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (m , n + 1)$ and $\mathrm{SSet\_\_Truncated\_\_StrictSegal\_\_\_auto\_1}$. Let $x$ be a path of $X$ and $m$. Then the spine to simplex of $m$ and $x$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $m$ and $h$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $m$, $h$ and $x$.

subcomplex of X (from the name)

Let $X$ be a set. Then a subcomplex of $X$ is an element of the function that maps $X$ to the set of subfunctors of $X$.

Assume that $\EqtMACRoH {x}{x_{1}}$. Then $\operatorname{eqToIso}$ applied to $h$ is an isomorphism of the underlying simplicial set of $x$ and the underlying simplicial set of $x_{1}$.

Let $A$ be a subcomplex of $X$. Let $p$ be a homomorphism of $Y$ and $X$. Then $\operatorname{fromPreimage}$ applied to $A$ and $p$ is a homomorphism of the underlying simplicial set of the preimage of $A$ and $p$ and the underlying simplicial set of $A$.

the homomorphism of h (from the name)

Assume that $x \leq x_{1}$. Then the homomorphism of $h$ is a homomorphism of the underlying simplicial set of $x$ and the underlying simplicial set of $x_{1}$ defined as the homomorphism of $h$.

the image of A and f (from the docstring)

Let $A$ be a subcomplex of $X$. Let $f$ be a homomorphism of $X$ and $Y$. Then the image of $A$ and $f$ is a subcomplex of $Y$ defined as the image of $A$ and $f$.

$\operatorname{isInitialBot}$ is an element of $\operatorname{IsInitial}$ applied to the underlying simplicial set of the bottom defined as $\operatorname{ofUnique}$ applied to the underlying simplicial set of the bottom.

the lift of f and hf (from the name)

Let $f$ be a homomorphism of $X$ and $Y$ such that the range of $f$ is less than or equal to $B$. Then the lift of $f$ and $\mathrm{hf}$ is a homomorphism of $X$ and the underlying simplicial set of $B$ defined as the lift of $f$ and $\mathrm{hf}$.

the subcomplex of x (from the docstring)

Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$. Then the subcomplex of $x$ is a subcomplex of $X$ defined as the subfunctor of $x$.

the preimage of A and p (from the docstring)

Let $A$ be a subcomplex of $X$. Let $p$ be a homomorphism of $Y$ and $X$. Then the preimage of $A$ and $p$ is a subcomplex of $Y$.

the range of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the range of $f$ is a subcomplex of $Y$ defined as the range of $f$.

the image of A and f (from the name)

Let $A$ be a subcomplex of $X$. Let $f$ be a homomorphism of $X$ and $Y$. Then the image of $A$ and $f$ is a homomorphism of the underlying simplicial set of $A$ and the underlying simplicial set of the image of $A$ and $f$.

the range of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the range of $f$ is a homomorphism of $X$ and the underlying simplicial set of the range of $f$ defined as the range of $f$.

the underlying simplicial set of A (from the docstring)

Let $A$ be a subcomplex of $X$. Then the underlying simplicial set of $A$ is a set defined as the subfunctor as a functor of $A$.

the set functor (from the name)

The set functor is a functor of the set of subcomplexes of $X$ and the set of sets.

the top isomorphism of X (from the name)

Let $X$ be a set. Then the top isomorphism of $X$ is an isomorphism of the underlying simplicial set of the top and $X$.

the inclusion of A (from the name)

Let $A$ be a subcomplex of $X$. Then the inclusion of $A$ is a homomorphism of the underlying simplicial set of $A$ and $X$ defined as the inclusion of $A$.

Let $x$, $x_{1}$, $x_{2}$ and $x_{3}$ be subcomplexes of $X$. Then $\operatorname{BicartSq}$ holds for $x$, $x_{1}$, $x_{2}$ and $x_{3}$, if $\operatorname{BicartSq}$ holds for $x$, $x_{1}$, $x_{2}$ and $x_{3}$.

Let $A$ be a subcomplex of $X$. Let $U$ and $V$ be functions from elements of $x$ to subcomplexes of $X$. Then $\operatorname{MulticoequalizerDiagram}$ holds for $A$, $U$ and $V$, if $\operatorname{MulticoequalizerDiagram}$ holds for $A$, $U$ and $V$.

Assume that $\operatorname{MulticoequalizerDiagram}$ holds for $A$, $U$ and $V$. Then $\operatorname{isColimit}$ applied to $h$ is an element of $\operatorname{IsColimit}$ applied to the map of the multicofork of $h$ and the set functor.

Assume that $\operatorname{MulticoequalizerDiagram}$ holds for $A$, $U$ and $V$. Then $\operatorname{isColimit'}$ applied to $h$ is an element of $\operatorname{IsColimit}$ applied to the map of the linear order of the multicofork of $h$ and the set functor.

the evaluation functor of X and j (from the docstring)

Let $X$ be a set. Let $j$ be an opposite of the set of simplex categories. Then the evaluation functor of $X$ and $j$ is a functor of the set of subcomplexes of $X$ and the power set of the action of $X$ and $j$.

the opposite of A (from the name)

Let $A$ be a subcomplex of $X$. Then the opposite of $A$ is a subcomplex of the opposite of $X$.

$\operatorname{ex}$ is a functor of the set of sets and the set of sets defined as the restricted lift Yoneda of $\operatorname{sd}$.

$\operatorname{sd}$ is a functor of the set of sets and the set of sets defined as the left Kan extension of $\operatorname{stdSimplex}$ and $\operatorname{sd}$.

the adjunction between the subdivision functor (from the docstring)

The adjunction between the subdivision functor is an adjunction of $\operatorname{sd}$ and $\operatorname{ex}$ defined as the lift Yoneda adjunction of the left Kan extension of $\operatorname{stdSimplex}$ and $\operatorname{sd}$ and the unit of the chosen left Kan extension of $\operatorname{stdSimplex}$ and $\operatorname{sd}$.

the natural isomorphism (from the docstring)

The natural isomorphism is an isomorphism of the composition of $\operatorname{stdSimplex}$ and $\operatorname{sd}$ and $\operatorname{sd}$ defined as $\operatorname{isExtensionAlongULiftYoneda}$ applied to $\operatorname{sd}$.

$\operatorname{sd}$ is a functor of the set of simplex categories and the set of sets defined as the composition of the part order and the composition of the functor and the functor.

the set object (from the name)

The set object is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and the action of the set and $\operatorname{I}$ defined as $\operatorname{homEquiv}$ applied to the set top adjoint, the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$, $\operatorname{I}$ and the homomorphism of the top object isomorphism.

the top object isomorphism (from the name)

The top object isomorphism is an isomorphism of the action of the top and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and $\operatorname{I}$ defined as the isomorphism of the composition of the homeomorphism between the topological realization of $\operatorname{mk}$ applied to $1$ and the standard topological simplex of dimension.

the homeomorphism between the topological realization of n (from the docstring)

Let $n$ be a simplex category. Then the homeomorphism between the topological realization of $n$ is a homeomorphism of the set of carriers of the action of the top and the action of $\operatorname{stdSimplex}$ and $n$ and $\operatorname{StdSimplex}$ applied to $\Real$ and $\mathrm{Fin}$ applied to the sum of the length in $n$ and $1$ defined as the composition of the homeomorphism of the application of the top simplex and $n$ and the lift.

the standard topological simplex of dimension (from the docstring)

The standard topological simplex of dimension is a homeomorphism of $\operatorname{StdSimplex}$ applied to $\Real$ and $\mathrm{Fin}$ applied to $2$ and the set of carriers of $\operatorname{I}$ defined as the composition of the homeomorphism and the inverse of the lift.

the set object equivalence (from the name)

The set object equivalence is an equivalence from the action of the action of the set and $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ to the set of carriers of $X$.

the singular chain complex functor with coefficients in C (from the docstring)

Let $C$ be a set. Then the singular chain complex functor with coefficients in $C$ is a functor of $C$ and the set of functors of the set of topological categories and the set of chain complexes of $C$ and $\Natural$ defined as the composition of the chain complex functor of $C$ and the action of the left whiskering of the set of sets and the set of chain complexes of $C$ and $\Natural$ and the set.

the adjunction of C and n (from the docstring)

Let $C$ be a set. Let $n$ be a natural number. Then the adjunction of $C$ and $n$ is an adjunction of the action of the action of the postcomposition and the evaluation of $\operatorname{down}$ applied to $\Natural$ and $n$ and the singular chain complex functor with coefficients in $C$ and the action of the evaluation of the set of topological categories and $C$ and the action of the top and $\operatorname{mk}$ applied to $n$ defined as the adjunction of the composition of the adjunction of $C$ and $n$ and the left whisker of $C$ and the set top adjoint and the map isomorphism of the evaluation of the set of topological categories and $C$ and the application of the top simplex and $\operatorname{mk}$ applied to $n$.

the singular chain complex functor isomorphism of R and X (from the name)

Let $C$ be a set. Let $R$ be an element of $C$. Let $X$ be a topological category. Then the singular chain complex functor isomorphism of $R$ and $X$ is an isomorphism of the action of the action of the singular chain complex functor with coefficients in $C$ and $R$ and $X$ and the action of the alternating constant and the sigma object of the function that maps $x_{2}$ to $R$ defined as the composition of the map isomorphism of the alternating face map complex of $C$ and the composition of the map isomorphism of the action of the whiskering of the set of sets and $C$ and the action of the sigma constant and $R$ and the singular simplicial set of $X$ and the constant composition of the set of carriers of $X$ and the action of the sigma constant and $R$ and the application of the alternating face complex of the constant complex and the action of the action of the sigma constant and $R$ and the set of carriers of $X$.

the singular homology functor of C and n (from the name)

Let $C$ be a set. Let $n$ be a natural number. Then the singular homology functor of $C$ and $n$ is a functor of $C$ and the set of functors of the set of topological categories and $C$ defined as the composition of the singular chain complex functor with coefficients in $C$ and the action of the right whiskering of the set of chain complexes of $C$ and $\Natural$ and $C$ and the homology functor of $\operatorname{down}$ applied to $\Natural$ and $n$.

the singular homology functor zero of R and X (from the name)

Let $C$ be a set. Let $R$ be an element of $C$. Let $X$ be a topological category. Then the singular homology functor zero of $R$ and $X$ is an isomorphism of the action of the action of the singular homology functor of $C$ and $0$ and $R$ and $X$ and the sigma object of the function that maps $x_{2}$ to $R$ defined as the composition of the map isomorphism of the homology functor of $\operatorname{down}$ applied to $\Natural$ and $0$ and the singular chain complex functor isomorphism of $R$ and $X$ and the alternating constant homology zero of the sigma object of the function that maps $x_{2}$ to $R$.

the singular homology of X and R (from the docstring)

Let $X$ be a topological category. Let $R$ be an element of $C$. Then the singular homology of $X$ and $R$ is an isomorphism of the action of the action of the singular homology functor of $C$ and $0$ and $R$ and $X$ and the sigma object of the function that maps $x_{2}$ to $R$ defined as the composition of the homology of the action of the set and $X$ and $R$ and the map isomorphism of the action of the sigma constant and $R$ and the inverse of the isomorphism of the zeroth homotopy equivalence.

the singular homology of X and R (from the name)

Let $X$ be a topological category. Let $R$ be an element of $C$. Then the singular homology of $X$ and $R$ is a homomorphism of the action of the action of the singular homology functor of $C$ and $0$ and $R$ and $X$ and $R$ defined as the homology of the action of the set and $X$ and $R$.

the singular chain complex functor object map of H and R (from the name)

Let $H$ be a homotopy of $f$ and $g$. Let $R$ be an element of $C$. Then the singular chain complex functor object map of $H$ and $R$ is a homotopy of the map of the action of the singular chain complex functor with coefficients in $C$ and $R$ and $f$ and the map of the action of the singular chain complex functor with coefficients in $C$ and $R$ and $g$ defined as the chain complex map of the set of $H$ and $R$.

$\operatorname{stdSimplexToTop}$ is a homomorphism of $\operatorname{stdSimplex}$ and the composition of the top and the set defined as the composition of the left whisker of $\operatorname{stdSimplex}$ and the unit of the set top adjoint and the right whisker of the homomorphism of the top simplex and the set.

the top (from the name)

The top is a functor of the set of sets and the set of topological categories defined as the left Kan extension of $\operatorname{stdSimplex}$ and the top.

the top simplex (from the name)

The top simplex is an isomorphism of the composition of $\operatorname{stdSimplex}$ and the top and the top defined as $\operatorname{isExtensionAlongULiftYoneda}$ applied to the top.

the set (from the name)

The set is a functor of the set of topological categories and the set of sets defined as the restricted lift Yoneda of the top.

the singular simplicial set of X (from the docstring)

Let $X$ be a topological category. Then the singular simplicial set of $X$ is an isomorphism of the action of the set and $X$ and the action of the constant of the set of opposites of the set of simplex categories and the set of carriers of $X$.

the set object equivalence of X and n (from the name)

Let $X$ be a topological category. Let $n$ be an opposite of the set of simplex categories. Then the set object equivalence of $X$ and $n$ is an equivalence from the action of the action of the set and $X$ and $n$ to the set of continuous maps of $\operatorname{StdSimplex}$ applied to $\Real$ and $\mathrm{Fin}$ applied to the sum of the length in the opposite of $n$ and $1$ and the set of carriers of $X$ defined as the composition of the lift and the composition of the homomorphism equivalence and the continuous map congruence of the lift and the identity of the set of carriers of $X$.

the set top adjoint (from the name)

The set top adjoint is an adjunction of the top and the set defined as the lift Yoneda adjunction of the left Kan extension of $\operatorname{stdSimplex}$ and the top and the unit of the chosen left Kan extension of $\operatorname{stdSimplex}$ and the top.

the top (from the name)

The top is a functor of the set of simplex categories and the set of topological categories defined as the composition of the top and the lift functor.

the top (from the name)

The top is a cosimplicial object of the set of topological categories.