Definitions: Mathlib.CategoryTheory, part 25 of 25

P is triangulated (from the name)

Let $P$ be an object property of $C$. Then we can say that $P$ is triangulated.

Let $P$ be an object property of $C$. Then we can say that $\mathrm{CategoryTheory\_\_ObjectProperty\_\_IsTriangulatedClosed\_u2081\_}$ holds for $P$.

Let $P$ be an object property of $C$. Then we can say that $\mathrm{CategoryTheory\_\_ObjectProperty\_\_IsTriangulatedClosed\_u2082\_}$ holds for $P$.

Let $P$ be an object property of $C$. Then we can say that $\mathrm{CategoryTheory\_\_ObjectProperty\_\_IsTriangulatedClosed\_u2083\_}$ holds for $P$.

the extension product of P and Q (from the name)

Let $P$ and $Q$ be object properties of $C$. Then the extension product of $P$ and $Q$ is an object property of $C$ defined as the function that maps $X$ to the proposition that there exist elements $Y$ and $Z$ of $C$, such that there exists a homomorphism $f$ of $Y$ and $X$, such that there exists a homomorphism $g$ of $X$ and $Z$, such that there exists a homomorphism $h_{2}$ of $Z$ and the action of the shift functor of $C$ and $1$ and $Y$, such that $\operatorname{mk}$ applied to $f$, $g$ and $h_{2}$ is an element of the distinguished triangle, $P$ holds for $Y$ and $Q$ holds for $Z$.

Let $P$ be an object property of $C$. Let $n$ be a natural number. Then there is an object property of $C$. Proof. Let $P$ be arbitrary. Let $n$ be arbitrary. By P. By CategoryTheory__ObjectProperty__extensionProduct. By n. By P. By Nat__iterate.

the trace of P (from the name)

Let $P$ be an object property of $C$. Then the trace of $P$ is a morphism property of $C$ defined as the function that maps $X$, $Y$ and $f$ to the proposition that there exists an element $Z$ of $C$, such that there exists a homomorphism $g$ of $Y$ and $Z$, such that there exists a homomorphism $h_{2}$ of $Z$ and the action of the shift functor of $C$ and $1$ and $X$, such that there exists an element $h_{3}$ of $\operatorname{mem}$ applied to $\operatorname{mk}$ applied to $f$, $g$ and $h_{2}$ and the distinguished triangle, such that $P$ holds for $Z$.

the admissible morphism of x5 (from the name)

Let $x_{5}$ be a functor of $A$ and $C$. Then the admissible morphism of $x_{5}$ is a morphism property of $A$ defined as the function that maps $x_{6}$, $x_{7}$ and $x_{8}$ to the proposition that for all elements $x_{9}$ of $C$, for all homomorphisms $x_{10}$ of the action of $x_{5}$ and $x_{7}$ and $x_{9}$, for all homomorphisms $x_{11}$ of $x_{9}$ and the action of the shift functor of $C$ and $1$ and the action of $x_{5}$ and $x_{6}$, if $\operatorname{mk}$ applied to the map of $x_{5}$ and $x_{8}$, $x_{10}$ and $x_{11}$ is an element of the distinguished triangle, then there exist elements $K$ and $Q$ of $A$, such that there exists a homomorphism $x_{12}$ of the action of the shift functor of $C$ and $1$ and the action of $x_{5}$ and $K$ and $x_{9}$, such that there exists a homomorphism $x_{13}$ of $x_{9}$ and the action of $x_{5}$ and $Q$, such that there exists a homomorphism $x_{14}$ of the action of $x_{5}$ and $Q$ and the action of the shift functor of $C$ and $1$ and the action of the shift functor of $C$ and $1$ and the action of $x_{5}$ and $K$, such that $\operatorname{mk}$ applied to $x_{12}$, $x_{13}$ and $x_{14}$ is an element of the distinguished triangle.

Assume that for all elements $X$ and $Y$ of $A$, for all integers $n$, for all homomorphisms $f$ of the action of $x_{5}$ and $X$ and the action of the shift functor of $C$ and $n$ and the action of $x_{5}$ and $Y$, if $n < 0$, then $\EqtMACRoH {f}{0}$. Assume that $\operatorname{mk}$ applied to the map of $x_{5}$ and $x_{8}$, $x_{10}$ and $x_{11}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{12}$, $x_{13}$ and $x_{14}$ is an element of the distinguished triangle. Then $\operatorname{isColimitCokernelCofork}$ applied to $h_{2}$, $\mathrm{hT}$ and $\mathrm{hT'}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection to the cokernel of $x_{10}$ and $x_{13}$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_AbelianSubcategory\_\_mor\_u2081\_\_\_u3c0\_Q}$ applied to $\mathrm{hT}$ and $x_{13}$.

Assume that for all elements $X$ and $Y$ of $A$, for all integers $n$, for all homomorphisms $f$ of the action of $x_{5}$ and $X$ and the action of the shift functor of $C$ and $n$ and the action of $x_{5}$ and $Y$, if $n < 0$, then $\EqtMACRoH {f}{0}$. Let $x_{10}$ be a homomorphism of $x_{7}$ and $x_{8}$. Let $x_{11}$ be a homomorphism of $x_{8}$ and $x_{9}$. Let $x_{12}$ be a homomorphism of the action of $x_{5}$ and $x_{9}$ and the action of the shift functor of $C$ and $1$ and the action of $x_{5}$ and $x_{7}$ such that $\operatorname{mk}$ applied to the map of $x_{5}$ and $x_{10}$, the map of $x_{5}$ and $x_{11}$ and $x_{12}$ is an element of the distinguished triangle. Then $\operatorname{isColimitCokernelCoforkOfDistTriang}$ applied to $h_{2}$, $x_{10}$, $x_{11}$, $x_{12}$ and $\mathrm{hT}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $x_{11}$ and $\mathrm{CategoryTheory\_\_Functor\_\_map\_injective}$ applied to $x_{5}$, the composition of $x_{10}$ and $x_{11}$, $0$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_AbelianSubcategory\_\_isLimitKernelForkOfDistTriang\_\_\_proof\_2}$ applied to $x_{10}$, $x_{11}$, $x_{12}$ and $\mathrm{hT}$.

Assume that for all elements $X$ and $Y$ of $A$, for all integers $n$, for all homomorphisms $f$ of the action of $x_{5}$ and $X$ and the action of the shift functor of $C$ and $n$ and the action of $x_{5}$ and $Y$, if $n < 0$, then $\EqtMACRoH {f}{0}$. Assume that $\operatorname{mk}$ applied to the map of $x_{5}$ and $x_{8}$, $x_{10}$ and $x_{11}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{12}$, $x_{13}$ and $x_{14}$ is an element of the distinguished triangle. Then $\operatorname{isLimitKernelFork}$ applied to $h_{2}$, $\mathrm{hT}$ and $\mathrm{hT'}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of the kernel of $x_{11}$ and $x_{12}$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_AbelianSubcategory\_\_\_u3b9\_K\_mor\_u2081\_}$ applied to $\mathrm{hT}$ and $x_{12}$.

Assume that for all elements $X$ and $Y$ of $A$, for all integers $n$, for all homomorphisms $f$ of the action of $x_{5}$ and $X$ and the action of the shift functor of $C$ and $n$ and the action of $x_{5}$ and $Y$, if $n < 0$, then $\EqtMACRoH {f}{0}$. Let $x_{10}$ be a homomorphism of $x_{7}$ and $x_{8}$. Let $x_{11}$ be a homomorphism of $x_{8}$ and $x_{9}$. Let $x_{12}$ be a homomorphism of the action of $x_{5}$ and $x_{9}$ and the action of the shift functor of $C$ and $1$ and the action of $x_{5}$ and $x_{7}$ such that $\operatorname{mk}$ applied to the map of $x_{5}$ and $x_{10}$, the map of $x_{5}$ and $x_{11}$ and $x_{12}$ is an element of the distinguished triangle. Then $\operatorname{isLimitKernelForkOfDistTriang}$ applied to $h_{2}$, $x_{10}$, $x_{11}$, $x_{12}$ and $\mathrm{hT}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $x_{10}$ and $\mathrm{CategoryTheory\_\_Functor\_\_map\_injective}$ applied to $x_{5}$, the composition of $x_{10}$ and $x_{11}$, $0$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_AbelianSubcategory\_\_isLimitKernelForkOfDistTriang\_\_\_proof\_2}$ applied to $x_{10}$, $x_{11}$, $x_{12}$ and $\mathrm{hT}$.

the inclusion of the kernel of x6 and x7 (from the docstring)

Let $x_{6}$ be a homomorphism of $x_{5}$ and the action of the shift functor of $C$ and $1$ and the action of $x_{3}$ and $x_{4}$. Let $x_{7}$ be a homomorphism of the action of the shift functor of $C$ and $1$ and the action of $x_{3}$ and $K$ and $x_{5}$. Then the inclusion of the kernel of $x_{6}$ and $x_{7}$ is a homomorphism of $K$ and $x_{4}$ defined as the choice of the composition of $x_{3}$ and the shift functor of $C$ and $1$ and the composition of $x_{7}$ and $x_{6}$.

the projection to the cokernel of x5 and x6 (from the docstring)

Let $x_{5}$ be a homomorphism of the action of $x_{2}$ and $x_{3}$ and $x_{4}$. Let $x_{6}$ be a homomorphism of $x_{4}$ and the action of $x_{2}$ and $Q$. Then the projection to the cokernel of $x_{5}$ and $x_{6}$ is a homomorphism of $x_{3}$ and $Q$ defined as the choice of $x_{2}$ and the composition of $x_{5}$ and $x_{6}$.

structure of C (from the name)

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

Let $t$ be a structure of $C$. Let $X$ be an element of $C$. Let $n$ be an integer. Then we can say that $\operatorname{IsGE}$ holds for $t$, $X$ and $n$.

Let $t$ be a structure of $C$. Let $X$ be an element of $C$. Let $n$ be an integer. Then we can say that $\operatorname{IsLE}$ holds for $t$, $X$ and $n$.

Let $t$ be a structure of $C$. Then there is an object property of $C$. Proof. Let $t$ be arbitrary. By t. By CategoryTheory__Triangulated__TStructure__plus. By t. By CategoryTheory__Triangulated__TStructure__minus. By Min__min.

Let $\mathrm{self}$ be a structure of $C$. Let $n$ be an integer. Then there is an object property of $C$. Proof. Let $\mathrm{self}$ be arbitrary. Let $n$ be arbitrary. By self. By n. By CategoryTheory__Triangulated__TStructure__proj1.

Let $\mathrm{self}$ be a structure of $C$. Let $n$ be an integer. Then there is an object property of $C$. Proof. Let $\mathrm{self}$ be arbitrary. Let $n$ be arbitrary. By self. By n. By CategoryTheory__Triangulated__TStructure__proj0.

the minus of t (from the name)

Let $t$ be a structure of $C$. Then the minus of $t$ is an object property of $C$ defined as the function that maps $X$ to the proposition that there exists an integer $n$, such that $\operatorname{IsLE}$ holds for $t$, $X$ and $n$.

the plus of t (from the name)

Let $t$ be a structure of $C$. Then the plus of $t$ is an object property of $C$ defined as the function that maps $X$ to the proposition that there exists an integer $n$, such that $\operatorname{IsGE}$ holds for $t$, $X$ and $n$.

Let $t$ be a structure of $C$. Then $\operatorname{eTriangleLTGE}$ applied to $t$ is a functor of the set of integers and the set of functors of $C$ and the set of triangles of $C$.

Let $t$ be a structure of $C$. Then $\operatorname{eTruncGE}$ applied to $t$ is a functor of the set of integers and the set of functors of $C$ and $C$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a \leq b$. Then $\operatorname{eTruncGEIsoGEGE}$ applied to $t$, $a$, $b$ and $\mathrm{hab}$ is an isomorphism of the action of $\operatorname{eTruncGE}$ applied to $t$ and $b$ and the composition of the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncGE}$ applied to $t$ and $b$ defined as $\operatorname{asIso}$ applied to $\operatorname{eTruncGEToGEGE}$ applied to $t$, $a$ and $b$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{eTruncGEToGEGE}$ applied to $t$, $a$ and $b$ is a homomorphism of the action of $\operatorname{eTruncGE}$ applied to $t$ and $b$ and the composition of the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncGE}$ applied to $t$ and $b$ defined as the composition of the inverse of the left unitor of the action of $\operatorname{eTruncGE}$ applied to $t$ and $b$ and the right whisker of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_eTruncGE\_u3c0\_}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncGE}$ applied to $t$ and $b$.

Let $t$ be a structure of $C$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_eTruncGE\_u3b4\_LT}$ applied to $t$ is a homomorphism of $\operatorname{eTruncGE}$ applied to $t$ and the composition of $\operatorname{eTruncLT}$ applied to $t$ and the action of the right whiskering of $C$ and $C$ and the shift functor of $C$ and $1$.

Let $t$ be a structure of $C$. Let $i$ be an integer. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_eTruncGE\_u3c0\_}$ applied to $t$ and $i$ is a homomorphism of the identity of $C$ and the action of $\operatorname{eTruncGE}$ applied to $t$ and $i$.

