Definitions: Mathlib.CategoryTheory, part 5 of 25

the comma map equivalence of x9 and X (from the name)

Let $x_{8}$ be a homomorphism of the composition of $x_{6}$ and $\mathrm{L'}$ and the composition of $L$ and $F$. Let $x_{9}$ be a homomorphism of the composition of $R$ and $F$ and the composition of $x_{7}$ and $\mathrm{R'}$. Let $X$ be a comma of $\mathrm{L'}$ and $\mathrm{R'}$. Then the comma map equivalence of $x_{9}$ and $X$ is an equivalence of the set of structured arrows of $X$ and the map of $x_{8}$ and $x_{9}$ and the set of commas of the map of the identity morphism of the action of $\mathrm{L'}$ and the left subobject of $X$ and $x_{8}$ and the map of the homomorphism of $X$ and the inverse of $x_{9}$.

the comma map equivalence counit isomorphism of x9 and X (from the name)

Let $x_{8}$ be a homomorphism of the composition of $x_{6}$ and $\mathrm{L'}$ and the composition of $L$ and $F$. Let $x_{9}$ be a homomorphism of the composition of $R$ and $F$ and the composition of $x_{7}$ and $\mathrm{R'}$. Let $X$ be a comma of $\mathrm{L'}$ and $\mathrm{R'}$. Then the comma map equivalence counit isomorphism of $x_{9}$ and $X$ is an isomorphism of the composition of the comma map equivalence inverse of $x_{9}$ and $X$ and the comma map equivalence functor of $x_{9}$ and $X$ and the identity of the set of commas of the map of the identity morphism of the action of $\mathrm{L'}$ and the left subobject of $X$ and $x_{8}$ and the map of the homomorphism of $X$ and the inverse of $x_{9}$.

the comma map equivalence functor of x9 and X (from the name)

Let $x_{8}$ be a homomorphism of the composition of $x_{6}$ and $\mathrm{L'}$ and the composition of $L$ and $F$. Let $x_{9}$ be a homomorphism of the composition of $R$ and $F$ and the composition of $x_{7}$ and $\mathrm{R'}$. Let $X$ be a comma of $\mathrm{L'}$ and $\mathrm{R'}$. Then the comma map equivalence functor of $x_{9}$ and $X$ is a functor of the set of structured arrows of $X$ and the map of $x_{8}$ and $x_{9}$ and the set of commas of the map of the identity morphism of the action of $\mathrm{L'}$ and the left subobject of $X$ and $x_{8}$ and the map of the homomorphism of $X$ and the inverse of $x_{9}$.

the comma map equivalence inverse of x9 and X (from the name)

Let $x_{8}$ be a homomorphism of the composition of $x_{6}$ and $\mathrm{L'}$ and the composition of $L$ and $F$. Let $x_{9}$ be a homomorphism of the composition of $R$ and $F$ and the composition of $x_{7}$ and $\mathrm{R'}$. Let $X$ be a comma of $\mathrm{L'}$ and $\mathrm{R'}$. Then the comma map equivalence inverse of $x_{9}$ and $X$ is a functor of the set of commas of the map of the identity morphism of the action of $\mathrm{L'}$ and the left subobject of $X$ and $x_{8}$ and the map of the homomorphism of $X$ and the inverse of $x_{9}$ and the set of structured arrows of $X$ and the map of $x_{8}$ and $x_{9}$.

the comma map equivalence unit isomorphism of x9 and X (from the name)

Let $x_{8}$ be a homomorphism of the composition of $x_{6}$ and $\mathrm{L'}$ and the composition of $L$ and $F$. Let $x_{9}$ be a homomorphism of the composition of $R$ and $F$ and the composition of $x_{7}$ and $\mathrm{R'}$. Let $X$ be a comma of $\mathrm{L'}$ and $\mathrm{R'}$. Then the comma map equivalence unit isomorphism of $x_{9}$ and $X$ is an isomorphism of the identity of the set of structured arrows of $X$ and the map of $x_{8}$ and $x_{9}$ and the composition of the comma map equivalence functor of $x_{9}$ and $X$ and the comma map equivalence inverse of $x_{9}$ and $X$.

the comma to Grothendieck precomposition functor of L and R (from the name)

Let $L$ be a functor of $C$ and $D$. Let $R$ be a functor of $E$ and $D$. Then the comma to Grothendieck precomposition functor of $L$ and $R$ is a functor of the set of commas of $L$ and $R$ and $\operatorname{Grothendieck}$ applied to the composition of $R$ and the functor of $L$.

the functor of T (from the name)

Let $T$ be a functor of $C$ and $D$. Then the functor of $T$ is a functor of $D$ and the set of categories.

the Grothendieck precomposition functor equivalence of L and R (from the name)

Let $L$ be a functor of $C$ and $D$. Let $R$ be a functor of $E$ and $D$. Then the Grothendieck precomposition functor equivalence of $L$ and $R$ is an equivalence of $\operatorname{Grothendieck}$ applied to the composition of $R$ and the functor of $L$ and the set of commas of $L$ and $R$.

the Grothendieck precomposition functor to comma of L and R (from the name)

Let $L$ be a functor of $C$ and $D$. Let $R$ be a functor of $E$ and $D$. Then the Grothendieck precomposition functor to comma of $L$ and $R$ is a functor of $\operatorname{Grothendieck}$ applied to the composition of $R$ and the functor of $L$ and the set of commas of $L$ and $R$.

the Grothendieck projection of L (from the name)

Let $L$ be a functor of $C$ and $D$. Then the Grothendieck projection of $L$ is a functor of $\operatorname{Grothendieck}$ applied to the functor of $L$ and $C$ defined as the composition of the Grothendieck precomposition functor to comma of $L$ and the identity of $D$ and the first component of $L$ and the identity of $D$.

the map composition inclusion composition Grothendieck projection of L and f (from the name)

Let $L$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map composition inclusion composition Grothendieck projection of $L$ and $f$ is an isomorphism of the composition of the map of $f$ and the composition of the inclusion of the functor of $L$ and $Y$ and the Grothendieck projection of $L$ and the projection of $L$ and $X$ defined as the left isomorphism whisker of the map of $f$ and the inclusion composition Grothendieck precomposition functor to comma composition first component of the identity of $D$ and $Y$.

the functor of S and T (from the docstring)

Let $S$ be a functor of $C$ and $D$. Let $T$ be a functor of $D$ and $E$. Then the functor of $S$ and $T$ is a homomorphism of the functor of the composition of $S$ and $T$ and the functor of $T$.

the inclusion composition Grothendieck precomposition functor to comma composition first component of R and X (from the name)

Let $L$ be a functor of $C$ and $D$. Let $R$ be a functor of $E$ and $D$. Let $X$ be an element of $E$. Then the inclusion composition Grothendieck precomposition functor to comma composition first component of $R$ and $X$ is an isomorphism of the composition of the inclusion of the composition of $R$ and the functor of $L$ and $X$ and the composition of the Grothendieck precomposition functor to comma of $L$ and $R$ and the first component of $L$ and $R$ and the projection of $L$ and the action of $R$ and $X$.

the inclusion composition Grothendieck projection of L and X (from the name)

Let $L$ be a functor of $C$ and $D$. Let $X$ be an element of $D$. Then the inclusion composition Grothendieck projection of $L$ and $X$ is an isomorphism of the composition of the inclusion of the functor of $L$ and $X$ and the Grothendieck projection of $L$ and the projection of $L$ and $X$ defined as the inclusion composition Grothendieck precomposition functor to comma composition first component of the identity of $D$ and $X$.

the functor of T (from the name)

Let $T$ be a functor of $C$ and $D$. Then the functor of $T$ is a functor of the set of opposites of $D$ and the set of categories.

composable arrow of C and n (from the name)

Let $C$ be a set. Let $n$ be a natural number. Then a composable arrow of $C$ and $n$ is an element of the function that maps $C$ and $n$ to the set of functors of $\mathrm{Fin}$ applied to $n + 1$ and $C$.

the map of i and j (from the name)

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $2$ such that $i \leq j$. Then the map of $i$ and $j$ is a homomorphism of the object of $x_{2}$ and $i$ and the object of $x_{2}$ and $j$.

the object of x1 and x2 (from the name)

Let $x$ and $x_{1}$ be elements of $C$. Let $x_{2}$ be an element of $\mathrm{Fin}$ applied to $2$. Then the object of $x_{1}$ and $x_{2}$ is an element of $C$.

the object of X and x1 (from the name)

Let $F$ be a composable arrow of $C$ and $n$. Let $X$ be an element of $C$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $n + 1 + 1$. Then the object of $X$ and $x_{1}$ is an element of $C$.

the application of x1 and i (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $G$. Let $i$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (i , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_app'\_\_\_auto\_1}$. Then the application of $x_{1}$ and $i$ is a homomorphism of the object of $F$ and $i$ and the object of $G$ and $i$.

the arrow of F and i (from the name)

Let $F$ be a composable arrow of $C$ and $n$. Let $i$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Lt} (i , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_arrow\_\_\_auto\_1}$. Then the arrow of $F$ and $i$ is a composable arrow of $C$ and $1$.

the arrow equivalence (from the name)

The arrow equivalence is an equivalence from the set of composable arrows of $C$ and $1$ to the set of arrows of $C$.

the homomorphism of F (from the name)

Let $F$ be a composable arrow of $C$ and $n$. Then the homomorphism of $F$ is a homomorphism of the leftmost object of $F$ and the rightmost object of $F$.

the homomorphism of app and i1 (from the name)

Let $\mathrm{app}$ be a function from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n + 1$ to homomorphisms of the action of $F$ and $i_{1}$ and the action of $G$ and $i_{1}$ such that for all natural numbers $i$, for all elements $\mathrm{hi}$ of $\mathrm{Proof}$ applied to $\mathrm{Lt} (i , n)$, the composition of the map of $i$ and $i + 1$ and $\mathrm{app}$ applied to $\operatorname{mk}$ applied to $i + 1$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_map'\_\_\_proof\_8}$ applied to $i + 1$ and $\mathrm{hi}$ is equal to the composition of $\mathrm{app}$ applied to $\operatorname{mk}$ applied to $i$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_map'\_\_\_proof\_6}$ applied to $i$, $i + 1$, $\mathrm{CategoryTheory\_\_ComposableArrows\_\_homMk\_\_\_proof\_2}$ applied to $i$ and $\mathrm{hi}$ and the map of $i$ and $i + 1$. Then the homomorphism of $i_{1}$ and $\mathrm{app}$ is a homomorphism of $F$ and $G$.

the homomorphism successor of x1 and x2 (from the name)

Let $x_{1}$ be a homomorphism of the object of $F$ and $0$ and the object of $G$ and $0$. Let $x_{2}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_\_u3b4\_\_u2080\_}$ applied to $F$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_\_u3b4\_\_u2080\_}$ applied to $G$ such that the composition of the map of $0$ and $1$ and the application of $x_{2}$ and $0$ is equal to the composition of $x_{1}$ and the map of $0$ and $1$. Then the homomorphism successor of $x_{1}$ and $x_{2}$ is a homomorphism of $F$ and $G$.

the homomorphism of f (from the name)

Let $f$ be a homomorphism of the object of $F$ and $0$ and the object of $G$ and $0$. Then the homomorphism of $f$ is a homomorphism of $F$ and $G$.

the homomorphism of left and right (from the name)

Let $\mathrm{left}$ be a homomorphism of the object of $F$ and $0$ and the object of $G$ and $0$. Let $\mathrm{right}$ be a homomorphism of the object of $F$ and $1$ and the object of $G$ and $1$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $0$ and $1$ and $\mathrm{right}$ is equal to the composition of $\mathrm{left}$ and the map of $0$ and $1$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_homMk\_u2081\_\_\_\_auto\_1}$. Then the homomorphism of $\mathrm{left}$ and $\mathrm{right}$ is a homomorphism of $F$ and $G$.

the homomorphism of x2 and x3 (from the name)

Let $x_{1}$ be a homomorphism of the object of $f$ and $0$ and the object of $g$ and $0$. Let $x_{2}$ be a homomorphism of the object of $f$ and $1$ and the object of $g$ and $1$. Let $x_{3}$ be a homomorphism of the object of $f$ and $2$ and the object of $g$ and $2$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $0$ and $1$ and $x_{2}$ is equal to the composition of $x_{1}$ and the map of $0$ and $1$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_259}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $1$ and $2$ and $x_{3}$ is equal to the composition of $x_{2}$ and the map of $1$ and $2$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_261}$. Then the homomorphism of $x_{2}$ and $x_{3}$ is a homomorphism of $f$ and $g$ defined as the homomorphism successor of $x_{1}$ and the homomorphism of $x_{2}$ and $x_{3}$.

the homomorphism of x3 and x4 (from the name)

Let $x_{1}$ be a homomorphism of the object of $f$ and $0$ and the object of $g$ and $0$. Let $x_{2}$ be a homomorphism of the object of $f$ and $1$ and the object of $g$ and $1$. Let $x_{3}$ be a homomorphism of the object of $f$ and $2$ and the object of $g$ and $2$. Let $x_{4}$ be a homomorphism of the object of $f$ and $3$ and the object of $g$ and $3$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $0$ and $1$ and $x_{2}$ is equal to the composition of $x_{1}$ and the map of $0$ and $1$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_305}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $1$ and $2$ and $x_{3}$ is equal to the composition of $x_{2}$ and the map of $1$ and $2$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_307}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $2$ and $3$ and $x_{4}$ is equal to the composition of $x_{3}$ and the map of $2$ and $3$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_309}$. Then the homomorphism of $x_{3}$ and $x_{4}$ is a homomorphism of $f$ and $g$ defined as the homomorphism successor of $x_{1}$ and the homomorphism of $x_{3}$ and $x_{4}$.

the homomorphism of x4 and x5 (from the name)

Let $x_{1}$ be a homomorphism of the object of $f$ and $0$ and the object of $g$ and $0$. Let $x_{2}$ be a homomorphism of the object of $f$ and $1$ and the object of $g$ and $1$. Let $x_{3}$ be a homomorphism of the object of $f$ and $2$ and the object of $g$ and $2$. Let $x_{4}$ be a homomorphism of the object of $f$ and $3$ and the object of $g$ and $3$. Let $x_{5}$ be a homomorphism of the object of $f$ and $4$ and the object of $g$ and $4$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $0$ and $1$ and $x_{2}$ is equal to the composition of $x_{1}$ and the map of $0$ and $1$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_361}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $1$ and $2$ and $x_{3}$ is equal to the composition of $x_{2}$ and the map of $1$ and $2$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_363}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $2$ and $3$ and $x_{4}$ is equal to the composition of $x_{3}$ and the map of $2$ and $3$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_365}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $3$ and $4$ and $x_{5}$ is equal to the composition of $x_{4}$ and the map of $3$ and $4$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_367}$. Then the homomorphism of $x_{4}$ and $x_{5}$ is a homomorphism of $f$ and $g$ defined as the homomorphism successor of $x_{1}$ and the homomorphism of $x_{4}$ and $x_{5}$.

