Definitions: Mathlib.AlgebraicTopology, part 3 of 4

walking isomorphism (from the name)

A walking isomorphism is a codiscrete of $\mathrm{ULift}$ applied to $\mathrm{Bool}$.

the equivalence (from the name)

The equivalence is an equivalence from the set of functors of the set of walking isomorphisms and $C$ to $\Sigma$ applied to the function that maps $X$ to $\Sigma$ applied to the function that maps $Y$ to the set of isomorphisms of $X$ and $Y$.

the equivalence bool (from the name)

The equivalence bool is an equivalence from the set of walking isomorphisms to $\mathrm{Bool}$ defined as the composition of the codiscrete equivalence and the lift.

Let $e$ be an isomorphism of $X$ and $Y$. Then $\operatorname{fromIso}$ applied to $e$ is a functor of the set of walking isomorphisms and $C$.

the isomorphism (from the name)

The isomorphism is an isomorphism of the zero and the one defined as the isomorphism of the zero and the one.

the one (from the name)

The one is a walking isomorphism defined as $\operatorname{mk}$ applied to $\operatorname{up}$ applied to $\operatorname{true}$.

the isomorphism of F (from the name)

Let $F$ be a functor of the set of walking isomorphisms and $C$. Then the isomorphism of $F$ is an isomorphism of the action of $F$ and the zero and the action of $F$ and the one defined as the map isomorphism of $F$ and the isomorphism.

the zero (from the name)

The zero is a walking isomorphism defined as $\operatorname{mk}$ applied to $\operatorname{up}$ applied to $\operatorname{false}$.

the coherent isomorphism (from the name)

The coherent isomorphism is a set defined as the nerve of the set of walking isomorphisms.

the homomorphism (from the name)

The homomorphism is an edge of $\mathrm{SSet\_\_coherentIso\_\_x\_u2080\_}$ and $\mathrm{SSet\_\_coherentIso\_\_x\_u2081\_}$.

the homomorphism inverse identity (from the name)

The homomorphism inverse identity is an element of $\operatorname{CompStruct}$ applied to the homomorphism, the inverse and the identity of $\mathrm{SSet\_\_coherentIso\_\_x\_u2080\_}$.

the inverse (from the name)

The inverse is an edge of $\mathrm{SSet\_\_coherentIso\_\_x\_u2081\_}$ and $\mathrm{SSet\_\_coherentIso\_\_x\_u2080\_}$.

the inverse homomorphism identity (from the name)

The inverse homomorphism identity is an element of $\operatorname{CompStruct}$ applied to the inverse, the homomorphism and the identity of $\mathrm{SSet\_\_coherentIso\_\_x\_u2081\_}$.

$\operatorname{invStructHom}$ is an element of $\operatorname{InvStruct}$ applied to the homomorphism defined as $\operatorname{mk}$ applied to the inverse, the homomorphism inverse identity and the inverse homomorphism identity.

Assume that the edge of $f$ is equal to $\operatorname{hom}$ applied to the component of $g$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$ and the edge of the homomorphism. Then $\operatorname{invStructOfEqMapHom}$ applied to $\mathrm{hfg}$ is an element of $\operatorname{InvStruct}$ applied to $f$.

$\mathrm{SSet\_\_coherentIso\_\_x\_u2080\_}$ is an element of the action of the coherent isomorphism and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2080\_}$ applied to the zero.

$\mathrm{SSet\_\_coherentIso\_\_x\_u2081\_}$ is an element of the action of the coherent isomorphism and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2080\_}$ applied to the one.

edge of x and x1 (from the name)

Let $x$ and $x_{1}$ be elements of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$. Then an edge of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of edges of $x$ and $x_{1}$.

Let $x_{3}$ be an edge of $x$ and $x_{1}$. Let $x_{4}$ be an edge of $x_{1}$ and $x_{2}$. Let $x_{5}$ be an edge of $x$ and $x_{2}$. Then an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$ is an element of the function that maps $x_{3}$, $x_{4}$ and $x_{5}$ to $\operatorname{CompStruct}$ applied to $\operatorname{toTruncated}$ applied to $x_{3}$, $\operatorname{toTruncated}$ applied to $x_{4}$ and $\operatorname{toTruncated}$ applied to $x_{5}$.

the composition identity of e (from the name)

Let $e$ be an edge of $x$ and $x_{1}$. Then the composition identity of $e$ is an element of $\operatorname{CompStruct}$ applied to $e$, the identity of $x_{1}$ and $e$ defined as $\operatorname{ofTruncated}$ applied to the composition identity of $\operatorname{toTruncated}$ applied to $e$.

the identity composition of e (from the name)

Let $e$ be an edge of $x$ and $x_{1}$. Then the identity composition of $e$ is an element of $\operatorname{CompStruct}$ applied to the identity of $x$, $e$ and $e$ defined as $\operatorname{ofTruncated}$ applied to the identity composition of $\operatorname{toTruncated}$ applied to $e$.

the identity composition identity of x (from the name)

Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$. Then the identity composition identity of $x$ is an element of $\operatorname{CompStruct}$ applied to the identity of $x$, the identity of $x$ and the identity of $x$ defined as $\operatorname{ofTruncated}$ applied to the identity composition identity of $x$.

the map of h and f (from the name)

Let $h$ be an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $h$ and $f$ is an element of $\operatorname{CompStruct}$ applied to the map of $x_{3}$ and $f$, the map of $x_{4}$ and $f$ and the map of $x_{5}$ and $f$ defined as $\operatorname{ofTruncated}$ applied to the map of $\operatorname{toTruncated}$ applied to $h$ and the map of the truncation of $2$ and $f$.

Let $\mathrm{simplex}$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $2$ such that $\mathrm{autoParam}$ holds for the proposition that $\operatorname{hom}$ applied to $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_}$ applied to $X$ and $2$ and $\mathrm{simplex}$ is equal to the edge of $x_{3}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_CompStruct\_\_0\_\_\_auto\_95}$, $\mathrm{autoParam}$ holds for the proposition that $\operatorname{hom}$ applied to $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_}$ applied to $X$ and $0$ and $\mathrm{simplex}$ is equal to the edge of $x_{4}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_CompStruct\_\_0\_\_\_auto\_97}$ and $\mathrm{autoParam}$ holds for the proposition that $\operatorname{hom}$ applied to $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_}$ applied to $X$ and $1$ and $\mathrm{simplex}$ is equal to the edge of $x_{5}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_CompStruct\_\_0\_\_\_auto\_99}$. Then $\operatorname{mk}$ applied to $\mathrm{simplex}$, $h$, $h_{1}$ and $h_{2}$ is an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$.

Let $c$ be an element of $\operatorname{CompStruct}$ applied to $x_{6}$, $x_{8}$ and $x_{10}$. Assume that the edge of $x_{6}$ is equal to the edge of $x_{7}$. Assume that the edge of $x_{8}$ is equal to the edge of $x_{9}$. Assume that the edge of $x_{10}$ is equal to the edge of $x_{11}$. Then $\operatorname{ofEq}$ applied to $c$, $h$, $h_{1}$ and $h_{2}$ is an element of $\operatorname{CompStruct}$ applied to $x_{7}$, $x_{9}$ and $x_{11}$.

Let $h$ be an element of $\operatorname{CompStruct}$ applied to $\operatorname{toTruncated}$ applied to $x_{3}$, $\operatorname{toTruncated}$ applied to $x_{4}$ and $\operatorname{toTruncated}$ applied to $x_{5}$. Then $\operatorname{ofTruncated}$ applied to $h$ is an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$ defined as $h$.

the simplex of h (from the name)

Let $h$ be an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$. Then the simplex of $h$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $2$ defined as the simplex of $\operatorname{toTruncated}$ applied to $h$.

the subcomplex of h and A (from the name)

Let $h$ be an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$. Let $A$ be a subcomplex of $X$ such that the simplex of $h$ is an element of the object of $A$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $2$. Then the subcomplex of $h$ and $A$ is an element of $\operatorname{CompStruct}$ applied to the subcomplex of $x_{3}$ and $A$, the subcomplex of $x_{4}$ and $A$ and the subcomplex of $x_{5}$ and $A$.

Let $h$ be an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$. Then $\operatorname{toTruncated}$ applied to $h$ is an element of $\operatorname{CompStruct}$ applied to $\operatorname{toTruncated}$ applied to $x_{3}$, $\operatorname{toTruncated}$ applied to $x_{4}$ and $\operatorname{toTruncated}$ applied to $x_{5}$ defined as $h$.

Let $\mathrm{hom}$ be an edge of $x$ and $x_{1}$. Then the elements of $\operatorname{InvStruct}$ applied to $\mathrm{hom}$ are a basic type.

the homomorphism inverse identity of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{InvStruct}$ applied to $\mathrm{hom}$. Then the homomorphism inverse identity of $\mathrm{self}$ is an element of $\operatorname{CompStruct}$ applied to $\mathrm{hom}$, the inverse of $\mathrm{self}$ and the identity of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the inverse of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{InvStruct}$ applied to $\mathrm{hom}$. Then the inverse of $\mathrm{self}$ is an edge of $x_{1}$ and $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the inverse homomorphism identity of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{InvStruct}$ applied to $\mathrm{hom}$. Then the inverse homomorphism identity of $\mathrm{self}$ is an element of $\operatorname{CompStruct}$ applied to the inverse of $\mathrm{self}$, $\mathrm{hom}$ and the identity of $x_{1}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$. Then $\operatorname{invStructId}$ applied to $x$ is an element of $\operatorname{InvStruct}$ applied to the identity of $x$ defined as $\operatorname{mk}$ applied to the identity of $x$, the identity composition identity of $x$ and the identity composition identity of $x$.

Let $I$ be an element of $\operatorname{InvStruct}$ applied to $\mathrm{hom}$. Then $\operatorname{invStructInv}$ applied to $I$ is an element of $\operatorname{InvStruct}$ applied to the inverse of $I$ defined as $\operatorname{mk}$ applied to $\mathrm{hom}$, the inverse homomorphism identity of $I$ and the homomorphism inverse identity of $I$.

the map of I and f (from the name)

Let $I$ be an element of $\operatorname{InvStruct}$ applied to $\mathrm{hom}$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $I$ and $f$ is an element of $\operatorname{InvStruct}$ applied to the map of $\mathrm{hom}$ and $f$.

Let $I$ be an element of $\operatorname{InvStruct}$ applied to $\mathrm{hom}$. Assume that the edge of $\mathrm{hom}$ is equal to the edge of $\mathrm{hom'}$. Then $\operatorname{ofEq}$ applied to $I$ and $\mathrm{hhom}$ is an element of $\operatorname{InvStruct}$ applied to $\mathrm{hom'}$.

the edge of e (from the name)

Let $e$ be an edge of $x$ and $x_{1}$. Then the edge of $e$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$ defined as the edge of $\operatorname{toTruncated}$ applied to $e$.

the identity of x (from the name)

Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$. Then the identity of $x$ is an edge of $x$ and $x$ defined as the edge of the identity of $x$.

the map of e and f (from the name)

Let $e$ be an edge of $x$ and $x_{1}$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $e$ and $f$ is an edge of $\operatorname{hom}$ applied to the component of $f$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and $x$ and $\operatorname{hom}$ applied to the component of $f$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and $x_{1}$ defined as the edge of the map of $\operatorname{toTruncated}$ applied to $e$ and the map of the truncation of $2$ and $f$.

Let $\mathrm{edge}$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$ such that $\mathrm{autoParam}$ holds for $\EqtMACRoH {\operatorname{hom} (\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_} (X , 1), \mathrm{edge})}{x}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_CompStruct\_\_0\_\_\_auto\_32}$ and $\mathrm{autoParam}$ holds for $\EqtMACRoH {\operatorname{hom} (\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_} (X , 0), \mathrm{edge})}{x_{1}}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_CompStruct\_\_0\_\_\_auto\_34}$. Then $\operatorname{mk}$ applied to $\mathrm{edge}$, $\mathrm{src\_eq}$ and $\mathrm{tgt\_eq}$ is an edge of $x$ and $x_{1}$.

Let $s$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$. Then $\operatorname{mk'}$ applied to $s$ is an edge of $\operatorname{hom}$ applied to $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_}$ applied to $X$ and $1$ and $s$ and $\operatorname{hom}$ applied to $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_}$ applied to $X$ and $0$ and $s$.

the edge of e (from the name)

Let $e$ be an edge of $x$ and $x_{1}$. Assume that $\EqtMACRoH {x}{x_{2}}$. Assume that $\EqtMACRoH {x_{1}}{x_{3}}$. Then the edge of $e$ is an edge of $x_{2}$ and $x_{3}$.

the edge of e (from the name)

Let $e$ be an edge of $x$ and $x_{1}$. Then the edge of $e$ is an edge of $x$ and $x_{1}$ defined as $e$.

the subcomplex of e and A (from the name)

Let $e$ be an edge of $x$ and $x_{1}$. Let $A$ be a subcomplex of $X$ such that the edge of $e$ is an element of the object of $A$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$. Then the subcomplex of $e$ and $A$ is an edge of $x$ and $x_{1}$.

Let $e$ be an edge of $x$ and $x_{1}$. Then $\operatorname{toTruncated}$ applied to $e$ is an edge of $x$ and $x_{1}$ defined as $e$.

edge of x and x1 (from the name)

Let $x$ and $x_{1}$ be elements of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_Truncated\_\_Edge\_\_\_proof\_1}$. Then the edges of $x$ and $x_{1}$ are a basic type.

Let $x_{3}$ be an edge of $x$ and $x_{1}$. Let $x_{4}$ be an edge of $x_{1}$ and $x_{2}$. Let $x_{5}$ be an edge of $x$ and $x_{2}$. Then the elements of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$ are a basic type.

the composition identity of e (from the name)

Let $e$ be an edge of $x$ and $y$. Then the composition identity of $e$ is an element of $\operatorname{CompStruct}$ applied to $e$, the identity of $y$ and $e$.

the identity composition of e (from the name)

Let $e$ be an edge of $x$ and $y$. Then the identity composition of $e$ is an element of $\operatorname{CompStruct}$ applied to the identity of $x$, $e$ and $e$.

the identity composition identity of x (from the name)

Let $x$ be 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\_\_Edge\_\_\_proof\_1}$. Then the identity composition identity of $x$ is an element of $\operatorname{CompStruct}$ applied to the identity of $x$, the identity of $x$ and the identity of $x$ defined as the identity composition of the identity of $x$.

the map of h and f (from the name)

Let $h$ be an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $h$ and $f$ is an element of $\operatorname{CompStruct}$ applied to the map of $x_{3}$ and $f$, the map of $x_{4}$ and $f$ and the map of $x_{5}$ and $f$.