Let $t$ be a structure of $C$. Then $\operatorname{eTruncLT}$ applied to $t$ is a functor of the set of integers and the set of functors of $C$ and $C$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{eTruncLTGEIsoGELT}$ applied to $t$, $a$ and $b$ is an isomorphism of the composition of the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the composition of the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ defined as the composition of the inverse of $\operatorname{asIso}$ applied to $\operatorname{eTruncLTGELTSelfToLTGE}$ applied to $t$, $a$ and $b$ and $\operatorname{asIso}$ applied to $\operatorname{eTruncLTGELTSelfToGELT}$ applied to $t$, $a$ and $b$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{eTruncLTGELTSelfToGELT}$ applied to $t$, $a$ and $b$ is a homomorphism of the composition of the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the composition of the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the composition of the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ defined as the composition of the inverse of the associator of the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the composition of the left whisker of the composition of the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_eTruncLT\_u3b9\_}$ applied to $t$ and $b$ and the homomorphism of the right unitor of the composition of the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{eTruncLTGELTSelfToLTGE}$ applied to $t$, $a$ and $b$ is a homomorphism of the composition of the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the composition of the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the composition of the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ defined as the composition of the right whisker of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_eTruncLT\_u3b9\_}$ applied to $t$ and $b$ and the composition of the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the homomorphism of the left unitor of the composition of the action of $\operatorname{eTruncGE}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $b \leq a$. Then $\operatorname{eTruncLTLTIsoLT}$ applied to $t$, $a$, $b$ and $\mathrm{hab}$ is an isomorphism of the composition of the action of $\operatorname{eTruncLT}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ defined as $\operatorname{asIso}$ applied to $\operatorname{eTruncLTLTToLT}$ applied to $t$, $a$ and $b$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{eTruncLTLTToLT}$ applied to $t$, $a$ and $b$ is a homomorphism of the composition of the action of $\operatorname{eTruncLT}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ defined as the composition of the right whisker of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_eTruncLT\_u3b9\_}$ applied to $t$ and $a$ and the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$ and the homomorphism of the left unitor of the action of $\operatorname{eTruncLT}$ applied to $t$ and $b$.

Let $t$ be a structure of $C$. Let $i$ be an integer. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_eTruncLT\_u3b9\_}$ applied to $t$ and $i$ is a homomorphism of the action of $\operatorname{eTruncLT}$ applied to $t$ and $i$ and the identity of $C$.

t is a heart (from the name)

Let $t$ be a structure of $C$. Let $H$ be a set. Then we can say that $t$ is a heart.

the inclusion functor of t (from the docstring)

Let $t$ be a structure of $C$. Then the inclusion functor of $t$ is a functor of $H$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the heart of t (from the docstring)

Let $t$ be a structure of $C$. Then the heart of $t$ is an object property of $C$ defined as $\MinminMACRoAG {\operatorname{le} (t , 0)}{\operatorname{ge} (t , 0)}$.

the inclusion of t (from the docstring)

Let $t$ be a structure of $C$. Then the inclusion of $t$ is a functor of $H$ and $C$ defined as the inclusion functor of $t$.

Let $P$ be an object property of $C$. Let $t$ be a structure of $C$. Then we can say that $\operatorname{HasInducedTStructure}$ holds for $P$ and $t$.

the structure of P and t (from the name)

Let $P$ be an object property of $C$. Let $t$ be a structure of $C$. Then the structure of $P$ and $t$ is a structure of the set of full subcategories of $P$.

Let $t$ be a structure of $C$. Then $\operatorname{onBounded}$ applied to $t$ is a structure of the set of full subcategories of $\operatorname{bounded}$ applied to $t$ defined as the structure of $\operatorname{bounded}$ applied to $t$ and $t$.

Let $t$ be a structure of $C$. Then $\operatorname{onMinus}$ applied to $t$ is a structure of the set of full subcategories of the minus of $t$ defined as the structure of the minus of $t$ and $t$.

Let $t$ be a structure of $C$. Then $\operatorname{onPlus}$ applied to $t$ is a structure of the set of full subcategories of the plus of $t$ defined as the structure of the plus of $t$ and $t$.

the spectral object attached to an object of t and X (from the docstring)

Let $t$ be a structure of $C$. Let $X$ be an element of $C$. Then the spectral object attached to an object of $t$ and $X$ is a spectral object of $C$ and the set of integers.

the spectral object attached to an object of t (from the docstring)

Let $t$ be a structure of $C$. Then the spectral object attached to an object of $t$ is a functor of $C$ and the set of spectral objects of $C$ and the set of integers.

the triangle of b and c (from the name)

Let $t$ be a structure of $C$. Let $a$, $b$ and $c$ be integers such that $a \leq b \leq c$. Then the triangle of $b$ and $c$ is a functor of $C$ and the set of triangles of $C$ defined as the functor of the map of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_\_u3c9\_\_u2081\_}$ applied to $t$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_'}$ applied to $a$, $b$, $c$, $\mathrm{hab}$ and $\mathrm{hbc}$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_\_u3c9\_\_u2081\_\_u3b4\_}$ applied to $t$, $a$, $b$, $c$, $\mathrm{hab}$ and $\mathrm{hbc}$.

the triangle object isomorphism of c and X (from the name)

Let $t$ be a structure of $C$. Let $a$, $b$ and $c$ be integers such that $a \leq b \leq c$. Let $X$ be an element of $C$. Then the triangle object isomorphism of $c$ and $X$ is an isomorphism of the action of the triangle of $b$ and $c$ and $X$ and the action of the action of $\operatorname{eTriangleLTGE}$ applied to $t$ and $b$ and the action of the action of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_\_u3c9\_\_u2081\_}$ applied to $t$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to the homomorphism of $\operatorname{trans}$ applied to $\mathrm{hab}$ and $\mathrm{hbc}$ and $X$.

Let $t$ be a structure of $C$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_\_u3c9\_\_u2081\_}$ applied to $t$ is a functor of the set of composable arrows of the set of integers and $1$ and the set of functors of $C$ and $C$.

Let $t$ be a structure of $C$. Let $a$, $b$ and $c$ be integers such that $a \leq b \leq c$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_\_u3c9\_\_u2081\_\_u3b4\_}$ applied to $t$, $a$, $b$, $c$, $\mathrm{hab}$ and $\mathrm{hbc}$ is a homomorphism of the action of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_\_u3c9\_\_u2081\_}$ applied to $t$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to the homomorphism of $\mathrm{hbc}$ and the composition of the action of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_\_u3c9\_\_u2081\_}$ applied to $t$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to the homomorphism of $\mathrm{hab}$ and the shift functor of $C$ and $1$.

Let $F$ be a functor of $C$ and $D$. Let $x_{9}$ be a structure of $C$. Let $x_{10}$ be a structure of $D$. Then we can say that $\operatorname{LeftTExact}$ holds for $F$, $x_{9}$ and $x_{10}$.

Let $F$ be a functor of $C$ and $D$. Let $x_{9}$ be a structure of $C$. Let $x_{10}$ be a structure of $D$. Then we can say that $\operatorname{RightTExact}$ holds for $F$, $x_{9}$ and $x_{10}$.

Let $F$ be a functor of $C$ and $D$. Let $x_{9}$ be a structure of $C$. Let $x_{10}$ be a structure of $D$. Then we can say that $\operatorname{TExact}$ holds for $F$, $x_{9}$ and $x_{10}$.

Let $t$ be a structure of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Let $x_{4}$ and $x_{5}$ be integers such that $x_{4} + 1 = x_{5}$. Then $\operatorname{descTruncGT}$ applied to $t$, $f$, $x_{4}$, $x_{5}$ and $h_{2}$ is a homomorphism of the action of $\operatorname{truncGT}$ applied to $t$ and $x_{4}$ and $X$ and $Y$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_descTruncGT\_aux}$ applied to $t$, $f$, $x_{4}$, $x_{5}$ and $h_{2}$.

Let $t$ be a structure of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Let $n$ be an integer. Then $\operatorname{liftTruncLE}$ applied to $t$, $f$ and $n$ is a homomorphism of $X$ and the action of $\operatorname{truncLE}$ applied to $t$ and $n$ and $Y$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_liftTruncLE\_aux}$ applied to $t$, $f$ and $n$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a \leq b$. Then $\operatorname{natTransTruncLEOfLE}$ applied to $t$, $a$, $b$ and $h_{2}$ is a homomorphism of $\operatorname{truncLE}$ applied to $t$ and $a$ and $\operatorname{truncLE}$ applied to $t$ and $b$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a + 1 = b$. Then $\operatorname{triangleLEGE}$ applied to $t$, $a$, $b$ and $h_{2}$ is a functor of $C$ and the set of triangles of $C$ defined as the functor of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGE\_u3c0\_}$ applied to $t$ and $b$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGE\_u3b4\_LE}$ applied to $t$, $a$, $b$ and $h_{2}$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a + 1 = b$. Then $\operatorname{triangleLEGEIsoTriangleLTGE}$ applied to $t$, $a$, $b$ and $h_{2}$ is an isomorphism of $\operatorname{triangleLEGE}$ applied to $t$, $a$, $b$ and $h_{2}$ and the distinguished triangle of $t$ and $b$.

the distinguished triangle of t and n (from the docstring)

Let $t$ be a structure of $C$. Let $n$ be an integer. Then the distinguished triangle of $t$ and $n$ is a functor of $C$ and the set of triangles of $C$ defined as the functor of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGT\_u3c0\_}$ applied to $t$ and $n$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGT\_u3b4\_LE}$ applied to $t$ and $n$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a + 1 = b$. Then $\operatorname{triangleLEGTIsoTriangleLEGE}$ applied to $t$, $a$, $b$ and $h_{2}$ is an isomorphism of the distinguished triangle of $t$ and $a$ and $\operatorname{triangleLEGE}$ applied to $t$, $a$, $b$ and $h_{2}$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{truncGELE}$ applied to $t$, $a$ and $b$ is a functor of $C$ and $C$ defined as the composition of $\operatorname{truncLE}$ applied to $t$ and $b$ and $\operatorname{truncGE}$ applied to $t$ and $a$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{truncGELEIsoLEGE}$ applied to $t$, $a$ and $b$ is an isomorphism of $\operatorname{truncGELE}$ applied to $t$, $a$ and $b$ and $\operatorname{truncLEGE}$ applied to $t$, $a$ and $b$ defined as $\operatorname{truncGELTIsoLTGE}$ applied to $t$, $a$ and $b + 1$.

Let $t$ be a structure of $C$. Let $a$, $b$ and $\mathrm{b'}$ be integers such that $b + 1 = \mathrm{b'}$. Then $\operatorname{truncGELEIsoTruncGELT}$ applied to $t$, $a$, $b$, $\mathrm{b'}$ and $\mathrm{hb'}$ is an isomorphism of $\operatorname{truncGELE}$ applied to $t$, $a$ and $b$ and $\operatorname{truncGELT}$ applied to $t$, $a$ and $\mathrm{b'}$ defined as the right isomorphism whisker of $\operatorname{truncLEIsoTruncLT}$ applied to $t$, $b$, $\mathrm{b'}$ and $\mathrm{hb'}$ and $\operatorname{truncGE}$ applied to $t$ and $a$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a + 1 = b$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGE\_u3b4\_LE}$ applied to $t$, $a$, $b$ and $h_{2}$ is a homomorphism of $\operatorname{truncGE}$ applied to $t$ and $b$ and the composition of $\operatorname{truncLE}$ applied to $t$ and $a$ and the shift functor of $C$ and $1$ defined as the composition of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGE\_u3b4\_LT}$ applied to $t$ and $b$ and the right whisker of the inverse of $\operatorname{truncLEIsoTruncLT}$ applied to $t$, $a$, $b$ and $h_{2}$ and the shift functor of $C$ and $1$.

Let $t$ be a structure of $C$. Let $n$ be an integer. Then $\operatorname{truncGT}$ applied to $t$ and $n$ is a functor of $C$ and $C$ defined as $\operatorname{truncGE}$ applied to $t$ and $n + 1$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a + 1 = b$. Then $\operatorname{truncGTIsoTruncGE}$ applied to $t$, $a$, $b$ and $h_{2}$ is an isomorphism of $\operatorname{truncGT}$ applied to $t$ and $a$ and $\operatorname{truncGE}$ applied to $t$ and $b$.

Let $t$ be a structure of $C$. Let $n$ be an integer. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGT\_u3b4\_LE}$ applied to $t$ and $n$ is a homomorphism of $\operatorname{truncGT}$ applied to $t$ and $n$ and the composition of $\operatorname{truncLE}$ applied to $t$ and $n$ and the shift functor of $C$ and $1$.

Let $t$ be a structure of $C$. Let $n$ be an integer. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGT\_u3c0\_}$ applied to $t$ and $n$ is a homomorphism of the identity of $C$ and $\operatorname{truncGT}$ applied to $t$ and $n$ defined as $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGE\_u3c0\_}$ applied to $t$ and $n + 1$.