the homomorphism of x5 and x6 (from the name)

Let $x_{1}$ be a homomorphism of the object of $f$ and $0$ and the object of $g$ and $0$. Let $x_{2}$ be a homomorphism of the object of $f$ and $1$ and the object of $g$ and $1$. Let $x_{3}$ be a homomorphism of the object of $f$ and $2$ and the object of $g$ and $2$. Let $x_{4}$ be a homomorphism of the object of $f$ and $3$ and the object of $g$ and $3$. Let $x_{5}$ be a homomorphism of the object of $f$ and $4$ and the object of $g$ and $4$. Let $x_{6}$ be a homomorphism of the object of $f$ and $5$ and the object of $g$ and $5$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $0$ and $1$ and $x_{2}$ is equal to the composition of $x_{1}$ and the map of $0$ and $1$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_443}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $1$ and $2$ and $x_{3}$ is equal to the composition of $x_{2}$ and the map of $1$ and $2$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_445}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $2$ and $3$ and $x_{4}$ is equal to the composition of $x_{3}$ and the map of $2$ and $3$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_447}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $3$ and $4$ and $x_{5}$ is equal to the composition of $x_{4}$ and the map of $3$ and $4$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_449}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $4$ and $5$ and $x_{6}$ is equal to the composition of $x_{5}$ and the map of $4$ and $5$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_ComposableArrows\_\_Basic\_\_0\_\_\_auto\_451}$. Then the homomorphism of $x_{5}$ and $x_{6}$ is a homomorphism of $f$ and $g$ defined as the homomorphism successor of $x_{1}$ and the homomorphism of $x_{5}$ and $x_{6}$.

the isomorphism of app and i1 (from the name)

Let $\mathrm{app}$ be a function from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n + 1$ to isomorphisms of the action of $F$ and $i_{1}$ and the action of $G$ and $i_{1}$ such that for all natural numbers $i$, for all elements $\mathrm{hi}$ of $\mathrm{Proof}$ applied to $\mathrm{Lt} (i , n)$, the composition of the map of $i$ and $i + 1$ and the homomorphism of $\mathrm{app}$ applied to $\operatorname{mk}$ applied to $i + 1$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_map'\_\_\_proof\_8}$ applied to $i + 1$ and $\mathrm{hi}$ is equal to the composition of the homomorphism of $\mathrm{app}$ applied to $\operatorname{mk}$ applied to $i$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_map'\_\_\_proof\_6}$ applied to $i$, $i + 1$, $\mathrm{CategoryTheory\_\_ComposableArrows\_\_homMk\_\_\_proof\_2}$ applied to $i$ and $\mathrm{hi}$ and the map of $i$ and $i + 1$. Then the isomorphism of $i_{1}$ and $\mathrm{app}$ is an isomorphism of $F$ and $G$.

the isomorphism successor of x1 and x2 (from the name)

Let $x_{1}$ be an isomorphism of the object of $F$ and $0$ and the object of $G$ and $0$. Let $x_{2}$ be an isomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_\_u3b4\_\_u2080\_}$ applied to $F$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_\_u3b4\_\_u2080\_}$ applied to $G$ such that the composition of the map of $0$ and $1$ and the application of the homomorphism of $x_{2}$ and $0$ is equal to the composition of the homomorphism of $x_{1}$ and the map of $0$ and $1$. Then the isomorphism successor of $x_{1}$ and $x_{2}$ is an isomorphism of $F$ and $G$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of the object of $F$ and $0$ and the object of $G$ and $0$. Then the isomorphism of $e$ is an isomorphism of $F$ and $G$.

the isomorphism of left and right (from the name)

Let $\mathrm{left}$ be an isomorphism of the object of $F$ and $0$ and the object of $G$ and $0$. Let $\mathrm{right}$ be an isomorphism of the object of $F$ and $1$ and the object of $G$ and $1$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $0$ and $1$ and the homomorphism of $\mathrm{right}$ is equal to the composition of the homomorphism of $\mathrm{left}$ and the map of $0$ and $1$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_isoMk\_u2081\_\_\_\_auto\_1}$. Then the isomorphism of $\mathrm{left}$ and $\mathrm{right}$ is an isomorphism of $F$ and $G$.

the isomorphism of x2 and x3 (from the name)

Let $x_{1}$ be an isomorphism of the object of $f$ and $0$ and the object of $g$ and $0$. Let $x_{2}$ be an isomorphism of the object of $f$ and $1$ and the object of $g$ and $1$. Let $x_{3}$ be an isomorphism of the object of $f$ and $2$ and the object of $g$ and $2$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $0$ and $1$ and the homomorphism of $x_{2}$ is equal to the composition of the homomorphism of $x_{1}$ and the map of $0$ and $1$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_isoMk\_u2082\_\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $1$ and $2$ and the homomorphism of $x_{3}$ is equal to the composition of the homomorphism of $x_{2}$ and the map of $1$ and $2$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_isoMk\_u2082\_\_\_\_auto\_3}$. Then the isomorphism of $x_{2}$ and $x_{3}$ is an isomorphism of $f$ and $g$.

the isomorphism of x3 and x4 (from the name)

Let $x_{1}$ be an isomorphism of the object of $f$ and $0$ and the object of $g$ and $0$. Let $x_{2}$ be an isomorphism of the object of $f$ and $1$ and the object of $g$ and $1$. Let $x_{3}$ be an isomorphism of the object of $f$ and $2$ and the object of $g$ and $2$. Let $x_{4}$ be an isomorphism of the object of $f$ and $3$ and the object of $g$ and $3$. Assume that the composition of the map of $0$ and $1$ and the homomorphism of $x_{2}$ is equal to the composition of the homomorphism of $x_{1}$ and the map of $0$ and $1$. Assume that the composition of the map of $1$ and $2$ and the homomorphism of $x_{3}$ is equal to the composition of the homomorphism of $x_{2}$ and the map of $1$ and $2$. Assume that the composition of the map of $2$ and $3$ and the homomorphism of $x_{4}$ is equal to the composition of the homomorphism of $x_{3}$ and the map of $2$ and $3$. Then the isomorphism of $x_{3}$ and $x_{4}$ is an isomorphism of $f$ and $g$.

the isomorphism of x4 and x5 (from the name)

Let $x_{1}$ be an isomorphism of the object of $f$ and $0$ and the object of $g$ and $0$. Let $x_{2}$ be an isomorphism of the object of $f$ and $1$ and the object of $g$ and $1$. Let $x_{3}$ be an isomorphism of the object of $f$ and $2$ and the object of $g$ and $2$. Let $x_{4}$ be an isomorphism of the object of $f$ and $3$ and the object of $g$ and $3$. Let $x_{5}$ be an isomorphism of the object of $f$ and $4$ and the object of $g$ and $4$. Assume that the composition of the map of $0$ and $1$ and the homomorphism of $x_{2}$ is equal to the composition of the homomorphism of $x_{1}$ and the map of $0$ and $1$. Assume that the composition of the map of $1$ and $2$ and the homomorphism of $x_{3}$ is equal to the composition of the homomorphism of $x_{2}$ and the map of $1$ and $2$. Assume that the composition of the map of $2$ and $3$ and the homomorphism of $x_{4}$ is equal to the composition of the homomorphism of $x_{3}$ and the map of $2$ and $3$. Assume that the composition of the map of $3$ and $4$ and the homomorphism of $x_{5}$ is equal to the composition of the homomorphism of $x_{4}$ and the map of $3$ and $4$. Then the isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $f$ and $g$.

the isomorphism of x5 and x6 (from the name)

Let $x_{1}$ be an isomorphism of the object of $f$ and $0$ and the object of $g$ and $0$. Let $x_{2}$ be an isomorphism of the object of $f$ and $1$ and the object of $g$ and $1$. Let $x_{3}$ be an isomorphism of the object of $f$ and $2$ and the object of $g$ and $2$. Let $x_{4}$ be an isomorphism of the object of $f$ and $3$ and the object of $g$ and $3$. Let $x_{5}$ be an isomorphism of the object of $f$ and $4$ and the object of $g$ and $4$. Let $x_{6}$ be an isomorphism of the object of $f$ and $5$ and the object of $g$ and $5$. Assume that the composition of the map of $0$ and $1$ and the homomorphism of $x_{2}$ is equal to the composition of the homomorphism of $x_{1}$ and the map of $0$ and $1$. Assume that the composition of the map of $1$ and $2$ and the homomorphism of $x_{3}$ is equal to the composition of the homomorphism of $x_{2}$ and the map of $1$ and $2$. Assume that the composition of the map of $2$ and $3$ and the homomorphism of $x_{4}$ is equal to the composition of the homomorphism of $x_{3}$ and the map of $2$ and $3$. Assume that the composition of the map of $3$ and $4$ and the homomorphism of $x_{5}$ is equal to the composition of the homomorphism of $x_{4}$ and the map of $3$ and $4$. Assume that the composition of the map of $4$ and $5$ and the homomorphism of $x_{6}$ is equal to the composition of the homomorphism of $x_{5}$ and the map of $4$ and $5$. Then the isomorphism of $x_{5}$ and $x_{6}$ is an isomorphism of $f$ and $g$.

the leftmost object of F (from the docstring)

Let $F$ be a composable arrow of $C$ and $n$. Then the leftmost object of $F$ is an element of $C$.

the map of i and j (from the name)

Let $F$ be a composable arrow of $C$ and $n$. Let $i$ and $j$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (i , j)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_map'\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Leq} (j , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_map'\_\_\_auto\_3}$. Then the map of $i$ and $j$ is a homomorphism of the action of $F$ and $\operatorname{mk}$ applied to $i$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_map'\_\_\_proof\_6}$ applied to $i$, $j$, $\mathrm{hij}$ and $\mathrm{hjn}$ and the action of $F$ and $\operatorname{mk}$ applied to $j$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_map'\_\_\_proof\_8}$ applied to $j$ and $\mathrm{hjn}$.

Let $\mathrm{obj}$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $C$. Let $\mathrm{mapSucc}$ be a function from elements $i$ of $\mathrm{Fin}$ applied to $n$ to homomorphisms of $\mathrm{obj}$ applied to $\operatorname{castSucc}$ applied to $i$ and $\mathrm{obj}$ applied to $\operatorname{succ}$ applied to $i$. Then $\operatorname{mkOfObjOfMapSucc}$ applied to $\mathrm{obj}$, $i$ and $\mathrm{mapSucc}$ is a composable arrow of $C$ and $n$.

Let $X$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2080\_}$ applied to $X$ is a composable arrow of $C$ and $0$ defined as the action of the constant of $\mathrm{Fin}$ applied to $1$ and $X$.

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $f$ is a composable arrow of $C$ and $1$.

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a homomorphism of $x_{2}$ and $x_{3}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $f$ and $g$ is a composable arrow of $C$ and $2$ defined as the precomposition of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $g$ and $f$.

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $h$ be a homomorphism of $x_{3}$ and $x_{4}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $f$, $g$ and $h$ is a composable arrow of $C$ and $3$ defined as the precomposition of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $g$ and $h$ and $f$.

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $h$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $i$ be a homomorphism of $x_{4}$ and $x_{5}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2084\_}$ applied to $f$, $g$, $h$ and $i$ is a composable arrow of $C$ and $4$ defined as the precomposition of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $g$, $h$ and $i$ and $f$.

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $h$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $i$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $j$ be a homomorphism of $x_{5}$ and $x_{6}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2085\_}$ applied to $f$, $g$, $h$, $i$ and $j$ is a composable arrow of $C$ and $5$ defined as the precomposition of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2084\_}$ applied to $g$, $h$, $i$ and $j$ and $f$.

the functor of h (from the docstring)

Assume that $k + l \leq n$. Then the functor of $h$ is a functor of the set of composable arrows of $C$ and $n$ and the set of composable arrows of $C$ and $l$ defined as the functor of the functor of $h$.

the object of F and i (from the name)

Let $F$ be a composable arrow of $C$ and $n$. Let $i$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (i , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_obj'\_\_\_auto\_1}$. Then the object of $F$ and $i$ is an element of $C$.

the equivalence of C and n (from the docstring)

Let $C$ be a set. Let $n$ be a natural number. Then the equivalence of $C$ and $n$ is an equivalence of the set of opposites of the set of composable arrows of $C$ and $n$ and the set of composable arrows of the set of opposites of $C$ and $n$ defined as the composition of the opposite of the left congruence of the inverse of the composition of the inverse of the order dual equivalence of $\mathrm{Fin}$ applied to $n + 1$ and the equivalence of $\operatorname{revOrderIso}$ and the left opposite right opposite equivalence of $\mathrm{Fin}$ applied to $n + 1$ and $C$.

the precomposition of F and f (from the name)

Let $F$ be a composable arrow of $C$ and $n$. Let $f$ be a homomorphism of $X$ and the leftmost object of $F$. Then the precomposition of $F$ and $f$ is a composable arrow of $C$ and $n + 1$.

the rightmost object of F (from the docstring)

Let $F$ be a composable arrow of $C$ and $n$. Then the rightmost object of $F$ is an element of $C$.

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

Let $F$ be a composable arrow of $C$ and $m$. Let $x_{1}$ be a functor of $\mathrm{Fin}$ applied to $n + 1$ and $\mathrm{Fin}$ applied to $m + 1$. Then the left whisker of $F$ and $x_{1}$ is a composable arrow of $C$ and $n$ defined as the composition of $x_{1}$ and $F$.

the functor of x1 (from the docstring)

Let $x_{1}$ be a functor of $\mathrm{Fin}$ applied to $n + 1$ and $\mathrm{Fin}$ applied to $m + 1$. Then the functor of $x_{1}$ is a functor of the set of composable arrows of $C$ and $m$ and the set of composable arrows of $C$ and $n$.

Let $F$ be a composable arrow of $C$ and $n + 1$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_\_u3b4\_last}$ applied to $F$ is a composable arrow of $C$ and $n$ defined as the action of the functor and $F$.

the functor (from the docstring)

The functor is a functor of the set of composable arrows of $C$ and $n + 1$ and the set of composable arrows of $C$ and $n$ defined as the functor of the functor of $n + 1$.

Let $F$ be a composable arrow of $C$ and $n + 1$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_\_u3b4\_\_u2080\_}$ applied to $F$ is a composable arrow of $C$ and $n$ defined as the action of the functor and $F$.

the functor (from the docstring)

The functor is a functor of the set of composable arrows of $C$ and $n + 1$ and the set of composable arrows of $C$ and $n$ defined as the functor of the functor of $n + 1$.

the map composable arrow of G and n (from the name)