the simplex of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$. Then the simplex of $\mathrm{self}$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_Edge\_\_CompStruct\_\_\_proof\_1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the edge of self (from the name)

Let $\mathrm{self}$ be an edge of $x$ and $x_{1}$. Then the edge of $\mathrm{self}$ 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\_\_Edge\_\_\_proof\_2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the identity of x (from the name)

Let $x$ be 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\_\_Edge\_\_\_proof\_1}$. Then the identity of $x$ is an edge of $x$ and $x$.

the map of e and f (from the name)

Let $e$ be an edge of $x$ and $x_{1}$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $e$ and $f$ is an edge of $\operatorname{hom}$ applied to the component of $f$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_Truncated\_\_Edge\_\_\_proof\_1}$ and $x$ and $\operatorname{hom}$ applied to the component of $f$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_Truncated\_\_Edge\_\_\_proof\_1}$ and $x_{1}$.

Let $s$ be 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\_\_Edge\_\_\_proof\_2}$. Then $\operatorname{mk'}$ applied to $s$ is an edge of $\operatorname{hom}$ applied to the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $1$, $\mathrm{SSet\_\_Truncated\_\_Edge\_\_\_proof\_1}$ and $\mathrm{SSet\_\_Truncated\_\_Edge\_\_\_proof\_3}$ and $s$ and $\operatorname{hom}$ applied to the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $0$, $\mathrm{SSet\_\_Truncated\_\_Edge\_\_\_proof\_1}$ and $\mathrm{SSet\_\_Truncated\_\_Edge\_\_\_proof\_3}$ and $s$.

$\mathrm{CategoryTheory\_\_Nerve\_\_cosk\_u2082\_Iso}$ is an isomorphism of the nerve and the composition of the essential data of the nerve functor and $\operatorname{cosk}$ applied to $2$.

the essential data of the nerve functor (from the docstring)

The essential data of the nerve functor is a functor of the set of categories and $\operatorname{Truncated}$ applied to $2$ defined as the composition of the nerve and the truncation of $2$.

Let $\mathrm{sx}$ be an element of $\operatorname{StrictSegal}$ applied to $X$. Then $\operatorname{IsPointwiseRightKanExtension}$ holds for the right extension inclusion of $X$ and $2$. Proof. Let $\mathrm{sx}$ be arbitrary. Let $x$ be arbitrary. By sx. By x. By Opposite__unop. By SimplexCategory__len. By SSet__StrictSegal__isPointwiseRightKanExtensionAt.

Let $\mathrm{sx}$ be an element of $\operatorname{StrictSegal}$ applied to $X$. Let $n$ be a natural number. Then $\operatorname{isPointwiseRightKanExtensionAt}$ applied to $\mathrm{sx}$ and $n$ is an element of $\operatorname{IsPointwiseRightKanExtensionAt}$ applied to the right extension inclusion of $X$ and $2$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$.

the lift of s and x (from the name)

Let $\mathrm{sx}$ be an element of $\operatorname{StrictSegal}$ applied to $X$. Let $s$ be a cone of the composition of the projection of $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and the opposite of the inclusion of $2$ and the composition of the opposite of the inclusion of $2$ and $X$. Let $x$ be an element of $\operatorname{pt}$ applied to $s$. Then the lift of $s$ and $x$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$.

Let $x$ be a homomorphism of $\operatorname{mk}$ applied to $i$ and $\operatorname{mk}$ applied to $n$. Assume that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (i , 2)$ and $\mathrm{SSet\_\_StrictSegal\_\_isPointwiseRightKanExtensionAt\_\_strArrowMk\_u2082\_\_\_\_auto\_1}$. Then $\mathrm{SSet\_\_StrictSegal\_\_isPointwiseRightKanExtensionAt\_\_strArrowMk\_u2082\_}$ applied to $x$ and $\mathrm{hi}$ is a structured arrow of $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and the opposite of the inclusion of $2$ defined as $\operatorname{mk}$ applied to the opposite in $x$.

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

Let $X$ be a set. 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$.

Let $X$ be a set. Let $n$ be a natural number. Then $\operatorname{degenerate}$ applied to $X$ and $n$ is an element of the power set of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ defined as $\operatorname{ofPred}$ applied to the function that maps $x$ to the proposition that there exists a natural number $m$, such that there exists an element $h$ of $\mathrm{Lt} (m , n)$, such that there exists a homomorphism $f$ of $\operatorname{mk}$ applied to $n$ and $\operatorname{mk}$ applied to $m$, such that $x$ is an element of the range of $\operatorname{coe}$ applied to the homomorphism of the map of $X$ and the opposite in $f$.

Let $X$ be a set. Let $n$ be a natural number. Then $\operatorname{nonDegenerate}$ applied to $X$ and $n$ is an element of the power set of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ defined as the complement of $\operatorname{degenerate}$ applied to $X$ and $n$.

the non degenerate equivalence of e (from the name)

Let $e$ be an isomorphism of $X$ and $Y$. Then the non degenerate equivalence of $e$ is an equivalence from the set of elements of $\operatorname{nonDegenerate}$ applied to $X$ and $n$ to the set of elements of $\operatorname{nonDegenerate}$ applied to $Y$ and $n$.

Let $X$ be a set. Let $d$ be a natural number. Then $\operatorname{HasDimensionLE}$ holds for $X$ and $d$, if $\operatorname{HasDimensionLT}$ holds for $X$ and $d + 1$.

Let $X$ be a set. Let $d$ be a natural number. Then we can say that $\operatorname{HasDimensionLT}$ holds for $X$ and $d$.

X is finite (from the docstring)

Let $X$ be a set. Then we can say that $X$ is finite.

fundamental groupoid of X (from the name)

Let $X$ be a set. Then a fundamental groupoid of $X$ is an element of the function that maps $X$ to the set of fundamental groupoids of the action of the truncation of $2$ and $X$.

Let $\mathrm{obj}$ be a function from elements of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ to elements of $D$. Let $\mathrm{map}$ be a function from elements $x_{8}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and elements $y$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and edges of $x_{8}$ and $y$ to homomorphisms of $\mathrm{obj}$ applied to $x_{8}$ and $\mathrm{obj}$ applied to $y$ such that for all elements $x_{1}$, $x_{2}$ and $x_{3}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$, 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 $\operatorname{desc}$ applied to $\mathrm{obj}$, $x_{8}$, $y$, $\mathrm{map}$ and $\mathrm{map\_comp}$ is a functor of the set of fundamental groupoids of $X$ and $D$ defined as the function that maps $\mathrm{map}$ and $\mathrm{map\_comp}$ to $\operatorname{desc}$ applied to $\mathrm{obj}$, the function that maps $x_{1}$ and $x_{2}$ to $x_{8}$ applied to $x_{1}$ and $x_{2}$, the function that maps $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$ to $y$ applied to $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$, $\mathrm{map}$ and $\mathrm{map\_comp}$.

the homomorphism of e (from the name)

Let $e$ be an edge of $x$ and $y$. Then the homomorphism of $e$ is a homomorphism of $\operatorname{mk}$ applied to $x$ and $\operatorname{mk}$ applied to $y$ defined as the homomorphism of $e$.

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

the natural isomorphism of app and x2 (from the name)

Let $\mathrm{app}$ be a function from elements $x_{2}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ to isomorphisms of the action of $F$ and $\operatorname{mk}$ applied to $x_{2}$ and the action of $G$ and $\operatorname{mk}$ applied to $x_{2}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{1}$ and $y$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$, for all edges $e$ of $x_{1}$ and $y$, the composition of the map of $F$ and the homomorphism of $e$ and the homomorphism of $\mathrm{app}$ applied to $y$ is equal to the composition of the homomorphism of $\mathrm{app}$ applied to $x_{1}$ and the map of $G$ and the homomorphism of $e$ and $\mathrm{SSet\_\_FundamentalGroupoid\_\_natIsoMk\_\_\_auto\_1}$. Then the natural isomorphism of $x_{2}$ and $\mathrm{app}$ is an isomorphism of $F$ and $G$.

the natural transformation of app and x2 (from the name)

Let $\mathrm{app}$ be a function from elements $x_{2}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ to homomorphisms of the action of $F$ and $\operatorname{mk}$ applied to $x_{2}$ and the action of $G$ and $\operatorname{mk}$ applied to $x_{2}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{1}$ and $y$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$, for all edges $e$ of $x_{1}$ and $y$, the composition of the map of $F$ and the homomorphism of $e$ and $\mathrm{app}$ applied to $y$ is equal to the composition of $\mathrm{app}$ applied to $x_{1}$ and the map of $G$ and the homomorphism of $e$ and $\mathrm{SSet\_\_FundamentalGroupoid\_\_natTransMk\_\_\_auto\_1}$. Then the natural transformation of $x_{2}$ and $\mathrm{app}$ is a homomorphism of $F$ and $G$.

fundamental groupoid of X (from the name)

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

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\_\_FundamentalGroupoid\_\_\_proof\_1}$ to elements of $D$. Let $\mathrm{map}$ be a function from 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\_\_FundamentalGroupoid\_\_\_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\_\_FundamentalGroupoid\_\_\_proof\_1}$ and edges of $x_{8}$ and $y$ to homomorphisms of $\mathrm{obj}$ applied to $x_{8}$ and $\mathrm{obj}$ applied to $y$ such that for all elements $x_{1}$, $x_{2}$ and $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\_\_FundamentalGroupoid\_\_\_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 $\operatorname{desc}$ applied to $\mathrm{obj}$, $x_{8}$, $y$, $\mathrm{map}$ and $\mathrm{map\_comp}$ is a functor of the set of fundamental groupoids of $X$ and $D$.

the equivalence free groupoid (from the name)

The equivalence free groupoid is an equivalence from the set of fundamental groupoids of $X$ to the set of free groupoids of the set of homotopy categories of $X$.

the equivalence free groupoid of X (from the name)

Let $X$ be an element of $\operatorname{Truncated}$ applied to $2$. Then the equivalence free groupoid of $X$ is an equivalence of the set of fundamental groupoids of $X$ and the set of free groupoids of the set of homotopy categories of $X$ defined as the equivalence of the isomorphism category free groupoid of $X$.

the homomorphism of e (from the name)

Let $e$ be an edge of $x$ and $y$. Then the homomorphism of $e$ is a homomorphism of $\operatorname{mk}$ applied to $x$ and $\operatorname{mk}$ applied to $y$ defined as $\operatorname{mk}$ applied to the homomorphism of the morphism in the homotopy category of $e$.

the isomorphism category free groupoid of X (from the name)

Let $X$ be an element of $\operatorname{Truncated}$ applied to $2$. Then the isomorphism category free groupoid of $X$ is an isomorphism category of the set of fundamental groupoids of $X$ and the set of free groupoids of the set of homotopy categories of $X$ defined as the isomorphism category of the equivalence free groupoid.