Let $t$ be a structure of $C$. Let $n$ be an integer. Then $\operatorname{truncLE}$ applied to $t$ and $n$ is a functor of $C$ and $C$ defined as $\operatorname{truncLT}$ applied to $t$ and $n + 1$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{truncLEGE}$ applied to $t$, $a$ and $b$ is a functor of $C$ and $C$ defined as the composition of $\operatorname{truncGE}$ applied to $t$ and $a$ and $\operatorname{truncLE}$ applied to $t$ and $b$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a + 1 = b$. Then $\operatorname{truncLEIsoTruncLT}$ applied to $t$, $a$, $b$ and $h_{2}$ is an isomorphism of $\operatorname{truncLE}$ applied to $t$ and $a$ and $\operatorname{truncLT}$ applied to $t$ and $b$.

Let $t$ be a structure of $C$. Let $n$ be an integer. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncLE\_u3b9\_}$ applied to $t$ and $n$ is a homomorphism of $\operatorname{truncLE}$ applied to $t$ and $n$ and the identity of $C$ defined as $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncLT\_u3b9\_}$ applied to $t$ and $n + 1$.

Let $t$ be a structure of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Let $n$ be an integer. Then $\operatorname{descTruncGE}$ applied to $t$, $f$ and $n$ is a homomorphism of the action of $\operatorname{truncGE}$ applied to $t$ and $n$ and $X$ and $Y$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_descTruncGE\_aux}$ applied to $t$, $f$ and $n$.

Let $t$ be a structure of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Let $x_{4}$ and $x_{5}$ be integers such that $x_{4} + 1 = x_{5}$. Then $\operatorname{liftTruncLT}$ applied to $t$, $f$, $x_{4}$, $x_{5}$ and $h_{2}$ is a homomorphism of $X$ and the action of $\operatorname{truncLT}$ applied to $t$ and $x_{5}$ and $Y$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_liftTruncLT\_aux}$ applied to $t$, $f$, $x_{4}$, $x_{5}$ and $h_{2}$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a \leq b$. Then $\operatorname{natTransTriangleLTGEOfLE}$ applied to $t$, $a$, $b$ and $h_{2}$ is a homomorphism of the distinguished triangle of $t$ and $a$ and the distinguished triangle of $t$ and $b$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a \leq b$. Then $\operatorname{natTransTruncGEOfLE}$ applied to $t$, $a$, $b$ and $h_{2}$ is a homomorphism of $\operatorname{truncGE}$ applied to $t$ and $a$ and $\operatorname{truncGE}$ applied to $t$ and $b$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a \leq b$. Then $\operatorname{natTransTruncLTOfLE}$ applied to $t$, $a$, $b$ and $h_{2}$ is a homomorphism of $\operatorname{truncLT}$ applied to $t$ and $a$ and $\operatorname{truncLT}$ applied to $t$ and $b$.

the distinguished triangle of t and n (from the docstring)

Let $t$ be a structure of $C$. Let $n$ be an integer. Then the distinguished triangle of $t$ and $n$ is a functor of $C$ and the set of triangles of $C$ defined as the functor of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGE\_u3c0\_}$ applied to $t$ and $n$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGE\_u3b4\_LT}$ applied to $t$ and $n$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers such that $a \leq b$. Then $\operatorname{triangleLTLTGELT}$ applied to $t$, $a$, $b$ and $h_{2}$ is a functor of $C$ and the set of triangles of $C$ defined as the functor of the left whisker of $\operatorname{truncLT}$ applied to $t$ and $b$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGE\_u3c0\_}$ applied to $t$ and $a$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGELT\_u3b4\_LT}$ applied to $t$, $a$ and $b$.

Let $t$ be a structure of $C$. Let $n$ be an integer. Then $\operatorname{truncGE}$ applied to $t$ and $n$ is a functor of $C$ and $C$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{truncGELT}$ applied to $t$, $a$ and $b$ is a functor of $C$ and $C$ defined as the composition of $\operatorname{truncLT}$ applied to $t$ and $b$ and $\operatorname{truncGE}$ applied to $t$ and $a$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{truncGELTIsoLTGE}$ applied to $t$, $a$ and $b$ is an isomorphism of $\operatorname{truncGELT}$ applied to $t$, $a$ and $b$ and $\operatorname{truncLTGE}$ applied to $t$, $a$ and $b$ defined as $\operatorname{asIso}$ applied to $\operatorname{truncGELTToLTGE}$ applied to $t$, $a$ and $b$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{truncGELTToLTGE}$ applied to $t$, $a$ and $b$ is a homomorphism of $\operatorname{truncGELT}$ applied to $t$, $a$ and $b$ and $\operatorname{truncLTGE}$ applied to $t$, $a$ and $b$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGELT\_u3b4\_LT}$ applied to $t$, $a$ and $b$ is a homomorphism of $\operatorname{truncGELT}$ applied to $t$, $a$ and $b$ and the composition of $\operatorname{truncLT}$ applied to $t$ and $a$ and the shift functor of $C$ and $1$ defined as the composition of the left whisker of $\operatorname{truncLT}$ applied to $t$ and $b$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGE\_u3b4\_LT}$ applied to $t$ and $a$ and the right whisker of $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncLT\_u3b9\_}$ applied to $t$ and $b$ and the composition of $\operatorname{truncLT}$ applied to $t$ and $a$ and the shift functor of $C$ and $1$.

Let $t$ be a structure of $C$. Let $n$ be an integer. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGE\_u3b4\_LT}$ applied to $t$ and $n$ is a homomorphism of $\operatorname{truncGE}$ applied to $t$ and $n$ and the composition of $\operatorname{truncLT}$ applied to $t$ and $n$ and the shift functor of $C$ and $1$.

Let $t$ be a structure of $C$. Let $n$ be an integer. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncGE\_u3c0\_}$ applied to $t$ and $n$ is a homomorphism of the identity of $C$ and $\operatorname{truncGE}$ applied to $t$ and $n$.

Let $t$ be a structure of $C$. Let $n$ be an integer. Then $\operatorname{truncLT}$ applied to $t$ and $n$ is a functor of $C$ and $C$.

Let $t$ be a structure of $C$. Let $a$ and $b$ be integers. Then $\operatorname{truncLTGE}$ applied to $t$, $a$ and $b$ is a functor of $C$ and $C$ defined as the composition of $\operatorname{truncGE}$ applied to $t$ and $a$ and $\operatorname{truncLT}$ applied to $t$ and $b$.

Let $t$ be a structure of $C$. Let $n$ be an integer. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_TStructure\_\_truncLT\_u3b9\_}$ applied to $t$ and $n$ is a homomorphism of $\operatorname{truncLT}$ applied to $t$ and $n$ and the identity of $C$.

the shift functor of C and n (from the docstring)

Let $C$ be a set. Let $n$ be an integer. Then the shift functor of $C$ and $n$ is a functor of the set of triangles of $C$ and the set of triangles of $C$.

the shift functor sum of b and n (from the name)

Let $C$ be a set. Let $a$, $b$ and $n$ be integers such that $a + b = n$. Then the shift functor sum of $b$ and $n$ is an isomorphism of the shift functor of $C$ and $n$ and the composition of the shift functor of $C$ and $a$ and the shift functor of $C$ and $b$.

the shift functor zero of C (from the name)

Let $C$ be a set. Then the shift functor zero of $C$ is an isomorphism of the shift functor of $C$ and $0$ and the identity of the set of triangles of $C$.

Let $C$ be a set. Then $\operatorname{invRotateInvRotateInvRotateIso}$ applied to $C$ is an isomorphism of the composition of $\operatorname{invRotate}$ applied to $C$ and the composition of $\operatorname{invRotate}$ applied to $C$ and $\operatorname{invRotate}$ applied to $C$ and the shift functor of $C$ and $\operatorname{neg}$ applied to $1$.

Let $C$ be a set. Then $\operatorname{invRotateIsoRotateRotateShiftFunctorNegOne}$ applied to $C$ is an isomorphism of $\operatorname{invRotate}$ applied to $C$ and the composition of $\operatorname{rotate}$ applied to $C$ and the composition of $\operatorname{rotate}$ applied to $C$ and the shift functor of $C$ and $\operatorname{neg}$ applied to $1$.

Let $C$ be a set. Then $\operatorname{rotateRotateRotateIso}$ applied to $C$ is an isomorphism of the composition of $\operatorname{rotate}$ applied to $C$ and the composition of $\operatorname{rotate}$ applied to $C$ and $\operatorname{rotate}$ applied to $C$ and the shift functor of $C$ and $1$.

C is triangulated (from the name)

Let $C$ be a set. Then we can say that $C$ is triangulated.

octahedron of h3 and h4 (from the name)

Assume that the composition of $x_{10}$ and $x_{11}$ is equal to $x_{12}$. Assume that $\operatorname{mk}$ applied to $x_{10}$, $x_{13}$ and $x_{14}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{11}$, $x_{15}$ and $x_{16}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{12}$, $x_{17}$ and $x_{18}$ is an element of the distinguished triangle. Then the octahedrons of $h_{3}$ and $h_{4}$ are a basic type.

octahedron of h3 and h4 (from the name)

Assume that the composition of $x_{10}$ and $x_{11}$ is equal to $x_{12}$. Assume that $\operatorname{mk}$ applied to $x_{13}$, $x_{10}$ and $x_{14}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{15}$, $x_{11}$ and $x_{16}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{17}$, $x_{12}$ and $x_{18}$ is an element of the distinguished triangle. Then the octahedrons of $h_{3}$ and $h_{4}$ are a basic type.

Let $\mathrm{self}$ be an octahedron of $h_{3}$ and $h_{4}$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_Octahedron'\_\_m\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $x_{7}$ and $x_{9}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an octahedron of $h_{3}$ and $h_{4}$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_Octahedron'\_\_m\_u2083\_}$ applied to $\mathrm{self}$ is a homomorphism of $x_{9}$ and $x_{8}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the triangle of h5 (from the name)

Assume that the composition of $x_{10}$ and $x_{11}$ is equal to $x_{12}$. Assume that $\operatorname{mk}$ applied to $x_{13}$, $x_{10}$ and $x_{14}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{15}$, $x_{11}$ and $x_{16}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{17}$, $x_{12}$ and $x_{18}$ is an element of the distinguished triangle. Let $h_{5}$ be an octahedron of $h_{3}$ and $h_{4}$. Then the triangle of $h_{5}$ is a triangle of $C$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_Triangulated\_\_Octahedron'\_\_m\_u2081\_}$ applied to $h_{5}$, $\mathrm{CategoryTheory\_\_Triangulated\_\_Octahedron'\_\_m\_u2083\_}$ applied to $h_{5}$ and the composition of $x_{15}$ and $x_{14}$.

the triangle morphism of h5 (from the name)

Assume that the composition of $x_{10}$ and $x_{11}$ is equal to $x_{12}$. Assume that $\operatorname{mk}$ applied to $x_{13}$, $x_{10}$ and $x_{14}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{15}$, $x_{11}$ and $x_{16}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{17}$, $x_{12}$ and $x_{18}$ is an element of the distinguished triangle. Let $h_{5}$ be an octahedron of $h_{3}$ and $h_{4}$. Then the triangle morphism of $h_{5}$ is a homomorphism of $\operatorname{mk}$ applied to $x_{13}$, $x_{10}$ and $x_{14}$ and $\operatorname{mk}$ applied to $x_{17}$, $x_{12}$ and $x_{18}$.

the triangle morphism of h5 (from the name)

Assume that the composition of $x_{10}$ and $x_{11}$ is equal to $x_{12}$. Assume that $\operatorname{mk}$ applied to $x_{13}$, $x_{10}$ and $x_{14}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{15}$, $x_{11}$ and $x_{16}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{17}$, $x_{12}$ and $x_{18}$ is an element of the distinguished triangle. Let $h_{5}$ be an octahedron of $h_{3}$ and $h_{4}$. Then the triangle morphism of $h_{5}$ is a homomorphism of $\operatorname{mk}$ applied to $x_{17}$, $x_{12}$ and $x_{18}$ and $\operatorname{mk}$ applied to $x_{15}$, $x_{11}$ and $x_{16}$.

Let $\mathrm{self}$ be an octahedron of $h_{3}$ and $h_{4}$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_Octahedron\_\_m\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $x_{7}$ and $x_{9}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an octahedron of $h_{3}$ and $h_{4}$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_Octahedron\_\_m\_u2083\_}$ applied to $\mathrm{self}$ is a homomorphism of $x_{9}$ and $x_{8}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the octahedron of h9 and #26 (from the name)