Let $G$ be a functor of $C$ and $D$. Let $n$ be a natural number. Then the map composable arrow of $G$ and $n$ is a functor of the set of composable arrows of $C$ and $n$ and the set of composable arrows of $D$ and $n$ defined as the action of the right whiskering of $C$ and $D$ and $G$.

the map composable arrow object isomorphism of G and f (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map composable arrow object isomorphism of $G$ and $f$ is an isomorphism of the action of the map composable arrow of $G$ and $1$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $f$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to the map of $G$ and $f$.

the map composable arrow object isomorphism of f and g (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the map composable arrow object isomorphism of $f$ and $g$ is an isomorphism of the action of the map composable arrow of $G$ and $2$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $f$ and $g$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to the map of $G$ and $f$ and the map of $G$ and $g$.

the map composable arrow opposite isomorphism of G and n (from the name)

Let $G$ be a functor of $C$ and $D$. Let $n$ be a natural number. Then the map composable arrow opposite isomorphism of $G$ and $n$ is an isomorphism of the composition of the map composable arrow of $G$ and $n$ and the right opposite of the functor of the equivalence of $D$ and $n$ and the composition of the right opposite of the functor of the equivalence of $C$ and $n$ and the opposite of the map composable arrow of the opposite of $G$ and $n$ defined as the identity of the composition of the map composable arrow of $G$ and $n$ and the right opposite of the functor of the equivalence of $D$ and $n$.

the functor of n (from the docstring)

Let $n$ be a natural number. Then the functor of $n$ is a functor of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + 1$.

the functor of h (from the docstring)

Assume that $k + l \leq n$. Then the functor of $h$ is a functor of $\mathrm{Fin}$ applied to $l + 1$ and $\mathrm{Fin}$ applied to $n + 1$.

the functor of n (from the docstring)

Let $n$ be a natural number. Then the functor of $n$ is a functor of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + 1$.

Let $x_{6}$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{8}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $x_{9}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{10}$ be a homomorphism of $x_{1}$ and $x_{3}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{6}$ and $x_{7}$ is equal to $x_{10}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$ and $h$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{10}$, $x_{8}$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{7}$, $x_{8}$ and $x_{9}$.

Let $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ be elements of $x$ such that $x_{2} \leq x_{3} \leq x_{4} \leq x_{5} \leq x_{6}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $h$, $h_{1}$, $h_{2}$ and $h_{3}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to the homomorphism of $\operatorname{trans}$ applied to $h$ and $h_{1}$, the homomorphism of $h_{2}$ and the homomorphism of $h_{3}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to the homomorphism of $h_{1}$, the homomorphism of $h_{2}$ and the homomorphism of $h_{3}$.

Let $x_{6}$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{8}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $x_{9}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{10}$ be a homomorphism of $x_{1}$ and $x_{3}$. Let $x_{11}$ be a homomorphism of $x_{2}$ and $x_{4}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{6}$ and $x_{7}$ is equal to $x_{10}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{7}$ and $x_{8}$ is equal to $x_{11}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_\_\_\_auto\_3}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $h$ and $h_{1}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{6}$, $x_{11}$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{10}$, $x_{8}$ and $x_{9}$.

Let $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ be elements of $x$ such that $x_{2} \leq x_{3} \leq x_{4} \leq x_{5} \leq x_{6}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $h$, $h_{1}$, $h_{2}$ and $h_{3}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to the homomorphism of $h$, the homomorphism of $\operatorname{trans}$ applied to $h_{1}$ and $h_{2}$ and the homomorphism of $h_{3}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to the homomorphism of $\operatorname{trans}$ applied to $h$ and $h_{1}$, the homomorphism of $h_{2}$ and the homomorphism of $h_{3}$.

Let $x_{6}$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{8}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $x_{9}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{10}$ be a homomorphism of $x_{2}$ and $x_{4}$. Let $x_{11}$ be a homomorphism of $x_{3}$ and $x_{5}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{7}$ and $x_{8}$ is equal to $x_{10}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2083\_To\_u3b4\_\_u2082\_\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{8}$ and $x_{9}$ is equal to $x_{11}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2083\_To\_u3b4\_\_u2082\_\_\_\_auto\_3}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2083\_To\_u3b4\_\_u2082\_}$ applied to $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $h$ and $h_{1}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{6}$, $x_{7}$ and $x_{11}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{6}$, $x_{10}$ and $x_{9}$.

Let $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ be elements of $x$ such that $x_{2} \leq x_{3} \leq x_{4} \leq x_{5} \leq x_{6}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2083\_To\_u3b4\_\_u2082\_'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $h$, $h_{1}$, $h_{2}$ and $h_{3}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to the homomorphism of $h$, the homomorphism of $h_{1}$ and the homomorphism of $\operatorname{trans}$ applied to $h_{2}$ and $h_{3}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to the homomorphism of $h$, the homomorphism of $\operatorname{trans}$ applied to $h_{1}$ and $h_{2}$ and the homomorphism of $h_{3}$.

Let $x_{6}$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{8}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $x_{9}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{10}$ be a homomorphism of $x_{3}$ and $x_{5}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{8}$ and $x_{9}$ is equal to $x_{10}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2084\_To\_u3b4\_\_u2083\_\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2084\_To\_u3b4\_\_u2083\_}$ applied to $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$ and $h$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{6}$, $x_{7}$ and $x_{8}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to $x_{6}$, $x_{7}$ and $x_{10}$.

Let $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ be elements of $x$ such that $x_{2} \leq x_{3} \leq x_{4} \leq x_{5} \leq x_{6}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_four\_u3b4\_\_u2084\_To\_u3b4\_\_u2083\_'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $h$, $h_{1}$, $h_{2}$ and $h_{3}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to the homomorphism of $h$, the homomorphism of $h_{1}$ and the homomorphism of $h_{2}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2083\_}$ applied to the homomorphism of $h$, the homomorphism of $h_{1}$ and the homomorphism of $\operatorname{trans}$ applied to $h_{2}$ and $h_{3}$.

the functor arrow of j and n (from the name)

Let $C$ be a set. Let $i$, $j$ and $n$ be natural numbers such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (i , j)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_functorArrows\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for $\mathrm{Leq} (j , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_functorArrows\_\_\_auto\_3}$. Then the functor arrow of $j$ and $n$ is a functor of the set of composable arrows of $C$ and $n$ and the set of composable arrows of $C$ and $1$.

the map functor arrow of h and h1 (from the name)

Let $C$ be a set. Let $i$, $j$, $\mathrm{i'}$, $\mathrm{j'}$ and $n$ be elements of $\Natural$ such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (i , j)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mapFunctorArrows\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for $\mathrm{Leq} (\mathrm{i'} , \mathrm{j'})$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mapFunctorArrows\_\_\_auto\_3}$, $\mathrm{autoParam}$ holds for $\mathrm{Leq} (i , \mathrm{i'})$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mapFunctorArrows\_\_\_auto\_5}$, $\mathrm{autoParam}$ holds for $\mathrm{Leq} (j , \mathrm{j'})$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mapFunctorArrows\_\_\_auto\_7}$ and $\mathrm{autoParam}$ holds for $\mathrm{Leq} (\mathrm{j'} , n)$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mapFunctorArrows\_\_\_auto\_9}$. Then the map functor arrow of $\mathrm{j'}$ and $n$ is a homomorphism of the functor arrow of $j$ and $n$ and the functor arrow of $\mathrm{j'}$ and $n$.

Let $x_{1}$ be a homomorphism of $i$ and $j$. Let $x_{2}$ be a homomorphism of $j$ and $k$. Let $x_{3}$ be a homomorphism of $k$ and $l$. Let $x_{4}$ be a homomorphism of $i$ and $k$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{1}$ and $x_{2}$ is equal to $x_{4}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $x_{1}$, $x_{2}$, $x_{3}$, $x_{4}$ and $h$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $x_{4}$ and $x_{3}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $x_{2}$ and $x_{3}$.

Let $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ be elements of $x$ such that $x_{2} \leq x_{3} \leq x_{4} \leq x_{5}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $h$, $h_{1}$ and $h_{2}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to the homomorphism of $\operatorname{trans}$ applied to $h$ and $h_{1}$ and the homomorphism of $h_{2}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to the homomorphism of $h_{1}$ and the homomorphism of $h_{2}$.

Let $x_{1}$ be a homomorphism of $i$ and $j$. Let $x_{2}$ be a homomorphism of $j$ and $k$. Let $x_{3}$ be a homomorphism of $k$ and $l$. Let $x_{4}$ be a homomorphism of $i$ and $k$. Let $x_{5}$ be a homomorphism of $j$ and $l$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{1}$ and $x_{2}$ is equal to $x_{4}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{2}$ and $x_{3}$ is equal to $x_{5}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_\_\_\_auto\_3}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $x_{1}$, $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $h$ and $h_{1}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $x_{1}$ and $x_{5}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $x_{4}$ and $x_{3}$.

Let $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ be elements of $x$ such that $x_{2} \leq x_{3} \leq x_{4} \leq x_{5}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $h$, $h_{1}$ and $h_{2}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to the homomorphism of $h$ and the homomorphism of $\operatorname{trans}$ applied to $h_{1}$ and $h_{2}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to the homomorphism of $\operatorname{trans}$ applied to $h$ and $h_{1}$ and the homomorphism of $h_{2}$.

Let $x_{1}$ be a homomorphism of $i$ and $j$. Let $x_{2}$ be a homomorphism of $j$ and $k$. Let $x_{3}$ be a homomorphism of $k$ and $l$. Let $x_{4}$ be a homomorphism of $j$ and $l$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{2}$ and $x_{3}$ is equal to $x_{4}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2083\_To\_u3b4\_\_u2082\_\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2083\_To\_u3b4\_\_u2082\_}$ applied to $x_{1}$, $x_{2}$, $x_{3}$, $x_{4}$ and $h$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $x_{1}$ and $x_{4}$.

Let $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ be elements of $x$ such that $x_{2} \leq x_{3} \leq x_{4} \leq x_{5}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_three\_u3b4\_\_u2083\_To\_u3b4\_\_u2082\_'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$, $h$, $h_{1}$ and $h_{2}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to the homomorphism of $h$ and the homomorphism of $h_{1}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to the homomorphism of $h$ and the homomorphism of $\operatorname{trans}$ applied to $h_{1}$ and $h_{2}$.

Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $f$ and $g$ is equal to $\mathrm{fg}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $\mathrm{fg}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $g$.

Let $x_{2}$, $x_{3}$ and $x_{4}$ be elements of $x$ such that $x_{2} \leq x_{3} \leq x_{4}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2081\_To\_u3b4\_\_u2080\_'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $h$ and $h_{1}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to the homomorphism of $\operatorname{trans}$ applied to $h$ and $h_{1}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to the homomorphism of $h_{1}$.

Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Let $\mathrm{fg}$ be a homomorphism of $i$ and $k$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $f$ and $g$ is equal to $\mathrm{fg}$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_\_\_\_auto\_1}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_}$ applied to $f$, $g$, $\mathrm{fg}$ and $h$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $f$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $\mathrm{fg}$.