Let $\mathrm{self}$ be a fundamental groupoid of $X$. Then $\operatorname{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\_\_FundamentalGroupoid\_\_\_proof\_1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the map fundamental groupoid of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map fundamental groupoid of $f$ is a functor of the set of fundamental groupoids of $X$ and the set of fundamental groupoids of $Y$.

the map isomorphism fundamental groupoid of e (from the name)

Let $e$ be an isomorphism of $X$ and $Y$. Then the map isomorphism fundamental groupoid of $e$ is an isomorphism category of the set of fundamental groupoids of $X$ and the set of fundamental groupoids of $Y$.

the map fundamental groupoid of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map fundamental groupoid of $f$ is a functor of the set of fundamental groupoids of $X$ and the set of fundamental groupoids of $Y$ defined as the map fundamental groupoid of the map of the truncation of $2$ and $f$.

Let $h$ be a homotopy of $f$ and $g$. Let $e$ be an edge of $x$ and $y$. Then $\operatorname{ofSimplicialObjectHomotopy}$ applied to $h$ and $e$ is an element of $\operatorname{CompStruct}$ applied to the map of $e$ and $f$, the edge connecting of $h$ and $y$ and the diagonal of $h$ and $e$.

Let $h$ be a homotopy of $f$ and $g$. Let $e$ be an edge of $x$ and $y$. Then $\operatorname{ofSimplicialObjectHomotopy'}$ applied to $h$ and $e$ is an element of $\operatorname{CompStruct}$ applied to the edge connecting of $h$ and $x$, the map of $e$ and $g$ and the diagonal of $h$ and $e$.

the diagonal of h and e (from the name)

Let $h$ be a homotopy of $f$ and $g$. Let $e$ be an edge of $x$ and $y$. Then the diagonal of $h$ and $e$ is an edge of $\operatorname{hom}$ applied to the component of $f$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and $x$ and $\operatorname{hom}$ applied to the component of $g$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and $y$.

the edge connecting of h and x (from the docstring)

Let $h$ be a homotopy of $f$ and $g$. Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$. Then the edge connecting of $h$ and $x$ is an edge of $\operatorname{hom}$ applied to the component of $f$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and $x$ and $\operatorname{hom}$ applied to the component of $g$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and $x$.

the congruence map fundamental groupoid of h (from the name)

Let $h$ be a homotopy of $f$ and $g$. Then the congruence map fundamental groupoid of $h$ is an isomorphism of the map fundamental groupoid of $f$ and the map fundamental groupoid of $g$ defined as the congruence map fundamental groupoid of the simplicial object homotopy of $h$.

the congruence map fundamental groupoid of h (from the name)

Let $h$ be a homotopy of $f$ and $g$. Then the congruence map fundamental groupoid of $h$ is an isomorphism of the map fundamental groupoid of $f$ and the map fundamental groupoid of $g$.

the tensor of hx and hy (from the name)

Let $\mathrm{hx}$ be an element of $\operatorname{CompStruct}$ applied to $x_{3}$, $x_{4}$ and $x_{5}$. Let $\mathrm{hy}$ be an element of $\operatorname{CompStruct}$ applied to $x_{9}$, $x_{10}$ and $x_{11}$. Then the tensor of $\mathrm{hx}$ and $\mathrm{hy}$ is an element of $\operatorname{CompStruct}$ applied to the tensor of $x_{3}$ and $x_{9}$, the tensor of $x_{4}$ and $x_{10}$ and the tensor of $x_{5}$ and $x_{11}$.

the tensor of x1 and x2 (from the name)

Let $x_{1}$ be an edge of $x$ and $\mathrm{x'}$. Let $x_{2}$ be an edge of $y$ and $\mathrm{y'}$. Then the tensor of $x_{1}$ and $x_{2}$ is an edge of $\ProdmkMACRoU {x}{y}$ and $\ProdmkMACRoU {\mathrm{x'}}{\mathrm{y'}}$.

the associativity isomorphism of Y and Z (from the name)

Let $X$, $Y$ and $Z$ be elements of $\operatorname{Truncated}$ applied to $2$. Then the associativity isomorphism of $Y$ and $Z$ is an isomorphism of the composition of the product of the inverse of $X$ and $Y$ and the identity of the set of homotopy categories of $Z$ and the composition of the inverse of the tensor object of $X$ and $Y$ and $Z$ and the map homotopy category of the homomorphism of the associator of $Y$ and $Z$ and the composition of the functor of the associativity of the set of homotopy categories of $Y$ and the set of homotopy categories of $Z$ and the composition of the product of the identity of the set of homotopy categories of $X$ and the inverse of $Y$ and $Z$ and the inverse of $X$ and the tensor object of $Y$ and $Z$ defined as the composition of the inverse of the left unitor of the composition of the product of the inverse of $X$ and $Y$ and the identity of the set of homotopy categories of $Z$ and the composition of the inverse of the tensor object of $X$ and $Y$ and $Z$ and the map homotopy category of the homomorphism of the associator of $Y$ and $Z$ and the composition of the right isomorphism whisker of the unit isomorphism of the associativity of the set of homotopy categories of $Y$ and the set of homotopy categories of $Z$ and the composition of the product of the inverse of $X$ and $Y$ and the identity of the set of homotopy categories of $Z$ and the composition of the inverse of the tensor object of $X$ and $Y$ and $Z$ and the map homotopy category of the homomorphism of the associator of $Y$ and $Z$ and the composition of the associator of the inverse of the associativity of the set of homotopy categories of $Y$ and the set of homotopy categories of $Z$ and the composition of the product of the inverse of $X$ and $Y$ and the identity of the set of homotopy categories of $Z$ and the composition of the inverse of the tensor object of $X$ and $Y$ and $Z$ and the map homotopy category of the homomorphism of the associator of $Y$ and $Z$ and the left isomorphism whisker of the functor of the associativity of the set of homotopy categories of $Y$ and the set of homotopy categories of $Z$ and $\operatorname{associativity'Iso}$ applied to $X$, $Y$ and $Z$.

the curried inverse of X and Y (from the name)

Let $X$ and $Y$ be elements of $\operatorname{Truncated}$ applied to $2$. Then the curried inverse of $X$ and $Y$ is a functor of the set of homotopy categories of $X$ and the set of functors of the set of homotopy categories of $Y$ and the set of homotopy categories of the tensor object of $X$ and $Y$.

the equivalence of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $\operatorname{Truncated}$ applied to $2$. Then the equivalence of $X$ and $Y$ is an equivalence of the set of homotopy categories of the tensor object of $X$ and $Y$ and $\mathrm{Prod}$ applied to the set of homotopy categories of $X$ and the set of homotopy categories of $Y$.

the functor of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $\operatorname{Truncated}$ applied to $2$. Then the functor of $X$ and $Y$ is a functor of the set of homotopy categories of the tensor object of $X$ and $Y$ and $\mathrm{Prod}$ applied to the set of homotopy categories of $X$ and the set of homotopy categories of $Y$ defined as the product of the map homotopy category of the first projection from the product of $X$ and $Y$ and the map homotopy category of the second projection from the product of $X$ and $Y$.

the identity product map homotopy category composition inverse isomorphism of X and g (from the name)

Let $X$ be an element of $\operatorname{Truncated}$ applied to $2$. Let $g$ be a homomorphism of $Y$ and $\mathrm{Y'}$. Then the identity product map homotopy category composition inverse isomorphism of $X$ and $g$ is an isomorphism of the composition of the product of the identity of the set of homotopy categories of $X$ and the map homotopy category of $g$ and the inverse of $X$ and $\mathrm{Y'}$ and the composition of the inverse of $X$ and $Y$ and the map homotopy category of the left whisker of $X$ and $g$.

the inverse of X and Y (from the name)

Let $X$ and $Y$ be elements of $\operatorname{Truncated}$ applied to $2$. Then the inverse of $X$ and $Y$ is a functor of $\mathrm{Prod}$ applied to the set of homotopy categories of $X$ and the set of homotopy categories of $Y$ and the set of homotopy categories of the tensor object of $X$ and $Y$ defined as the action of $\operatorname{uncurry}$ and the curried inverse of $X$ and $Y$.

the inverse composition map homotopy category first component isomorphism of X and Y (from the name)

Let $X$ and $Y$ be elements of $\operatorname{Truncated}$ applied to $2$. Then the inverse composition map homotopy category first component isomorphism of $X$ and $Y$ is an isomorphism of the composition of the inverse of $X$ and $Y$ and the map homotopy category of the first projection from the product of $X$ and $Y$ and the first component of the set of homotopy categories of $X$ and the set of homotopy categories of $Y$.

the inverse composition map homotopy category second component isomorphism of X and Y (from the name)

Let $X$ and $Y$ be elements of $\operatorname{Truncated}$ applied to $2$. Then the inverse composition map homotopy category second component isomorphism of $X$ and $Y$ is an isomorphism of the composition of the inverse of $X$ and $Y$ and the map homotopy category of the second projection from the product of $X$ and $Y$ and the second component of the set of homotopy categories of $X$ and the set of homotopy categories of $Y$.

the isomorphism of X and Y (from the name)

Let $X$ and $Y$ be elements of $\operatorname{Truncated}$ applied to $2$. Then the isomorphism of $X$ and $Y$ is an isomorphism of $\operatorname{of}$ applied to the set of homotopy categories of the tensor object of $X$ and $Y$ and $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to the set of homotopy categories of $X$ and the set of homotopy categories of $Y$.

the map homotopy category product identity composition inverse isomorphism of Y and f (from the name)

Let $Y$ be an element of $\operatorname{Truncated}$ applied to $2$. Let $f$ be a homomorphism of $X$ and $\mathrm{X'}$. Then the map homotopy category product identity composition inverse isomorphism of $Y$ and $f$ is an isomorphism of the composition of the product of the map homotopy category of $f$ and the identity of the set of homotopy categories of $Y$ and the inverse of $\mathrm{X'}$ and $Y$ and the composition of the inverse of $X$ and $Y$ and the map homotopy category of the right whisker of $f$ and $Y$.

the isomorphism terminal of X (from the name)

Let $X$ be an element of $\operatorname{Truncated}$ applied to $2$. Then the isomorphism terminal of $X$ is an isomorphism of $\operatorname{of}$ applied to the set of homotopy categories of $X$ and the chosen terminal defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{isTerminal}$ applied to $X$ and $\operatorname{chosenTerminalIsTerminal}$.

the unit homomorphism equivalence of X (from the name)

Let $X$ be a set. Then the unit homomorphism equivalence of $X$ is an equivalence from the set of homomorphisms of the tensor unity in the monoidal structure of the set of sets and $X$ to the set of functors of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the chosen terminal and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of $\operatorname{hoFunctor}$ and $X$ defined as the composition of the unit homomorphism equivalence of $X$ and the composition of the inverse of the object equivalence and the inverse of $\operatorname{fromChosenTerminalEquiv}$.

the chain complex of X and R (from the name)

Let $X$ be a set. Let $R$ be an element of $C$. Then the chain complex of $X$ and $R$ is a chain complex of $C$ and $\Natural$ defined as the action of the action of the chain complex functor of $C$ and $R$ and $X$.

the chain complex functor of C (from the name)

Let $C$ be a set. Then the chain complex functor of $C$ is a functor of $C$ and the set of functors of the set of sets and the set of chain complexes of $C$ and $\Natural$ defined as the action of the action of the postcomposition and the alternating face map complex of $C$ and the composition of the sigma constant and the whiskering of the set of sets and $C$.

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 chain complex functor of $C$ and the action of the evaluation of the set of sets and $C$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$.

the chain complex map of f and R (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $R$ be an element of $C$. Then the chain complex map of $f$ and $R$ is a homomorphism of the chain complex of $X$ and $R$ and the chain complex of $Y$ and $R$ defined as the map of the action of the chain complex functor of $C$ and $R$ and $f$.

the chain complex cofan of R and n (from the name)

Let $X$ be a set. Let $R$ be an element of $C$. Let $n$ be a natural number. Then the chain complex cofan of $R$ and $n$ is a cofan of the function that maps $x_{2}$ to $R$ defined as $\operatorname{mk}$ applied to $\operatorname{X}$ applied to the chain complex of $X$ and $R$ and $n$ and $\mathrm{SSet\_\_\_u3b9\_ChainComplex}$ applied to $X$.

the simplicial homology with coefficients in X (from the docstring)

Let $X$ be a set. Let $R$ be an element of $C$. Let $n$ be a natural number. Then the simplicial homology with coefficients in $X$ is an element of $C$ defined as the homology of the chain complex of $X$ and $R$ and $n$.

the homology functor of R and n (from the name)

Let $R$ be an element of $C$. Let $n$ be a natural number. Then the homology functor of $R$ and $n$ is a functor of the set of sets and $C$.

the homology map of R and n (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $R$ be an element of $C$. Let $n$ be a natural number. Then the homology map of $R$ and $n$ is a homomorphism of the simplicial homology with coefficients in $X$ and the simplicial homology with coefficients in $Y$ defined as the map of the chain complex map of $f$ and $R$ and $n$.

Let $X$ be a set. Let $R$ be an element of $C$. Let $n$ be a natural number. Then $\operatorname{isColimitChainComplexXCofan}$ applied to $X$, $R$ and $n$ is an element of $\operatorname{IsColimit}$ applied to the chain complex cofan of $R$ and $n$ defined as $\operatorname{coproductIsCoproduct}$ applied to the function that maps $x_{2}$ to $R$.

the inclusion of X and x2 (from the docstring)

Let $X$ be a set. Let $x_{2}$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$. Then the inclusion of $X$ and $x_{2}$ is a homomorphism of $R$ and $\operatorname{X}$ applied to the chain complex of $X$ and $R$ and $n$ defined as the inclusion of the function that maps $x_{3}$ to $R$ and $x_{2}$.

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

Let $X$ be a set. Let $R$ be an element of $C$. Then the homology data of $X$ and $R$ is a homology data of $\operatorname{sc'}$ applied to the chain complex of $X$ and $R$, $1$, $0$ and $0$.

the homology of X and R (from the docstring)

Let $X$ be a set. Let $R$ be an element of $C$. Then the homology of $X$ and $R$ is an isomorphism of the simplicial homology with coefficients in $X$ and the sigma object of the function that maps $x_{2}$ to $R$.

the homology of X and R (from the name)

Let $X$ be a set. Let $R$ be an element of $C$. Then the homology of $X$ and $R$ is a homomorphism of the simplicial homology with coefficients in $X$ and $R$ defined as the composition of the homomorphism of the homology of $X$ and $R$ and $\operatorname{desc}$ applied to the function that maps $x_{2}$ to the identity morphism of $R$.

Let $X$ be a set. Let $R$ be an element of $C$. Then $\operatorname{isColimitCokernelCoforkChainComplexDOneZero}$ applied to $X$ and $R$ is an element of $\operatorname{IsColimit}$ applied to the projection of $\mathrm{SSet\_\_\_u3c0\_\_u2080\_\_\_fromChainComplexXZero}$ applied to $X$ and $R$ and $\mathrm{SSet\_\_\_u3c0\_\_u2080\_\_\_d\_fromChainComplexXZero}$ applied to $X$, $R$ and $1$.

Let $X$ be a set. Let $R$ be an element of $C$. Then $\mathrm{SSet\_\_\_u3c0\_\_u2080\_\_\_fromChainComplexXZero}$ applied to $X$ and $R$ is a homomorphism of $\operatorname{X}$ applied to the chain complex of $X$ and $R$ and $0$ and the sigma object of the function that maps $x_{2}$ to $R$ defined as the map of the action of the sigma constant and $R$ and the type category of $\mathrm{SSet\_\_\_u3c0\_\_u2080\_\_\_mk}$.

the set chain complex 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 set chain complex map of $H$ and $R$ is a homotopy of the chain complex map of $f$ and $R$ and the chain complex map of $g$ and $R$ defined as the chain homotopy of the right whisker of $H$ and the action of the sigma constant and $R$.

the chain complex 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 chain complex map of $H$ and $R$ is a homotopy of the chain complex map of $f$ and $R$ and the chain complex map of $g$ and $R$ defined as the set chain complex map of the simplicial object homotopy of $H$ and $R$.

the chain complex functor object composition map isomorphism of F and R (from the name)

Let $F$ be a functor of $C$ and $D$. Let $R$ be an element of $C$. Then the chain complex functor object composition map isomorphism of $F$ and $R$ is an isomorphism of the composition of the action of the chain complex functor of $C$ and $R$ and the map homological complex of $F$ and $\operatorname{down}$ applied to $\Natural$ and the action of the chain complex functor of $D$ and the action of $F$ and $R$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the associator of the alternating face map complex of $C$ and the map homological complex of $F$ and $\operatorname{down}$ applied to $\Natural$ and the left isomorphism whisker of the action of the whiskering of the set of sets and $C$ and the action of the sigma constant and $R$ and the alternating face map complex composition map homological complex isomorphism of $F$ and the inverse of the associator of the action of the whiskering of $C$ and $D$ and $F$ and the alternating face map complex of $D$ and the right isomorphism whisker of the whiskering right object composition isomorphism of the action of the sigma constant and $R$ and $F$ and the alternating face map complex of $D$ and the right isomorphism whisker of the map isomorphism of the whiskering of the set of sets and $D$ and the sigma constant object composition isomorphism of $F$ and $R$ and the alternating face map complex of $D$.

the cofan normalized chain complex of R and n (from the name)

Let $X$ be a set. Let $R$ be an element of $C$. Let $n$ be a natural number. Then the cofan normalized chain complex of $R$ and $n$ is a cofan of the function that maps $x_{2}$ to $R$ defined as $\operatorname{mk}$ applied to $\operatorname{X}$ applied to the normalized chain complex of $X$ and $R$ and $n$ and the function that maps $x_{2}$ to the inclusion normalized chain complex of $X$ and $x_{2}$.

Let $X$ be a set. Let $R$ be an element of $C$. Then $\operatorname{fromNormalizedChainComplex}$ applied to $X$ and $R$ is a homomorphism of the normalized chain complex of $X$ and $R$ and the chain complex of $X$ and $R$ defined as $\operatorname{fromNondegComplex}$ applied to the map of the canonical splitting of $X$ and the action of the sigma constant and $R$.

the homotopy equivalence normalized chain complex of X and R (from the name)

Let $X$ be a set. Let $R$ be an element of $C$. Then the homotopy equivalence normalized chain complex of $X$ and $R$ is a homotopy equivalence of the chain complex of $X$ and $R$ and the normalized chain complex of $X$ and $R$ defined as $\operatorname{homotopyEquivNondegComplex}$ applied to the map of the canonical splitting of $X$ and the action of the sigma constant and $R$.

Let $X$ be a set. Let $R$ be an element of $C$. Let $n$ be a natural number. Then $\operatorname{isColimitCofanNormalizedChainComplex}$ applied to $X$, $R$ and $n$ is an element of $\operatorname{IsColimit}$ applied to the cofan normalized chain complex of $R$ and $n$.

the normalized chain complex of X and R (from the docstring)

Let $X$ be a set. Let $R$ be an element of $C$. Then the normalized chain complex of $X$ and $R$ is a chain complex of $C$ and $\Natural$ defined as $\operatorname{nondegComplex}$ applied to the map of the canonical splitting of $X$ and the action of the sigma constant and $R$.

the normalized chain complex functor object of R (from the name)

Let $R$ be an element of $C$. Then the normalized chain complex functor object of $R$ is a functor of the set of sets and the set of chain complexes of $C$ and $\Natural$.

the normalized chain complex map of f and R (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $R$ be an element of $C$. Then the normalized chain complex map of $f$ and $R$ is a homomorphism of the normalized chain complex of $X$ and $R$ and the normalized chain complex of $Y$ and $R$ defined as the composition of $\operatorname{fromNormalizedChainComplex}$ applied to $X$ and $R$ and the composition of the chain complex map of $f$ and $R$ and the normalized chain complex of $Y$ and $R$.

the normalized chain complex of X and R (from the name)

Let $X$ be a set. Let $R$ be an element of $C$. Then the normalized chain complex of $X$ and $R$ is a homomorphism of the chain complex of $X$ and $R$ and the normalized chain complex of $X$ and $R$ defined as $\operatorname{toNondegComplex}$ applied to the map of the canonical splitting of $X$ and the action of the sigma constant and $R$.

the normalized chain complex natural transformation of R (from the name)

Let $R$ be an element of $C$. Then the normalized chain complex natural transformation of $R$ is a homomorphism of the action of the chain complex functor of $C$ and $R$ and the normalized chain complex functor object of $R$.

the inclusion normalized chain complex of X and x2 (from the name)

Let $X$ be a set. Let $x_{2}$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$. Then the inclusion normalized chain complex of $X$ and $x_{2}$ is a homomorphism of $R$ and $\operatorname{X}$ applied to the normalized chain complex of $X$ and $R$ and $n$ defined as the composition of the inclusion of $X$ and $x_{2}$ and $\operatorname{f}$ applied to the normalized chain complex of $X$ and $R$ and $n$.

the relative chain complex of P and R (from the docstring)

Let $P$ be a set pair. Let $R$ be an element of $C$. Then the relative chain complex of $P$ and $R$ is a chain complex of $C$ and $\Natural$ defined as the action of the action of the chain complex functor of $C$ and $R$ and $P$.

the chain complex functor of C (from the name)

Let $C$ be a set. Then the chain complex functor of $C$ is a functor of $C$ and the set of functors of the set of set pairs and the set of chain complexes of $C$ and $\Natural$ defined as the cokernel of $\operatorname{chainComplexFunctorLeftToRight}$ applied to $C$.

the left chain complex functor of C (from the name)

Let $C$ be a set. Then the left chain complex functor of $C$ is a functor of $C$ and the set of functors of the set of set pairs 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 composition of $\operatorname{forget}$ and the left function.

Let $C$ be a set. Then $\operatorname{chainComplexFunctorLeftToRight}$ applied to $C$ is a homomorphism of the left chain complex functor of $C$ and the right chain complex functor of $C$ defined as the left whisker of the chain complex functor of $C$ and the map of the left whiskering of the set of sets and the set of chain complexes of $C$ and $\Natural$ and the left whisker of $\operatorname{forget}$ and $\operatorname{leftToRight}$.

the right chain complex functor of C (from the name)

Let $C$ be a set. Then the right chain complex functor of $C$ is a functor of $C$ and the set of functors of the set of set pairs 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 composition of $\operatorname{forget}$ and the right function.

the chain complex functor projection of C (from the name)

Let $C$ be a set. Then the chain complex functor projection of $C$ is a homomorphism of the right chain complex functor of $C$ and the chain complex functor of $C$ defined as the projection of $\operatorname{chainComplexFunctorLeftToRight}$ applied to $C$.

the chain complex map of f and R (from the name)

Let $f$ be a homomorphism of $P$ and $\mathrm{P'}$. Let $R$ be an element of $C$. Then the chain complex map of $f$ and $R$ is a homomorphism of the relative chain complex of $P$ and $R$ and the relative chain complex of $\mathrm{P'}$ and $R$ defined as the map of the action of the chain complex functor of $C$ and $R$ and $f$.

the chain complex short complex of P and R (from the name)

Let $P$ be a set pair. Let $R$ be an element of $C$. Then the chain complex short complex of $P$ and $R$ is a short complex of the set of chain complexes of $C$ and $\Natural$ defined as $\operatorname{mk}$ applied to the chain complex map of the homomorphism of $\operatorname{toComma}$ applied to $P$ and $R$, the chain complex projection of $P$ and $R$ and $\mathrm{SSetPair\_\_chainComplex\_condition}$ applied to $P$ and $R$.

the chain complex projection of P and R (from the name)

Let $P$ be a set pair. Let $R$ be an element of $C$. Then the chain complex projection of $P$ and $R$ is a homomorphism of the chain complex of the right subobject of $\operatorname{toComma}$ applied to $P$ and $R$ and the relative chain complex of $P$ and $R$ defined as the component of the component of the chain complex functor projection of $C$ and $R$ and $P$.

the cokernel cofork chain complex of P and R (from the name)

Let $P$ be a set pair. Let $R$ be an element of $C$. Then the cokernel cofork chain complex of $P$ and $R$ is a cokernel cofork of the chain complex map of the homomorphism of $\operatorname{toComma}$ applied to $P$ and $R$ defined as the projection of the chain complex projection of $P$ and $R$ and $\mathrm{SSetPair\_\_chainComplex\_condition}$ applied to $P$ and $R$.

Let $C$ be a set. Then $\operatorname{cokernelCoforkChainComplexFunctorLeftToRight}$ applied to $C$ is a cokernel cofork of $\operatorname{chainComplexFunctorLeftToRight}$ applied to $C$ defined as the projection of the chain complex functor projection of $C$ and $\mathrm{SSetPair\_\_chainComplexFunctor\_condition}$ applied to $C$.

the cokernel cofork chain complex of R and n (from the name)

Let $P$ be a set pair. Let $R$ be an element of $C$. Let $n$ be a natural number. Then the cokernel cofork chain complex of $R$ and $n$ is a cokernel cofork of $\operatorname{f}$ applied to the chain complex map of the homomorphism of $\operatorname{toComma}$ applied to $P$ and $R$ and $n$ defined as the projection of $\operatorname{f}$ applied to the chain complex projection of $P$ and $R$ and $n$ and $\mathrm{SSetPair\_\_chainComplex\_condition\_f}$ applied to $P$, $R$ and $n$.

the relative simplicial homology with coefficients in P (from the docstring)

Let $P$ be a set pair. Let $R$ be an element of $C$. Let $n$ be a natural number. Then the relative simplicial homology with coefficients in $P$ is an element of $C$ defined as the homology of the relative chain complex of $P$ and $R$ and $n$.

the homology functor of R and n (from the name)

Let $R$ be an element of $C$. Let $n$ be a natural number. Then the homology functor of $R$ and $n$ is a functor of the set of set pairs and $C$.

the homology map of R and n (from the name)

Let $f$ be a homomorphism of $P$ and $\mathrm{P'}$. Let $R$ be an element of $C$. Let $n$ be a natural number. Then the homology map of $R$ and $n$ is a homomorphism of the relative simplicial homology with coefficients in $P$ and the relative simplicial homology with coefficients in $\mathrm{P'}$ defined as the map of the chain complex map of $f$ and $R$ and $n$.

the homology of n and m (from the name)

Let $P$ be a set pair. Let $R$ be an element of $A$. Let $n$ and $m$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Eq} (m + 1 , n)$ and $\mathrm{SSetPair\_\_homology\_u3b4\_\_\_\_auto\_1}$. Then the homology of $n$ and $m$ is a homomorphism of the relative simplicial homology with coefficients in $P$ and the simplicial homology with coefficients in the left subobject of $\operatorname{toComma}$ applied to $P$.

the homology projection of R and n (from the name)

Let $P$ be a set pair. Let $R$ be an element of $C$. Let $n$ be a natural number. Then the homology projection of $R$ and $n$ is a homomorphism of the simplicial homology with coefficients in the right subobject of $\operatorname{toComma}$ applied to $P$ and the relative simplicial homology with coefficients in $P$ defined as the map of the chain complex projection of $P$ and $R$ and $n$.

Let $P$ be a set pair. Let $R$ be an element of $C$. Then $\operatorname{isColimitCokernelCoforkChainComplex}$ applied to $P$ and $R$ is an element of $\operatorname{IsColimit}$ applied to the cokernel cofork chain complex of $P$ and $R$ defined as the forward map of the underlying cocone of $\operatorname{cokernelCoforkChainComplexFunctorLeftToRight}$ applied to $C$ and the composition of the action of the evaluation of $C$ and the set of functors of the set of set pairs and the set of chain complexes of $C$ and $\Natural$ and $R$ and the action of the evaluation of the set of set pairs and the set of chain complexes of $C$ and $\Natural$ and $P$ and $\operatorname{isColimitOfPreserves}$ applied to the composition of the action of the evaluation of $C$ and the set of functors of the set of set pairs and the set of chain complexes of $C$ and $\Natural$ and $R$ and the action of the evaluation of the set of set pairs and the set of chain complexes of $C$ and $\Natural$ and $P$ and $\operatorname{isColimitCokernelCoforkChainComplexFunctorLeftToRight}$ applied to $C$.

Let $C$ be a set. Then $\operatorname{isColimitCokernelCoforkChainComplexFunctorLeftToRight}$ applied to $C$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{cokernelCoforkChainComplexFunctorLeftToRight}$ applied to $C$ defined as $\operatorname{cokernelIsCokernel}$ applied to $\operatorname{chainComplexFunctorLeftToRight}$ applied to $C$.

Let $P$ be a set pair. Let $R$ be an element of $C$. Let $n$ be a natural number. Then $\operatorname{isColimitCokernelCoforkChainComplexX}$ applied to $P$, $R$ and $n$ is an element of $\operatorname{IsColimit}$ applied to the cokernel cofork chain complex of $R$ and $n$ defined as $\operatorname{mapIsColimit}$ applied to the cokernel cofork chain complex of $P$ and $R$, $\operatorname{isColimitCokernelCoforkChainComplex}$ applied to $P$ and $R$ and the evaluation of $\operatorname{down}$ applied to $\Natural$ and $n$.

homotopy of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then a homotopy of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of homotopies of $\operatorname{symm}$ applied to the bottom equivalence and $f$ and $\operatorname{symm}$ applied to the bottom equivalence and $g$.

the simplicial object homotopy of H (from the name)

Let $H$ be a homotopy of $f$ and $g$. Then the simplicial object homotopy of $H$ is a homotopy of $f$ and $g$.

the bottom equivalence (from the name)

The bottom equivalence is an equivalence from the set of relative morphisms of the bottom and $\operatorname{to}$ applied to $\operatorname{isInitialBot}$ and the underlying simplicial set of the bottom to the set of homomorphisms of $X$ and $Y$.

homotopy category of X (from the name)

Let $X$ be a set. Then a homotopy category of $X$ is an element of the function that maps $X$ to the set of homotopy categories of the action of the truncation of $2$ and $X$.

the homomorphism of e (from the name)

Let $e$ be an edge of $x$ and $y$. Then the homomorphism of $e$ is a homomorphism of $\operatorname{mk}$ applied to $x$ and $\operatorname{mk}$ applied to $y$ defined as the morphism in the homotopy category of $\operatorname{toTruncated}$ applied to $e$.

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

the object equivalence (from the name)

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

one truncation of S (from the name)

Let $S$ be an element of $\operatorname{Truncated}$ applied to $2$. Then the one truncations of $S$ are a basic type.

Let $V$ be an element of $\operatorname{Truncated}$ applied to $2$. Then there is a homomorphism relation of the set of free identities of the set of one truncations of $V$.

the map of f (from the name)

Let $f$ be a homomorphism of $S$ and $T$. Then the map of $f$ is an identity prefunctor of the set of one truncations of $S$ and the set of one truncations of $T$.

the nerve equivalence (from the name)

The nerve equivalence is an equivalence from the set of one truncations of the action of the truncation of $2$ and the nerve of $C$ to $C$ defined as the nerve equivalence.

the nerve homomorphism equivalence (from the name)

The nerve homomorphism equivalence is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_nerveEquiv\_\_app}$ applied to $X$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_nerveEquiv\_\_app}$ applied to $Y$ defined as the homomorphism equivalence.

the one truncation of C (from the name)

Let $C$ be a set. Then the one truncation of $C$ is an isomorphism of $\operatorname{of}$ applied to the set of one truncations of the action of the truncation of $2$ and the nerve of $C$ and $\operatorname{of}$ applied to $C$ defined as the isomorphism of the nerve equivalence and the function that maps $x_{1}$ and $x_{2}$ to the nerve homomorphism equivalence.

the natural isomorphism (from the name)

The natural isomorphism is an isomorphism of the composition of the essential data of the nerve functor and the one truncation and $\operatorname{forget}$.

homotopy category of V (from the name)

Let $V$ be an element of $\operatorname{Truncated}$ applied to $2$. Then a homotopy category of $V$ is an element of the function that maps $V$ to the set of quotients of $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_HoRel\_u2082\_}$ applied to $V$.

the morphism in the homotopy category of e (from the docstring)

Let $e$ be an edge of $x$ and $x_{1}$. Then the morphism in the homotopy category of $e$ is a homomorphism of $\operatorname{mk}$ applied to $x$ and $\operatorname{mk}$ applied to $x_{1}$ defined as the map of the quotient functor of $V$ and the homomorphism of $e$.

Let $X$ be an element of $\operatorname{Truncated}$ applied to $2$. Then $\operatorname{isTerminal}$ applied to $X$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{of}$ applied to the set of homotopy categories of $X$ defined as $\operatorname{isTerminalOfUniqueOfIsDiscrete}$.

the lift of obj and map (from the name)

Let $\mathrm{obj}$ be a function from elements of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$ to elements of $D$. Let $\mathrm{map}$ be a function from elements $x_{9}$ of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$ and elements $y$ of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_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 $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_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 $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$, for all elements $x_{2}$ of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$, for all elements $x_{3}$ of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_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 the lift of $\mathrm{obj}$ and $x_{9}$ is a functor of the set of homotopy categories of $V$ and $D$.

Let $x$ be an element of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$. Then $\operatorname{mk}$ applied to $x$ is a homotopy category of $V$ defined as the action of the quotient functor of $V$ and $\operatorname{mk}$ applied to $x$.

the natural isomorphism of iso and x2 (from the name)

Let $\mathrm{iso}$ be a function from elements $x_{2}$ of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$ to isomorphisms of the action of $F$ and $\operatorname{mk}$ applied to $x_{2}$ and the action of $G$ and $\operatorname{mk}$ applied to $x_{2}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{1}$ and $y$ of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$, for all edges $e$ of $x_{1}$ and $y$, the composition of the map of $F$ and the morphism in the homotopy category of $e$ and the homomorphism of $\mathrm{iso}$ applied to $y$ is equal to the composition of the homomorphism of $\mathrm{iso}$ applied to $x_{1}$ and the map of $G$ and the morphism in the homotopy category of $e$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_HomotopyCat\_\_0\_\_\_auto\_150}$. Then the natural isomorphism of $x_{2}$ and $\mathrm{iso}$ is an isomorphism of $F$ and $G$.

the natural transformation of x1 and x3 (from the name)

Let $x_{1}$ be a function from elements $x_{3}$ of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$ to homomorphisms of the action of $F$ and $\operatorname{mk}$ applied to $x_{3}$ and the action of $G$ and $\operatorname{mk}$ applied to $x_{3}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{2}$ and $y$ of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$, for all edges $e$ of $x_{2}$ and $y$, the composition of the map of $F$ and the morphism in the homotopy category of $e$ and $x_{1}$ applied to $y$ is equal to the composition of $x_{1}$ applied to $x_{2}$ and the map of $G$ and the morphism in the homotopy category of $e$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_HomotopyCat\_\_0\_\_\_auto\_137}$. Then the natural transformation of $x_{3}$ and $x_{1}$ is a homomorphism of $F$ and $G$.

the morphism property homomorphism of V (from the name)

Let $V$ be an element of $\operatorname{Truncated}$ applied to $2$. Then the morphism property homomorphism of $V$ is a morphism property of the set of homotopy categories of $V$ defined as the morphism property of the function that maps $e$ to the morphism in the homotopy category of $\operatorname{snd}$ applied to $\operatorname{snd}$ applied to $e$.

the quotient functor of V (from the name)

Let $V$ be an element of $\operatorname{Truncated}$ applied to $2$. Then the quotient functor of $V$ is a functor of the set of free identities of the set of one truncations of $V$ and the set of homotopy categories of $V$ defined as the functor of $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_HoRel\_u2082\_}$ applied to $V$.