Let $x_{10}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{11}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{12}$ be a homomorphism of $x_{4}$ and $x_{6}$ such that the composition of $x_{10}$ and $x_{11}$ is equal to $x_{12}$. Assume that $\operatorname{mk}$ applied to $x_{10}$, $x_{13}$ and $x_{14}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{11}$, $x_{15}$ and $x_{16}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{12}$, $x_{17}$ and $x_{18}$ is an element of the distinguished triangle. Let $x_{25}$ be a homomorphism of $x_{19}$ and $x_{20}$. Let $x_{26}$ be a homomorphism of $x_{20}$ and $x_{21}$. Let $x_{27}$ be a homomorphism of $x_{19}$ and $x_{21}$ such that the composition of $x_{25}$ and $x_{26}$ is equal to $x_{27}$. Let $x_{28}$ be an isomorphism of $x_{4}$ and $x_{19}$. Let $x_{29}$ be an isomorphism of $x_{5}$ and $x_{20}$. Let $x_{30}$ be an isomorphism of $x_{6}$ and $x_{21}$. Assume that the composition of $x_{10}$ and the homomorphism of $x_{29}$ is equal to the composition of the homomorphism of $x_{28}$ and $x_{25}$. Assume that the composition of $x_{11}$ and the homomorphism of $x_{30}$ is equal to the composition of the homomorphism of $x_{29}$ and $x_{26}$. Let $x_{31}$ be a homomorphism of $x_{20}$ and $x_{22}$. Let $x_{32}$ be a homomorphism of $x_{22}$ and the action of the shift functor of $C$ and $1$ and $x_{19}$ such that $\operatorname{mk}$ applied to $x_{25}$, $x_{31}$ and $x_{32}$ is an element of the distinguished triangle. Let $x_{33}$ be a homomorphism of $x_{21}$ and $x_{23}$. Let $x_{34}$ be a homomorphism of $x_{23}$ and the action of the shift functor of $C$ and $1$ and $x_{20}$ such that $\operatorname{mk}$ applied to $x_{26}$, $x_{33}$ and $x_{34}$ is an element of the distinguished triangle. Let $x_{35}$ be a homomorphism of $x_{21}$ and $x_{24}$. Let $x_{36}$ be a homomorphism of $x_{24}$ and the action of the shift functor of $C$ and $1$ and $x_{19}$ such that $\operatorname{mk}$ applied to $x_{27}$, $x_{35}$ and $x_{36}$ is an element of the distinguished triangle. Let $H$ be an octahedron of $h_{8}$ and $h_{9}$. Then the octahedron of $x_{36}$ and $H$ is an octahedron of $h_{3}$ and $h_{4}$.

the triangle of h5 (from the docstring)

Let $h_{5}$ be an octahedron of $h_{3}$ and $h_{4}$. Then the triangle of $h_{5}$ is a triangle of $C$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_Triangulated\_\_Octahedron\_\_m\_u2081\_}$ applied to $h_{5}$, $\mathrm{CategoryTheory\_\_Triangulated\_\_Octahedron\_\_m\_u2083\_}$ applied to $h_{5}$ and the composition of $x_{16}$ and the map of the shift functor of $C$ and $1$ and $x_{13}$.

the triangle morphism of h5 (from the name)

Let $h_{5}$ be an octahedron of $h_{3}$ and $h_{4}$. Then the triangle morphism of $h_{5}$ is a homomorphism of $\operatorname{mk}$ applied to $x_{10}$, $x_{13}$ and $x_{14}$ and $\operatorname{mk}$ applied to $x_{12}$, $x_{17}$ and $x_{18}$.

the triangle morphism of h5 (from the name)

Let $h_{5}$ be an octahedron of $h_{3}$ and $h_{4}$. Then the triangle morphism of $h_{5}$ is a homomorphism of $\operatorname{mk}$ applied to $x_{12}$, $x_{17}$ and $x_{18}$ and $\operatorname{mk}$ applied to $x_{11}$, $x_{15}$ and $x_{16}$.

Assume that the composition of $x_{10}$ and $x_{11}$ is equal to $x_{12}$. Assume that $\operatorname{mk}$ applied to $x_{10}$, $x_{13}$ and $x_{14}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{11}$, $x_{15}$ and $x_{16}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{12}$, $x_{17}$ and $x_{18}$ is an element of the distinguished triangle. Then $\operatorname{someOctahedron}$ applied to $\mathrm{comm}$, $h_{3}$, $h_{4}$ and $h_{5}$ is an octahedron of $h_{4}$ and $h_{5}$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_IsTriangulated\_\_octahedron\_axiom}$ applied to $\mathrm{comm}$, $h_{3}$, $h_{4}$ and $h_{5}$.

Assume that the composition of $x_{10}$ and $x_{11}$ is equal to $x_{12}$. Assume that $\operatorname{mk}$ applied to $x_{13}$, $x_{10}$ and $x_{14}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{15}$, $x_{11}$ and $x_{16}$ is an element of the distinguished triangle. Assume that $\operatorname{mk}$ applied to $x_{17}$, $x_{12}$ and $x_{18}$ is an element of the distinguished triangle. Then $\operatorname{someOctahedron'}$ applied to $\mathrm{comm}$, $h_{3}$, $h_{4}$ and $h_{5}$ is an octahedron of $h_{4}$ and $h_{5}$.

Let $T$ be a triangle of $C$ such that $T$ is an element of the distinguished triangle. Then $\operatorname{isWeakLimitKernelForkOfDistTriangle}$ applied to $T$ and $\mathrm{dT}$ is an element of $\operatorname{IsWeakLimit}$ applied to the kernel fork of $T$ and $\mathrm{dT}$.

the kernel fork of T and dT (from the name)

Let $T$ be a triangle of $C$ such that $T$ is an element of the distinguished triangle. Then the kernel fork of $T$ and $\mathrm{dT}$ is a kernel fork of the second morphism of $T$ defined as the inclusion of the first morphism of $T$ and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_comp\_distTriang\_mor\_zero\_u2081\_\_u2082\_}$ applied to $T$ and $\mathrm{dT}$.

the section of F (from the name)