Let $x_{2}$, $x_{3}$ and $x_{4}$ be elements of $x$ such that $x_{2} \leq x_{3} \leq x_{4}$. Then $\mathrm{CategoryTheory\_\_ComposableArrows\_\_two\_u3b4\_\_u2082\_To\_u3b4\_\_u2081\_'}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $h$ and $h_{1}$ is a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to the homomorphism of $h$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to the homomorphism of $\operatorname{trans}$ applied to $h$ and $h_{1}$.

FC is a concrete category (from the name)

Let $C$ be a set. Let $\mathrm{FC}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $C$ and elements of $C$ to sets. Then we can say that $\mathrm{FC}$ is a concrete category.

the homomorphism of x2 (from the name)

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

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 homomorphisms of $X$ and $Y$.

the concrete category of x2 (from the name)

Let $x_{2}$ be an element of $\mathrm{FC}$ applied to $X$ and $Y$. Then the concrete category of $x_{2}$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.

homomorphism of x3 and x4 (from the name)

Let $x_{3}$ and $x_{4}$ be elements of $C$. Then a homomorphism of $x_{3}$ and $x_{4}$ is an element of the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{FC}$ applied to $x_{3}$ and $x_{4}$.

type of x3 (from the name)

Let $x_{3}$ be an element of $C$. Then a type of $x_{3}$ is an element of the function that maps $x_{3}$ to $\mathrm{CC}$ applied to $x_{3}$.

Let $c$ be a function from sets to sets. Then the elements of $\operatorname{Bundled}$ applied to $c$ are a basic type.

the map of f and x (from the name)

Let $f$ be a function from sets $x$ and elements of $c$ applied to $x$ to elements of $d$ applied to $x$. Let $b$ be an element of $\operatorname{Bundled}$ applied to $c$. Then the map of $x$ and $f$ is an element of $\operatorname{Bundled}$ applied to $d$ defined as the function that maps $b$ to $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $f$, $x$ applied to $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $f$ and $\operatorname{str}$ applied to $f$ and $b$.

Let $x$ be a set. Then $\operatorname{of}$ applied to $x$ is an element of $\operatorname{Bundled}$ applied to $c$ defined as $\operatorname{mk}$ applied to $x$ and $\mathrm{str}$.

Let $\mathrm{self}$ be an element of $\operatorname{Bundled}$ applied to $c$. Then $\operatorname{str}$ applied to $\mathrm{self}$ is an element of $c$ applied to $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{Bundled}$ applied to $c$. Then an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

the functorial surjective injective factorization data of C (from the name)

Let $C$ be a set. Then the functorial surjective injective factorization data of $C$ is a functorial surjective injective factorization data of $C$.

Let $C$ and $D$ be sets. Then we can say that $\mathrm{CategoryTheory\_\_HasForget\_u2082\_}$ holds for $C$ and $D$.

$\mathrm{CategoryTheory\_\_HasForget\_u2082\_\_\_forget\_u2082\_}$ is a functor of $C$ and $D$ defined as $\mathrm{CategoryTheory\_\_HasForget\_u2082\_\_\_proj0}$ applied to $\mathrm{self}$.

the forgetful functor of C (from the docstring)

Let $C$ be a set. Then the forgetful functor of $C$ is a functor of $C$ and the set of sets.

the forgetful functor of C and D (from the docstring)

Let $C$ and $D$ be sets. Then the forgetful functor of $C$ and $D$ is a functor of $C$ and $D$ defined as $\mathrm{CategoryTheory\_\_HasForget\_u2082\_\_\_forget\_u2082\_}$.

Let $\mathrm{ty}$ be an element of $\operatorname{Expr}$. Then $\mathrm{CategoryTheory\_\_OfNotation\_\_explicitArgs?}$ applied to $\mathrm{ty}$ is an element of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$.

Let $\mathrm{ty}$ be an element of $\operatorname{Expr}$. Then $\operatorname{MetaM}$ holds for $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $\operatorname{Name}$ and $\Natural$.

the homomorphism equivalence of x4 (from the name)

Let $x_{4}$ be an element of $\operatorname{RepresentableBy}$ applied to the composition of $F$ and the forgetful functor of $D$ and $Y$. Then the homomorphism equivalence of $x_{4}$ is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of types of the action of $F$ and $\operatorname{op}$ applied to $X$ defined as the homomorphism equivalence of $x_{4}$.

the conjugate of x1 (from the name)

Let $x_{1}$ be an isomorphism of $X$ and $Y$. Then the conjugate of $x_{1}$ is a multiplicative equivalence of the set of ends of $X$ and the set of ends of $Y$.

the conjugate automorphism of x1 (from the name)

Let $x_{1}$ be an isomorphism of $X$ and $Y$. Then the conjugate automorphism of $x_{1}$ is a multiplicative equivalence of the set of automorphisms of $X$ and the set of automorphisms of $Y$ defined as the composition of the inverse of the unit end equivalence automorphism of $X$ and the composition of the map equivalence of the conjugate of $x_{1}$ and the unit end equivalence automorphism of $Y$.

connected component of J (from the name)

Let $J$ be a set. Then a connected component of $J$ is an element of the function that maps $J$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $J$.

component of j (from the name)

Let $j$ be a connected component of $J$. Then a component of $j$ is an element of the function that maps $j$ to the set of full subcategories of the object property of $j$.

Let $X$ be a set. Let $f$ be a function from connected components of $J$ to elements of $X$. Then $\operatorname{functorToDiscrete}$ applied to $X$ and $f$ is a functor of $J$ and $\operatorname{Discrete}$ applied to $X$.

the lift functor of F and x1 (from the name)

Let $J$ be a set. Let $F$ be a functor of $J$ and $\operatorname{Discrete}$ applied to $X$. Let $x_{1}$ be a connected component of $J$. Then the lift functor of $F$ and $x_{1}$ is an element of $X$.

Let $j$ be an element of $J$. Then $\operatorname{mk}$ applied to $j$ is a connected component of $J$ defined as $\operatorname{mk''}$ applied to $j$.

the object property of j (from the name)

Let $j$ be a connected component of $J$. Then the object property of $j$ is an object property of $J$ defined as the function that maps $k$ to $\EqtMACRoH {\operatorname{mk''} (k)}{j}$.

the type to category homomorphism equivalence of J and X (from the name)

Let $J$ and $X$ be sets. Then the type to category homomorphism equivalence of $J$ and $X$ is an equivalence from the set of functions from connected components of $J$ to elements of $X$ to the set of functors of $J$ and $\operatorname{Discrete}$ applied to $X$.

the inclusion functor of j (from the docstring)

Let $j$ be a connected component of $J$. Then the inclusion functor of $j$ is a functor of the set of components of $j$ and $J$ defined as the inclusion of the object property of $j$.

Let $J$ be a set. Then an element of $\operatorname{Decomposed}$ applied to $J$ is an element of the function that maps $J$ to $\Sigma$ applied to the function that maps $j$ to the set of components of $j$.

the map of F and x2 (from the docstring)

Let $F$ be a functor of $J$ and $K$. Let $x_{2}$ be a connected component of $J$. Then the map of $F$ and $x_{2}$ is a connected component of $K$.

the decomposed equivalence (from the name)

The decomposed equivalence is an equivalence of $\operatorname{Decomposed}$ applied to $J$ and $J$ defined as $\operatorname{asEquivalence}$ applied to $\operatorname{decomposedTo}$ applied to $J$.

Let $J$ be a set. Then $\operatorname{decomposedTo}$ applied to $J$ is a functor of $\operatorname{Decomposed}$ applied to $J$ and $J$ defined as $\operatorname{desc}$ applied to $\mathrm{CategoryTheory\_\_ConnectedComponents\_\_\_u3b9\_}$.

the inclusion of j (from the docstring)

Let $j$ be a connected component of $J$. Then the inclusion of $j$ is a functor of the set of components of $j$ and $\operatorname{Decomposed}$ applied to $J$ defined as the inclusion of $j$.

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

f is deterministic (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then $f$ is deterministic, if $f$ is a comonoid homomorphism.

Let $P$ be a morphism property of $C$. Let $c$ be an element of $C$. Then we can say that $\operatorname{IsStableUnderComonoid}$ holds for $P$ and $c$.

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

$\operatorname{forgetFunctorToCore}$ is a functor of the set of functors of $G$ and $\operatorname{Core}$ applied to $C$ and the set of functors of $G$ and $C$ defined as the action of the right whiskering of $\operatorname{Core}$ applied to $C$ and $C$ and the core of $C$.

Let $F$ be a functor of $G$ and $C$. Then $\operatorname{functorToCore}$ applied to $F$ is a functor of $G$ and $\operatorname{Core}$ applied to $C$.

the functor of H and F (from the docstring)

Let $H$ be a functor of $G$ and $C$. Let $F$ be a functor of $\mathrm{G'}$ and $G$. Then the functor of $H$ and $F$ is an isomorphism of $\operatorname{functorToCore}$ applied to the composition of $F$ and $H$ and the composition of $F$ and $\operatorname{functorToCore}$ applied to $H$.

the functor of H and F (from the docstring)

Let $H$ be a functor of $G$ and $C$. Let $F$ be a functor of $C$ and $\mathrm{C'}$. Then the functor of $H$ and $F$ is an isomorphism of $\operatorname{functorToCore}$ applied to the composition of $H$ and $F$ and the composition of $\operatorname{functorToCore}$ applied to $H$ and $\operatorname{core}$ applied to $F$ defined as the identity of $\operatorname{functorToCore}$ applied to the composition of $H$ and $F$.

the functor (from the docstring)

The functor is an isomorphism of $\operatorname{functorToCore}$ applied to the core of $C$ and the identity of $\operatorname{Core}$ applied to $C$ defined as the identity of $\operatorname{functorToCore}$ applied to the core of $C$.

the core of C (from the docstring)

Let $C$ be a set. Then the core of $C$ is a functor of $\operatorname{Core}$ applied to $C$ and $C$.

the functor (from the docstring)

The functor is an isomorphism of the composition of the core of $G$ and $\operatorname{functorToCore}$ applied to the identity of $G$ and the identity of $\operatorname{Core}$ applied to $G$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $\operatorname{of}$ applied to $x_{1}$ and $\operatorname{of}$ applied to $y$. Then the isomorphism of $e$ is an isomorphism of $x_{1}$ and $y$ defined as $\operatorname{symm}$ applied to the isomorphism equivalence homomorphism of $x_{1}$ and $y$ and $\operatorname{mk}$ applied to $e$.

Let $\mathrm{self}$ be an element of $\operatorname{Core}$ applied to $C$. Then $\operatorname{of}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be elements of $\operatorname{Core}$ applied to $C$. Then the homomorphisms of $X$ and $Y$ are a basic type.

the isomorphism of self (from the name)

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

Let $E$ be an equivalence of $C$ and $D$. Then $\operatorname{core}$ applied to $E$ is an equivalence of $\operatorname{Core}$ applied to $C$ and $\operatorname{Core}$ applied to $D$.

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{core}$ applied to $F$ is a functor of $\operatorname{Core}$ applied to $C$ and $\operatorname{Core}$ applied to $D$ defined as $\operatorname{functorToCore}$ applied to the composition of the core of $C$ and $F$.

the 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 composition of $F$ and $G$ is an isomorphism of $\operatorname{core}$ applied to the composition of $F$ and $G$ and the composition of $\operatorname{core}$ applied to $F$ and $\operatorname{core}$ applied to $G$ defined as the identity of $\operatorname{core}$ applied to the composition of $F$ and $G$.

the natural isomorphism of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the natural isomorphism of $F$ is an isomorphism of the composition of $\operatorname{core}$ applied to $F$ and the core of $D$ and the composition of the core of $C$ and $F$ defined as the identity of the composition of $\operatorname{core}$ applied to $F$ and the core of $D$.

the core of the identity functor of C (from the docstring)

Let $C$ be a set. Then the core of the identity functor of $C$ is an isomorphism of $\operatorname{core}$ applied to the identity of $C$ and the identity of $\operatorname{Core}$ applied to $C$ defined as the identity of $\operatorname{core}$ applied to the identity of $C$.

Let $x_{2}$ be an isomorphism of $F$ and $G$. Then $\operatorname{core}$ applied to $x_{2}$ is an isomorphism of $\operatorname{core}$ applied to $F$ and $\operatorname{core}$ applied to $G$.

the functor of C and D (from the name)

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

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 $\operatorname{Core}$ applied to the set of sets and $\operatorname{Core}$ applied to the set of sets.

J is a countable category (from the name)

Let $J$ be a set. Then we can say that $J$ is a countable category.

homomorphism as type of x (from the name)

Let $x$ be a set. Then a homomorphism as type of $x$ is an element of the function that maps $x$ to the set of shrink homs of the set of objects as type of $x$.

object as type of x (from the name)

Let $x$ be a set. Then an object as type of $x$ is an element of the function that maps $x$ to the set of induced categories of $x$ and $\operatorname{coe}$ applied to the inverse of the equivalence shrink of $x$.

the homomorphism as type equivalence of x (from the name)

Let $x$ be a set. Then the homomorphism as type equivalence of $x$ is an equivalence of the set of homomorphisms as type of $x$ and $x$ defined as the composition of the inverse of the equivalence of the set of objects as type of $x$ and the object as type equivalence of $x$.

the object as type equivalence of x (from the name)

Let $x$ be a set. Then the object as type equivalence of $x$ is an equivalence of the set of objects as type of $x$ and $x$ defined as $\operatorname{asEquivalence}$ applied to the induced functor of $\operatorname{coe}$ applied to the inverse of the equivalence shrink of $x$.

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

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be elements of $\operatorname{Dial}$ applied to $C$. Then the homomorphisms of $X$ and $Y$ are a basic type.

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

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

the isomorphism of x1 and x2 (from the name)

Let $x_{1}$ be an isomorphism of $\operatorname{src}$ applied to $X$ and $\operatorname{src}$ applied to $Y$. Let $x_{2}$ be an isomorphism of $\operatorname{tgt}$ applied to $X$ and $\operatorname{tgt}$ applied to $Y$ such that the relation of $X$ is equal to the action of the pullback of the map of the homomorphism of $x_{1}$ and the homomorphism of $x_{2}$ and the relation of $Y$. Then the isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of $X$ and $Y$.

the relation of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{Dial}$ applied to $C$. Then the relation of $\mathrm{self}$ is a subobject of the product of $\operatorname{src}$ applied to $\mathrm{self}$ and $\operatorname{tgt}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{Dial}$ applied to $C$. Then $\operatorname{src}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{Dial}$ applied to $C$. Then $\operatorname{tgt}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the braiding isomorphism of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $\operatorname{Dial}$ applied to $C$. Then the braiding isomorphism of $X$ and $Y$ is an isomorphism of the tensor object of $X$ and $Y$ and the tensor object of $Y$ and $X$.

differential object of S and C (from the name)

Let $S$ and $C$ be sets. Then the differential objects of $S$ and $C$ are a basic type.

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be differential objects of $S$ and $C$. Then the homomorphisms of $X$ and $Y$ are a basic type.

the composition of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the composition of $f$ and $g$ is a homomorphism of $X$ and $Z$.

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

the identity morphism of X (from the docstring)

Let $X$ be a differential object of $S$ and $C$. Then the identity morphism of $X$ is a homomorphism of $X$ and $X$.

homomorphism subtype of X and Y (from the name)

Let $S$ and $C$ be sets. Let $X$ and $Y$ be differential objects of $S$ and $C$. Then a homomorphism subtype of $X$ and $Y$ is an element of the function that maps $S$, $C$, $X$ and $Y$ to $\SubtypeSet {f}{(\EqtMACRoH {\operatorname{comp} (\operatorname{d} (X), \operatorname{map} (\operatorname{shiftFunctor} (C , 1), \operatorname{ofHom} (f)))}{\operatorname{comp} (\operatorname{ofHom} (f), \operatorname{d} (Y))})}$.

Let $\mathrm{self}$ be a differential object of $S$ and $C$. Then $\operatorname{d}$ applied to $\mathrm{self}$ is a homomorphism of the underlying object of $\mathrm{self}$ and the action of the shift functor of $C$ and $1$ and the underlying object of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

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

the isomorphism application of f (from the name)

Let $f$ be an isomorphism of $X$ and $Y$. Then the isomorphism application of $f$ is an isomorphism of the underlying object of $X$ and the underlying object of $Y$.

the isomorphism of f and hf (from the name)

Let $f$ be an isomorphism of the underlying object of $X$ and the underlying object of $Y$ such that the composition of $\operatorname{d}$ applied to $X$ and the map of the shift functor of $C$ and $1$ and the homomorphism of $f$ is equal to the composition of the homomorphism of $f$ and $\operatorname{d}$ applied to $Y$. Then the isomorphism of $f$ and $\mathrm{hf}$ is an isomorphism of $X$ and $Y$.

the underlying object of self (from the docstring)

Let $\mathrm{self}$ be a differential object of $S$ and $C$. Then the underlying object of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

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

Let $C$ be a set. Let $n$ be an element of $S$. Then the shift functor of $C$ and $n$ is a functor of the set of differential objects of $S$ and $C$ and the set of differential objects of $S$ and $C$.

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

Let $C$ be a set. Let $m$ and $n$ be elements of $S$. Then the shift functor sum of $m$ and $n$ is an isomorphism of the shift functor of $C$ and $m + n$ and the composition of the shift functor of $C$ and $m$ and the shift functor of $C$ and $n$.

the shift by zero of C (from the docstring)

Let $C$ be a set. Then the shift by zero of $C$ is an isomorphism of the shift functor of $C$ and $0$ and the identity of the set of differential objects of $S$ and $C$.

the map differential object of F and x7 (from the name)

Let $D$ be a set. Let $F$ be a functor of $C$ and $D$. Let $x_{7}$ be a homomorphism of the composition of the shift functor of $C$ and $1$ and $F$ and the composition of $F$ and the shift functor of $D$ and $1$. Assume that for all elements $c$ and $\mathrm{c'}$ of $C$, the map of $F$ and $0$ is equal to $0$. Then the map differential object of $F$ and $x_{7}$ is a functor of the set of differential objects of $S$ and $C$ and the set of differential objects of $S$ and $D$.

Let $F$ and $G$ be functors of the set of opposites of $C$ and the set of functors of $C$ and $D$. Then the elements of $\operatorname{DinatTrans}$ applied to $F$ and $G$ are a basic type.

the component of self and X (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{DinatTrans}$ applied to $F$ and $G$. Let $X$ be an element of $C$. Then the component of $\mathrm{self}$ and $X$ is a homomorphism of the action of the action of $F$ and $\operatorname{op}$ applied to $X$ and $X$ and the action of the action of $G$ and $\operatorname{op}$ applied to $X$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $X$.

the composition natural transformation of x2 and x3 (from the name)

Let $x_{2}$ be an element of $\operatorname{DinatTrans}$ applied to $F$ and $G$. Let $x_{3}$ be a homomorphism of $G$ and $H$. Then the composition natural transformation of $x_{2}$ and $x_{3}$ is an element of $\operatorname{DinatTrans}$ applied to $F$ and $H$.

the precomposition natural transformation of x2 and x3 (from the name)

Let $x_{2}$ be an element of $\operatorname{DinatTrans}$ applied to $G$ and $H$. Let $x_{3}$ be a homomorphism of $F$ and $G$. Then the precomposition natural transformation of $x_{2}$ and $x_{3}$ is an element of $\operatorname{DinatTrans}$ applied to $F$ and $H$.

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

homomorphism of a and b (from the name)

Let $a$ and $b$ be elements of $x$. Then the homomorphisms of $a$ and $b$ are a basic type.

Let $\mathrm{self}$ be an element of $\operatorname{Discrete}$ applied to $x$. Then $\operatorname{as}$ applied to $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $F$ be a function from elements of $I$ to elements of $C$. Let $G$ be a functor of $C$ and $D$. Then $\operatorname{compNatIsoDiscrete}$ applied to $F$ and $G$ is an isomorphism of the composition of the functor of $F$ and $G$ and the functor of $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to $G$ and $F$ defined as the natural isomorphism of the function that maps $x_{2}$ to the identity of the action of the composition of the functor of $F$ and $G$ and $x_{2}$.

the discrete case (from the name)

Assume that $\EqtMACRoH {\operatorname{as} (X)}{\operatorname{as} (Y)}$. Then $\operatorname{eqToHom}$ applied to $h$ is a homomorphism of $X$ and $Y$.

Assume that $\EqtMACRoH {a}{b}$. Then $\operatorname{eqToHom'}$ applied to $h$ is a homomorphism of $\operatorname{mk}$ applied to $a$ and $\operatorname{mk}$ applied to $b$ defined as $\operatorname{eqToHom}$ applied to $h$.

Assume that $\EqtMACRoH {\operatorname{as} (X)}{\operatorname{as} (Y)}$. Then $\operatorname{eqToIso}$ applied to $h$ is an isomorphism of $X$ and $Y$.

Assume that $\EqtMACRoH {a}{b}$. Then $\operatorname{eqToIso'}$ applied to $h$ is an isomorphism of $\operatorname{mk}$ applied to $a$ and $\operatorname{mk}$ applied to $b$ defined as $\operatorname{eqToIso}$ applied to $h$.

the equivalence of h (from the name)

Let $h$ be an equivalence of $\operatorname{Discrete}$ applied to $x$ and $\operatorname{Discrete}$ applied to $x_{1}$. Then the equivalence of $h$ is an equivalence from $x$ to $x_{1}$.

the equivalence of e (from the name)

Let $e$ be an equivalence from $I$ to $J$. Then the equivalence of $e$ is an equivalence of $\operatorname{Discrete}$ applied to $I$ and $\operatorname{Discrete}$ applied to $J$.

the functor of F (from the name)

Let $F$ be a function from elements of $I$ to elements of $C$. Then the functor of $F$ is a functor of $\operatorname{Discrete}$ applied to $I$ and $C$.

the functor composition of f and g (from the name)

Let $f$ be a function from elements of $J$ to elements of $C$. Let $g$ be a function from elements of $I$ to elements of $J$. Then the functor composition of $f$ and $g$ is an isomorphism of the functor of $\operatorname{comp}$ applied to $f$ and $g$ and the composition of the functor of $\operatorname{comp}$ applied to $\operatorname{mk}$ and $g$ and the functor of $f$.

the natural isomorphism of f (from the name)

Let $f$ be a function from elements $i$ of $\operatorname{Discrete}$ applied to $I$ to isomorphisms of the action of $F$ and $i$ and the action of $G$ and $i$. Then the natural isomorphism of $i$ is an isomorphism of $F$ and $G$.

the natural isomorphism functor (from the name)

The natural isomorphism functor is an isomorphism of $F$ and the functor of $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to $F$ and $\operatorname{mk}$ defined as the natural isomorphism of the function that maps $x_{1}$ to the identity of the action of $F$ and $x_{1}$.

the natural transformation of f (from the name)

Let $f$ be a function from elements $i$ of $\operatorname{Discrete}$ applied to $I$ to homomorphisms of the action of $F$ and $i$ and the action of $G$ and $i$. Then the natural transformation of $i$ is a homomorphism of $F$ and $G$.

the opposite of x (from the name)

Let $x$ be a set. Then the opposite of $x$ is an equivalence of the set of opposites of $\operatorname{Discrete}$ applied to $x$ and $\operatorname{Discrete}$ applied to $x$.

C is discrete (from the name)

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

the discrete equivalence (from the name)

The discrete equivalence is an element of $\EquivMACRoAE {\operatorname{Discrete} (x)}{x}$.

Let $J$ and $C$ be sets. Then $\operatorname{piEquivalenceFunctorDiscrete}$ applied to $J$ and $C$ is an equivalence of the set of functions from elements of $J$ to elements of $C$ and the set of functors of $\operatorname{Discrete}$ applied to $J$ and $C$.

the product equivalence functor discrete composition evaluation isomorphism of C and j (from the name)

Let $C$ be a set. Let $j$ be an element of $J$. Then the product equivalence functor discrete composition evaluation isomorphism of $C$ and $j$ is an isomorphism of the composition of the functor of $\operatorname{piEquivalenceFunctorDiscrete}$ applied to $J$ and $C$ and the action of the evaluation of $\operatorname{Discrete}$ applied to $J$ and $C$ and $\operatorname{mk}$ applied to $j$ and the evaluation of the function that maps $x_{1}$ to $C$ and $j$.

the costructured arrow equivalence of F and t (from the name)

Let $F$ be a functor of $C$ and $\operatorname{Discrete}$ applied to $T$. Let $t$ be an element of $T$. Then the costructured arrow equivalence of $F$ and $t$ is an equivalence of the set of costructured arrows of $F$ and $\operatorname{mk}$ applied to $t$ and $C$.

the structured arrow equivalence of F and t (from the name)

Let $F$ be a functor of $C$ and $\operatorname{Discrete}$ applied to $T$. Let $t$ be an element of $T$. Then the structured arrow equivalence of $F$ and $t$ is an equivalence of the set of structured arrows of $\operatorname{mk}$ applied to $t$ and $F$ and $C$.

the discrete category (from the docstring)

The discrete category is an equivalence of $\operatorname{Discrete}$ applied to $\mathrm{Prod}$ applied to $J$ and $K$ and $\mathrm{Prod}$ applied to $\operatorname{Discrete}$ applied to $J$ and $\operatorname{Discrete}$ applied to $K$.

the discrete category (from the docstring)

The discrete category is an equivalence of $\operatorname{Discrete}$ applied to $\mathrm{Sum}$ applied to $J$ and $K$ and $\mathrm{Sum}$ applied to $\operatorname{Discrete}$ applied to $J$ and $\operatorname{Discrete}$ applied to $K$.

Let $C$ be a set. Then $\operatorname{IsCartesianDistributive}$ holds for $C$, if $C$ is distributive.

C is distributive (from the docstring)

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

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

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

Let $X$, $Y$ and $Z$ be elements of $C$. Then $\operatorname{leftDistrib}$ applied to $X$, $Y$ and $Z$ is an isomorphism of the coproduct of the tensor object of $X$ and $Y$ and the tensor object of $X$ and $Z$ and the tensor object of $X$ and the coproduct of $Y$ and $Z$ defined as the isomorphism of $Y$ and $Z$.

Let $X$, $Y$ and $Z$ be elements of $C$. Then $\operatorname{rightDistrib}$ applied to $X$, $Y$ and $Z$ is an isomorphism of the coproduct of the tensor object of $Y$ and $X$ and the tensor object of $Z$ and $X$ and the tensor object of the coproduct of $Y$ and $Z$ and $X$ defined as the isomorphism of $Y$ and $Z$.

f is a effective epimorphism (from the name)

Let $f$ be a homomorphism of $Y$ and $X$. Then we can say that $f$ is an effective epimorphism.

Let $f$ be a homomorphism of $Y$ and $X$. Let $e$ be a homomorphism of $Y$ and $W$ such that for all elements $Z$ of $C$, for all homomorphisms $x_{1}$ and $x_{2}$ of $Z$ and $Y$, if the composition of $x_{1}$ and $f$ is equal to the composition of $x_{2}$ and $f$, then the composition of $x_{1}$ and $e$ is equal to the composition of $x_{2}$ and $e$. Then $\operatorname{desc}$ applied to $f$, $e$ and $h_{1}$ is a homomorphism of $X$ and $W$ defined as $\operatorname{desc}$ applied to $\operatorname{getStruct}$ applied to $f$, $e$ and the function that maps $x_{1}$ to $h_{1}$ applied to $x_{1}$.

Let $f$ be a homomorphism of $Y$ and $X$. Then $\operatorname{getStruct}$ applied to $f$ is an element of $\operatorname{EffectiveEpiStruct}$ applied to $f$ defined as $\operatorname{some}$ applied to $\operatorname{effectiveEpi}$.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Let $x_{2}$ be a function from elements $a$ of $x_{1}$ to homomorphisms of $X$ applied to $a$ and $B$. Then we can say that $\operatorname{EffectiveEpiFamily}$ holds for $X$, $a$ and $x_{2}$.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Let $x_{2}$ be a function from elements $a_{1}$ of $x_{1}$ to homomorphisms of $X$ applied to $a_{1}$ and $B$. Let $e$ be a function from elements $a$ of $x_{1}$ to homomorphisms of $X$ applied to $a$ and $W$ such that for all elements $Z$ of $C$, for all elements $x_{3}$ and $x_{4}$ of $x_{1}$, for all homomorphisms $x_{5}$ of $Z$ and $X$ applied to $x_{3}$, for all homomorphisms $x_{6}$ of $Z$ and $X$ applied to $x_{4}$, if the composition of $x_{5}$ and $x_{2}$ applied to $x_{3}$ is equal to the composition of $x_{6}$ and $x_{2}$ applied to $x_{4}$, then the composition of $x_{5}$ and $e$ applied to $x_{3}$ is equal to the composition of $x_{6}$ and $e$ applied to $x_{4}$. Then $\operatorname{desc}$ applied to $X$, $a_{1}$, $x_{2}$, $a$, $e$ and $h_{1}$ is a homomorphism of $B$ and $W$ defined as the function that maps $e$ and $h_{1}$ to $\operatorname{desc}$ applied to $\operatorname{getStruct}$ applied to $X$ and $a_{1}$, $x_{2}$, the function that maps $x_{3}$ to $a$ applied to $x_{3}$, $e$ and $h_{1}$.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Let $x_{2}$ be a function from elements $a$ of $x_{1}$ to homomorphisms of $X$ applied to $a$ and $B$. Then $\operatorname{getStruct}$ applied to $X$, $a$ and $x_{2}$ is an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to $X$ and $x_{2}$ defined as the function that maps $x_{2}$ to $\operatorname{some}$ applied to $\operatorname{effectiveEpiFamily}$ and $x_{2}$.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Let $x_{2}$ be a function from elements $a$ of $x_{1}$ to homomorphisms of $X$ applied to $a$ and $B$. Then the elements of $\operatorname{EffectiveEpiFamilyStruct}$ applied to $X$, $a$ and $x_{2}$ are a basic type.

Let $\mathrm{self}$ be an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to $X$ and $x_{2}$. Let $e$ be a function from elements $a$ of $x_{1}$ to homomorphisms of $X$ applied to $a$ and $W$ such that for all elements $Z$ of $C$, for all elements $x_{3}$ and $x_{4}$ of $x_{1}$, for all homomorphisms $x_{5}$ of $Z$ and $X$ applied to $x_{3}$, for all homomorphisms $x_{6}$ of $Z$ and $X$ applied to $x_{4}$, if the composition of $x_{5}$ and $x_{2}$ applied to $x_{3}$ is equal to the composition of $x_{6}$ and $x_{2}$ applied to $x_{4}$, then the composition of $x_{5}$ and $e$ applied to $x_{3}$ is equal to the composition of $x_{6}$ and $e$ applied to $x_{4}$. Then $\operatorname{desc}$ applied to $\mathrm{self}$, $a$, $e$ and $h$ is a homomorphism of $B$ and $W$ defined as the function that maps $h$ to $\operatorname{proj0}$ applied to $\mathrm{self}$, $a$, $e$ and $h$.

the reindexing of a2 and e (from the name)

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Let $x_{3}$ be a function from elements $a_{2}$ of $x_{1}$ to homomorphisms of $X$ applied to $a_{2}$ and $B$. Let $e$ be an equivalence from $x_{2}$ to $x_{1}$. Let $P$ be an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to the function that maps $a$ to $X$ applied to $e$ applied to $a$ and the function that maps $a_{1}$ to $x_{3}$ applied to $e$ applied to $a_{1}$. Then the reindexing of $x_{3}$ and $e$ is an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to $X$ and $x_{3}$.

Let $f$ be a homomorphism of $Y$ and $X$. Then the elements of $\operatorname{EffectiveEpiStruct}$ applied to $f$ are a basic type.

Let $\mathrm{self}$ be an element of $\operatorname{EffectiveEpiStruct}$ applied to $f$. Let $e$ be a homomorphism of $Y$ and $W$ such that for all elements $Z$ of $C$, for all homomorphisms $x_{1}$ and $x_{2}$ of $Z$ and $Y$, if the composition of $x_{1}$ and $f$ is equal to the composition of $x_{2}$ and $f$, then the composition of $x_{1}$ and $e$ is equal to the composition of $x_{2}$ and $e$. Then $\operatorname{desc}$ applied to $\mathrm{self}$, $e$ and $h$ is a homomorphism of $X$ and $W$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $e$ and $h$.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Let $x_{2}$ be a function from elements $a$ of $x_{1}$ to homomorphisms of $X$ applied to $a$ and $B$. Then $\operatorname{effectiveEpiFamilyStructOfIsIsoDesc}$ applied to $X$, $a$ and $x_{2}$ is an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to $X$ and $x_{2}$.

Let $f$ be a homomorphism of $X$ and $B$. Then $\operatorname{effectiveEpiFamilyStructSingletonOfEffectiveEpi}$ applied to $f$ is an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to the function that maps $x_{1}$ to $X$ and the function that maps $x_{2}$ to $f$.

Let $f$ be a homomorphism of $X$ and $B$. Then $\operatorname{effectiveEpiStructOfEffectiveEpiFamilySingleton}$ applied to $f$ is an element of $\operatorname{EffectiveEpiStruct}$ applied to $f$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{effectiveEpiStructOfIsIso}$ applied to $f$ is an element of $\operatorname{EffectiveEpiStruct}$ applied to $f$.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Let $x_{2}$ be a function from elements $a_{1}$ of $x_{1}$ to homomorphisms of $X$ applied to $a_{1}$ and $B$. Let $i$ be a homomorphism of $B$ and $\mathrm{B'}$. Then $\operatorname{effectiveEpiFamilyStructCompIso}$ applied to $X$, $a_{1}$, $x_{2}$ and $i$ is an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to $X$ and the function that maps $a$ to the composition of $x_{2}$ applied to $a$ and $i$.

Let $f$ be a function from elements $a_{2}$ of $x_{1}$ to homomorphisms of $X$ applied to $a_{2}$ and $B$. Let $g$ be a function from elements $a_{1}$ of $x_{1}$ to homomorphisms of $Y$ applied to $a_{1}$ and $X$ applied to $a_{1}$. Then $\operatorname{effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi}$ applied to $a_{2}$, $f$, $a_{1}$ and $g$ is an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to $Y$ and the function that maps $a$ to the composition of $g$ applied to $a$ and $f$ applied to $a$.

Let $f$ be a function from elements $a_{4}$ of $x_{1}$ to homomorphisms of $X$ applied to $a_{4}$ and $B$. Let $g$ be a function from elements $a_{3}$ of $x_{1}$ to homomorphisms of $Y$ applied to $a_{3}$ and $X$ applied to $a_{3}$. Let $i$ be a function from elements $a_{2}$ of $x_{1}$ to homomorphisms of $X$ applied to $a_{2}$ and $Y$ applied to $a_{2}$ such that for all elements $a_{1}$ of $x_{1}$, the composition of $i$ applied to $a_{1}$ and $g$ applied to $a_{1}$ is equal to the identity morphism of $X$ applied to $a_{1}$. Then $\operatorname{effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi'}$ applied to $a_{4}$, $f$, $a_{3}$, $g$, $a_{2}$, $i$ and $\mathrm{hi}$ is an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to $Y$ and the function that maps $a$ to the composition of $g$ applied to $a$ and $f$ applied to $a$.

Let $g$ be a function from elements $i_{1}$ of $I$ to homomorphisms of $Z$ applied to $i_{1}$ and $Y$ applied to $i_{1}$. Let $f$ be a function from elements $i$ of $I$ to homomorphisms of $Y$ applied to $i$ and $X$. Then $\operatorname{effectiveEpiFamilyStructOfComp}$ applied to $i_{1}$, $g$, $i$ and $f$ is an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to $Y$ and $f$.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Let $x_{2}$ be a function from elements $a$ of $x_{1}$ to homomorphisms of $X$ applied to $a$ and $B$. Then $\operatorname{effectiveEpiFamilyStructOfEffectiveEpiDesc}$ applied to $X$, $a$ and $x_{2}$ is an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to $X$ and $x_{2}$.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Let $c$ be a cofan of $X$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $x_{2}$ be a function from elements $a$ of $x_{1}$ to homomorphisms of $X$ applied to $a$ and $B$. Then $\operatorname{effectiveEpiStructIsColimitDescOfEffectiveEpiFamily}$ applied to $X$, $c$, $\mathrm{hc}$, $a$ and $x_{2}$ is an element of $\operatorname{EffectiveEpiStruct}$ applied to $\operatorname{desc}$ applied to $\mathrm{hc}$ and $\operatorname{mk}$ applied to $B$ and $x_{2}$.

effective presentation of F and X (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $D$. Then the effective presentations of $F$ and $X$ are a basic type.

Let $\mathrm{self}$ be an effective presentation of $F$ and $X$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of the action of $F$ and $\operatorname{p}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an effective presentation of $F$ and $X$. Then $\operatorname{p}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{EffectivelyEnough}$ holds for $F$.

the epimorphism of F and X (from the docstring)

Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $D$. Then the epimorphism of $F$ and $X$ is a homomorphism of the effective epimorphism over object of $F$ and $X$ and $X$ defined as $\operatorname{f}$ applied to $\operatorname{some}$ applied to $\operatorname{presentation}$ applied to $X$.

the effective epimorphism over object of F and X (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $D$. Then the effective epimorphism over object of $F$ and $X$ is an element of $D$ defined as the action of $F$ and $\operatorname{p}$ applied to $\operatorname{some}$ applied to $\operatorname{presentation}$ applied to $X$.

the equivalence effective presentation of e and X (from the name)

Let $e$ be an equivalence of $C$ and $D$. Let $X$ be an element of $D$. Then the equivalence effective presentation of $e$ and $X$ is an effective presentation of the functor of $e$ and $X$.

F preserves effective epimorphism families (from the name)

Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ preserves effective epimorphism families.

Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{PreservesEffectiveEpis}$ holds for $F$.

F preserves finite effective epimorphism families (from the name)

Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ preserves finite effective epimorphism families.

F reflects effective epimorphism families (from the name)

Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ reflects effective epimorphism families.

Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{ReflectsEffectiveEpis}$ holds for $F$.

F reflects finite effective epimorphism families (from the name)

Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ reflects finite effective epimorphism families.

the regular epimorphism of c and hc (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $F$ be a functor of $C$ and $D$. Let $c$ be a pullback cone of $f$ and $f$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the regular epimorphism of $c$ and $\mathrm{hc}$ is a regular epimorphism of the map of $F$ and $f$.

Let $e$ be an equivalence of $C$ and $D$. Let $X$ be a function from elements of $x_{2}$ to elements of $C$. Let $x_{3}$ be a function from elements $a_{2}$ of $x_{2}$ to homomorphisms of $X$ applied to $a_{2}$ and $B$. Then $\operatorname{effectiveEpiFamilyStructOfEquivalence}$ applied to $e$, $X$, $a_{2}$ and $x_{3}$ is an element of $\operatorname{EffectiveEpiFamilyStruct}$ applied to the function that maps $a$ to the action of the functor of $e$ and $X$ applied to $a$ and the function that maps $a_{1}$ to the map of the functor of $e$ and $x_{3}$ applied to $a_{1}$.

element of F (from the name)

Let $F$ be a functor of $C$ and the set of sets. Then the elements of $F$ are a basic type.

homomorphism of x1 and y (from the name)

Let $x_{1}$ and $y$ be elements of $F$. Then the homomorphisms of $x_{1}$ and $y$ are a basic type.

the homomorphism of self (from the name)

Let $\mathrm{self}$ be a homomorphism of $x_{1}$ and $y$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of the underlying object of $x_{1}$ and the underlying object of $y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the costructured arrow shrink Yoneda equivalence of F (from the name)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the costructured arrow shrink Yoneda equivalence of $F$ is an equivalence of the set of opposites of the set of elements of $F$ and the set of costructured arrows of the Yoneda embedding and $F$.

the functor of the equivalence of F (from the docstring)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the functor of the equivalence of $F$ is an isomorphism of the composition of the functor of the costructured arrow shrink Yoneda equivalence of $F$ and the projection of the Yoneda embedding and $F$ and the left opposite of the projection of $F$ defined as the identity of the composition of the functor of the costructured arrow shrink Yoneda equivalence of $F$ and the projection of the Yoneda embedding and $F$.

the costructured arrow lift Yoneda equivalence of F (from the name)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the costructured arrow lift Yoneda equivalence of $F$ is an equivalence of the set of opposites of the set of elements of $F$ and the set of costructured arrows of the lift Yoneda and $F$.

the functor of the equivalence of F (from the docstring)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the functor of the equivalence of $F$ is an isomorphism of the composition of the functor of the costructured arrow lift Yoneda equivalence of $F$ and the projection of the lift Yoneda and $F$ and the left opposite of the projection of $F$ defined as the identity of the composition of the functor of the costructured arrow lift Yoneda equivalence of $F$ and the projection of the lift Yoneda and $F$.

the equivalence of F (from the docstring)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the equivalence of $F$ is an equivalence of the set of opposites of the set of elements of $F$ and the set of costructured arrows of the Yoneda and $F$.

the equivalence of F (from the docstring)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the equivalence of $F$ is an isomorphism of the composition of the functor of the equivalence of $F$ and the projection of the Yoneda and $F$ and the left opposite of the projection of $F$ defined as the identity of the composition of the functor of the equivalence of $F$ and the projection of the Yoneda and $F$.

the equivalence of F (from the docstring)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the equivalence of $F$ is an isomorphism of the composition of the inverse of the equivalence of $F$ and the left opposite of the projection of $F$ and the projection of the Yoneda and $F$ defined as the identity of the composition of the inverse of the equivalence of $F$ and the left opposite of the projection of $F$.

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{fromCostructuredArrow}$ applied to $F$ is a functor of the set of opposites of the set of costructured arrows of the Yoneda and $F$ and the set of elements of $F$.

Let $F$ be a functor of $C$ and the set of sets. Then $\operatorname{fromStructuredArrow}$ applied to $F$ is a functor of the set of structured arrows of $\mathrm{PUnit}$ and $F$ and the set of elements of $F$.

the homomorphism of f and hf (from the name)

Let $f$ be a homomorphism of the underlying object of $x_{1}$ and the underlying object of $y$ such that $\mathrm{autoParam}$ holds for the proposition that $\operatorname{hom}$ applied to the map of $F$ and $f$ and the value of the element of $x_{1}$ is equal to the value of the element of $y$ and $\mathrm{CategoryTheory\_\_Functor\_\_Elements\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $f$ and $\mathrm{hf}$ is a homomorphism of $x_{1}$ and $y$ defined as $\operatorname{mk}$ applied to $f$ and $\mathrm{hf}$.

the initial object in h (from the docstring)

Let $h$ be an element of $\operatorname{CorepresentableBy}$ applied to $F$ and $X$. Then the initial object in $h$ is an element of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{homEquiv}$ applied to $h$ and the identity morphism of $X$.

the initial object in h (from the docstring)

Let $h$ be an element of $\operatorname{RepresentableBy}$ applied to $F$ and $X$. Then the initial object in $h$ is an element of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{homEquiv}$ applied to $h$ and the identity morphism of $X$.

the initial Yoneda object of A (from the name)

Let $A$ be an element of $C$. Then the initial Yoneda object of $A$ is an element of the action of the Yoneda and $A$ defined as $\operatorname{mk}$ applied to the identity morphism of $A$.

Let $h$ be an element of $\operatorname{CorepresentableBy}$ applied to $F$ and $X$. Then $\operatorname{isInitialOfCorepresentableBy}$ applied to $h$ is an element of $\operatorname{IsInitial}$ applied to the initial object in $h$.

Let $h$ be an element of $\operatorname{RepresentableBy}$ applied to $F$ and $X$. Then $\operatorname{isInitialOfRepresentableBy}$ applied to $h$ is an element of $\operatorname{IsInitial}$ applied to the initial object in $h$.

Let $A$ be an element of $C$. Then $\operatorname{isInitialYonedaObj}$ applied to $A$ is an element of $\operatorname{IsInitial}$ applied to the initial Yoneda object of $A$ defined as $\operatorname{isInitialOfRepresentableBy}$ applied to the Yoneda of $A$.

the isomorphism of e and he (from the name)

Let $e$ be an isomorphism of the underlying object of $x_{1}$ and the underlying object of $y$ such that $\mathrm{autoParam}$ holds for the proposition that $\operatorname{hom}$ applied to the map of $F$ and the homomorphism of $e$ and the value of the element of $x_{1}$ is equal to the value of the element of $y$ and $\mathrm{CategoryTheory\_\_Functor\_\_Elements\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $e$ and $\mathrm{he}$ is an isomorphism of $x_{1}$ and $y$.

the underlying object of self (from the docstring)

Let $\mathrm{self}$ be an element of $F$. Then the underlying object of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the precomposition of F and G (from the name)

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and the set of sets. Then the precomposition of $F$ and $G$ is a functor of the set of elements of the composition of $F$ and $G$ and the set of elements of $G$.

the structured arrow equivalence of F (from the name)

Let $F$ be a functor of $C$ and the set of sets. Then the structured arrow equivalence of $F$ is an equivalence of the set of elements of $F$ and the set of structured arrows of $\mathrm{PUnit}$ and $F$.

the costructured arrow of F (from the name)

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the costructured arrow of $F$ is a functor of the set of opposites of the set of elements of $F$ and the set of costructured arrows of the Yoneda and $F$.

the structured arrow of F (from the name)

Let $F$ be a functor of $C$ and the set of sets. Then the structured arrow of $F$ is a functor of the set of elements of $F$ and the set of structured arrows of $\mathrm{PUnit}$ and $F$.

the value of the element of self (from the docstring)

Let $\mathrm{self}$ be an element of $F$. Then the value of the element of $\mathrm{self}$ is an element of the action of $F$ and the underlying object of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the projection of F (from the name)

Let $F$ be a functor of $C$ and the set of sets. Then the projection of $F$ is a functor of the set of elements of $F$ and $C$.

the element functor (from the name)

The element functor is a functor of the set of functors of $C$ and the set of sets and the set of categories.

the element of X and x1 (from the name)

Let $F$ be a functor of $C$ and the set of sets. Let $X$ be an element of $C$. Let $x_{1}$ be an element of the action of $F$ and $X$. Then the element of $X$ and $x_{1}$ is an element of $F$ defined as $\operatorname{mk}$ applied to $x_{1}$.

the map element of x1 (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $G$. Then the map element of $x_{1}$ is a functor of the set of elements of $F$ and the set of elements of $G$.

the map element composition projection isomorphism of x1 (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $G$. Then the map element composition projection isomorphism of $x_{1}$ is an isomorphism of the composition of the map element of $x_{1}$ and the projection of $G$ and the projection of $F$ defined as the identity of the composition of the map element of $x_{1}$ and the projection of $G$.

the map element opposite composition to costructured arrow isomorphism of x3 (from the name)

Let $x_{3}$ be a homomorphism of $x_{1}$ and $x_{2}$. Then the map element opposite composition to costructured arrow isomorphism of $x_{3}$ is an isomorphism of the composition of the opposite of the map element of $x_{3}$ and the costructured arrow of $x_{2}$ and the composition of the costructured arrow of $x_{1}$ and the map of $x_{3}$.

the counit isomorphism of adj (from the name)

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the counit isomorphism of $\mathrm{adj}$ is an isomorphism of the composition of the algebra of $\mathrm{adj}$ and the coalgebra of $\mathrm{adj}$ and the identity of the set of coalgebras of $G$.

the unit isomorphism of adj (from the name)

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the unit isomorphism of $\mathrm{adj}$ is an isomorphism of the identity of the set of algebras of $F$ and the composition of the coalgebra of $\mathrm{adj}$ and the algebra of $\mathrm{adj}$.

the coalgebra of adj (from the name)

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the coalgebra of $\mathrm{adj}$ is a functor of the set of algebras of $F$ and the set of coalgebras of $G$.

the algebra of adj (from the name)

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the algebra of $\mathrm{adj}$ is a functor of the set of coalgebras of $G$ and the set of algebras of $F$.

the algebra coalgebra equivalence of adj (from the name)

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the algebra coalgebra equivalence of $\mathrm{adj}$ is an equivalence of the set of algebras of $F$ and the set of coalgebras of $G$.

algebra of F (from the name)

Let $F$ be a functor of $C$ and $C$. Then the algebras of $F$ are a basic type.

homomorphism of x1 and x2 (from the name)

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

the composition of f and g (from the name)

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the composition of $f$ and $g$ is a homomorphism of $x_{1}$ and $x_{3}$.

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

the identity morphism of A (from the docstring)

Let $A$ be an algebra of $F$. Then the identity morphism of $A$ is a homomorphism of $A$ and $A$.

the inverse of the structure map of h (from the docstring)

Let $h$ be an element of $\operatorname{IsInitial}$ applied to $A$. Then the inverse of the structure map of $h$ is a homomorphism of $\operatorname{a}$ applied to $A$ and the action of $F$ and $\operatorname{a}$ applied to $A$ defined as $\operatorname{f}$ applied to $\operatorname{to}$ applied to $h$ and $\operatorname{mk}$ applied to the action of $F$ and $\operatorname{a}$ applied to $A$ and the map of $F$ and $\operatorname{str}$ applied to $A$.

Let $\mathrm{self}$ be an algebra of $F$. Then $\operatorname{a}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the equivalence of x1 (from the name)

Let $x_{1}$ be an isomorphism of $F$ and $G$. Then the equivalence of $x_{1}$ is an equivalence of the set of algebras of $F$ and the set of algebras of $G$.

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

the functor of x1 (from the name)

Let $x_{1}$ be a homomorphism of $G$ and $F$. Then the functor of $x_{1}$ is a functor of the set of algebras of $F$ and the set of algebras of $G$.

the functor of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $x_{5}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the functor of $x_{4}$ and $x_{5}$ is an isomorphism of the functor of the composition of $x_{4}$ and $x_{5}$ and the composition of the functor of $x_{5}$ and the functor of $x_{4}$.

the functor of h (from the name)

Assume that $\EqtMACRoH {x_{1}}{x_{2}}$. Then the functor of $h$ is an isomorphism of the functor of $x_{1}$ and the functor of $x_{2}$.

the functor (from the name)

The functor is an isomorphism of the functor of the identity morphism of $F$ and the identity of the set of algebras of $F$.

the isomorphism of h and w (from the name)

Let $h$ be an isomorphism of $\operatorname{a}$ applied to $x_{1}$ and $\operatorname{a}$ applied to $x_{2}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the homomorphism of $h$ and $\operatorname{str}$ applied to $x_{2}$ is equal to the composition of $\operatorname{str}$ applied to $x_{1}$ and the homomorphism of $h$ and $\mathrm{CategoryTheory\_\_Endofunctor\_\_Algebra\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $h$ and $w$ is an isomorphism of $x_{1}$ and $x_{2}$.

Let $\mathrm{self}$ be an algebra of $F$. Then $\operatorname{str}$ applied to $\mathrm{self}$ is a homomorphism of the action of $F$ and $\operatorname{a}$ applied to $\mathrm{self}$ and $\operatorname{a}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

coalgebra of F (from the name)

Let $F$ be a functor of $C$ and $C$. Then the coalgebras of $F$ are a basic type.

homomorphism of x1 and x2 (from the name)

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

the composition of f and g (from the name)

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the composition of $f$ and $g$ is a homomorphism of $x_{1}$ and $x_{3}$.

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

the identity morphism of V (from the docstring)

Let $V$ be a coalgebra of $F$. Then the identity morphism of $V$ is a homomorphism of $V$ and $V$.

the inverse of the structure map of h (from the docstring)

Let $h$ be an element of $\operatorname{IsTerminal}$ applied to $A$. Then the inverse of the structure map of $h$ is a homomorphism of the action of $F$ and $\operatorname{V}$ applied to $A$ and $\operatorname{V}$ applied to $A$ defined as $\operatorname{f}$ applied to $\operatorname{from}$ applied to $h$ and $\operatorname{mk}$ applied to the action of $F$ and $\operatorname{V}$ applied to $A$ and the map of $F$ and $\operatorname{str}$ applied to $A$.

Let $\mathrm{self}$ be a coalgebra of $F$. Then $\operatorname{V}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the equivalence of x1 (from the name)

Let $x_{1}$ be an isomorphism of $F$ and $G$. Then the equivalence of $x_{1}$ is an equivalence of the set of coalgebras of $F$ and the set of coalgebras of $G$.

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

the functor of x1 (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $G$. Then the functor of $x_{1}$ is a functor of the set of coalgebras of $F$ and the set of coalgebras of $G$.

the functor of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $x_{5}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the functor of $x_{4}$ and $x_{5}$ is an isomorphism of the functor of the composition of $x_{4}$ and $x_{5}$ and the composition of the functor of $x_{4}$ and the functor of $x_{5}$.

the functor of h (from the name)

Assume that $\EqtMACRoH {x_{1}}{x_{2}}$. Then the functor of $h$ is an isomorphism of the functor of $x_{1}$ and the functor of $x_{2}$.

the functor (from the name)

The functor is an isomorphism of the functor of the identity morphism of $F$ and the identity of the set of coalgebras of $F$.

the isomorphism of h and w (from the name)

Let $h$ be an isomorphism of $\operatorname{V}$ applied to $x_{1}$ and $\operatorname{V}$ applied to $x_{2}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $\operatorname{str}$ applied to $x_{1}$ and the map of $F$ and the homomorphism of $h$ is equal to the composition of the homomorphism of $h$ and $\operatorname{str}$ applied to $x_{2}$ and $\mathrm{CategoryTheory\_\_Endofunctor\_\_Coalgebra\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $h$ and $w$ is an isomorphism of $x_{1}$ and $x_{2}$.

Let $\mathrm{self}$ be a coalgebra of $F$. Then $\operatorname{str}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{V}$ applied to $\mathrm{self}$ and the action of $F$ and $\operatorname{V}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

automorphism of X (from the name)

Let $X$ be an element of $C$. Then the automorphisms of $X$ are a basic type.

the underlying isomorphism of self (from the docstring)

Let $\mathrm{self}$ be an automorphism of $X$. Then the underlying isomorphism of $\mathrm{self}$ is an isomorphism of $X$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the automorphism multiplicative equivalence of h (from the name)

Let $h$ be an isomorphism of $X$ and $Y$. Then the automorphism multiplicative equivalence of $h$ is a multiplicative equivalence of the set of automorphisms of $X$ and the set of automorphisms of $Y$.

the isomorphism equivalence (from the name)

The isomorphism equivalence is an equivalence from the set of automorphisms of $X$ to the set of isomorphisms of $X$ and $X$.

the end (from the name)

The end is a monoid homomorphism of the set of automorphisms of $X$ and the set of ends of $X$.

the unit end equivalence automorphism of X (from the name)

Let $X$ be an element of $C$. Then the unit end equivalence automorphism of $X$ is a multiplicative equivalence of the set of units of the set of ends of $X$ and the set of automorphisms of $X$.

end of X (from the name)

Let $X$ be an element of $C$. Then the ends of $X$ are a basic type.

Let $\mathrm{self}$ be an end of $X$. Then $\operatorname{asHom}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the homomorphism equivalence (from the name)

The homomorphism equivalence is an equivalence from the set of ends of $X$ to the set of homomorphisms of $X$ and $X$.

the automorphism multiplicative equivalence 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 automorphism multiplicative equivalence of $\mathrm{hf}$ and $X$ is a multiplicative equivalence of the set of automorphisms of $X$ and the set of automorphisms of the action of $f$ and $X$.

the multiplicative equivalence end 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 multiplicative equivalence end of $\mathrm{hf}$ and $X$ is a multiplicative equivalence of the set of ends of $X$ and the set of ends of the action of $f$ and $X$.

the map automorphism of X and f (from the name)

Let $X$ be an element of $C$. Let $f$ be a functor of $C$ and $D$. Then the map automorphism of $X$ and $f$ is a monoid homomorphism of the set of automorphisms of $X$ and the set of automorphisms of the action of $f$ and $X$.

the map end of X and f (from the name)

Let $X$ be an element of $C$. Let $f$ be a functor of $C$ and $D$. Then the map end of $X$ and $f$ is a monoid homomorphism of the set of ends of $X$ and the set of ends of the action of $f$ and $X$.

the end equivalence (from the name)

The end equivalence is a multiplicative equivalence of the set of ends of $X$ and the set of ends of $F$ applied to $X$.

Let $V$ and $C$ be sets. Then we can say that $\operatorname{EnrichedCategory}$ holds for $V$ and $C$.

the homomorphism of x2 and x3 (from the name)

Let $x_{2}$ and $x_{3}$ be elements of $C$. Then the homomorphism of $x_{2}$ and $x_{3}$ is an element of $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

the composition of Y and Z (from the name)

Let $X$, $Y$ and $Z$ be elements of $C$. Then the composition of $Y$ and $Z$ is a homomorphism of the tensor object of the homomorphism of $X$ and $Y$ and the homomorphism of $Y$ and $Z$ and the homomorphism of $X$ and $Z$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $X$, $Y$ and $Z$.

the identity of X (from the name)

Let $X$ be an element of $C$. Then the identity of $X$ is a homomorphism of the tensor unity in the monoidal structure of $V$ and the homomorphism of $X$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $X$.

enriched functor of C and D (from the name)

Let $V$, $C$ and $D$ be sets. Then the enriched functors of $C$ and $D$ are a basic type.

the composition of F and G (from the name)

Let $V$ be a set. Let $F$ be an enriched functor of $C$ and $D$. Let $G$ be an enriched functor of $D$ and $E$. Then the composition of $F$ and $G$ is an enriched functor of $C$ and $E$.

Let $F$ be an enriched functor of $C$ and $D$. Then $\operatorname{forget}$ applied to $F$ is a functor of $\operatorname{ForgetEnrichment}$ applied to $W$ and $C$ and $\operatorname{ForgetEnrichment}$ applied to $W$ and $D$.

Let $F$ be an enriched functor of $C$ and $D$. Let $G$ be an enriched functor of $D$ and $E$. Then $\operatorname{forgetComp}$ applied to $F$ and $G$ is an isomorphism of $\operatorname{forget}$ applied to the composition of $F$ and $G$ and the composition of $\operatorname{forget}$ applied to $F$ and $\operatorname{forget}$ applied to $G$.

Let $W$ and $C$ be sets. Then $\operatorname{forgetId}$ applied to $W$ and $C$ is an isomorphism of $\operatorname{forget}$ applied to the identity enriched functor of $W$ and $C$ and the identity of $\operatorname{ForgetEnrichment}$ applied to $W$ and $C$.

the identity enriched functor of V and C (from the docstring)

Let $V$ and $C$ be sets. Then the identity enriched functor of $V$ and $C$ is an enriched functor of $C$ and $C$.

the isomorphism of h (from the name)

Let $h$ be an isomorphism of $\operatorname{forget}$ applied to $F$ and $\operatorname{forget}$ applied to $G$. Then the isomorphism of $h$ is an isomorphism of $F$ and $G$.

the map of X and Y (from the name)

Let $\mathrm{self}$ be an enriched functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then the map of $X$ and $Y$ is a homomorphism of the homomorphism of $X$ and $Y$ and the homomorphism of the object of $\mathrm{self}$ and $X$ and the object of $\mathrm{self}$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $X$ and $Y$.

the object of self and x4 (from the name)

Let $\mathrm{self}$ be an enriched functor of $C$ and $D$. Let $x_{4}$ be an element of $C$. Then the object of $\mathrm{self}$ and $x_{4}$ is an element of $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

enriched natural transformation of F and G (from the name)

Let $F$ and $G$ be enriched functors of $C$ and $D$. Then the enriched natural transformations of $F$ and $G$ are a basic type.

Let $\mathrm{self}$ be an enriched natural transformation of $F$ and $G$. Then $\operatorname{out}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{forget}$ applied to $F$ and $\operatorname{forget}$ applied to $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $W$ and $C$ be sets. Then an element of $\operatorname{ForgetEnrichment}$ applied to $W$ and $C$ is an element of the function that maps $W$ and $C$ to $C$.

the homomorphism of W and f (from the name)

Let $W$ be a set. Let $f$ be a homomorphism of the tensor unity in the monoidal structure of $W$ and the homomorphism of $X$ and $Y$. Then the homomorphism of $W$ and $f$ is a homomorphism of $\operatorname{of}$ applied to $W$ and $X$ and $\operatorname{of}$ applied to $W$ and $Y$ defined as $f$.

Let $W$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{homTo}$ applied to $W$ and $f$ is a homomorphism of the tensor unity in the monoidal structure of $W$ and the homomorphism of $\operatorname{to}$ applied to $W$ and $X$ and $\operatorname{to}$ applied to $W$ and $Y$ defined as $f$.

Let $W$ be a set. Let $X$ be an element of $C$. Then $\operatorname{of}$ applied to $W$ and $X$ is an element of $\operatorname{ForgetEnrichment}$ applied to $W$ and $C$ defined as $X$.

Let $W$ be a set. Let $X$ be an element of $\operatorname{ForgetEnrichment}$ applied to $W$ and $C$. Then $\operatorname{to}$ applied to $W$ and $X$ is an element of $C$ defined as $X$.

graded natural transformation of F and G (from the name)

Let $A$ be a center of $V$. Let $F$ and $G$ be enriched functors of $C$ and $D$. Then the graded natural transformations of $F$ and $G$ are a basic type.

the graded natural transformation of self and X (from the name)

Let $\mathrm{self}$ be a graded natural transformation of $F$ and $G$. Let $X$ be an element of $C$. Then the graded natural transformation of $\mathrm{self}$ and $X$ is a homomorphism of $\operatorname{fst}$ applied to $A$ and the homomorphism of the object of $F$ and $X$ and the object of $G$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $X$.

Let $F$ be a functor of $V$ and $W$. Let $C$ be a set. Then an element of $\operatorname{TransportEnrichment}$ applied to $F$ and $C$ is an element of the function that maps $F$ and $C$ to $C$.

the composition of Y and Z (from the name)

Let $V$ be a set. Let $X$, $Y$ and $Z$ be elements of $C$. Then the composition of $Y$ and $Z$ is a homomorphism of the tensor object of the homomorphism of $X$ and $Y$ and the homomorphism of $Y$ and $Z$ and the homomorphism of $X$ and $Z$ defined as the composition of $Y$ and $Z$.

the identity of V and X (from the name)

Let $V$ be a set. Let $X$ be an element of $C$. Then the identity of $V$ and $X$ is a homomorphism of the tensor unity in the monoidal structure of $V$ and the homomorphism of $X$ and $X$ defined as the identity of $X$.

the enriched category type equivalence category of C (from the name)

Let $C$ be a set. Then the enriched category type equivalence category of $C$ is an equivalence from $\operatorname{EnrichedCategory}$ applied to the set of sets and $C$ to the proposition that $C$ is a category.

the enriched functor type equivalence functor (from the name)

The enriched functor type equivalence functor is an equivalence from the set of enriched functors of $C$ and $D$ to the set of functors of $C$ and $D$.

the enriched natural transformation Yoneda of F and G (from the name)

Let $F$ and $G$ be enriched functors of $C$ and $D$. Then the enriched natural transformation Yoneda of $F$ and $G$ is a functor of the set of opposites of $V$ and the set of sets.

the enriched natural transformation Yoneda type isomorphism Yoneda natural transformation of F and G (from the name)

Let $F$ and $G$ be enriched functors of $C$ and $D$. Then the enriched natural transformation Yoneda type isomorphism Yoneda natural transformation of $F$ and $G$ is an isomorphism of the enriched natural transformation Yoneda of $F$ and $G$ and the action of the Yoneda and the set of homomorphisms of $\operatorname{enrichedFunctorTypeEquivFunctor}$ applied to $F$ and $\operatorname{enrichedFunctorTypeEquivFunctor}$ applied to $G$.

enriched category of V (from the name)

Let $V$ be a set. Then an enriched category of $V$ is an element of the function that maps $V$ to $\operatorname{Bundled}$ applied to $\operatorname{EnrichedCategory}$ applied to $V$.

the associator of G and H (from the name)

Let $F$ be an enriched functor of $C$ and $D$. Let $G$ be an enriched functor of $D$ and $E$. Let $H$ be an enriched functor of $E$ and $\mathrm{E'}$. Then the associator of $G$ and $H$ is an isomorphism of the composition of the composition of $F$ and $G$ and $H$ and the composition of $F$ and the composition of $G$ and $H$ defined as the isomorphism of the composition of $\operatorname{forgetComp}$ applied to the composition of $F$ and $G$ and $H$ and the composition of the right isomorphism whisker of $\operatorname{forgetComp}$ applied to $F$ and $G$ and $\operatorname{forget}$ applied to $H$ and the composition of the associator of $\operatorname{forget}$ applied to $G$ and $\operatorname{forget}$ applied to $H$ and the composition of the left isomorphism whisker of $\operatorname{forget}$ applied to $F$ and the inverse of $\operatorname{forgetComp}$ applied to $G$ and $H$ and the inverse of $\operatorname{forgetComp}$ applied to $F$ and the composition of $G$ and $H$.

the left unitor of F (from the name)

Let $F$ be an enriched functor of $C$ and $D$. Then the left unitor of $F$ is an isomorphism of the composition of the identity enriched functor of $V$ and $C$ and $F$ and $F$ defined as the isomorphism of the composition of $\operatorname{forgetComp}$ applied to the identity enriched functor of $V$ and $C$ and $F$ and the composition of the right isomorphism whisker of $\operatorname{forgetId}$ applied to $V$ and $C$ and $\operatorname{forget}$ applied to $F$ and the left unitor of $\operatorname{forget}$ applied to $F$.

Let $V$ and $C$ be sets. Then $\operatorname{of}$ applied to $V$ and $C$ is an enriched category of $V$ defined as $\operatorname{of}$ applied to $C$.

the right unitor of F (from the name)

Let $F$ be an enriched functor of $C$ and $D$. Then the right unitor of $F$ is an isomorphism of the composition of $F$ and the identity enriched functor of $V$ and $D$ and $F$ defined as the isomorphism of the composition of $\operatorname{forgetComp}$ applied to $F$ and the identity enriched functor of $V$ and $D$ and the composition of the left isomorphism whisker of $\operatorname{forget}$ applied to $F$ and $\operatorname{forgetId}$ applied to $V$ and $D$ and the right unitor of $\operatorname{forget}$ applied to $F$.

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

Let $F$ be an enriched functor of $C$ and $D$. Let $x_{5}$ be a homomorphism of $G$ and $H$. Then the left whisker of $F$ and $x_{5}$ is a homomorphism of the composition of $F$ and $G$ and the composition of $F$ and $H$ defined as $\operatorname{mk}$ applied to the composition of the homomorphism of $\operatorname{forgetComp}$ applied to $F$ and $G$ and the composition of the left whisker of $\operatorname{forget}$ applied to $F$ and $\operatorname{out}$ applied to $x_{5}$ and the inverse of $\operatorname{forgetComp}$ applied to $F$ and $H$.

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

Let $x_{5}$ be a homomorphism of $F$ and $G$. Let $H$ be an enriched functor of $D$ and $E$. Then the right whisker of $x_{5}$ and $H$ is a homomorphism of the composition of $F$ and $H$ and the composition of $G$ and $H$ defined as $\operatorname{mk}$ applied to the composition of the homomorphism of $\operatorname{forgetComp}$ applied to $F$ and $H$ and the composition of the right whisker of $\operatorname{out}$ applied to $x_{5}$ and $\operatorname{forget}$ applied to $H$ and the inverse of $\operatorname{forgetComp}$ applied to $G$ and $H$.

Let $V$ be a set. Let $x_{5}$ and $x_{6}$ be functors of $J$ and $C$. Then $\operatorname{HasEnrichedHom}$ holds for $V$, $x_{5}$ and $x_{6}$, if the diagram of $x_{5}$ and $x_{6}$ has ends.

Let $V$ be a set. Let $x_{5}$ and $x_{6}$ be functors of $J$ and $C$. Then $\operatorname{HasFunctorEnrichedHom}$ holds for $V$, $x_{5}$ and $x_{6}$, if for all elements $j$ of $J$, $\operatorname{HasEnrichedHom}$ holds for $V$, the composition of $\operatorname{forget}$ applied to $j$ and $x_{5}$ and the composition of $\operatorname{forget}$ applied to $j$ and $x_{6}$.

the cone functor enriched homomorphism of x5 and x6 (from the name)

Let $V$ be a set. Let $x_{5}$ and $x_{6}$ be functors of $J$ and $C$. Then the cone functor enriched homomorphism of $x_{5}$ and $x_{6}$ is a cone of the functor enriched homomorphism of $x_{5}$ and $x_{6}$.

the diagram of x5 and x6 (from the name)

Let $V$ be a set. Let $x_{5}$ and $x_{6}$ be functors of $J$ and $C$. Then the diagram of $x_{5}$ and $x_{6}$ is a functor of the set of opposites of $J$ and the set of functors of $J$ and $V$ defined as the composition of the opposite of $x_{5}$ and the composition of the homomorphism functor of $V$ and $C$ and the action of the left whiskering of $C$ and $V$ and $x_{6}$.

the enriched composition of x6 and x7 (from the name)

Let $V$ be a set. Let $x_{5}$, $x_{6}$ and $x_{7}$ be functors of $J$ and $C$. Then the enriched composition of $x_{6}$ and $x_{7}$ is a homomorphism of the tensor object of the enriched homomorphism of $x_{5}$ and $x_{6}$ and the enriched homomorphism of $x_{6}$ and $x_{7}$ and the enriched homomorphism of $x_{5}$ and $x_{7}$.

the enriched homomorphism of x5 and x6 (from the name)

Let $V$ be a set. Let $x_{5}$ and $x_{6}$ be functors of $J$ and $C$. Then the enriched homomorphism of $x_{5}$ and $x_{6}$ is an element of $V$ defined as the end of the diagram of $x_{5}$ and $x_{6}$.

the enriched homomorphism projection of x6 and j (from the name)

Let $V$ be a set. Let $x_{5}$ and $x_{6}$ be functors of $J$ and $C$. Let $j$ be an element of $J$. Then the enriched homomorphism projection of $x_{6}$ and $j$ is a homomorphism of the enriched homomorphism of $x_{5}$ and $x_{6}$ and the homomorphism of the action of $x_{5}$ and $j$ and the action of $x_{6}$ and $j$ defined as the projection of the diagram of $x_{5}$ and $x_{6}$ and $j$.

the enriched identity of V and x5 (from the name)

Let $V$ be a set. Let $x_{5}$ be a functor of $J$ and $C$. Then the enriched identity of $V$ and $x_{5}$ is a homomorphism of the tensor unity in the monoidal structure of $V$ and the enriched homomorphism of $x_{5}$ and $x_{5}$ defined as $\operatorname{homEquiv}$ applied to $V$ and the identity morphism of $x_{5}$.

the functor enriched composition of x6 and x7 (from the name)

Let $V$ be a set. Let $x_{5}$, $x_{6}$ and $x_{7}$ be functors of $J$ and $C$. Then the functor enriched composition of $x_{6}$ and $x_{7}$ is a homomorphism of the tensor object of the functor enriched homomorphism of $x_{5}$ and $x_{6}$ and the functor enriched homomorphism of $x_{6}$ and $x_{7}$ and the functor enriched homomorphism of $x_{5}$ and $x_{7}$.

the functor enriched homomorphism of x5 and x6 (from the name)

Let $V$ be a set. Let $x_{5}$ and $x_{6}$ be functors of $J$ and $C$. Then the functor enriched homomorphism of $x_{5}$ and $x_{6}$ is a functor of $J$ and $V$.

the functor enriched identity of V and x5 (from the name)

Let $V$ be a set. Let $x_{5}$ be a functor of $J$ and $C$. Then the functor enriched identity of $V$ and $x_{5}$ is a homomorphism of the tensor unity in the monoidal structure of the set of functors of $J$ and $V$ and the functor enriched homomorphism of $x_{5}$ and $x_{5}$.

the functor homomorphism equivalence of V (from the name)

Let $V$ be a set. Then the functor homomorphism equivalence of $V$ is an equivalence from the set of homomorphisms of $x_{5}$ and $x_{6}$ to the set of homomorphisms of the tensor unity in the monoidal structure of the set of functors of $J$ and $V$ and the functor enriched homomorphism of $x_{5}$ and $x_{6}$ defined as the composition of the homomorphism equivalence of $V$ and the homomorphism equivalence of the limit of $V$.

the homomorphism equivalence of V (from the name)

Let $V$ be a set. Then the homomorphism equivalence of $V$ is an equivalence from the set of homomorphisms of $x_{5}$ and $x_{6}$ to the set of homomorphisms of the tensor unity in the monoidal structure of $V$ and the enriched homomorphism of $x_{5}$ and $x_{6}$.

the limit of V (from the docstring)

Let $V$ be a set. Let $x_{5}$ and $x_{6}$ be functors of $J$ and $C$. Then the limit of $V$ is an element of $\operatorname{IsLimit}$ applied to the cone functor enriched homomorphism of $x_{5}$ and $x_{6}$.

the precomposition enriched homomorphism of x7 and G (from the name)

Let $V$ be a set. Let $x_{6}$ and $x_{7}$ be functors of $J$ and $C$. Let $G$ be a functor of $K$ and $J$. Then the precomposition enriched homomorphism of $x_{7}$ and $G$ is a homomorphism of the enriched homomorphism of $x_{6}$ and $x_{7}$ and the enriched homomorphism of the composition of $G$ and $x_{6}$ and the composition of $G$ and $x_{7}$ defined as the precomposition enriched homomorphism of the identity of the composition of $G$ and $x_{6}$ and the identity of the composition of $G$ and $x_{7}$.

the precomposition enriched homomorphism of x10 and x11 (from the name)

Let $V$ be a set. Let $G$ be a functor of $K$ and $J$. Let $x_{10}$ be an isomorphism of the composition of $G$ and $x_{6}$ and $x_{8}$. Let $x_{11}$ be an isomorphism of the composition of $G$ and $x_{7}$ and $x_{9}$. Then the precomposition enriched homomorphism of $x_{10}$ and $x_{11}$ is a homomorphism of the enriched homomorphism of $x_{6}$ and $x_{7}$ and the enriched homomorphism of $x_{8}$ and $x_{9}$.

the homomorphism congruence of x6 and x7 (from the name)

Let $V$ be a set. Let $x_{6}$ be an isomorphism of $X$ and $x_{4}$. Let $x_{7}$ be an isomorphism of $Y$ and $x_{5}$. Then the homomorphism congruence of $x_{6}$ and $x_{7}$ is an isomorphism of the homomorphism of $X$ and $Y$ and the homomorphism of $x_{4}$ and $x_{5}$.

Let $V$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $F$ be a functor of $J$ and $C$. Then we can say that $\operatorname{HasConicalLimit}$ holds for $V$ and $F$.

V has conical limits (from the name)

Let $V$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $C$ be a set. Then $V$ has conical limits, if $\operatorname{HasConicalLimitsOfSize}$ holds for $V$ and $C$.

V has conical limits of shapes (from the name)

Let $J$ and $C$ be sets. Let $V$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $V$ has conical limits of shapes.

Let $V$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $C$ be a set. Then we can say that $\operatorname{HasConicalLimitsOfSize}$ holds for $V$ and $C$.

f has conical products (from the name)

Let $V$ be a set. Let $f$ be a function from elements of $I$ to elements of $C$. Then $f$ has conical products, if $\operatorname{HasConicalLimit}$ holds for $V$ and the functor of $f$.

V has conical products (from the name)

Let $V$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $C$ be a set. Then we can say that $V$ has conical products.

Let $V$ be a set. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{HasConicalPullback}$ holds for $V$, $f$ and $g$, if $\operatorname{HasConicalLimit}$ holds for $V$ and the cospan of $f$ and $g$.

Let $V$ and $C$ be sets. Then $\operatorname{HasConicalPullbacks}$ holds for $V$ and $C$, if $V$ has conical limits of shapes.

V has conical terminals (from the name)

Let $V$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $C$ be a set. Then $V$ has conical terminals, if $V$ has conical limits of shapes.

Let $V$ and $C$ be sets. Then $\operatorname{forgetEnrichmentOppositeEquivalence}$ applied to $V$ and $C$ is an equivalence of $\operatorname{ForgetEnrichment}$ applied to $V$ and the set of opposites of $C$ and the set of opposites of $\operatorname{ForgetEnrichment}$ applied to $V$ and $C$.

the functor of V and C (from the name)

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

the inverse of V and C (from the name)

Let $V$ and $C$ be sets. Then the inverse of $V$ and $C$ is a functor of the set of opposites of $\operatorname{ForgetEnrichment}$ applied to $V$ and $C$ and $\operatorname{ForgetEnrichment}$ applied to $V$ and the set of opposites of $C$.