Let $x$ be an element of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$. Then $\mathrm{SSet\_\_Truncated\_\_ev01\_u2082\_}$ applied to $x$ is a homomorphism of $\mathrm{SSet\_\_Truncated\_\_ev0\_u2082\_}$ applied to $x$ and $\mathrm{SSet\_\_Truncated\_\_ev1\_u2082\_}$ applied to $x$.

Let $x$ be an element of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$. Then $\mathrm{SSet\_\_Truncated\_\_ev02\_u2082\_}$ applied to $x$ is a homomorphism of $\mathrm{SSet\_\_Truncated\_\_ev0\_u2082\_}$ applied to $x$ and $\mathrm{SSet\_\_Truncated\_\_ev2\_u2082\_}$ applied to $x$.

Let $x$ be an element of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$. Then $\mathrm{SSet\_\_Truncated\_\_ev0\_u2082\_}$ applied to $x$ is an one truncation of $V$ defined as $\operatorname{hom}$ applied to the map of $V$ and the opposite in the inclusion and $x$.

Let $x$ be an element of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$. Then $\mathrm{SSet\_\_Truncated\_\_ev12\_u2082\_}$ applied to $x$ is a homomorphism of $\mathrm{SSet\_\_Truncated\_\_ev1\_u2082\_}$ applied to $x$ and $\mathrm{SSet\_\_Truncated\_\_ev2\_u2082\_}$ applied to $x$.