Let $F$ be a functor of $J$ and the set of sets. Then the section of $F$ is an element of the power set of the set of functions from elements $j$ of $J$ to elements of the action of $F$ and $j$ defined as $\operatorname{ofPred}$ applied to the function that maps $u$ to the proposition that for all elements $j$ and $\mathrm{j'}$ of $J$, for all homomorphisms $f$ of $j$ and $\mathrm{j'}$, $\operatorname{hom}$ applied to the map of $F$ and $f$ and $u$ applied to $j$ is equal to $u$ applied to $\mathrm{j'}$.

the section functor of J (from the name)

Let $J$ be a set. Then the section functor of $J$ is a functor of the set of functors of $J$ and the set of sets and the set of sets.

the equivalence of i (from the name)

Let $i$ be an isomorphism of $X$ and $Y$. Then the equivalence of $i$ is an equivalence from $X$ to $Y$.

the fully faithful lift functor (from the name)

the homomorphism of x (from the name)

Let $x$ be an element of $X$. Then the homomorphism of $x$ is a homomorphism of $\mathrm{PUnit}$ and $X$ defined as the type category of the function that maps $x_{1}$ to $x$.

the category theory of m (from the name)

Let $m$ be a function from sets to sets. Then the category theory of $m$ is a functor of the set of sets and the set of sets.

the functor embedding (from the docstring)

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

the functor embedding (from the docstring)

The functor embedding is an isomorphism of the functor embedding and the identity of the set of sets.

Let $V$ be a set. Then $\operatorname{uliftTrivial}$ applied to $V$ is an isomorphism of $\mathrm{ULift}$ applied to $V$ and $V$.

the isomorphism of e (from the name)

Let $e$ be an equivalence from $X$ to $Y$. Then the isomorphism of $e$ is an isomorphism of $X$ and $Y$.

function of X and Y (from the name)

Let $X$ and $Y$ be sets. Then the functions of $X$ and $Y$ are a basic type.

the composition of f and g (from the name)

Let $f$ be a function of $Y$ and $Z$. Let $g$ be a function of $X$ and $Y$. Then the composition of $f$ and $g$ is a function of $X$ and $Z$ defined as $\operatorname{mk}$ applied to $\operatorname{comp}$ applied to $\operatorname{toFun}$ applied to $f$ and $\operatorname{toFun}$ applied to $g$.

the homomorphism equivalence of X and Y (from the name)

Let $X$ and $Y$ be sets. Then the homomorphism equivalence of $X$ and $Y$ is an equivalence from the set of functions of $X$ and $Y$ to the set of functions from elements of $X$ to elements of $Y$.

the identity function of X (from the docstring)

Let $X$ be a set. Then the identity function of $X$ is a function of $X$ and $X$ defined as $\operatorname{mk}$ applied to $\mathrm{id}$.

the underlying function of self and x (from the docstring)

Let $\mathrm{self}$ be a function of $X$ and $Y$. Let $x$ be an element of $X$. Then the underlying function of $\mathrm{self}$ and $x$ is an element of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be sets. Then the homomorphisms of $X$ and $Y$ are a basic type.

the homomorphism of f (from the name)

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

the homomorphism of self (from the name)

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

the homomorphism equivalence (from the name)

The homomorphism equivalence is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of functions from elements of $X$ to elements of $Y$ defined as the composition of the homomorphism equivalence and the homomorphism equivalence of $X$ and $Y$.

the type category of f (from the name)

Let $f$ be a function from elements of $X$ to elements of $Y$. Then the type category of $f$ is a homomorphism of $X$ and $Y$ defined as the concrete category of $\operatorname{mk}$ applied to $f$.

the equivalence equivalence isomorphism (from the name)

The equivalence equivalence isomorphism is an equivalence from $\EquivMACRoAE {X}{Y}$ to the set of isomorphisms of $X$ and $Y$ defined as the equivalence of the equivalence isomorphism isomorphism.

the equivalence isomorphism isomorphism (from the name)

The equivalence isomorphism isomorphism is an isomorphism of $\EquivMACRoAE {X}{Y}$ and the set of isomorphisms of $X$ and $Y$.

the functor to type (from the name)

The functor to type is a functor of $\wp X$ and the set of sets.

the witness (from the name)

The witness is a functor of the set of sets and the set of sets defined as the composition of the functor embedding and the inverse of the functor embedding.

the right whiskering of hF and C (from the name)

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Let $C$ be a set. Then the right whiskering of $\mathrm{hF}$ and $C$ is an element of $\operatorname{FullyFaithful}$ applied to the action of the right whiskering of $D$ and $E$ and $F$.

the left isomorphism whisker of F and x3 (from the name)

Let $F$ be a functor of $C$ and $D$. Let $x_{3}$ be an isomorphism of $G$ and $H$. Then the left isomorphism whisker of $F$ and $x_{3}$ is an isomorphism of the composition of $F$ and $G$ and the composition of $F$ and $H$ defined as the map isomorphism of the action of the left whiskering of $D$ and $E$ and $F$ and $x_{3}$.

the right isomorphism whisker of x3 and F (from the name)

Let $x_{3}$ be an isomorphism of $G$ and $H$. Let $F$ be a functor of $D$ and $E$. Then the right isomorphism whisker of $x_{3}$ and $F$ is an isomorphism of the composition of $G$ and $F$ and the composition of $H$ and $F$ defined as the map isomorphism of the action of the right whiskering of $D$ and $E$ and $F$ and $x_{3}$.

the postcomposition (from the name)

The postcomposition is a functor of the set of functors of $E$ and $\mathrm{E'}$ and the set of functors of the set of functors of $x$ and the set of functors of $x_{1}$ and $E$ and the set of functors of $x$ and the set of functors of $x_{1}$ and $\mathrm{E'}$ defined as the composition of the right whiskering of $E$ and $\mathrm{E'}$ and the right whiskering of the set of functors of $x_{1}$ and $E$ and the set of functors of $x_{1}$ and $\mathrm{E'}$.

the postcomposition (from the name)

The postcomposition is a functor of the set of functors of $E$ and $\mathrm{E'}$ and the set of functors of the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$ and the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $\mathrm{E'}$ defined as the composition of the right whiskering of $E$ and $\mathrm{E'}$ and the composition of the right whiskering of the set of functors of $x_{2}$ and $E$ and the set of functors of $x_{2}$ and $\mathrm{E'}$ and the right whiskering of the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $\mathrm{E'}$.

the postcomposition (from the name)

The postcomposition is a functor of the set of functors of $E$ and $\mathrm{E'}$ and the set of functors of the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$ and the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $\mathrm{E'}$ defined as the composition of the right whiskering of $E$ and $\mathrm{E'}$ and the composition of the right whiskering of the set of functors of $x_{3}$ and $E$ and the set of functors of $x_{3}$ and $\mathrm{E'}$ and the composition of the right whiskering of the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $\mathrm{E'}$ and the right whiskering of the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $\mathrm{E'}$.

the left whisker of F and x3 (from the name)

Let $F$ be a functor of $C$ and $D$. Let $x_{3}$ be a homomorphism of $G$ and $H$. Then the left whisker of $F$ and $x_{3}$ is a homomorphism of the composition of $F$ and $G$ and the composition of $F$ and $H$.

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

Let $x_{3}$ be a homomorphism of $G$ and $H$. Let $F$ be a functor of $D$ and $E$. Then the right whisker of $x_{3}$ and $F$ is a homomorphism of the composition of $G$ and $F$ and the composition of $H$ and $F$.

the left whiskering of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the left whiskering of $D$ and $E$ is a functor of the set of functors of $C$ and $D$ and the set of functors of the set of functors of $D$ and $E$ and the set of functors of $C$ and $E$.

the whiskering left object composition isomorphism of F and G (from the name)

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $\mathrm{D'}$. Then the whiskering left object composition isomorphism of $F$ and $G$ is an isomorphism of the action of the left whiskering of $\mathrm{D'}$ and $E$ and the composition of $F$ and $G$ and the composition of the action of the left whiskering of $\mathrm{D'}$ and $E$ and $G$ and the action of the left whiskering of $D$ and $E$ and $F$ defined as the identity of the action of the left whiskering of $\mathrm{D'}$ and $E$ and the composition of $F$ and $G$.

the whiskering left object identity isomorphism (from the name)

The whiskering left object identity isomorphism is an isomorphism of the action of the left whiskering of $C$ and $E$ and the identity of $C$ and the identity of the set of functors of $C$ and $E$ defined as the identity of the action of the left whiskering of $C$ and $E$ and the identity of $C$.

the left whiskering of E (from the name)

Let $E$ be a set. Then the left whiskering of $E$ is a functor of the set of functors of $x$ and $x_{2}$ and the set of functors of the set of functors of $x_{1}$ and $x_{3}$ and the set of functors of the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$ and the set of functors of $x$ and the set of functors of $x_{1}$ and $E$.

the left whiskering of E (from the name)

Let $E$ be a set. Then the left whiskering of $E$ is a functor of the set of functors of $x$ and $x_{3}$ and the set of functors of the set of functors of $x_{1}$ and $x_{4}$ and the set of functors of the set of functors of $x_{2}$ and $x_{5}$ and the set of functors of the set of functors of $x_{3}$ and the set of functors of $x_{4}$ and the set of functors of $x_{5}$ and $E$ and the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and $E$.

the left whiskering of E (from the name)

Let $E$ be a set. Then the left whiskering of $E$ is a functor of the set of functors of $x$ and $x_{4}$ and the set of functors of the set of functors of $x_{1}$ and $x_{5}$ and the set of functors of the set of functors of $x_{2}$ and $x_{6}$ and the set of functors of the set of functors of $x_{3}$ and $x_{7}$ and the set of functors of the set of functors of $x_{4}$ and the set of functors of $x_{5}$ and the set of functors of $x_{6}$ and the set of functors of $x_{7}$ and $E$ and the set of functors of $x$ and the set of functors of $x_{1}$ and the set of functors of $x_{2}$ and the set of functors of $x_{3}$ and $E$.

the right whiskering of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the right whiskering of $D$ and $E$ is a functor of the set of functors of $D$ and $E$ and the set of functors of the set of functors of $C$ and $D$ and the set of functors of $C$ and $E$.

the whiskering right object composition isomorphism of F and G (from the name)

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $\mathrm{D'}$. Then the whiskering right object composition isomorphism of $F$ and $G$ is an isomorphism of the composition of the action of the right whiskering of $C$ and $D$ and $F$ and the action of the right whiskering of $D$ and $\mathrm{D'}$ and $G$ and the action of the right whiskering of $C$ and $\mathrm{D'}$ and the composition of $F$ and $G$ defined as the identity of the composition of the action of the right whiskering of $C$ and $D$ and $F$ and the action of the right whiskering of $D$ and $\mathrm{D'}$ and $G$.

the whiskering right object identity isomorphism (from the name)

The whiskering right object identity isomorphism is an isomorphism of the action of the right whiskering of $C$ and $C$ and the identity of $C$ and the identity of the set of functors of $E$ and $C$ defined as the identity of the action of the right whiskering of $C$ and $C$ and the identity of $C$.

induced wide category of _F and _P (from the name)

Let $D$ be a set. Let $\mathrm{\_F}$ be a function from elements of $C$ to elements of $D$. Let $\mathrm{\_P}$ be a morphism property of $D$. Then an induced wide category of $\mathrm{\_F}$ and $\mathrm{\_P}$ is an element of the function that maps $D$, $\mathrm{\_F}$ and $\mathrm{\_P}$ to $C$.

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be induced wide categories of $F$ and $P$. Then the homomorphisms of $X$ and $Y$ are a basic type.

the homomorphism of self (from the name)

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

wide subcategory of _P (from the name)

Let $\mathrm{\_P}$ be a morphism property of $C$. Then the wide subcategories of $\mathrm{\_P}$ are a basic type.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of the object of $X$ and the object of $Y$ such that $P$ holds for the object of $X$, the object of $Y$ and the homomorphism of $e$ and $P$ holds for the object of $Y$, the object of $X$ and the inverse of $e$. Then the isomorphism of $e$ is an isomorphism of $X$ and $Y$.

the object of self (from the name)

Let $\mathrm{self}$ be a wide subcategory of $\mathrm{\_P}$. Then the object of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the wide induced functor of F and P (from the name)

Let $F$ be a function from elements of $C$ to elements of $D$. Let $P$ be a morphism property of $D$. Then the wide induced functor of $F$ and $P$ is a functor of the set of induced wide categories of $F$ and $P$ and $D$.

the wide subcategory inclusion of P (from the name)

Let $P$ be a morphism property of $C$. Then the wide subcategory inclusion of $P$ is a functor of the set of wide subcategories of $P$ and $C$ defined as the wide induced functor of $\operatorname{obj}$ and $P$.

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

homomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{WithInitial}$ applied to $C$. Then the homomorphisms of $x_{1}$ and $x_{2}$ are a basic type.

the composition of x1 and x2 (from the name)

Let $x_{1}$ be a homomorphism of $X$ and $Y$. Let $x_{2}$ be a homomorphism of $Y$ and $Z$. Then the composition of $x_{1}$ and $x_{2}$ is a homomorphism of $X$ and $Z$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x$ of $C$ to elements of $\mathrm{motive}$ applied to $\operatorname{of}$ applied to $x$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the star.

Let $f$ be a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$. Then $\operatorname{down}$ applied to $f$ is a homomorphism of $X$ and $Y$ defined as $f$.

the equivalence comma (from the name)

The equivalence comma is an equivalence of the set of functors of $\operatorname{WithInitial}$ applied to $C$ and $D$ and the set of commas of the constant of $C$ and the identity of the set of functors of $C$ and $D$.

Let $X$ be an element of $C$. Then $\operatorname{homTo}$ applied to $X$ is a homomorphism of the star and the action of the inclusion and $X$ defined as $\operatorname{to}$ applied to $\operatorname{starInitial}$ and the action of the inclusion and $X$.

the identity of X (from the name)

Let $X$ be an element of $\operatorname{WithInitial}$ applied to $C$. Then the identity of $X$ is a homomorphism of $X$ and $X$.

the inclusion (from the name)

The inclusion is a functor of $C$ and $\operatorname{WithInitial}$ applied to $C$.

the inclusion lift of F and M (from the name)

Let $F$ be a functor of $C$ and $D$. Let $M$ be a function from elements $x_{3}$ of $C$ to homomorphisms of $Z$ and the action of $F$ and $x_{3}$ such that for all elements $x_{2}$ and $y$ of $C$, for all homomorphisms $f$ of $x_{2}$ and $y$, the composition of $M$ applied to $x_{2}$ and the map of $F$ and $f$ is equal to $M$ applied to $y$. Then the inclusion lift of $F$ and $x_{3}$ is an isomorphism of the composition of the inclusion and the lift of $F$ and $M$ and $F$.

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hZ}$ be an element of $\operatorname{IsInitial}$ applied to $Z$. Then $\operatorname{inclLiftToInitial}$ applied to $F$ and $\mathrm{hZ}$ is an isomorphism of the composition of the inclusion and $\operatorname{liftToInitial}$ applied to $F$ and $\mathrm{hZ}$ and $F$.

the lift of F and M (from the name)

Let $F$ be a functor of $C$ and $D$. Let $M$ be a function from elements $x_{3}$ of $C$ to homomorphisms of $Z$ and the action of $F$ and $x_{3}$ such that for all elements $x_{2}$ and $y$ of $C$, for all homomorphisms $f$ of $x_{2}$ and $y$, the composition of $M$ applied to $x_{2}$ and the map of $F$ and $f$ is equal to $M$ applied to $y$. Then the lift of $F$ and $x_{3}$ is a functor of $\operatorname{WithInitial}$ applied to $C$ and $D$.

the lift star of F and M (from the name)

Let $F$ be a functor of $C$ and $D$. Let $M$ be a function from elements $x_{3}$ of $C$ to homomorphisms of $Z$ and the action of $F$ and $x_{3}$ such that for all elements $x_{2}$ and $y$ of $C$, for all homomorphisms $f$ of $x_{2}$ and $y$, the composition of $M$ applied to $x_{2}$ and the map of $F$ and $f$ is equal to $M$ applied to $y$. Then the lift star of $F$ and $x_{3}$ is an isomorphism of the action of the lift of $F$ and $M$ and the star and $Z$.

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hZ}$ be an element of $\operatorname{IsInitial}$ applied to $Z$. Then $\operatorname{liftToInitial}$ applied to $F$ and $\mathrm{hZ}$ is a functor of $\operatorname{WithInitial}$ applied to $C$ and $D$.

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hZ}$ be an element of $\operatorname{IsInitial}$ applied to $Z$. Let $G$ be a functor of $\operatorname{WithInitial}$ applied to $C$ and $D$. Let $h$ be an isomorphism of the composition of the inclusion and $G$ and $F$. Let $\mathrm{hG}$ be an isomorphism of the action of $G$ and the star and $Z$. Then $\operatorname{liftToInitialUnique}$ applied to $F$, $\mathrm{hZ}$, $G$, $h$ and $\mathrm{hG}$ is an isomorphism of $G$ and $\operatorname{liftToInitial}$ applied to $F$ and $\mathrm{hZ}$.

the uniqueness of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Let $M$ be a function from elements $x_{4}$ of $C$ to homomorphisms of $Z$ and the action of $F$ and $x_{4}$ such that for all elements $x_{3}$ and $y$ of $C$, for all homomorphisms $f$ of $x_{3}$ and $y$, the composition of $M$ applied to $x_{3}$ and the map of $F$ and $f$ is equal to $M$ applied to $y$. Let $G$ be a functor of $\operatorname{WithInitial}$ applied to $C$ and $D$. Let $h$ be an isomorphism of the composition of the inclusion and $G$ and $F$. Let $\mathrm{hG}$ be an isomorphism of the action of $G$ and the star and $Z$ such that for all elements $x_{2}$ of $C$, the composition of the homomorphism of the inverse of $\mathrm{hG}$ and the map of $G$ and $\operatorname{to}$ applied to $\operatorname{starInitial}$ and the action of the inclusion and $x_{2}$ is equal to the composition of $M$ applied to $x_{2}$ and the component of the homomorphism of the inverse of $h$ and $x_{2}$. Then the uniqueness of $F$ is an isomorphism of $G$ and the lift of $F$ and $M$.

the map of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the map of $F$ is a functor of $\operatorname{WithInitial}$ applied to $C$ and $\operatorname{WithInitial}$ applied to $D$.

the map composition of F and G (from the name)

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the map composition of $F$ and $G$ is an isomorphism of the map of the composition of $F$ and $G$ and the composition of the map of $F$ and the map of $G$.

the map identity of C (from the name)

Let $C$ be a set. Then the map identity of $C$ is an isomorphism of the map of the identity of $C$ and the identity of $\operatorname{WithInitial}$ applied to $C$.

the map of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the map of $x_{2}$ is a homomorphism of the map of $F$ and the map of $G$.

the comma morphism of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the comma morphism of $x_{2}$ is a homomorphism of the comma object of $F$ and the comma object of $G$.

the comma object of F (from the name)

Let $F$ be a functor of $\operatorname{WithInitial}$ applied to $C$ and $D$. Then the comma object of $F$ is a comma of the constant of $C$ and the identity of the set of functors of $C$ and $D$.

Let $x$ be an element of $C$. Then $\operatorname{of}$ applied to $x$ is an element of $\operatorname{WithInitial}$ applied to $C$.

Let $x_{2}$ be a homomorphism of $c$ and $\mathrm{c'}$. Then $\operatorname{ofCommaMorphism}$ applied to $x_{2}$ is a homomorphism of $\operatorname{ofCommaObject}$ applied to $c$ and $\operatorname{ofCommaObject}$ applied to $\mathrm{c'}$.

Let $c$ be a comma of the constant of $C$ and the identity of the set of functors of $C$ and $D$. Then $\operatorname{ofCommaObject}$ applied to $c$ is a functor of $\operatorname{WithInitial}$ applied to $C$ and $D$.

the opposite category of C (from the docstring)

Let $C$ be a set. Then the opposite category of $C$ is an equivalence of the set of opposites of $\operatorname{WithInitial}$ applied to $C$ and $\operatorname{WithTerminal}$ applied to the set of opposites of $C$.

$\operatorname{prelaxfunctor}$ is a prelax functor of the set of categories and the set of categories.

the pseudofunctor (from the name)

The pseudofunctor is a pseudofunctor of the set of categories and the set of categories.

the star (from the name)

The star is an element of $\operatorname{WithInitial}$ applied to $C$.

$\operatorname{starInitial}$ is an element of $\operatorname{IsInitial}$ applied to the star defined as $\operatorname{ofUnique}$ applied to the star.

$\operatorname{starIsoInitial}$ is an isomorphism of the star and $\operatorname{initial}$ applied to $\operatorname{WithInitial}$ applied to $C$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{starInitial}$ and $\operatorname{initialIsInitial}$.

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

homomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{WithTerminal}$ applied to $C$. Then the homomorphisms of $x_{1}$ and $x_{2}$ are a basic type.

the composition of x1 and x2 (from the name)

Let $x_{1}$ be a homomorphism of $X$ and $Y$. Let $x_{2}$ be a homomorphism of $Y$ and $Z$. Then the composition of $x_{1}$ and $x_{2}$ is a homomorphism of $X$ and $Z$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x$ of $C$ to elements of $\mathrm{motive}$ applied to $\operatorname{of}$ applied to $x$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the star.

Let $f$ be a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$. Then $\operatorname{down}$ applied to $f$ is a homomorphism of $X$ and $Y$ defined as $f$.

the equivalence comma (from the name)

The equivalence comma is an equivalence of the set of functors of $\operatorname{WithTerminal}$ applied to $C$ and $D$ and the set of commas of the identity of the set of functors of $C$ and $D$ and the constant of $C$.

Let $X$ be an element of $C$. Then $\operatorname{homFrom}$ applied to $X$ is a homomorphism of the action of the inclusion and $X$ and the star defined as $\operatorname{from}$ applied to the star terminal and the action of the inclusion and $X$.

the identity of X (from the name)

Let $X$ be an element of $\operatorname{WithTerminal}$ applied to $C$. Then the identity of $X$ is a homomorphism of $X$ and $X$.

the inclusion (from the name)

The inclusion is a functor of $C$ and $\operatorname{WithTerminal}$ applied to $C$.

the inclusion lift of F and M (from the name)

Let $F$ be a functor of $C$ and $D$. Let $M$ be a function from elements $x_{3}$ of $C$ to homomorphisms of the action of $F$ and $x_{3}$ and $Z$ such that for all elements $x_{2}$ and $y$ of $C$, for all homomorphisms $f$ of $x_{2}$ and $y$, the composition of the map of $F$ and $f$ and $M$ applied to $y$ is equal to $M$ applied to $x_{2}$. Then the inclusion lift of $F$ and $x_{3}$ is an isomorphism of the composition of the inclusion and the lift of $F$ and $M$ and $F$.

the inclusion lift to terminal of F and hZ (from the name)

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hZ}$ be an element of $\operatorname{IsTerminal}$ applied to $Z$. Then the inclusion lift to terminal of $F$ and $\mathrm{hZ}$ is an isomorphism of the composition of the inclusion and the lift to terminal of $F$ and $\mathrm{hZ}$ and $F$.

the lift of F and M (from the name)

Let $F$ be a functor of $C$ and $D$. Let $M$ be a function from elements $x_{3}$ of $C$ to homomorphisms of the action of $F$ and $x_{3}$ and $Z$ such that for all elements $x_{2}$ and $y$ of $C$, for all homomorphisms $f$ of $x_{2}$ and $y$, the composition of the map of $F$ and $f$ and $M$ applied to $y$ is equal to $M$ applied to $x_{2}$. Then the lift of $F$ and $x_{3}$ is a functor of $\operatorname{WithTerminal}$ applied to $C$ and $D$.

the lift star of F and M (from the name)

Let $F$ be a functor of $C$ and $D$. Let $M$ be a function from elements $x_{3}$ of $C$ to homomorphisms of the action of $F$ and $x_{3}$ and $Z$ such that for all elements $x_{2}$ and $y$ of $C$, for all homomorphisms $f$ of $x_{2}$ and $y$, the composition of the map of $F$ and $f$ and $M$ applied to $y$ is equal to $M$ applied to $x_{2}$. Then the lift star of $F$ and $x_{3}$ is an isomorphism of the action of the lift of $F$ and $M$ and the star and $Z$.

the lift to terminal of F and hZ (from the name)

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hZ}$ be an element of $\operatorname{IsTerminal}$ applied to $Z$. Then the lift to terminal of $F$ and $\mathrm{hZ}$ is a functor of $\operatorname{WithTerminal}$ applied to $C$ and $D$.

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hZ}$ be an element of $\operatorname{IsTerminal}$ applied to $Z$. Let $G$ be a functor of $\operatorname{WithTerminal}$ applied to $C$ and $D$. Let $h$ be an isomorphism of the composition of the inclusion and $G$ and $F$. Let $\mathrm{hG}$ be an isomorphism of the action of $G$ and the star and $Z$. Then $\operatorname{liftToTerminalUnique}$ applied to $F$, $\mathrm{hZ}$, $G$, $h$ and $\mathrm{hG}$ is an isomorphism of $G$ and the lift to terminal of $F$ and $\mathrm{hZ}$.

the uniqueness of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Let $M$ be a function from elements $x_{4}$ of $C$ to homomorphisms of the action of $F$ and $x_{4}$ and $Z$ such that for all elements $x_{3}$ and $y$ of $C$, for all homomorphisms $f$ of $x_{3}$ and $y$, the composition of the map of $F$ and $f$ and $M$ applied to $y$ is equal to $M$ applied to $x_{3}$. Let $G$ be a functor of $\operatorname{WithTerminal}$ applied to $C$ and $D$. Let $h$ be an isomorphism of the composition of the inclusion and $G$ and $F$. Let $\mathrm{hG}$ be an isomorphism of the action of $G$ and the star and $Z$ such that for all elements $x_{2}$ of $C$, the composition of the map of $G$ and $\operatorname{from}$ applied to the star terminal and the action of the inclusion and $x_{2}$ and the homomorphism of $\mathrm{hG}$ is equal to the composition of the component of the homomorphism of $h$ and $x_{2}$ and $M$ applied to $x_{2}$. Then the uniqueness of $F$ is an isomorphism of $G$ and the lift of $F$ and $M$.

the map of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the map of $F$ is a functor of $\operatorname{WithTerminal}$ applied to $C$ and $\operatorname{WithTerminal}$ applied to $D$.

the map composition of F and G (from the name)

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the map composition of $F$ and $G$ is an isomorphism of the map of the composition of $F$ and $G$ and the composition of the map of $F$ and the map of $G$.

the map identity of C (from the name)

Let $C$ be a set. Then the map identity of $C$ is an isomorphism of the map of the identity of $C$ and the identity of $\operatorname{WithTerminal}$ applied to $C$.

the map of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the map of $x_{2}$ is a homomorphism of the map of $F$ and the map of $G$.

the comma morphism of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the comma morphism of $x_{2}$ is a homomorphism of the comma object of $F$ and the comma object of $G$.

the comma object of F (from the name)

Let $F$ be a functor of $\operatorname{WithTerminal}$ applied to $C$ and $D$. Then the comma object of $F$ is a comma of the identity of the set of functors of $C$ and $D$ and the constant of $C$.

Let $x$ be an element of $C$. Then $\operatorname{of}$ applied to $x$ is an element of $\operatorname{WithTerminal}$ applied to $C$.

Let $x_{2}$ be a homomorphism of $c$ and $\mathrm{c'}$. Then $\operatorname{ofCommaMorphism}$ applied to $x_{2}$ is a homomorphism of $\operatorname{ofCommaObject}$ applied to $c$ and $\operatorname{ofCommaObject}$ applied to $\mathrm{c'}$.

Let $c$ be a comma of the identity of the set of functors of $C$ and $D$ and the constant of $C$. Then $\operatorname{ofCommaObject}$ applied to $c$ is a functor of $\operatorname{WithTerminal}$ applied to $C$ and $D$.

the opposite category of C (from the docstring)

Let $C$ be a set. Then the opposite category of $C$ is an equivalence of the set of opposites of $\operatorname{WithTerminal}$ applied to $C$ and $\operatorname{WithInitial}$ applied to the set of opposites of $C$.

$\operatorname{prelaxfunctor}$ is a prelax functor of the set of categories and the set of categories.

the pseudofunctor (from the name)

The pseudofunctor is a pseudofunctor of the set of categories and the set of categories.

the star (from the name)

The star is an element of $\operatorname{WithTerminal}$ applied to $C$.

the star isomorphism terminal (from the name)

The star isomorphism terminal is an isomorphism of the star and $\operatorname{terminal}$ applied to $\operatorname{WithTerminal}$ applied to $C$ defined as $\operatorname{uniqueUpToIso}$ applied to the star terminal and $\operatorname{terminalIsTerminal}$.

the star terminal (from the name)

The star terminal is an element of $\operatorname{IsTerminal}$ applied to the star defined as $\operatorname{ofUnique}$ applied to the star.

the wide pullback shape equivalence (from the name)

The wide pullback shape equivalence is an equivalence of the set of wide pullback shapes of $J$ and $\operatorname{WithTerminal}$ applied to $\operatorname{Discrete}$ applied to $J$.

the default (from the name)

The default is an element of $\operatorname{WithInitial}$ applied to $C$ defined as the star.

the default (from the name)

The default is an element of $\operatorname{WithTerminal}$ applied to $C$ defined as the star.

the cocone equivalence (from the name)

The cocone equivalence is an equivalence of the set of cocones of $K$ and the set of cocones of the action of $\operatorname{liftFromUnder}$ and $K$.

$\operatorname{commaFromUnder}$ is a functor of the set of functors of $J$ and $\operatorname{Under}$ applied to $X$ and the set of commas of the constant of $J$ and the identity of the set of functors of $J$ and $C$.

$\operatorname{isColimitEquiv}$ is an equivalence from $\operatorname{IsColimit}$ applied to the action of the functor of the cocone equivalence and $t$ to $\operatorname{IsColimit}$ applied to $t$ defined as $\operatorname{ofCoconeEquiv}$ applied to the cocone equivalence.

$\operatorname{liftFromUnder}$ is a functor of the set of functors of $J$ and $\operatorname{Under}$ applied to $X$ and the set of functors of $\operatorname{WithInitial}$ applied to $J$ and $C$ defined as the composition of $\operatorname{commaFromUnder}$ and the inverse of the equivalence comma.

the extension (from the docstring)

The extension is an isomorphism of the action of $\operatorname{liftFromUnder}$ and the composition of $K$ and the post of $F$ and the composition of the action of $\operatorname{liftFromUnder}$ and $K$ and $F$.

$\operatorname{commaFromOver}$ is a functor of the set of functors of $J$ and $\operatorname{Over}$ applied to $X$ and the set of commas of the identity of the set of functors of $J$ and $C$ and the constant of $J$.

the cone equivalence (from the name)

The cone equivalence is an equivalence of the set of cones of $K$ and the set of cones of the action of $\operatorname{liftFromOver}$ and $K$.

$\operatorname{isLimitEquiv}$ is an equivalence from $\operatorname{IsLimit}$ applied to the action of the functor of the cone equivalence and $t$ to $\operatorname{IsLimit}$ applied to $t$ defined as $\operatorname{ofConeEquiv}$ applied to the cone equivalence.

$\operatorname{liftFromOver}$ is a functor of the set of functors of $J$ and $\operatorname{Over}$ applied to $X$ and the set of functors of $\operatorname{WithTerminal}$ applied to $J$ and $C$ defined as the composition of $\operatorname{commaFromOver}$ and the inverse of the equivalence comma.

the extension (from the docstring)

The extension is an isomorphism of the action of $\operatorname{liftFromOver}$ and the composition of $K$ and the post of $F$ and the composition of the action of $\operatorname{liftFromOver}$ and $K$ and $F$.

the option equivalence of C (from the name)

Let $C$ be a set. Then the option equivalence of $C$ is an element of $\EquivMACRoAE {\mathrm{Option} (C)}{\operatorname{WithInitial} (C)}$.

the option equivalence of C (from the name)

Let $C$ be a set. Then the option equivalence of $C$ is an element of $\EquivMACRoAE {\mathrm{Option} (C)}{\operatorname{WithTerminal} (C)}$.

the extension of p and Z4 (from the name)