Let $x$ be an element of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$. Then $\mathrm{SSet\_\_Truncated\_\_ev1\_u2082\_}$ applied to $x$ is an one truncation of $V$ defined as $\operatorname{hom}$ applied to the map of $V$ and the opposite in the inclusion and $x$.

Let $x$ be an element of the action of $V$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$. Then $\mathrm{SSet\_\_Truncated\_\_ev2\_u2082\_}$ applied to $x$ is an one truncation of $V$ defined as $\operatorname{hom}$ applied to the map of $V$ and the opposite in the inclusion and $x$.

$\mathrm{SSet\_\_Truncated\_\_hoFunctor\_u2082\_}$ is a functor of $\operatorname{Truncated}$ applied to $2$ and the set of categories.

the map homotopy category of f (from the name)

Let $f$ be a homomorphism of $V$ and $W$. Then the map homotopy category of $f$ is a functor of the set of homotopy categories of $V$ and the set of homotopy categories of $W$.

$\mathrm{SSet\_\_Truncated\_\_\_u3b4\_0\_u2082\_}$ is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_5}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$.

$\mathrm{SSet\_\_Truncated\_\_\_u3b4\_1\_u2082\_}$ is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_5}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$.

$\mathrm{SSet\_\_Truncated\_\_\_u3b4\_2\_u2082\_}$ is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_5}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$.

the inclusion (from the name)

The inclusion is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$.

the inclusion (from the name)

The inclusion is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$.

the inclusion (from the name)

The inclusion is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{SSet\_\_OneTruncation\_u2082\_\_\_\_proof\_1}$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{SSet\_\_Truncated\_\_\_u3b9\_0\_u2082\_\_\_\_proof\_3}$.

$\operatorname{hoFunctor}$ is a functor of the set of sets and the set of categories.

$\operatorname{isTerminalHoFunctorDeltaZero}$ is an element of $\operatorname{IsTerminal}$ applied to the action of $\operatorname{hoFunctor}$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $0$ defined as $\operatorname{isTerminalOfUniqueOfIsDiscrete}$.

the map homotopy category of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map homotopy category of $f$ is a functor of the set of homotopy categories of $X$ and the set of homotopy categories of $Y$ defined as the map homotopy category of the map of the truncation of $2$ and $f$.

the one truncation (from the name)

The one truncation is a functor of $\operatorname{Truncated}$ applied to $2$ and $\operatorname{ReflQuiv}$.

the horn of n and i (from the name)

Let $n$ be a natural number. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the horn of $n$ and $i$ is a subcomplex of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$.

the constant of k and m (from the name)

Let $n$ be a natural number. Let $i$ and $k$ be elements of $\mathrm{Fin}$ applied to $n + 3$. Let $m$ be an opposite of the set of simplex categories. Then the constant of $k$ and $m$ is an element of the object of the horn of $n + 2$ and $i$ and $m$ defined as $\operatorname{yonedaEquiv}$ applied to the constant of $\operatorname{symm}$ applied to the object equivalence and $k$.

the edge of n (from the docstring)

Let $n$ be a natural number. Let $i$, $a$ and $b$ be elements of $\mathrm{Fin}$ applied to $n + 1$ such that $a \leq b$ and $\FinsetcardMACRoM {\operatorname{insert} (i , \operatorname{insert} (a , \operatorname{singleton} (b)))}\leq n$. Then the edge of $n$ is an element of the action of the underlying simplicial set of the horn of $n$ and $i$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$ defined as the edge of $a$ and $b$.

the edge of a and b (from the name)

Let $n$ be a natural number. Let $i$, $a$ and $b$ be elements of $\mathrm{Fin}$ applied to $n + 1$ such that $a \leq b$. Assume that $3 \leq n$. Then the edge of $a$ and $b$ is an element of the action of the underlying simplicial set of the horn of $n$ and $i$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$.

the face of i and j (from the name)

Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $n + 2$ such that $j \neq i$. Then the face of $i$ and $j$ is an element of the action of the underlying simplicial set of the horn of $n + 1$ and $i$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$.

the face inclusion of i and j (from the name)

Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $n + 1$ such that $j \neq i$. Then the face inclusion of $i$ and $j$ is a homomorphism of the underlying simplicial set of the face of the complement of $\operatorname{singleton}$ applied to $j$ and the underlying simplicial set of the horn of $n$ and $i$ defined as the homomorphism of $\mathrm{SSet\_\_face\_le\_horn}$ applied to $j$, $i$ and $\mathrm{hij}$.

the edge of h (from the docstring)

Assume that $0 < i$. Assume that $i < \operatorname{last} (n)$. Let $j$ be an element of $\mathrm{Fin}$ applied to $n$. Then the edge of $h$ is an element of the action of the underlying simplicial set of the horn of $n$ and $i$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$.

the primitive triangle of i and k (from the name)

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 4$ such that $0 < i < \operatorname{last} (n + 3)$. Let $k$ be a natural number such that $k < n + 2$. Then the primitive triangle of $i$ and $k$ is an element of the action of the underlying simplicial set of the horn of $n + 3$ and $i$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $2$.

the inclusion of i and j (from the name)

Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $n + 2$ such that $j \neq i$. Then the inclusion of $i$ and $j$ is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and the underlying simplicial set of the horn of $n + 1$ and $i$ defined as $\operatorname{symm}$ applied to the Yoneda equivalence and the face of $i$ and $j$.

f is compatible (from the name)

Let $f$ be a function from elements $j$ of $\mathrm{Fin}$ applied to $n + 2$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Neq} (j , i)$ to homomorphisms of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and $X$. Then we can say that $j$ is compatible.

Assume that $f$ is compatible. Then $\operatorname{desc}$ applied to $\mathrm{hf}$ is a homomorphism of the underlying simplicial set of the horn of $n + 1$ and $i$ and $X$ defined as $\operatorname{choose}$ applied to $\mathrm{SSet\_\_horn\_\_IsCompatible\_\_exists\_desc}$ applied to $\mathrm{hf}$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{isColimit}$ applied to $i$ is an element of $\operatorname{IsColimit}$ applied to the map of the linear order of the multicofork of $\operatorname{multicoequalizerDiagram}$ applied to $i$ and the set functor defined as $\operatorname{isColimit'}$ applied to $\operatorname{multicoequalizerDiagram}$ applied to $i$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and the underlying simplicial set of the horn of $2$ and $0$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and the underlying simplicial set of the horn of $2$ and $0$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and the underlying simplicial set of the horn of $2$ and $1$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and the underlying simplicial set of the horn of $2$ and $1$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and the underlying simplicial set of the horn of $2$ and $2$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and the underlying simplicial set of the horn of $2$ and $2$.

Let $x$, $x_{1}$ and $x_{2}$ be homomorphisms of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $2$ and $X$ such that the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $2$ and $x$ is equal to the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $0$ and $x_{2}$, the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $1$ and $x$ is equal to the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $0$ and $x_{1}$ and the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $2$ and $x_{1}$ is equal to the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $2$ and $x_{2}$. Then $\mathrm{SSet\_\_horn\_u2083\_\_u2081\_\_\_desc}$ applied to $x$, $x_{1}$, $x_{2}$, $h$, $h_{1}$ and $h_{2}$ is a homomorphism of the underlying simplicial set of the horn of $3$ and $1$ and $X$ defined as $\operatorname{desc}$ applied to $\operatorname{isColimit}$ applied to $1$ and $\mathrm{SSet\_\_horn\_u2083\_\_u2081\_\_\_desc\_\_multicofork}$ applied to $x$, $x_{1}$, $x_{2}$, $h$, $h_{1}$ and $h_{2}$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $2$ and the underlying simplicial set of the horn of $3$ and $1$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $2$ and the underlying simplicial set of the horn of $3$ and $1$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $2$ and the underlying simplicial set of the horn of $3$ and $1$.

Let $x$, $x_{1}$ and $x_{2}$ be homomorphisms of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $2$ and $X$ such that the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $2$ and $x_{1}$ is equal to the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $1$ and $x_{2}$, the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $2$ and $x$ is equal to the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $0$ and $x_{2}$ and the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $0$ and $x$ is equal to the composition of $\mathrm{CategoryTheory\_\_CosimplicialObject\_\_\_u3b4\_}$ applied to $\operatorname{stdSimplex}$ and $0$ and $x_{1}$. Then $\mathrm{SSet\_\_horn\_u2083\_\_u2082\_\_\_desc}$ applied to $x$, $x_{1}$, $x_{2}$, $h$, $h_{1}$ and $h_{2}$ is a homomorphism of the underlying simplicial set of the horn of $3$ and $2$ and $X$ defined as $\operatorname{desc}$ applied to $\operatorname{isColimit}$ applied to $2$ and $\mathrm{SSet\_\_horn\_u2083\_\_u2082\_\_\_desc\_\_multicofork}$ applied to $x$, $x_{1}$, $x_{2}$, $h$, $h_{1}$ and $h_{2}$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $2$ and the underlying simplicial set of the horn of $3$ and $2$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $2$ and the underlying simplicial set of the horn of $3$ and $2$.

the inclusion (from the docstring)

The inclusion is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $2$ and the underlying simplicial set of the horn of $3$ and $2$.

S is a Kan complex (from the name)

Let $S$ be a set. Then $S$ is a Kan complex, if $S$ is fibrant.

the lift of hf (from the name)

Assume that $f$ is compatible. Then the lift of $\mathrm{hf}$ 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\_of\_kanComplex}$ applied to $\mathrm{hf}$.

Let $X$ be a set. Let $n$ be a natural number. Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$. Then an element of $\operatorname{PtSimplex}$ applied to $X$, $n$ and $x$ is an element of the function that maps $X$, $n$ and $x$ to the set of relative morphisms of the subcomplex of $x$ and the constant of $x$.

Let $f$, $g$ and $\mathrm{fg}$ be elements of $\operatorname{PtSimplex}$ applied to $X$, $n$ and $x$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then the elements of $\operatorname{MulStruct}$ applied to $f$, $g$, $\mathrm{fg}$ and $i$ are a basic type.

the associator of x8 and h1 (from the name)

Let $x_{7}$ be an element of $\operatorname{MulStruct}$ applied to $x_{1}$, $x_{2}$, $x_{4}$ and $i$. Let $x_{8}$ be an element of $\operatorname{MulStruct}$ applied to $x_{2}$, $x_{3}$, $x_{5}$ and $i$. Let $h_{1}$ be an element of $\operatorname{MulStruct}$ applied to $x_{1}$, $x_{5}$, $x_{6}$ and $i$. Then the associator of $x_{8}$ and $h_{1}$ is an element of $\operatorname{MulStruct}$ applied to $x_{4}$, $x_{3}$, $x_{6}$ and $i$.

the associator of x8 and h1 (from the name)

Let $x_{7}$ be an element of $\operatorname{MulStruct}$ applied to $x_{1}$, $x_{2}$, $x_{4}$ and $i$. Let $x_{8}$ be an element of $\operatorname{MulStruct}$ applied to $x_{2}$, $x_{3}$, $x_{5}$ and $i$. Let $h_{1}$ be an element of $\operatorname{MulStruct}$ applied to $x_{4}$, $x_{3}$, $x_{6}$ and $i$. Then the associator of $x_{8}$ and $h_{1}$ is an element of $\operatorname{MulStruct}$ applied to $x_{1}$, $x_{5}$, $x_{6}$ and $i$.

the map of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{MulStruct}$ applied to $f$, $g$, $\mathrm{fg}$ and $i$. Then the map of $\mathrm{self}$ is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n + 1$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the multiplicative one of f and i (from the name)

Let $f$ be an element of $\operatorname{PtSimplex}$ applied to $X$, $n$ and $x$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then the multiplicative one of $f$ and $i$ is an element of $\operatorname{MulStruct}$ applied to $f$, the constant, $f$ and $i$ defined as $\operatorname{relStructSuccEquivMulStruct}$ applied to the identity of $f$ and $\operatorname{succ}$ applied to $i$.

Let $h_{1}$ be an element of $\operatorname{MulStruct}$ applied to the constant, $p$, $q$ and $i$. Then $\operatorname{mulOneEqOfOneMulEq}$ applied to $h_{1}$ is an element of $\operatorname{MulStruct}$ applied to $p$, the constant, $q$ and $i$ defined as $\operatorname{mulOneEqSymm}$ applied to the associator of the multiplicative one of $p$ and $i$ and the one product of $p$ and $i$.

Let $h_{1}$ be an element of $\operatorname{MulStruct}$ applied to $p$, the constant, $q$ and $i$. Then $\operatorname{mulOneEqSymm}$ applied to $h_{1}$ is an element of $\operatorname{MulStruct}$ applied to $q$, the constant, $p$ and $i$ defined as the associator of the multiplicative one of the constant and $i$ and the multiplicative one of $p$ and $i$.

Let $h_{1}$ be an element of $\operatorname{MulStruct}$ applied to $p$, the constant, $q$ and $i$. Let $\mathrm{h'}$ be an element of $\operatorname{MulStruct}$ applied to $q$, the constant, $r$ and $i$. Then $\operatorname{mulOneEqTrans}$ applied to $h_{1}$ and $\mathrm{h'}$ is an element of $\operatorname{MulStruct}$ applied to $p$, the constant, $r$ and $i$ defined as the associator of $h_{1}$ and $\operatorname{oneMulEqOfMulOneEq}$ applied to $\mathrm{h'}$.

the one product of f and i (from the name)

Let $f$ be an element of $\operatorname{PtSimplex}$ applied to $X$, $n$ and $x$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then the one product of $f$ and $i$ is an element of $\operatorname{MulStruct}$ applied to the constant, $f$, $f$ and $i$ defined as $\operatorname{relStructCastSuccEquivMulStruct}$ applied to the identity of $f$ and $\operatorname{castSucc}$ applied to $i$.

Let $h_{1}$ be an element of $\operatorname{MulStruct}$ applied to $p$, the constant, $q$ and $i$. Then $\operatorname{oneMulEqOfMulOneEq}$ applied to $h_{1}$ is an element of $\operatorname{MulStruct}$ applied to the constant, $p$, $q$ and $i$ defined as $\operatorname{oneMulEqSymm}$ applied to the associator of $h_{1}$ and the multiplicative one of $p$ and $i$.

Let $h_{1}$ be an element of $\operatorname{MulStruct}$ applied to the constant, $p$, $q$ and $i$. Then $\operatorname{oneMulEqSymm}$ applied to $h_{1}$ is an element of $\operatorname{MulStruct}$ applied to the constant, $q$, $p$ and $i$ defined as the associator of $h_{1}$ and the one product of $p$ and $i$.

Let $h_{1}$ be an element of $\operatorname{MulStruct}$ applied to the constant, $p$, $q$ and $i$. Let $\mathrm{h'}$ be an element of $\operatorname{MulStruct}$ applied to the constant, $q$, $r$ and $i$. Then $\operatorname{oneMulEqTrans}$ applied to $h_{1}$ and $\mathrm{h'}$ is an element of $\operatorname{MulStruct}$ applied to the constant, $p$, $r$ and $i$ defined as the associator of the multiplicative one of $p$ and $i$ and $\operatorname{mulOneEqOfOneMulEq}$ applied to $\mathrm{h'}$.

the opposite of h and hij (from the name)

Let $h$ be an element of $\operatorname{MulStruct}$ applied to $f$, $g$, $\mathrm{fg}$ and $i$. Assume that $\mathrm{autoParam}$ holds for $\EqtMACRoH {\operatorname{rev} (i)}{j}$ and $\mathrm{SSet\_\_PtSimplex\_\_MulStruct\_\_op\_\_\_auto\_1}$. Then the opposite of $h$ and $\mathrm{hij}$ is an element of $\operatorname{MulStruct}$ applied to the opposite of $g$, the opposite of $f$, the opposite of $\mathrm{fg}$ and $j$.

the opposite of h and hij (from the name)

Let $h$ be an element of $\operatorname{MulStruct}$ applied to the opposite of $g$, the opposite of $f$, the opposite of $\mathrm{fg}$ and $i$. Assume that $\mathrm{autoParam}$ holds for $\EqtMACRoH {\operatorname{rev} (i)}{j}$ and $\mathrm{SSet\_\_PtSimplex\_\_MulStruct\_\_unop\_\_\_auto\_1}$. Then the opposite of $h$ and $\mathrm{hij}$ is an element of $\operatorname{MulStruct}$ applied to $f$, $g$, $\mathrm{fg}$ and $j$.

Let $f$ and $g$ be elements of $\operatorname{PtSimplex}$ applied to $X$, $n$ and $x$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the elements of $\operatorname{RelStruct}$ applied to $f$, $g$ and $i$ are a basic type.

the copy of r (from the name)

Let $r$ be an element of $\operatorname{RelStruct}$ applied to $f$, $g$ and $i$. Assume that $\EqtMACRoH {f}{\mathrm{f'}}$. Assume that $\EqtMACRoH {g}{\mathrm{g'}}$. Then the copy of $r$ is an element of $\operatorname{RelStruct}$ applied to $\mathrm{f'}$, $\mathrm{g'}$ and $i$.

the map of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{RelStruct}$ applied to $f$, $g$ and $i$. Then the map of $\mathrm{self}$ is a homomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n + 1$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Assume that $\EqtMACRoH {f}{g}$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{ofEq}$ applied to $h$ and $i$ is an element of $\operatorname{RelStruct}$ applied to $f$, $g$ and $i$.

the identity of f and i (from the name)

Let $f$ be an element of $\operatorname{PtSimplex}$ applied to $X$, $n$ and $x$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the identity of $f$ and $i$ is an element of $\operatorname{RelStruct}$ applied to $f$, $f$ and $i$.

Let $f$ and $g$ be elements of $\operatorname{PtSimplex}$ applied to $X$, $n$ and $x$. Then an element of $\mathrm{SSet\_\_PtSimplex\_\_RelStruct\_u2080\_}$ applied to $f$ and $g$ is an element of the function that maps $f$ and $g$ to $\operatorname{RelStruct}$ applied to $f$, $g$ and $0$.

the equivalence (from the name)

The equivalence is an equivalence from $\mathrm{SSet\_\_PtSimplex\_\_RelStruct\_u2080\_}$ applied to $f$ and $g$ to the set of edges of $\mathrm{SSet\_\_PtSimplex\_\_equiv\_u2080\_\_\_app}$ applied to $x$ and $g$ and $\mathrm{SSet\_\_PtSimplex\_\_equiv\_u2080\_\_\_app}$ applied to $x$ and $f$.

the equivalence of x (from the name)

Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$. Then the equivalence of $x$ is an equivalence from $\operatorname{PtSimplex}$ applied to $X$, $0$ and $x$ to the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$.

the opposite of f (from the name)

Let $f$ be an element of $\operatorname{PtSimplex}$ applied to $X$, $n$ and $x$. Then the opposite of $f$ is an element of $\operatorname{PtSimplex}$ applied to the opposite of $X$, $n$ and $\operatorname{symm}$ applied to the opposite object equivalence and $x$ defined as $\operatorname{symm}$ applied to the opposite equivalence and $f$.

the opposite equivalence (from the name)

The opposite equivalence is an equivalence from $\operatorname{PtSimplex}$ applied to the opposite of $X$, $n$ and $\operatorname{symm}$ applied to the opposite object equivalence and $x$ to $\operatorname{PtSimplex}$ applied to $X$, $n$ and $x$.

$\operatorname{relStructCastSuccEquivMulStruct}$ is an equivalence from $\operatorname{RelStruct}$ applied to $f$, $g$ and $\operatorname{castSucc}$ applied to $i$ to $\operatorname{MulStruct}$ applied to the constant, $f$, $g$ and $i$.

$\operatorname{relStructSuccEquivMulStruct}$ is an equivalence from $\operatorname{RelStruct}$ applied to $f$, $g$ and $\operatorname{succ}$ applied to $i$ to $\operatorname{MulStruct}$ applied to $g$, the constant, $f$ and $i$.

the opposite of f (from the name)

Let $f$ be an element of $\operatorname{PtSimplex}$ applied to the opposite of $X$, $n$ and $\operatorname{symm}$ applied to the opposite object equivalence and $x$. Then the opposite of $f$ is an element of $\operatorname{PtSimplex}$ applied to $X$, $n$ and $x$ defined as $\operatorname{opEquiv}$ applied to $f$.

the product of A and B (from the name)

Let $A$ be a subcomplex of $X$. Let $B$ be a subcomplex of $Y$. Then the product of $A$ and $B$ is a subcomplex of the tensor object of $X$ and $Y$.

the isomorphism of A and B (from the docstring)

Let $A$ be a subcomplex of $X$. Let $B$ be a subcomplex of $Y$. Then the isomorphism of $A$ and $B$ is an isomorphism of the underlying simplicial set of the product of $A$ and $B$ and the tensor object of the underlying simplicial set of $A$ and the underlying simplicial set of $B$.

the union product of S and T (from the name)

Let $S$ be a subcomplex of $X$. Let $T$ be a subcomplex of $Y$. Then the union product of $S$ and $T$ is a subcomplex of the tensor object of $X$ and $Y$ defined as the maximum of the product of the top and $T$ and the product of $S$ and the top.

the isomorphism of S and T (from the docstring)

Let $S$ be a subcomplex of $X$. Let $T$ be a subcomplex of $Y$. Then the isomorphism of $S$ and $T$ is an isomorphism of the underlying simplicial set of the union product of $S$ and $T$ and the underlying simplicial set of the union product of $T$ and $S$.

the inclusion of S and T (from the docstring)

Let $S$ be a subcomplex of $X$. Let $T$ be a subcomplex of $Y$. Then the inclusion of $S$ and $T$ is a homomorphism of the tensor object of $X$ and the underlying simplicial set of $T$ and the underlying simplicial set of the union product of $S$ and $T$.

the inclusion of S and T (from the docstring)

Let $S$ be a subcomplex of $X$. Let $T$ be a subcomplex of $Y$. Then the inclusion of $S$ and $T$ is a homomorphism of the tensor object of the underlying simplicial set of $S$ and $Y$ and the underlying simplicial set of the union product of $S$ and $T$.

the object (from the docstring)

The object is an element of $\operatorname{IsTerminal}$ applied to the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $0$.

the unit homomorphism equivalence of K (from the name)

Let $K$ be a set. Then the unit homomorphism equivalence of $K$ is an equivalence from the set of homomorphisms of the tensor unity in the monoidal structure of the set of sets and $K$ to the action of $K$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$.

the inclusion (from the docstring)

The inclusion is a homomorphism of $X$ and the tensor object of $X$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ defined as the lift of the identity morphism of $X$ and the constant of $\operatorname{symm}$ applied to the object equivalence and $0$.

the inclusion (from the docstring)

The inclusion is a homomorphism of $X$ and the tensor object of $X$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ defined as the lift of the identity morphism of $X$ and the constant of $\operatorname{symm}$ applied to the object equivalence and $1$.

the nerve of C (from the docstring)

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

the edge of f (from the name)

Let $f$ be a homomorphism of $x_{1}$ and $y$. Then the edge of $f$ is an edge of $\operatorname{symm}$ applied to the nerve equivalence and $x_{1}$ and $\operatorname{symm}$ applied to the nerve equivalence and $y$.

the homomorphism equivalence (from the name)

The homomorphism equivalence is an equivalence from the set of edges of $x_{1}$ and $y$ to the set of homomorphisms of $\operatorname{nerveEquiv}$ applied to $x_{1}$ and $\operatorname{nerveEquiv}$ applied to $y$.

Let $x$ be a set. Let $e$ be an order isomorphism of $x$ and $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{representableBy}$ applied to $x$ and $e$ is an element of $\operatorname{RepresentableBy}$ applied to the nerve of $x$ and $\operatorname{mk}$ applied to $n$.

the nerve equivalence (from the name)

The nerve equivalence is an equivalence from the set of composable arrows of $C$ and $0$ to $C$.

the nerve (from the docstring)

The nerve is a functor of the set of categories and the set of sets.

the nerve map of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the nerve map of $F$ is a homomorphism of the nerve of $C$ and the nerve of $D$.

the functor (from the docstring)

The functor is a functor of the set of part orders and the set of sets.

the fully faithful nerve functor (from the name)

the functor of x2 (from the docstring)

Let $x_{2}$ be a homomorphism of the action of the essential data of the nerve functor and $\operatorname{of}$ applied to $C$ and the action of the essential data of the nerve functor and $\operatorname{of}$ applied to $D$. Then the functor of $x_{2}$ is a functor of $C$ and $D$.

the adjunction between the nerve functor and the homotopy category functor (from the docstring)

The adjunction between the nerve functor and the homotopy category functor is an adjunction of $\operatorname{hoFunctor}$ and the nerve defined as the adjunction of the composition of $\operatorname{coskAdj}$ applied to $2$ and the nerve adjoint and the inverse of $\mathrm{CategoryTheory\_\_Nerve\_\_cosk\_u2082\_Iso}$.

$\operatorname{fullyfaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the nerve defined as $\operatorname{ofFullyFaithful}$ applied to the nerve.

$\operatorname{nerveFunctorCompHoFunctorIso}$ is an isomorphism of the composition of the nerve and $\operatorname{hoFunctor}$ and the identity of the set of categories defined as $\operatorname{asIso}$ applied to the counit of the adjunction between the nerve functor and the homotopy category functor.

Let $x_{1}$ be a homomorphism of $X$ and the action of the truncation of $2$ and the nerve of $C$. Then $\operatorname{descOfTruncation}$ applied to $x_{1}$ is a functor of the set of homotopy categories of $X$ and $C$.

the functor equivalence (from the name)

The functor equivalence is an equivalence from the set of functors of the set of homotopy categories of $X$ and $C$ to the set of homomorphisms of $X$ and the action of the truncation of $2$ and the nerve of $C$.

the homomorphism to nerve of F (from the name)

Let $F$ be a functor of the set of homotopy categories of $X$ and $C$. Then the homomorphism to nerve of $F$ is a homomorphism of $X$ and the action of the truncation of $2$ and the nerve of $C$.

the lift of x1 and hY (from the name)

Let $x$ 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{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ to elements of the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$. Let $x_{1}$ be a function from elements of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$ to elements of the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$ such that for all elements $x_{5}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$, $x$ applied to $\operatorname{hom}$ applied to the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $1$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_14}$ and $x_{5}$ is equal to $\operatorname{hom}$ applied to the map of $Y$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $1$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_14}$ and $x_{1}$ applied to $x_{5}$, for all elements $x_{4}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$, $x$ applied to $\operatorname{hom}$ applied to the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $0$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_14}$ and $x_{4}$ is equal to $\operatorname{hom}$ applied to the map of $Y$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $0$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_14}$ and $x_{1}$ applied to $x_{4}$, for all elements $x_{3}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_15}$, for all elements $y$ of the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $2$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_15}$, if $x_{1}$ applied to $\operatorname{hom}$ applied to the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $2$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_16}$ and $x_{3}$ is equal to $\operatorname{hom}$ applied to the map of $Y$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $2$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_16}$ and $y$, then if $x_{1}$ applied to $\operatorname{hom}$ applied to the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $0$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_16}$ and $x_{3}$ is equal to $\operatorname{hom}$ applied to the map of $Y$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $0$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_16}$ and $y$, then $x_{1}$ applied to $\operatorname{hom}$ applied to the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $1$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_16}$ and $x_{3}$ is equal to $\operatorname{hom}$ applied to the map of $Y$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $1$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_16}$ and $y$ and 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{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$, $x_{1}$ applied to $\operatorname{hom}$ applied to the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3c3\_\_u2082\_}$ applied to $0$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_14}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ and $x_{2}$ is equal to $\operatorname{hom}$ applied to the map of $Y$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3c3\_\_u2082\_}$ applied to $0$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_14}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ and $x$ applied to $x_{2}$. Let $\mathrm{hY}$ be an element of $\operatorname{StrictSegal}$ applied to $Y$. Then the lift of $x_{1}$ and $\mathrm{hY}$ is a homomorphism of $X$ and $Y$.