Let $X$ and $Y$ be elements of $C$. Let $p$ be a function from elements $Z_{4}$ of $C$ and homomorphisms of $X$ and $Z_{4}$ to homomorphisms of $Y$ and $Z_{4}$. Let $q$ be a function from elements $Z_{3}$ of $C$ and homomorphisms of $Y$ and $Z_{3}$ to homomorphisms of $X$ and $Z_{3}$ such that for all elements $Z_{2}$ of $C$, for all homomorphisms $f_{2}$ of $X$ and $Z_{2}$, $\EqtMACRoH {q (Z_{2} , p (Z_{2} , f_{2}))}{f_{2}}$, for all elements $Z_{1}$ of $C$, for all homomorphisms $f_{1}$ of $Y$ and $Z_{1}$, $\EqtMACRoH {p (Z_{1} , q (Z_{1} , f_{1}))}{f_{1}}$ and for all elements $Z$ of $C$, for all elements $\mathrm{Z'}$ of $C$, for all homomorphisms $f$ of $Y$ and $Z$, for all homomorphisms $g$ of $Z$ and $\mathrm{Z'}$, $q$ applied to $\mathrm{Z'}$ and the composition of $f$ and $g$ is equal to the composition of $q$ applied to $Z$ and $f$ and $g$. Then the extension of $Z_{4}$ and $p$ is an isomorphism of $X$ and $Y$.

$\operatorname{fullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the Coyoneda.

the object opposite opposite of X (from the name)

Let $X$ be an element of $C$. Then the object opposite opposite of $X$ is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to $\operatorname{op}$ applied to $X$ and the action of the Yoneda and $X$.

the opposite isomorphism (from the name)

The opposite isomorphism is an isomorphism of the composition of the Yoneda and the action of the left whiskering of the set of opposites of the set of opposites of $C$ and the set of sets and the functor of $C$ and the Coyoneda.

the preimage of f (from the name)

Let $f$ be a homomorphism of the action of the Coyoneda and $X$ and the action of the Coyoneda and $Y$. Then the preimage of $f$ is a homomorphism of $X$ and $Y$ defined as the opposite in $\operatorname{hom}$ applied to the component of $f$ and the opposite of $X$ and the identity morphism of the opposite of $X$.

$\operatorname{punitIso}$ is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to $\mathrm{PUnit}$ and the identity of the set of sets.

Let $F$ be a functor of $C$ and the set of sets. Let $X$ be an element of $C$. Then the elements of $\operatorname{CorepresentableBy}$ applied to $F$ and $X$ are a basic type.

the Coyoneda of X (from the name)

Let $X$ be an opposite of $C$. Then the Coyoneda of $X$ is an element of $\operatorname{CorepresentableBy}$ applied to the action of the Coyoneda and $X$ and the opposite of $X$ defined as $\operatorname{symm}$ applied to $\operatorname{corepresentableByEquiv}$ and the identity of the action of the Coyoneda and $\operatorname{op}$ applied to the opposite of $X$.

the equivalence of e (from the name)

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

the equivalence lift Coyoneda isomorphism of F and X (from the name)

Let $F$ be a functor of $C$ and the set of sets. Let $X$ be an element of $C$. Then the equivalence lift Coyoneda isomorphism of $F$ and $X$ is an equivalence from $\operatorname{CorepresentableBy}$ applied to $F$ and $X$ to the set of isomorphisms of the action of the lift Coyoneda and $\operatorname{op}$ applied to $X$ and $F$.

the homomorphism equivalence of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{CorepresentableBy}$ applied to $F$ and $X$. Then the homomorphism equivalence of $\mathrm{self}$ is an equivalence from the set of homomorphisms of $X$ and $Y$ to the action of $F$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the identity (from the name)

The identity is an element of $\operatorname{CorepresentableBy}$ applied to the identity of the set of sets and $\mathrm{PUnit}$ defined as $\operatorname{symm}$ applied to $\operatorname{corepresentableByEquiv}$ and $\operatorname{punitIso}$.

Let $e$ be an element of $\operatorname{CorepresentableBy}$ applied to $F$ and $Y$. Then $\operatorname{isoCoreprX}$ applied to $e$ is an isomorphism of $Y$ and $\operatorname{coreprX}$ applied to $F$ defined as $\operatorname{uniqueUpToIso}$ applied to $e$ and $\operatorname{corepresentableBy}$ applied to $F$.

Let $e$ be an element of $\operatorname{CorepresentableBy}$ applied to $F$ and $X$. Let $\mathrm{e'}$ be an isomorphism of $F$ and $\mathrm{F'}$. Then $\operatorname{ofIso}$ applied to $e$ and $\mathrm{e'}$ is an element of $\operatorname{CorepresentableBy}$ applied to $\mathrm{F'}$ and $X$.

Let $R$ be an element of $\operatorname{CorepresentableBy}$ applied to $F$ and $X$. Let $e$ be an isomorphism of $Y$ and $X$. Then $\operatorname{ofIsoObj}$ applied to $R$ and $e$ is an element of $\operatorname{CorepresentableBy}$ applied to $F$ and $Y$.

the isomorphism of e (from the docstring)

Let $e$ be an element of $\operatorname{CorepresentableBy}$ applied to $F$ and $X$. Then the isomorphism of $e$ is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to $X$ and $F$ defined as $\operatorname{corepresentableByEquiv}$ applied to $e$.

Let $e$ be an element of $\operatorname{CorepresentableBy}$ applied to $F$ and $X$. Let $\mathrm{e'}$ be an element of $\operatorname{CorepresentableBy}$ applied to $F$ and $\mathrm{X'}$. Then $\operatorname{uniqueUpToIso}$ applied to $e$ and $\mathrm{e'}$ is an isomorphism of $X$ and $\mathrm{X'}$.

the left composition lift Coyoneda composition whiskering of hF (from the name)

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the left composition lift Coyoneda composition whiskering of $\mathrm{hF}$ is an isomorphism of the composition of the opposite of $F$ and the composition of the lift Coyoneda and the action of the left whiskering of $D$ and the set of sets and $F$ and the lift Coyoneda.

the left composition lift Yoneda composition whiskering of hF (from the name)

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the left composition lift Yoneda composition whiskering of $\mathrm{hF}$ is an isomorphism of the composition of $F$ and the composition of the lift Yoneda and the action of the left whiskering of the set of opposites of $D$ and the set of sets and the opposite of $F$ and the lift Yoneda.

the homomorphism natural isomorphism of hF and X (from the name)

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Let $X$ be an element of $C$. Then the homomorphism natural isomorphism of $\mathrm{hF}$ and $X$ is an isomorphism of the composition of the opposite of $F$ and the action of the lift Yoneda and the action of $F$ and $X$ and the action of the lift Yoneda and $X$.

the homomorphism natural isomorphism of hF and X (from the name)

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Let $X$ be an element of $C$. Then the homomorphism natural isomorphism of $\mathrm{hF}$ and $X$ is an isomorphism of the composition of $F$ and the action of the lift Coyoneda and $\operatorname{op}$ applied to the action of $F$ and $X$ and the action of the lift Coyoneda and $\operatorname{op}$ applied to $X$.

F is corepresentable (from the name)

Let $F$ be a functor of $C$ and the set of sets. Then we can say that $F$ is corepresentable.

F is representable (from the name)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then we can say that $F$ is representable.

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Let $Y$ be an element of $C$. Then the elements of $\operatorname{RepresentableBy}$ applied to $F$ and $Y$ are a basic type.

the equivalence of e (from the name)

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

the equivalence lift Yoneda isomorphism of F and X (from the name)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Let $X$ be an element of $C$. Then the equivalence lift Yoneda isomorphism of $F$ and $X$ is an equivalence from $\operatorname{RepresentableBy}$ applied to $F$ and $X$ to the set of isomorphisms of the action of the lift Yoneda and $X$ and $F$.

the homomorphism equivalence of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{RepresentableBy}$ applied to $F$ and $Y$. Then the homomorphism equivalence of $\mathrm{self}$ is an equivalence from the set of homomorphisms of $X$ and $Y$ to the action of $F$ and $\operatorname{op}$ applied to $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the isomorphism representation of F and e (from the name)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Let $e$ be an element of $\operatorname{RepresentableBy}$ applied to $F$ and $Y$. Then the isomorphism representation of $F$ and $e$ is an isomorphism of $Y$ and the representation of $F$ defined as $\operatorname{uniqueUpToIso}$ applied to $e$ and $\operatorname{representableBy}$ applied to $F$.

Let $e$ be an element of $\operatorname{RepresentableBy}$ applied to $F$ and $Y$. Let $\mathrm{e'}$ be an isomorphism of $F$ and $\mathrm{F'}$. Then $\operatorname{ofIso}$ applied to $e$ and $\mathrm{e'}$ is an element of $\operatorname{RepresentableBy}$ applied to $\mathrm{F'}$ and $Y$.

Let $R$ be an element of $\operatorname{RepresentableBy}$ applied to $F$ and $X$. Let $e$ be an isomorphism of $Y$ and $X$. Then $\operatorname{ofIsoObj}$ applied to $R$ and $e$ is an element of $\operatorname{RepresentableBy}$ applied to $F$ and $Y$.

the isomorphism of e (from the docstring)

Let $e$ be an element of $\operatorname{RepresentableBy}$ applied to $F$ and $Y$. Then the isomorphism of $e$ is an isomorphism of the action of the Yoneda and $Y$ and $F$ defined as $\operatorname{representableByEquiv}$ applied to $e$.

Let $e$ be an element of $\operatorname{RepresentableBy}$ applied to $F$ and $Y$. Let $\mathrm{e'}$ be an element of $\operatorname{RepresentableBy}$ applied to $F$ and $\mathrm{Y'}$. Then $\operatorname{uniqueUpToIso}$ applied to $e$ and $\mathrm{e'}$ is an isomorphism of $Y$ and $\mathrm{Y'}$.

the Yoneda of X (from the name)

Let $X$ be an element of $C$. Then the Yoneda of $X$ is an element of $\operatorname{RepresentableBy}$ applied to the action of the Yoneda and $X$ and $X$ defined as $\operatorname{symm}$ applied to $\operatorname{representableByEquiv}$ and the identity of the action of the Yoneda and $X$.

Let $F$ be a functor of $C$ and the set of sets. Then $\operatorname{coreprW}$ applied to $F$ is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to $\operatorname{coreprX}$ applied to $F$ and $F$ defined as the isomorphism of $\operatorname{corepresentableBy}$ applied to $F$.

Let $F$ be a functor of $C$ and the set of sets. Then $\operatorname{coreprX}$ applied to $F$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsCorepresentable\_\_has\_corepresentation}$.

Let $F$ be a functor of $C$ and the set of sets. Then $\operatorname{corepresentableBy}$ applied to $F$ is an element of $\operatorname{CorepresentableBy}$ applied to $F$ and $\operatorname{coreprX}$ applied to $F$.

$\operatorname{corepresentableByEquiv}$ is an equivalence from $\operatorname{CorepresentableBy}$ applied to $F$ and $X$ to the set of isomorphisms of the action of the Coyoneda and $\operatorname{op}$ applied to $X$ and $F$.

$\operatorname{corepresentableByUliftFunctorEquiv}$ is an equivalence from $\operatorname{CorepresentableBy}$ applied to the composition of $F$ and the functor embedding and $X$ to $\operatorname{CorepresentableBy}$ applied to $F$ and $X$.

Let $F$ be a functor of $C$ and the set of sets. Then $\operatorname{coreprx}$ applied to $F$ is an element of the action of $F$ and $\operatorname{coreprX}$ applied to $F$ defined as $\operatorname{homEquiv}$ applied to $\operatorname{corepresentableBy}$ applied to $F$ and the identity morphism of $\operatorname{coreprX}$ applied to $F$.

the representation of F (from the name)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the representation of $F$ is an isomorphism of the action of the Yoneda and the representation of $F$ and $F$ defined as the isomorphism of $\operatorname{representableBy}$ applied to $F$.

the representation of F (from the name)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the representation of $F$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsRepresentable\_\_has\_representation}$.

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{representableBy}$ applied to $F$ is an element of $\operatorname{RepresentableBy}$ applied to $F$ and the representation of $F$.

$\operatorname{representableByEquiv}$ is an equivalence from $\operatorname{RepresentableBy}$ applied to $F$ and $Y$ to the set of isomorphisms of the action of the Yoneda and $Y$ and $F$.

$\operatorname{representableByUliftFunctorEquiv}$ is an equivalence from $\operatorname{RepresentableBy}$ applied to the composition of $F$ and the functor embedding and $X$ to $\operatorname{RepresentableBy}$ applied to $F$ and $X$.

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{reprx}$ applied to $F$ is an element of the action of $F$ and $\operatorname{op}$ applied to the representation of $F$ defined as $\operatorname{homEquiv}$ applied to $\operatorname{representableBy}$ applied to $F$ and the identity morphism of the representation of $F$.

the section equivalence homomorphism of F and X (from the name)

Let $F$ be a functor of $C$ and the set of sets. Let $X$ be a set. Then the section equivalence homomorphism of $F$ and $X$ is an equivalence from the set of elements of the section of $F$ to the set of homomorphisms of the action of the constant of $C$ and $X$ and $F$.

Let $F$ be a functor of $C$ and the set of sets. Then $\operatorname{uliftCoyonedaCoreprXIso}$ applied to $F$ is an isomorphism of the action of the lift Coyoneda and $\operatorname{op}$ applied to $\operatorname{coreprX}$ applied to $F$ and $F$ defined as $\operatorname{equivUliftCoyonedaIso}$ applied to $F$, $\operatorname{coreprX}$ applied to $F$ and $\operatorname{corepresentableBy}$ applied to $F$.

the lift Yoneda representation isomorphism of F (from the name)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the lift Yoneda representation isomorphism of $F$ is an isomorphism of the action of the lift Yoneda and the representation of $F$ and $F$ defined as $\operatorname{equivUliftYonedaIso}$ applied to $F$, the representation of $F$ and $\operatorname{representableBy}$ applied to $F$.

the extension of p and Z4 (from the name)