the naturality property of x1 and hY (from the name)

Let $x$ 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{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ to elements of the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $0$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$. Let $x_{1}$ be a function from elements of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$ to elements of the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$ such that for all elements $x_{3}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$, $x$ applied to $\operatorname{hom}$ applied to the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $1$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_14}$ and $x_{3}$ is equal to $\operatorname{hom}$ applied to the map of $Y$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $1$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_14}$ and $x_{1}$ applied to $x_{3}$ and for all elements $x_{2}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $1$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_13}$, $x$ applied to $\operatorname{hom}$ applied to the map of $X$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $0$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_14}$ and $x_{2}$ is equal to $\operatorname{hom}$ applied to the map of $Y$ and the opposite in $\mathrm{SimplexCategory\_\_Truncated\_\_\_u3b4\_\_u2082\_}$ applied to $0$, $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_12}$ and $\mathrm{\_private\_\_Mathlib\_\_AlgebraicTopology\_\_SimplicialSet\_\_NerveAdjunction\_\_0\_\_\_proof\_14}$ and $x_{1}$ applied to $x_{2}$. Let $\mathrm{hY}$ be an element of $\operatorname{StrictSegal}$ applied to $Y$. Then the naturality property of $x_{1}$ and $\mathrm{hY}$ is a morphism property of $\operatorname{Truncated}$ applied to $2$ defined as the opposite of the naturality property of $\operatorname{liftOfStrictSegal}$ applied to $x$, $x_{1}$, $h$, $h_{1}$ and $\mathrm{hY}$.

the nerve adjoint (from the name)

The nerve adjoint is an adjunction of $\mathrm{SSet\_\_Truncated\_\_hoFunctor\_u2082\_}$ and the essential data of the nerve functor.

the equivalence function (from the name)

The equivalence function is an equivalence from the action of the nerve of the set of codiscretes of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ to the set of functions from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $X$.

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

the cast of s and hd (from the name)

Let $s$ be an element of $\operatorname{N}$ applied to $X$ such that the dimension of the simplex of $\operatorname{toS}$ applied to $s$ is equal to $d$. Then the cast of $s$ and $\mathrm{hd}$ is an element of $\operatorname{N}$ applied to $X$.

the induction of mk and n (from the name)

Let $\mathrm{mk}$ be a function from natural numbers $n$ and elements $x$ of $\operatorname{nonDegenerate}$ applied to $X$ and $n$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $x$ and $\operatorname{property}$ applied to $x$. Let $s$ be an element of $\operatorname{N}$ applied to $X$. Then the induction of $n$ and $x$ is an element of $\mathrm{motive}$ applied to $s$ defined as the function that maps $\mathrm{mk}$ and $s$ to $n$ applied to the dimension of the simplex of $\operatorname{toS}$ applied to $x$, the simplex of $\operatorname{toS}$ applied to $x$, $\mathrm{mk}$ and $s$.

Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ such that $\MembershipmemMACRoT {\operatorname{nonDegenerate} (X , n)}{x}$. Then $\operatorname{mk}$ applied to $x$ and $\mathrm{hx}$ is an element of $\operatorname{N}$ applied to $X$ defined as $\operatorname{mk'}$ applied to $\operatorname{mk}$ applied to $x$ and $\mathrm{hx}$.

the opposite equivalence (from the name)

The opposite equivalence is an order isomorphism of $\operatorname{N}$ applied to the opposite of $X$ and $\operatorname{N}$ applied to $X$.

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 $\operatorname{N}$ applied to $X$ and $\operatorname{N}$ applied to $Y$.

Let $x$ be an element of $\operatorname{S}$ applied to $X$. Then $\operatorname{toN}$ applied to $x$ is an element of $\operatorname{N}$ applied to $X$.

the projection of x (from the name)

Let $x$ be an element of $\operatorname{S}$ applied to $X$. Then the projection of $x$ is a homomorphism of $\operatorname{mk}$ applied to the dimension of the simplex of $x$ and $\operatorname{mk}$ applied to the dimension of the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to $x$.

the order embedding of X (from the name)

Let $X$ be a set. Then the order embedding of $X$ is an order embedding of $\operatorname{N}$ applied to $X$ and the set of subcomplexes of $X$.

the cocone of X (from the name)

Let $X$ be a set. Then the cocone of $X$ is a cocone of the functor of $X$.

the functor of X (from the name)

Let $X$ be a set. Then the functor of $X$ is a functor of $\operatorname{N}$ applied to $X$ and the set of sets.

Let $X$ be a set. Then $\operatorname{isColimitCoconeN}$ applied to $X$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $X$.

Let $A$ be a subcomplex of $X$. Then the elements of $\operatorname{N}$ applied to $A$ are a basic type.

the cast of s and hd (from the name)

Let $s$ be an element of $\operatorname{N}$ applied to $A$ such that the dimension of the simplex of $\operatorname{toS}$ applied to $\operatorname{toN}$ applied to $s$ is equal to $d$. Then the cast of $s$ and $\mathrm{hd}$ is an element of $\operatorname{N}$ applied to $A$.

Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ such that $\MembershipmemMACRoT {\operatorname{nonDegenerate} (X , n)}{x}$ and $x$ is not an element of the object of $A$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$. Then $\operatorname{mk}$ applied to $x$, $\mathrm{hx}$ and $\mathrm{hx'}$ is an element of $\operatorname{N}$ applied to $A$ defined as $\operatorname{mk'}$ applied to $\operatorname{mk'}$ applied to $\operatorname{mk}$ applied to $x$ and $\mathrm{hx}$ and $\mathrm{hx'}$.

the opposite equivalence (from the name)

The opposite equivalence is an order isomorphism of $\operatorname{N}$ applied to the opposite of $A$ and $\operatorname{N}$ applied to $A$.

the order isomorphism of e and hA (from the name)

Let $e$ be an isomorphism of $X$ and $Y$ such that the preimage of $B$ and the homomorphism of $e$ is equal to $A$. Then the order isomorphism of $e$ and $\mathrm{hA}$ is an order isomorphism of $\operatorname{N}$ applied to $A$ and $\operatorname{N}$ applied to $B$.

X is nonempty (from the name)

Let $X$ be a set. Then $X$ is nonempty, if $\mathrm{Nonempty}$ holds for the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$.

Assume that $X$ is not nonempty. Then $\operatorname{isInitialOfNotNonempty}$ applied to $\mathrm{hX}$ is an element of $\operatorname{IsInitial}$ applied to $X$.

Assume that $x \leq y$. Then $\operatorname{monoOfLE}$ applied to $h_{1}$ is a homomorphism of $\operatorname{mk}$ applied to the dimension of the simplex of $\operatorname{toS}$ applied to $x$ and $\operatorname{mk}$ applied to the dimension of the simplex of $\operatorname{toS}$ applied to $y$.

X is nonsingular (from the name)

Let $X$ be a set. Then we can say that $X$ is nonsingular.

the isomorphism of x and hx (from the name)

Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ such that $\MembershipmemMACRoT {\operatorname{nonDegenerate} (X , n)}{x}$. Then the isomorphism of $x$ and $\mathrm{hx}$ is an isomorphism of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and the underlying simplicial set of the subcomplex of $x$ defined as $\operatorname{asIso}$ applied to the simplex of $x$.

the semi simplex category of X (from the name)

Let $X$ be a set. Then the semi simplex category of $X$ is a functor of $\operatorname{N}$ applied to $X$ and the set of semi simplex categories.

the cocone of X (from the name)

Let $X$ be a set. Then the cocone of $X$ is a cocone of the functor of $X$.

the functor of X (from the docstring)

Let $X$ be a set. Then the functor of $X$ is a functor of $\operatorname{N}$ applied to $X$ and the set of sets defined as the composition of the semi simplex category of $X$ and the composition of the simplex category and $\operatorname{stdSimplex}$.

the isomorphism of X (from the docstring)

Let $X$ be a set. Then the isomorphism of $X$ is an isomorphism of the functor of $X$ and the functor of $X$.

Let $X$ be a set. Then $\operatorname{isColimitCoconeN'}$ applied to $X$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $X$.

the opposite of X (from the name)

Let $X$ be a set. Then the opposite of $X$ is a set defined as the action of the opposite functor and $X$.

the opposite equivalence (from the name)

The opposite equivalence is an equivalence of the set of sets and the set of sets.

the opposite functor (from the name)

The opposite functor is a functor of the set of sets and the set of sets defined as the opposite functor.

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 sets.

the opposite object equivalence (from the name)

The opposite object equivalence is an equivalence from the action of the opposite of $X$ and $n$ to the action of $X$ and $n$ defined as the identity of the action of the opposite of $X$ and $n$.

path of X and n (from the name)

Let $X$ be a set. Let $n$ be a natural number. Then a path of $X$ and $n$ is an element of the function that maps $X$ and $n$ to the set of paths of the action of the truncation of $1$ and $X$ and $n$.

the arrow of f and i (from the name)

Let $f$ be a path of $X$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then the arrow of $f$ and $i$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$ defined as the arrow of $f$ and $i$.

the interval of j and l (from the name)

Let $f$ be a path of $X$ and $n$. Let $j$ and $l$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (j + l , n)$ and $\mathrm{SSet\_\_Path\_\_interval\_\_\_auto\_1}$. Then the interval of $j$ and $l$ is a path of $X$ and $l$ defined as the interval of $j$ and $l$.

the map of f and x (from the name)

Let $f$ be a path of $X$ and $n$. Let $x$ be a homomorphism of $X$ and $Y$. Then the map of $f$ and $x$ is a path of $Y$ and $n$ defined as the map of $f$ and the map of the truncation of $1$ and $x$.

the vertex of f and i (from the name)

Let $f$ be a path of $X$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the vertex of $f$ and $i$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ defined as the vertex of $f$ and $i$.

the lift path of A and p (from the name)

Let $A$ be a subcomplex of $X$. Let $p$ be a path of $X$ and $n$ such that for all elements $j_{1}$ of $\mathrm{Fin}$ applied to $n + 1$, the vertex of $p$ and $j_{1}$ is an element of the object of $A$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and for all elements $j$ of $\mathrm{Fin}$ applied to $n$, the arrow of $p$ and $j$ is an element of the object of $A$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$. Then the lift path of $A$ and $p$ is a path of the underlying simplicial set of $A$ and $n$.

path of X and m (from the name)

Let $X$ be an element of $\operatorname{Truncated}$ applied to $n + 1$. Let $m$ be a natural number. Then the paths of $X$ and $m$ are a basic type.

the arrow of f and i (from the name)

Let $f$ be a path of $X$ and $m$. Let $i$ be an element of $\mathrm{Fin}$ applied to $m$. Then the arrow of $f$ and $i$ 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\_\_Path\_\_arrow\_\_\_proof\_2}$ defined as the arrow of $f$ and $i$.

the interval of j and l (from the name)

Let $f$ be a path of $X$ and $m$. Let $j$ and $l$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (j + l , m)$ and $\mathrm{SSet\_\_Truncated\_\_Path\_\_interval\_\_\_auto\_1}$. Then the interval of $j$ and $l$ is a path of $X$ and $l$.

the map of f and x (from the name)

Let $f$ be a path of $X$ and $m$. Let $x$ be a homomorphism of $X$ and $Y$. Then the map of $f$ and $x$ is a path of $Y$ and $m$.

Let $p$ and $q$ be paths of $X$ and $1$ such that the vertex of $p$ and $1$ is equal to the vertex of $q$ and $0$. Then $\mathrm{SSet\_\_Truncated\_\_Path\_\_mk\_u2082\_}$ applied to $p$, $q$ and $h$ is a path of $X$ and $2$.

the vertex of f and i (from the name)

Let $f$ be a path of $X$ and $m$. Let $i$ be an element of $\mathrm{Fin}$ applied to $m + 1$. Then the vertex of $f$ and $i$ 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\_\_Path\_\_vertex\_\_\_proof\_2}$ defined as the vertex of $f$ and $i$.

path of X and n (from the name)

Let $X$ be an element of $\operatorname{Truncated}$ applied to $1$. Let $n$ be a natural number. Then the paths of $X$ and $n$ are a basic type.

the arrow of self and x (from the name)

Let $\mathrm{self}$ be a path of $X$ and $n$. Let $x$ be an element of $\mathrm{Fin}$ applied to $n$. Then the arrow of $\mathrm{self}$ 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\_\_Path\_u2081\_\_\_\_proof\_2}$ defined as $\mathrm{SSet\_\_Truncated\_\_Path\_u2081\_\_\_proj1}$ applied to $\mathrm{self}$ and $x$.