Let $X$ and $Y$ be elements of $C$. Let $p$ be a function from elements $Z_{4}$ of $C$ and homomorphisms of $Z_{4}$ and $X$ to homomorphisms of $Z_{4}$ and $Y$. Let $q$ be a function from elements $Z_{3}$ of $C$ and homomorphisms of $Z_{3}$ and $Y$ to homomorphisms of $Z_{3}$ and $X$ such that for all elements $Z_{2}$ of $C$, for all homomorphisms $f_{2}$ of $Z_{2}$ and $X$, $\EqtMACRoH {q (Z_{2} , p (Z_{2} , f_{2}))}{f_{2}}$ and for all elements $Z_{1}$ of $C$, for all homomorphisms $f_{1}$ of $Z_{1}$ and $Y$, $\EqtMACRoH {p (Z_{1} , q (Z_{1} , f_{1}))}{f_{1}}$. Assume that for all elements $Z$ and $\mathrm{Z'}$ of $C$, for all homomorphisms $f$ of $\mathrm{Z'}$ and $Z$, for all homomorphisms $g$ of $Z$ and $X$, $p$ applied to $\mathrm{Z'}$ and the composition of $f$ and $g$ is equal to the composition of $f$ and $p$ applied to $Z$ and $g$. Then the extension of $Z_{4}$ and $p$ is an isomorphism of $X$ and $Y$.

$\operatorname{fullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the Yoneda.

the Coyoneda (from the name)

The Coyoneda is a functor of the set of opposites of $C$ and the set of functors of $C$ and the set of sets defined as the flip of the Yoneda.

the Coyoneda composition Yoneda object of P (from the name)

Let $P$ be a functor of $C$ and the set of sets. Then the Coyoneda composition Yoneda object of $P$ is an isomorphism of the composition of the right opposite of the Coyoneda and the action of the Yoneda and $P$ and the composition of $P$ and the functor embedding defined as the right isomorphism whisker of the curried version of the Coyoneda lemma and the action of the evaluation of the set of functors of $C$ and the set of sets and the set of sets and $P$.

the Coyoneda equivalence (from the name)

The Coyoneda equivalence is an equivalence from the set of homomorphisms of the action of the Coyoneda and $\operatorname{op}$ applied to $X$ and $F$ to the action of $F$ and $X$.

the Coyoneda evaluation of C (from the name)

Let $C$ be a set. Then the Coyoneda evaluation of $C$ is a functor of $\mathrm{Prod}$ applied to $C$ and the set of functors of $C$ and the set of sets and the set of sets defined as the composition of $\operatorname{evaluationUncurried}$ applied to $C$ and the set of sets and the functor embedding.

the Coyoneda lemma of C (from the name)

Let $C$ be a set. Then the Coyoneda lemma of $C$ is an isomorphism of the Coyoneda pairing of $C$ and the Coyoneda evaluation of $C$.

the Coyoneda pairing of C (from the name)

Let $C$ be a set. Then the Coyoneda pairing of $C$ is a functor of $\mathrm{Prod}$ applied to $C$ and the set of functors of $C$ and the set of sets and the set of sets defined as the composition of the product of the right opposite of the Coyoneda and the identity of the set of functors of $C$ and the set of sets and the homomorphism of the set of functors of $C$ and the set of sets.

Let $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$ be elements of $C$. Then $\mathrm{CategoryTheory\_\_coyoneda\_obj\_obj\_eq\_hom}$ holds for $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$, if if $\EqtMACRoH {X}{\mathrm{X'}}$, then if $\EqtMACRoH {Y}{\mathrm{Y'}}$, then the action of the action of the Coyoneda and $\operatorname{op}$ applied to $X$ and $Y$ is equal to the set of homomorphisms of $\mathrm{X'}$ and $\mathrm{Y'}$.

Let $X$ and $\mathrm{X'}$ be elements of $C$. Let $Y$ and $\mathrm{Y'}$ be opposites of $C$. Then $\mathrm{CategoryTheory\_\_coyoneda\_obj\_obj\_eq\_hom'}$ holds for $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$, if if $\EqtMACRoH {X}{\mathrm{X'}}$, then if $\EqtMACRoH {Y}{\mathrm{Y'}}$, then the action of the action of the Coyoneda and $Y$ and $X$ is equal to the set of homomorphisms of the opposite of $\mathrm{Y'}$ and $\mathrm{X'}$.

the curried Coyoneda lemma (from the name)

The curried Coyoneda lemma is an isomorphism of the composition of the right opposite of the Coyoneda and the Coyoneda and the evaluation of $C$ and the set of sets.

the curried Coyoneda lemma (from the name)

The curried Coyoneda lemma is an isomorphism of the composition of the Yoneda and the action of the left whiskering of the set of opposites of the set of functors of $C$ and the set of sets and the set of sets and the right opposite of the Coyoneda and the identity of the set of functors of $C$ and the set of sets.

the curried Yoneda lemma (from the name)

The curried Yoneda lemma is an isomorphism of the composition of the opposite of the Yoneda and the Coyoneda and the evaluation of the set of opposites of $C$ and the set of sets.

the curried Yoneda lemma (from the name)

The curried Yoneda lemma is an isomorphism of the composition of the Yoneda and the action of the left whiskering of the set of opposites of the set of functors of the set of opposites of $C$ and the set of sets and the set of sets and the opposite of the Yoneda and the identity of the set of functors of the set of opposites of $C$ and the set of sets.

the curried version of the Coyoneda lemma (from the docstring)

The curried version of the Coyoneda lemma is an isomorphism of the composition of the right opposite of the Coyoneda and the Coyoneda and the composition of the evaluation of $C$ and the set of sets and the action of the right whiskering of the set of sets and the set of sets and the functor embedding.

the curried version of the Yoneda lemma (from the docstring)

The curried version of the Yoneda lemma is an isomorphism of the composition of the opposite of the Yoneda and the Coyoneda and the composition of the evaluation of the set of opposites of $C$ and the set of sets and the action of the right whiskering of the set of sets and the set of sets and the functor embedding.

the section functor natural isomorphism Coyoneda of X (from the name)

Let $X$ be a set. Then the section functor natural isomorphism Coyoneda of $X$ is an isomorphism of the section functor of $C$ and the action of the Coyoneda and $\operatorname{op}$ applied to the action of the constant of $C$ and $X$.

the lift Coyoneda (from the name)

The lift Coyoneda is a functor of the set of opposites of $C$ and the set of functors of $C$ and the set of sets defined as the flip of the lift Yoneda.

the lift Coyoneda equivalence (from the name)

The lift Coyoneda equivalence is an equivalence from the set of homomorphisms of the action of the lift Coyoneda and $X$ and $F$ to the action of $F$ and the opposite of $X$.

the lift Coyoneda isomorphism Coyoneda (from the name)

The lift Coyoneda isomorphism Coyoneda is an isomorphism of the lift Coyoneda and the Coyoneda.

the lift Coyoneda right opposite composition Coyoneda (from the name)

The lift Coyoneda right opposite composition Coyoneda is an isomorphism of the composition of the right opposite of the lift Coyoneda and the Coyoneda and the composition of the evaluation of $C$ and the set of sets and the action of the right whiskering of the set of sets and the set of sets and the functor embedding.

Let $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$ be elements of $C$. Then $\mathrm{CategoryTheory\_\_uliftCoyoneda\_obj\_obj\_eq\_hom}$ holds for $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$, if if $\EqtMACRoH {X}{\mathrm{X'}}$, then if $\EqtMACRoH {Y}{\mathrm{Y'}}$, then the action of the action of the lift Coyoneda and $\operatorname{op}$ applied to $X$ and $Y$ is equal to $\mathrm{ULift}$ applied to the set of homomorphisms of $\mathrm{Y'}$ and $\mathrm{X'}$.

Let $X$ and $\mathrm{X'}$ be opposites of $C$. Let $Y$ and $\mathrm{Y'}$ be elements of $C$. Then $\mathrm{CategoryTheory\_\_uliftCoyoneda\_obj\_obj\_eq\_hom'}$ holds for $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$, if if $\EqtMACRoH {X}{\mathrm{X'}}$, then if $\EqtMACRoH {Y}{\mathrm{Y'}}$, then the action of the action of the lift Coyoneda and $X$ and $Y$ is equal to $\mathrm{ULift}$ applied to the set of homomorphisms of $\mathrm{Y'}$ and the opposite of $\mathrm{X'}$.

the lift Yoneda (from the name)

The lift Yoneda is a functor of $C$ and the set of functors of the set of opposites of $C$ and the set of sets defined as the composition of the Yoneda and the action of the right whiskering of the set of sets and the set of sets and the functor embedding.

the lift Yoneda equivalence (from the name)

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

the lift Yoneda isomorphism Yoneda (from the name)

The lift Yoneda isomorphism Yoneda is an isomorphism of the lift Yoneda and the Yoneda.

the lift Yoneda map of F and X (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then the lift Yoneda map of $F$ and $X$ is a homomorphism of the action of the lift Yoneda and $X$ and the composition of the opposite of $F$ and the action of the lift Yoneda and the action of $F$ and $X$.

the lift Yoneda opposite composition Coyoneda (from the name)

The lift Yoneda opposite composition Coyoneda is an isomorphism of the composition of the opposite of the lift Yoneda and the Coyoneda and the composition of the evaluation of the set of opposites of $C$ and the set of sets and the action of the right whiskering of the set of sets and the set of sets and the functor embedding.

Let $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$ be elements of $C$. Then $\mathrm{CategoryTheory\_\_uliftYoneda\_obj\_obj\_eq\_hom}$ holds for $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$, if if $\EqtMACRoH {X}{\mathrm{X'}}$, then if $\EqtMACRoH {Y}{\mathrm{Y'}}$, then the action of the action of the lift Yoneda and $X$ and $\operatorname{op}$ applied to $Y$ is equal to $\mathrm{ULift}$ applied to the set of homomorphisms of $\mathrm{Y'}$ and $\mathrm{X'}$.

Let $X$ and $\mathrm{X'}$ be elements of $C$. Let $Y$ and $\mathrm{Y'}$ be opposites of $C$. Then $\mathrm{CategoryTheory\_\_uliftYoneda\_obj\_obj\_eq\_hom'}$ holds for $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$, if if $\EqtMACRoH {X}{\mathrm{X'}}$, then if $\EqtMACRoH {Y}{\mathrm{Y'}}$, then the action of the action of the lift Yoneda and $X$ and $Y$ is equal to $\mathrm{ULift}$ applied to the set of homomorphisms of the opposite of $\mathrm{Y'}$ and $\mathrm{X'}$.

the Yoneda (from the name)

The Yoneda is a functor of $C$ and the set of functors of the set of opposites of $C$ and the set of sets.

the Yoneda equivalence (from the name)

The Yoneda equivalence is an equivalence from the set of homomorphisms of the action of the Yoneda and $X$ and $F$ to the action of $F$ and $\operatorname{op}$ applied to $X$.

the Yoneda evaluation of C (from the name)

Let $C$ be a set. Then the Yoneda evaluation of $C$ is a functor of $\mathrm{Prod}$ applied to the set of opposites of $C$ and the set of functors of the set of opposites of $C$ and the set of sets and the set of sets defined as the composition of $\operatorname{evaluationUncurried}$ applied to the set of opposites of $C$ and the set of sets and the functor embedding.

the Yoneda lemma of C (from the name)

Let $C$ be a set. Then the Yoneda lemma of $C$ is an isomorphism of the Yoneda pairing of $C$ and the Yoneda evaluation of $C$.

the Yoneda map of F and X (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then the Yoneda map of $F$ and $X$ is a homomorphism of the action of the Yoneda and $X$ and the composition of the opposite of $F$ and the action of the Yoneda and the action of $F$ and $X$.

the Yoneda opposite composition Yoneda object of P (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Then the Yoneda opposite composition Yoneda object of $P$ is an isomorphism of the composition of the opposite of the Yoneda and the action of the Yoneda and $P$ and the composition of $P$ and the functor embedding defined as the right isomorphism whisker of the curried version of the Yoneda lemma and the action of the evaluation of the set of functors of the set of opposites of $C$ and the set of sets and the set of sets and $P$.

the Yoneda pairing of C (from the name)

Let $C$ be a set. Then the Yoneda pairing of $C$ is a functor of $\mathrm{Prod}$ applied to the set of opposites of $C$ and the set of functors of the set of opposites of $C$ and the set of sets and the set of sets defined as the composition of the product of the opposite of the Yoneda and the identity of the set of functors of the set of opposites of $C$ and the set of sets and the homomorphism of the set of functors of the set of opposites of $C$ and the set of sets.

Let $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$ be elements of $C$. Then $\mathrm{CategoryTheory\_\_yoneda\_obj\_obj\_eq\_hom}$ holds for $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$, if if $\EqtMACRoH {X}{\mathrm{X'}}$, then if $\EqtMACRoH {Y}{\mathrm{Y'}}$, then the action of the action of the Yoneda and $X$ and $\operatorname{op}$ applied to $Y$ is equal to the set of homomorphisms of $\mathrm{Y'}$ and $\mathrm{X'}$.

Let $X$ and $\mathrm{X'}$ be elements of $C$. Let $Y$ and $\mathrm{Y'}$ be opposites of $C$. Then $\mathrm{CategoryTheory\_\_yoneda\_obj\_obj\_eq\_hom'}$ holds for $X$, $\mathrm{X'}$, $Y$ and $\mathrm{Y'}$, if if $\EqtMACRoH {X}{\mathrm{X'}}$, then if $\EqtMACRoH {Y}{\mathrm{Y'}}$, then the action of the action of the Yoneda and $X$ and $Y$ is equal to the set of homomorphisms of the opposite of $\mathrm{Y'}$ and $\mathrm{X'}$.