the vertex of self and x (from the name)

Let $\mathrm{self}$ be a path of $X$ and $n$. Let $x$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the vertex of $\mathrm{self}$ and $x$ 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\_\_Path\_u2081\_\_\_\_proof\_1}$ defined as $\mathrm{SSet\_\_Truncated\_\_Path\_u2081\_\_\_proj0}$ applied to $\mathrm{self}$ and $x$.

the spine of m and x (from the name)

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

the spine identity of i (from the name)

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 3$ such that $0 < i < \operatorname{last} (n + 2)$. Then the spine identity of $i$ is a path of the underlying simplicial set of the horn of $n + 2$ and $i$ and $n + 2$.

the spine of n and x (from the name)

Let $X$ be a set. Let $n$ be a natural number. Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$. Then the spine of $n$ and $x$ is a path of $X$ and $n$.

the spine identity of n (from the name)

Let $n$ be a natural number. Then the spine identity of $n$ is a path of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $n$ and $n$ defined as the spine of $n$ and $\operatorname{symm}$ applied to the object equivalence and the identity morphism of the opposite of $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$.

X is connected (from the name)

Let $X$ be a set. Then we can say that $X$ is connected.

X is preconnected (from the name)

Let $X$ be a set. Then $X$ is preconnected, if the set of projections of $X$ is a subsingleton.

the cofork projection (from the name)

The cofork projection is a cofork of $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_}$ applied to $X$ and $1$ and $\mathrm{CategoryTheory\_\_SimplicialObject\_\_\_u3b4\_}$ applied to $X$ and $0$.

the cofork projection functor (from the name)

The cofork projection functor is a cofork of the map of the evaluation and the opposite in $\mathrm{SimplexCategory\_\_\_u3b4\_}$ applied to $1$ and the map of the evaluation and the opposite in $\mathrm{SimplexCategory\_\_\_u3b4\_}$ applied to $0$.

$\mathrm{SSet\_\_isColimitCofork\_u3c0\_\_u2080\_}$ is an element of $\operatorname{IsColimit}$ applied to the cofork projection.

the functor (from the docstring)

The functor is an element of $\operatorname{IsColimit}$ applied to the cofork projection functor.

the map of f and x (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be a projection of $X$. Then the map of $f$ and $x$ is a projection of $Y$.

the projection natural transformation (from the name)

The projection natural transformation is a homomorphism of the action of the evaluation and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and the projection functor.

projection of X (from the name)

Let $X$ be a set. Then a projection of $X$ is an element of the function that maps $X$ to $\mathrm{Quot}$ applied to $\mathrm{SSet\_\_\_u3c0\_\_u2080\_Rel}$.

the lift of f and x (from the name)

Let $f$ be a function from elements of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ to elements of $T$ such that for all elements $x_{1}$ and $x_{2}$ of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$, for all edges $x_{3}$ of $x_{1}$ and $x_{2}$, $\EqtMACRoH {f (x_{1})}{f (x_{2})}$. Let $x$ be a projection of $X$. Then the lift of $f$ and $x$ is an element of $T$.

Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$. Then $\mathrm{SSet\_\_\_u3c0\_\_u2080\_\_\_mk}$ applied to $x$ is a projection of $X$ defined as $\operatorname{mk}$ applied to $\mathrm{SSet\_\_\_u3c0\_\_u2080\_Rel}$ and $x$.

the projection functor (from the name)

The projection functor is a functor of the set of sets and the set of sets.

Let $x$ and $x_{1}$ be elements of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$. Then $\mathrm{SSet\_\_\_u3c0\_\_u2080\_Rel}$ holds for $x$ and $x_{1}$, if $\mathrm{Nonempty}$ holds for the set of edges of $x$ and $x_{1}$.

the isomorphism nerve of p and q (from the name)

Let $p$ and $q$ be natural numbers. Then the isomorphism nerve of $p$ and $q$ is an isomorphism of the tensor object of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $p$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $q$ and the nerve of $\mathrm{ULift}$ applied to $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $p + 1$ and $\mathrm{Fin}$ applied to $q + 1$.

the object equivalence (from the name)

The object equivalence is an equivalence from the tensor object of the action of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $p$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ and the action of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $q$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$ to the set of order homomorphisms of $\mathrm{Fin}$ applied to $n + 1$ and $\mathrm{Prod}$ applied to $\mathrm{Fin}$ applied to $p + 1$ and $\mathrm{Fin}$ applied to $q + 1$.

the order homomorphism of x and hm (from the name)

Let $x$ be an element of the action of the tensor object of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $p$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $q$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $n$. Assume that $p + q = m$. Then the order homomorphism of $x$ and $\mathrm{hm}$ is an order homomorphism of $\mathrm{Fin}$ applied to $n + 1$ and $\mathrm{Fin}$ applied to $m + 1$.

Let $j$ be an element of $\mathrm{Fin}$ applied to $p + 2$. Then $\mathrm{SSet\_\_prodStdSimplex\_u2081\_\_\_codimOneSimplex}$ applied to $j$ is an element of $\operatorname{nonDegenerate}$ applied to the tensor object of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $p$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and $p$ defined as $\ProdmkMACRoU {\operatorname{objMk} (\operatorname{id})}{\mathrm{SSet\_\_stdSimplex\_\_objMk\_u2081\_} (j)}$.

the filtration of j (from the docstring)

Let $j$ be an element of $\mathrm{Fin}$ applied to $p + 1$. Then the filtration of $j$ is a subcomplex of the tensor object of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $p$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ defined as the supremum of the function that maps $i$ to the subcomplex of $\mathrm{SSet\_\_prodStdSimplex\_u2081\_\_\_nonDegenerateEquiv\_\_app}$ applied to $i$.

Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $p + 1$. Then $\mathrm{SSet\_\_prodStdSimplex\_u2081\_\_\_intersectionNondeg}$ applied to $i$ and $j$ is a subcomplex of the tensor object of the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $p$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ defined as the minimum of the subcomplex of $\mathrm{SSet\_\_prodStdSimplex\_u2081\_\_\_nonDegenerateEquiv\_\_app}$ applied to $i$ and the subcomplex of $\mathrm{SSet\_\_prodStdSimplex\_u2081\_\_\_nonDegenerateEquiv\_\_app}$ applied to $j$.

the non degenerate equivalence (from the name)

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

the pushout object object of S and T (from the name)

Let $S$ be a subcomplex of $X$. Let $T$ be a subcomplex of $Y$. Then the pushout object object of $S$ and $T$ is a pushout object object of the inclusion of $S$ and the inclusion of $T$.

the inclusion of S and T (from the docstring)

Let $S$ be a subcomplex of $X$. Let $T$ be a subcomplex of $Y$. Then the inclusion of $S$ and $T$ is an isomorphism of $\operatorname{mk}$ applied to the inclusion of the union product of $S$ and $T$ and the action of the action of the pushout product and $\operatorname{mk}$ applied to the inclusion of $S$ and $\operatorname{mk}$ applied to the inclusion of $T$.

relative morphism of B and x (from the name)

Let $A$ be a subcomplex of $X$. Let $B$ be a subcomplex of $Y$. Let $x$ be a homomorphism of the underlying simplicial set of $A$ and the underlying simplicial set of $B$. Then the relative morphisms of $B$ and $x$ are a basic type.

homotopy of f and g (from the name)

Let $f$ and $g$ be relative morphisms of $B$ and $x$. Then the homotopies of $f$ and $g$ are a basic type.

Let $\mathrm{self}$ be a homotopy of $f$ and $g$. Then $\operatorname{h}$ applied to $\mathrm{self}$ is a homomorphism of the tensor object of $X$ and the action of $\operatorname{stdSimplex}$ and $\operatorname{mk}$ applied to $1$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the homotopy of h (from the name)

Assume that $\EqtMACRoH {f}{g}$. Then the homotopy of $h$ is a homotopy of $f$ and $g$.

the postcomposition of h and fac (from the name)

Let $h$ be a homotopy of $f$ and $g$. Let $\mathrm{f'}$ be a relative morphism of $C$ and $x_{1}$. Assume that the composition of $x$ and $x_{1}$ is equal to $x_{2}$. Then the postcomposition of $h$ and $\mathrm{f'}$ is a homotopy of the composition of $f$ and $\mathrm{f'}$ and the composition of $g$ and $\mathrm{f'}$.

the precomposition of h and f (from the name)

Let $h$ be a homotopy of $\mathrm{f'}$ and $\mathrm{g'}$. Let $f$ be a relative morphism of $B$ and $x$. Assume that the composition of $x$ and $x_{1}$ is equal to $x_{2}$. Then the precomposition of $h$ and $f$ is a homotopy of the composition of $f$ and $\mathrm{f'}$ and the composition of $f$ and $\mathrm{g'}$.

the identity of f (from the name)

Let $f$ be a relative morphism of $B$ and $x$. Then the identity of $f$ is a homotopy of $f$ and $f$.

homotopy class of B and x (from the name)

Let $A$ be a subcomplex of $X$. Let $B$ be a subcomplex of $Y$. Let $x$ be a homomorphism of the underlying simplicial set of $A$ and the underlying simplicial set of $B$. Then a homotopy class of $B$ and $x$ is an element of the function that maps $A$, $B$ and $x$ to $\mathrm{Quot}$ applied to the function that maps $f$ and $g$ to $\mathrm{Nonempty}$ applied to the set of homotopies of $f$ and $g$.

the postcomposition of h and fac (from the name)

Let $h$ be a homotopy class of $B$ and $x$. Let $\mathrm{f'}$ be a relative morphism of $C$ and $x_{1}$. Assume that the composition of $x$ and $x_{1}$ is equal to $x_{2}$. Then the postcomposition of $h$ and $\mathrm{f'}$ is a homotopy class of $C$ and $x_{2}$.

the precomposition of h and fac (from the name)

Let $h$ be a homotopy class of $C$ and $x_{1}$. Let $\mathrm{f'}$ be a relative morphism of $B$ and $x$. Assume that the composition of $x$ and $x_{1}$ is equal to $x_{2}$. Then the precomposition of $h$ and $\mathrm{f'}$ is a homotopy class of $C$ and $x_{2}$.

the composition of f and fac (from the name)

Let $f$ be a relative morphism of $B$ and $x$. Let $\mathrm{f'}$ be a relative morphism of $C$ and $x_{1}$. Assume that the composition of $x$ and $x_{1}$ is equal to $x_{2}$. Then the composition of $f$ and $\mathrm{f'}$ is a relative morphism of $C$ and $x_{2}$.

the constant (from the name)

The constant is a relative morphism of the subcomplex of $y$ and $x$.

the homotopy class of f (from the docstring)

Let $f$ be a relative morphism of $B$ and $x$. Then the homotopy class of $f$ is a homotopy class of $B$ and $x$ defined as $\operatorname{mk}$ applied to the function that maps $f_{1}$ and $g$ to $\mathrm{Nonempty}$ applied to the set of homotopies of $f_{1}$ and $g$ and $f$.

the map of self (from the name)

Let $\mathrm{self}$ be a relative morphism of $B$ and $x$. Then the map of $\mathrm{self}$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the relative morphism of x and y (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$. Let $y$ be an element of the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ such that $\operatorname{hom}$ applied to the component of $f$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $0$ and $x$ is equal to $y$. Then the relative morphism of $x$ and $y$ is a relative morphism of the subcomplex of $y$ and the constant of $y$.

the pair of A (from the name)

Let $A$ be a subcomplex of $X$. Then the pair of $A$ is a set pair defined as $\operatorname{of}$ applied to the inclusion of $A$.

the pair functor of X (from the name)

Let $X$ be a set. Then the pair functor of $X$ is a functor of the set of subcomplexes of $X$ and the set of set pairs.

the pair of X (from the name)

Let $X$ be a set. Then the pair of $X$ is a set pair defined as the pair of the bottom.

the functor (from the docstring)

The functor is a functor of the set of sets and the set of set pairs.

set pair (from the name)

A set pair is an arrow of the top and the top.

$\operatorname{forget}$ is a functor of the set of set pairs and the set of arrows of the set of sets defined as the forgetful functor from the full subcategory of the monomorphism of the set of sets.

the homomorphism of left and right (from the name)

Let $\mathrm{left}$ be a homomorphism of the left subobject of $\operatorname{toComma}$ applied to $X$ and the left subobject of $\operatorname{toComma}$ applied to $Y$. Let $\mathrm{right}$ be a homomorphism of the right subobject of $\operatorname{toComma}$ applied to $X$ and the right subobject of $\operatorname{toComma}$ applied to $Y$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $\mathrm{left}$ and the homomorphism of $\operatorname{toComma}$ applied to $Y$ is equal to the composition of the homomorphism of $\operatorname{toComma}$ applied to $X$ and $\mathrm{right}$ and $\mathrm{SSetPair\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $\mathrm{left}$ and $\mathrm{right}$ is a homomorphism of $X$ and $Y$.

Let $i$ be a homomorphism of $X$ and $Y$. Then $\operatorname{of}$ applied to $i$ is a set pair defined as $\operatorname{mk}$ applied to $i$ and $h$.

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

the cast of s and hd (from the name)

Let $s$ be an element of $\operatorname{S}$ applied to $X$ such that the dimension of the simplex of $s$ is equal to $d$. Then the cast of $s$ and $\mathrm{hd}$ is an element of $\operatorname{S}$ applied to $X$.

the dimension of the simplex of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{S}$ applied to $X$. Then the dimension of the simplex of $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the equivalence element (from the name)

The equivalence element is an equivalence from $\operatorname{S}$ applied to $X$ to the set of elements of $X$.

the equivalence of e (from the name)

Let $e$ be an isomorphism of $X$ and $Y$. Then the equivalence of $e$ is an element of $\EquivMACRoAE {\operatorname{S} (X)}{\operatorname{S} (Y)}$.

the map of f and s (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $s$ be an element of $\operatorname{S}$ applied to $X$. Then the map of $f$ and $s$ is an element of $\operatorname{S}$ applied to $Y$ defined as $\operatorname{mk}$ applied to $\operatorname{hom}$ applied to the component of $f$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to the dimension of the simplex of $s$ and the simplex of $s$.

the opposite equivalence (from the name)

The opposite equivalence is an equivalence from $\operatorname{S}$ applied to the opposite of $X$ to $\operatorname{S}$ applied to $X$.

the simplex of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{S}$ applied to $X$. Then the simplex of $\mathrm{self}$ is an element of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to the dimension of the simplex of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the subcomplex generated by a simplex of s (from the docstring)

Let $s$ be an element of $\operatorname{S}$ applied to $X$. Then the subcomplex generated by a simplex of $s$ is a subcomplex of $X$ defined as the subcomplex of the simplex of $s$.