Definitions: Mathlib.CategoryTheory, part 12 of 25

the diagonal object pullback first component isomorphism of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the diagonal object pullback first component isomorphism of $f$ and $g$ is an isomorphism of the diagonal object of the first projection of the pullback of $f$ and $g$ and the pullback of the composition of the second projection of the pullback of $g$ and $g$ and $g$ and $f$.

the diagonal morphism of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the diagonal morphism of $f$ is a homomorphism of $X$ and the diagonal object of $f$.

the diagonal object of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the diagonal object of $f$ is an element of $C$ defined as the pullback of $f$ and $f$.

the pullback diagonal map identity isomorphism of g and i (from the name)

Let $f$ be a homomorphism of $X$ and $T$. Let $g$ be a homomorphism of $Y$ and $T$. Let $i$ be a homomorphism of $T$ and $S$. Then the pullback diagonal map identity isomorphism of $g$ and $i$ is an isomorphism of the pullback of the diagonal morphism of $i$ and the map of $g$ and the identity morphism of $S$ and the pullback of $f$ and $g$.

the pullback diagonal map isomorphism of x3 and x4 (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $i$ be a homomorphism of $U$ and $Y$. Let $x_{3}$ be a homomorphism of $x_{1}$ and the pullback of $f$ and $i$. Let $x_{4}$ be a homomorphism of $x_{2}$ and the pullback of $f$ and $i$. Then the pullback diagonal map isomorphism of $x_{3}$ and $x_{4}$ is an isomorphism of the pullback of the diagonal morphism of $f$ and the map of the composition of $x_{4}$ and the first projection of the pullback of $f$ and $i$ and $i$ and the pullback of $x_{3}$ and $x_{4}$.

the homomorphism of x3 and x4 (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $i$ be a homomorphism of $U$ and $Y$. Let $x_{3}$ be a homomorphism of $x_{1}$ and the pullback of $f$ and $i$. Let $x_{4}$ be a homomorphism of $x_{2}$ and the pullback of $f$ and $i$. Then the homomorphism of $x_{3}$ and $x_{4}$ is a homomorphism of the pullback of the diagonal morphism of $f$ and the map of the composition of $x_{4}$ and the first projection of the pullback of $f$ and $i$ and $i$ and the pullback of $x_{3}$ and $x_{4}$.

the underlying inverse of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Let $i$ be a homomorphism of $U$ and $Y$. Let $x_{3}$ be a homomorphism of $x_{1}$ and the pullback of $f$ and $i$. Let $x_{4}$ be a homomorphism of $x_{2}$ and the pullback of $f$ and $i$. Then the underlying inverse of $f$ is a homomorphism of the pullback of $x_{3}$ and $x_{4}$ and the pullback of the diagonal morphism of $f$ and the map of the composition of $x_{4}$ and the first projection of the pullback of $f$ and $i$ and $i$.

the pullback first component first component isomorphism of h1 and h2 (from the name)

Let $f$ be a homomorphism of $X$ and $S$. Let $g$ be a homomorphism of $Y$ and $S$. Let $\mathrm{f'}$ be a homomorphism of $\mathrm{X'}$ and $\mathrm{S'}$. Let $\mathrm{g'}$ be a homomorphism of $\mathrm{Y'}$ and $\mathrm{S'}$. Let $x_{1}$ be a homomorphism of $X$ and $\mathrm{X'}$. Let $x_{2}$ be a homomorphism of $Y$ and $\mathrm{Y'}$. Let $x_{3}$ be a homomorphism of $S$ and $\mathrm{S'}$ such that the composition of $f$ and $x_{3}$ is equal to the composition of $x_{1}$ and $\mathrm{f'}$ and the composition of $g$ and $x_{3}$ is equal to the composition of $x_{2}$ and $\mathrm{g'}$. Then the pullback first component first component isomorphism of $x_{2}$ and $x_{3}$ is an isomorphism of the pullback of the first projection of the pullback of the first projection of the pullback of $\mathrm{f'}$ and $\mathrm{g'}$ and $x_{1}$ and the first projection of the pullback of the second projection of the pullback of $\mathrm{f'}$ and $\mathrm{g'}$ and $x_{2}$ and the pullback of $f$ and $g$.

the codiagonal morphism of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the codiagonal morphism of $f$ is a homomorphism of the codiagonal object of $f$ and $Y$.

the codiagonal object of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the codiagonal object of $f$ is an element of $C$ defined as the pushout of $f$ and $f$.

X is a binary coproduct disjoint with respect to Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then we can say that $X$ is a binary coproduct disjoint with respect to $Y$.

Let $C$ be a set. Then $\operatorname{BinaryCoproductsDisjoint}$ holds for $C$, if $\operatorname{CoproductsOfShapeDisjoint}$ holds for $C$ and the set of walking pairs.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Then we can say that $\operatorname{CoproductDisjoint}$ holds for $X$.

Let $C$ and $x_{1}$ be sets. Then we can say that $\operatorname{CoproductsOfShapeDisjoint}$ holds for $C$ and $x_{1}$.

$\operatorname{ofBinaryCoproductDisjoint}$ is an element of $\operatorname{IsInitial}$ applied to the pullback of the left injection and the right injection defined as $\operatorname{ofBinaryCoproductDisjointOfIsColimitOfIsLimit}$ applied to $\operatorname{isColimit}$ applied to the pair of $X$ and $Y$ and $\operatorname{isLimit}$ applied to the left injection and the right injection.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $f$ and $g$. Then $\operatorname{ofBinaryCoproductDisjointOfIsColimit}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsInitial}$ applied to the pullback of $f$ and $g$ defined as $\operatorname{ofBinaryCoproductDisjointOfIsColimitOfIsLimit}$ applied to $\mathrm{hc}$ and $\operatorname{isLimit}$ applied to $f$ and $g$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then $\operatorname{ofBinaryCoproductDisjointOfIsColimitOfIsLimit}$ applied to $\mathrm{hc}$ and $\mathrm{hs}$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{pt}$ applied to $s$.

Let $s$ be a pullback cone of the left injection and the right injection. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then $\operatorname{ofBinaryCoproductDisjointOfIsLimit}$ applied to $s$ and $\mathrm{hs}$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{pt}$ applied to $s$ defined as $\operatorname{ofBinaryCoproductDisjointOfIsColimitOfIsLimit}$ applied to $\operatorname{isColimit}$ applied to the pair of $X$ and $Y$ and $\mathrm{hs}$.

Assume that $i \neq j$. Then $\operatorname{ofCoproductDisjoint}$ applied to $\mathrm{hij}$ is an element of $\operatorname{IsInitial}$ applied to the pullback of the inclusion of $X$ and $i$ and the inclusion of $X$ and $j$ defined as $\operatorname{ofCoproductDisjointOfIsColimitOfIsLimit}$ applied to $\mathrm{hij}$, $\operatorname{isColimit}$ applied to the functor of $X$ and $\operatorname{isLimit}$ applied to the inclusion of $X$ and $i$ and the inclusion of $X$ and $j$.

Assume that $i \neq j$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{fst}$ be a homomorphism of $Z$ and $X$ applied to $i$. Let $\mathrm{snd}$ be a homomorphism of $Z$ and $X$ applied to $j$ such that the composition of $\mathrm{fst}$ and the injection of $c$ and $i$ is equal to the composition of $\mathrm{snd}$ and the injection of $c$ and $j$. Then $\operatorname{ofCoproductDisjointOfCommSq}$ applied to $\mathrm{hij}$, $\mathrm{hc}$, $\mathrm{fst}$, $\mathrm{snd}$ and $h_{2}$ is an element of $\operatorname{IsInitial}$ applied to $Z$ defined as $\operatorname{ofStrict}$ applied to the lift of $\mathrm{fst}$ and $\mathrm{snd}$ and $\operatorname{ofCoproductDisjointOfIsColimitOfIsLimit}$ applied to $\mathrm{hij}$, $\mathrm{hc}$ and $\operatorname{isLimit}$ applied to the cospan of the injection of $c$ and $i$ and the injection of $c$ and $j$.

Assume that $i \neq j$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $Z$ and $f$. Then $\operatorname{ofCoproductDisjointOfIsColimit}$ applied to $\mathrm{hij}$ and $\mathrm{hc}$ is an element of $\operatorname{IsInitial}$ applied to the pullback of $f$ applied to $i$ and $f$ applied to $j$ defined as $\operatorname{ofCoproductDisjointOfIsColimitOfIsLimit}$ applied to $\mathrm{hij}$, $\mathrm{hc}$ and $\operatorname{isLimit}$ applied to $f$ applied to $i$ and $f$ applied to $j$.

Assume that $i \neq j$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then $\operatorname{ofCoproductDisjointOfIsColimitOfIsLimit}$ applied to $\mathrm{hij}$, $\mathrm{hc}$ and $\mathrm{hs}$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{pt}$ applied to $s$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_CoproductDisjoint\_\_nonempty\_isInitial\_of\_ne}$ applied to $\mathrm{hc}$, $\mathrm{hij}$, $s$ and $\mathrm{hs}$.

Assume that $i \neq j$. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then $\operatorname{ofCoproductDisjointOfIsLimit}$ applied to $\mathrm{hij}$ and $\mathrm{hs}$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{pt}$ applied to $s$ defined as $\operatorname{ofCoproductDisjointOfIsColimitOfIsLimit}$ applied to $\mathrm{hij}$, $\operatorname{isColimit}$ applied to the functor of $X$ and $\mathrm{hs}$.

cowedge of F (from the name)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then a cowedge of $F$ is an element of the function that maps $F$ to the set of multicoforks of the multispan index coend of $F$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $f$ be a function from elements $j_{1}$ of $J$ to homomorphisms of the action of the action of $F$ and $\operatorname{op}$ applied to $j_{1}$ and $j_{1}$ and $X$ such that for all elements $i$ and $j$ of $J$, for all homomorphisms $g$ of $i$ and $j$, the composition of the component of the map of $F$ and the opposite in $g$ and $i$ and $f$ applied to $i$ is equal to the composition of the map of the action of $F$ and $\operatorname{op}$ applied to $j$ and $g$ and $f$ applied to $j$. Then $\operatorname{desc}$ applied to $\mathrm{hc}$, $j_{1}$, $f$ and $\mathrm{hf}$ is a homomorphism of $\operatorname{pt}$ applied to $c$ and $X$.

the extension of e and he (from the name)

Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $x_{2}$ and $\operatorname{pt}$ applied to $x_{3}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $j$ of $J$, the composition of the projection of $x_{2}$ and $j$ and the homomorphism of $e$ is equal to the projection of $x_{3}$ and $j$ and $\mathrm{CategoryTheory\_\_Limits\_\_Cowedge\_\_ext\_\_\_auto\_1}$. Then the extension of $e$ and $\mathrm{he}$ is an isomorphism of $x_{2}$ and $x_{3}$.

Let $\mathrm{pt}$ be an element of $C$. Let $x_{2}$ be a function from elements $j_{1}$ of $J$ to homomorphisms of the action of the action of $F$ and $\operatorname{op}$ applied to $j_{1}$ and $j_{1}$ and $\mathrm{pt}$ such that for all elements $i$ and $j$ of $J$, for all homomorphisms $f$ of $i$ and $j$, the composition of the component of the map of $F$ and the opposite in $f$ and $i$ and $x_{2}$ applied to $i$ is equal to the composition of the map of the action of $F$ and $\operatorname{op}$ applied to $j$ and $f$ and $x_{2}$ applied to $j$. Then $\operatorname{mk}$ applied to $\mathrm{pt}$, $j_{1}$, $x_{2}$ and $h$ is a cowedge of $F$.

F has coends (from the name)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then $F$ has coends, if the multispan index coend of $F$ has multicoequalizers.

F has ends (from the name)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then $F$ has ends, if the multicospan index end of $F$ has multiequalizers.

wedge of F (from the name)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then a wedge of $F$ is an element of the function that maps $F$ to the set of multiforks of the multicospan index end of $F$.

the lift of hc and f (from the name)

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $f$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $X$ and the action of the action of $F$ and $\operatorname{op}$ applied to $j_{1}$ and $j_{1}$ such that for all elements $i$ and $j$ of $J$, for all homomorphisms $g$ of $i$ and $j$, the composition of $f$ applied to $i$ and the map of the action of $F$ and $\operatorname{op}$ applied to $i$ and $g$ is equal to the composition of $f$ applied to $j$ and the component of the map of $F$ and the opposite in $g$ and $j$. Then the lift of $\mathrm{hc}$ and $j_{1}$ is a homomorphism of $X$ and $\operatorname{pt}$ applied to $c$.

the extension of e and he (from the name)

Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $x_{2}$ and $\operatorname{pt}$ applied to $x_{3}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $j$ of $J$, the inclusion of $x_{2}$ and $j$ is equal to the composition of the homomorphism of $e$ and the inclusion of $x_{3}$ and $j$ and $\mathrm{CategoryTheory\_\_Limits\_\_Wedge\_\_ext\_\_\_auto\_1}$. Then the extension of $e$ and $\mathrm{he}$ is an isomorphism of $x_{2}$ and $x_{3}$.

Let $\mathrm{pt}$ be an element of $C$. Let $x_{2}$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $\mathrm{pt}$ and the action of the action of $F$ and $\operatorname{op}$ applied to $j_{1}$ and $j_{1}$ such that for all elements $i$ and $j$ of $J$, for all homomorphisms $f$ of $i$ and $j$, the composition of $x_{2}$ applied to $i$ and the map of the action of $F$ and $\operatorname{op}$ applied to $i$ and $f$ is equal to the composition of $x_{2}$ applied to $j$ and the component of the map of $F$ and the opposite in $f$ and $j$. Then $\operatorname{mk}$ applied to $\mathrm{pt}$, $j_{1}$, $x_{2}$ and $h$ is a wedge of $F$.

the coend of F (from the name)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then the coend of $F$ is an element of $C$ defined as the multicoequalizer of the multispan index coend of $F$.

Let $f$ be a function from elements $j_{1}$ of $J$ to homomorphisms of the action of the action of $F$ and $\operatorname{op}$ applied to $j_{1}$ and $j_{1}$ and $X$ such that for all elements $i$ and $j$ of $J$, for all homomorphisms $g$ of $i$ and $j$, the composition of the component of the map of $F$ and the opposite in $g$ and $i$ and $f$ applied to $i$ is equal to the composition of the map of the action of $F$ and $\operatorname{op}$ applied to $j$ and $g$ and $f$ applied to $j$. Then $\operatorname{desc}$ applied to $j_{1}$, $f$ and $\mathrm{hf}$ is a homomorphism of the coend of $F$ and $X$ defined as the function that maps $\mathrm{hf}$ to $\operatorname{desc}$ applied to $\operatorname{isColimit}$ applied to the multispan of the multispan index coend of $F$, $j_{1}$, $f$ and $\mathrm{hf}$.

the map of f (from the name)

Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the map of $f$ is a homomorphism of the coend of $F$ and the coend of $\mathrm{F'}$.

the inclusion of F and j (from the name)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Let $j$ be an element of $J$. Then the inclusion of $F$ and $j$ is a homomorphism of the action of the action of $F$ and $\operatorname{op}$ applied to $j$ and $j$ and the coend of $F$ defined as the projection of the multispan index coend of $F$ and $j$.

the coend functor of J and C (from the name)

Let $J$ and $C$ be sets. Then the coend functor of $J$ and $C$ is a functor of the set of functors of the set of opposites of $J$ and the set of functors of $J$ and $C$ and $C$.

the end functor of J and C (from the name)

Let $J$ and $C$ be sets. Then the end functor of $J$ and $C$ is a functor of the set of functors of the set of opposites of $J$ and the set of functors of $J$ and $C$ and $C$.

the end of F (from the docstring)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then the end of $F$ is an element of $C$ defined as the multiequalizer of the multicospan index end of $F$.

the lift of f and j1 (from the name)

Let $f$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $X$ and the action of the action of $F$ and $\operatorname{op}$ applied to $j_{1}$ and $j_{1}$ such that for all elements $i$ and $j$ of $J$, for all homomorphisms $g$ of $i$ and $j$, the composition of $f$ applied to $i$ and the map of the action of $F$ and $\operatorname{op}$ applied to $i$ and $g$ is equal to the composition of $f$ applied to $j$ and the component of the map of $F$ and the opposite in $g$ and $j$. Then the lift of $j_{1}$ and $f$ is a homomorphism of $X$ and the end of $F$ defined as the function that maps $\mathrm{hf}$ to the lift of $\operatorname{isLimit}$ applied to the multicospan of the multicospan index end of $F$ and $j_{1}$.

the map of f (from the name)

Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the map of $f$ is a homomorphism of the end of $F$ and the end of $\mathrm{F'}$.

the projection of F and j (from the name)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Let $j$ be an element of $J$. Then the projection of $F$ and $j$ is a homomorphism of the end of $F$ and the action of the action of $F$ and $\operatorname{op}$ applied to $j$ and $j$ defined as the inclusion of the multicospan index end of $F$ and $j$.

the multicospan index end of F (from the name)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then the multicospan index end of $F$ is a multicospan index of the multicospan shape end of $J$ and $C$ defined as $\operatorname{mk}$ applied to the function that maps $j$ to the action of the action of $F$ and $\operatorname{op}$ applied to $j$ and $j$, the function that maps $f$ to the action of the action of $F$ and $\operatorname{op}$ applied to the left object of $f$ and the right object of $f$, the function that maps $f_{1}$ to the map of the action of $F$ and $\operatorname{op}$ applied to the left object of $f_{1}$ and the homomorphism of $f_{1}$ and the function that maps $f_{2}$ to the component of the map of $F$ and the opposite in the homomorphism of $f_{2}$ and the right object of $f_{2}$.

the multicospan shape end of J (from the name)

Let $J$ be a set. Then the multicospan shape end of $J$ is a shape defined as $\operatorname{mk}$ applied to $J$, the set of arrows of $J$, the function that maps $f$ to the left object of $f$ and the function that maps $f_{1}$ to the right object of $f_{1}$.

the multispan index coend of F (from the name)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then the multispan index coend of $F$ is a multispan index of the multispan shape coend of $J$ and $C$ defined as $\operatorname{mk}$ applied to the function that maps $f$ to the action of the action of $F$ and $\operatorname{op}$ applied to the right object of $f$ and the left object of $f$, the function that maps $j$ to the action of the action of $F$ and $\operatorname{op}$ applied to $j$ and $j$, the function that maps $f_{1}$ to the component of the map of $F$ and the opposite in the homomorphism of $f_{1}$ and the left object of $f_{1}$ and the function that maps $f_{2}$ to the map of the action of $F$ and $\operatorname{op}$ applied to the right object of $f_{2}$ and the homomorphism of $f_{2}$.

the multispan shape coend of J (from the name)

Let $J$ be a set. Then the multispan shape coend of $J$ is a shape defined as $\operatorname{mk}$ applied to the set of arrows of $J$, $J$, the function that maps $f$ to the left object of $f$ and the function that maps $f_{1}$ to the right object of $f_{1}$.

the cocone of t (from the name)

Let $t$ be a cofork of the map of $F$ and the left and the map of $F$ and the right. Then the cocone of $t$ is a cocone of $F$.

cofork of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $Y$ and $X$. Then a cofork of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of cocones of the parallel pair of $f$ and $g$.

Let $\mathrm{hs}$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $k$ be a homomorphism of $X$ and $W$ such that the composition of $f$ and $k$ is equal to the composition of $g$ and $k$. Then $\operatorname{desc}$ applied to $\mathrm{hs}$, $k$ and $h$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $W$ defined as $\operatorname{desc}$ applied to $\mathrm{hs}$ and the projection of $k$ and $h$.

Let $\mathrm{hs}$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $k$ be a homomorphism of $X$ and $W$ such that $\EqtMACRoH {\operatorname{comp} (f , k)}{\operatorname{comp} (g , k)}$. Then $\operatorname{desc'}$ applied to $\mathrm{hs}$, $k$ and $h$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_\_u3c0\_} (s), l)}{k})}$ defined as $\operatorname{desc}$ applied to $\mathrm{hs}$, $k$ and $h$.

the homomorphism isomorphism of ht and Z (from the name)

Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to $t$. Let $Z$ be an element of $C$. Then the homomorphism isomorphism of $\mathrm{ht}$ and $Z$ is an element of $\EquivMACRoAE {\operatorname{Hom} (\operatorname{pt} (t), Z)}{(\SubtypeSet {h}{(\EqtMACRoH {\operatorname{comp} (f , h)}{\operatorname{comp} (g , h)})})}$.

Let $t$ be a cofork of $f$ and $g$. Let $\mathrm{lift}$ be a function from coforks $s_{2}$ of $f$ and $g$ to homomorphisms of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s_{2}$ such that for all coforks $s_{1}$ of $f$ and $g$, the composition of the projection of $t$ and $\mathrm{lift}$ applied to $s_{1}$ is equal to the projection of $s_{1}$ and for all coforks $s$ of $f$ and $g$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s$, if the composition of the projection of $t$ and $m$ is equal to the projection of $s$, then $\EqtMACRoH {m}{\mathrm{lift} (s)}$. Then $\operatorname{mk}$ applied to $t$, $s_{2}$, $\mathrm{lift}$, $\mathrm{fac}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsColimit}$ applied to $t$.

Let $t$ be a cofork of $f$ and $g$. Let $\mathrm{create}$ be a function from coforks $s$ of $f$ and $g$ to elements of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_\_u3c0\_} (t), l)}{\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_\_u3c0\_} (s)}, \mathrm{forall} (\operatorname{Hom} (\operatorname{pt} (t), \operatorname{pt} (s)), \lambda m . \mathrm{if} (\EqtMACRoH {\operatorname{comp} (\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_\_u3c0\_} (t), m)}{\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_\_u3c0\_} (s)}, \EqtMACRoH {m}{l})))}$. Then $\operatorname{mk'}$ applied to $t$, $s$ and $\mathrm{create}$ is an element of $\operatorname{IsColimit}$ applied to $t$.

Assume that for all coforks $s$ of $f$ and $g$, $\mathrm{ExistsUnique}$ holds for the function that maps $l$ to the proposition that the composition of the projection of $t$ and $l$ is equal to the projection of $s$. Then $\operatorname{ofExistsUnique}$ applied to $\mathrm{hs}$ is an element of $\operatorname{IsColimit}$ applied to $t$.

the extension of i and w (from the name)

Let $i$ be an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the projection of $s$ and the homomorphism of $i$ is equal to the projection of $t$ and $\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_ext\_\_\_auto\_1}$. Then the extension of $i$ and $w$ is an isomorphism of $s$ and $t$.

Let $c$ be a cofork of $f$ and $g$. Let $\mathrm{c'}$ be a cofork of $\mathrm{f'}$ and $\mathrm{g'}$. Let $x_{1}$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $x_{2}$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $\mathrm{c'}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{1}$ and $\mathrm{f'}$ is equal to the composition of $f$ and the homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_isColimitEquivOfIsos\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{1}$ and $\mathrm{g'}$ is equal to the composition of $g$ and the homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_isColimitEquivOfIsos\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the inverse of $x_{2}$ and the composition of the projection of $c$ and the homomorphism of $e$ is equal to the projection of $\mathrm{c'}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_isColimitEquivOfIsos\_\_\_auto\_5}$. Then $\operatorname{isColimitEquivOfIsos}$ applied to $c$, $\mathrm{c'}$, $x_{1}$, $x_{2}$, $e$, $h$, $h_{1}$ and $h_{2}$ is an element of $\EquivMACRoAE {\operatorname{IsColimit} (c)}{\operatorname{IsColimit} (\mathrm{c'})}$.

Let $c$ be a cofork of $f$ and $g$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{c'}$ be a cofork of $\mathrm{f'}$ and $\mathrm{g'}$. Let $x_{1}$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $x_{2}$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $\mathrm{c'}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{1}$ and $\mathrm{f'}$ is equal to the composition of $f$ and the homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_isColimitOfIsos\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{1}$ and $\mathrm{g'}$ is equal to the composition of $g$ and the homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_isColimitOfIsos\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the inverse of $x_{2}$ and the composition of the projection of $c$ and the homomorphism of $e$ is equal to the projection of $\mathrm{c'}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_isColimitOfIsos\_\_\_auto\_5}$. Then $\operatorname{isColimitOfIsos}$ applied to $c$, $\mathrm{hc}$, $\mathrm{c'}$, $x_{1}$, $x_{2}$, $e$, $h$, $h_{1}$ and $h_{2}$ is an element of $\operatorname{IsColimit}$ applied to $\mathrm{c'}$.

the isomorphism cofork of c (from the name)

Let $c$ be a cofork of $f$ and $g$. Then the isomorphism cofork of $c$ is an isomorphism of $c$ and the projection of the projection of $c$ and $\operatorname{condition}$ applied to $c$.

the homomorphism of k and w (from the name)

Let $k$ be a homomorphism of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s$ such that the composition of the projection of $t$ and $k$ is equal to the projection of $s$. Then the homomorphism of $k$ and $w$ is a homomorphism of $t$ and $s$.

the cofork of t (from the name)

Let $t$ be a cocone of $F$. Then the cofork of $t$ is a cofork of the map of $F$ and the left and the map of $F$ and the right.

the projection of x1 and w (from the name)

Let $x_{1}$ be a homomorphism of $X$ and $P$ such that the composition of $f$ and $x_{1}$ is equal to the composition of $g$ and $x_{1}$. Then the projection of $x_{1}$ and $w$ is a cofork of $f$ and $g$.

the projection of t (from the name)

Let $t$ be a cofork of $f$ and $g$. Then the projection of $t$ is a homomorphism of $X$ and $\operatorname{pt}$ applied to $t$ defined as the component of the inclusion of $t$ and the one.

the extension of h and #3 (from the name)

Assume that the composition of $f$ and $x_{1}$ is equal to the composition of $g$ and $x_{1}$. Assume that the composition of $f$ and $x_{2}$ is equal to the composition of $g$ and $x_{2}$. Assume that $\EqtMACRoH {x_{1}}{x_{2}}$. Then the extension of $\mathrm{w'}$ and $h$ is an isomorphism of the projection of $x_{1}$ and $w$ and the projection of $x_{2}$ and $\mathrm{w'}$.

the cone of t (from the name)

Let $t$ be a fork of the map of $F$ and the left and the map of $F$ and the right. Then the cone of $t$ is a cone of $F$.

fork of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then a fork of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of cones of the parallel pair of $f$ and $g$.

the homomorphism isomorphism of ht and Z (from the name)

Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to $t$. Let $Z$ be an element of $C$. Then the homomorphism isomorphism of $\mathrm{ht}$ and $Z$ is an element of $\EquivMACRoAE {\operatorname{Hom} (Z , \operatorname{pt} (t))}{(\SubtypeSet {h}{(\EqtMACRoH {\operatorname{comp} (h , f)}{\operatorname{comp} (h , g)})})}$.

the lift of hs and k (from the name)

Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $k$ be a homomorphism of $W$ and $X$ such that the composition of $k$ and $f$ is equal to the composition of $k$ and $g$. Then the lift of $\mathrm{hs}$ and $k$ is a homomorphism of $W$ and $\operatorname{pt}$ applied to $s$ defined as the lift of $\mathrm{hs}$ and the inclusion of $k$ and $h$.

the lift of hs and k (from the name)

Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $k$ be a homomorphism of $W$ and $X$ such that $\EqtMACRoH {\operatorname{comp} (k , f)}{\operatorname{comp} (k , g)}$. Then the lift of $\mathrm{hs}$ and $k$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , \mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_\_u3b9\_} (s))}{k})}$ defined as the lift of $\mathrm{hs}$ and $k$.

Let $t$ be a fork of $f$ and $g$. Let $\mathrm{lift}$ be a function from forks $s_{2}$ of $f$ and $g$ to homomorphisms of $\operatorname{pt}$ applied to $s_{2}$ and $\operatorname{pt}$ applied to $t$ such that for all forks $s_{1}$ of $f$ and $g$, the composition of $\mathrm{lift}$ applied to $s_{1}$ and the inclusion of $t$ is equal to the inclusion of $s_{1}$ and for all forks $s$ of $f$ and $g$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$, if the composition of $m$ and the inclusion of $t$ is equal to the inclusion of $s$, then $\EqtMACRoH {m}{\mathrm{lift} (s)}$. Then $\operatorname{mk}$ applied to $t$, $s_{2}$, $\mathrm{lift}$, $\mathrm{fac}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsLimit}$ applied to $t$.

Let $t$ be a fork of $f$ and $g$. Let $\mathrm{create}$ be a function from forks $s$ of $f$ and $g$ to elements of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (l , \mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_\_u3b9\_} (t))}{\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_\_u3b9\_} (s)}, \mathrm{forall} (\operatorname{Hom} (\operatorname{pt} (s), \operatorname{pt} (t)), \lambda m . \mathrm{if} (\EqtMACRoH {\operatorname{comp} (m , \mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_\_u3b9\_} (t))}{\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_\_u3b9\_} (s)}, \EqtMACRoH {m}{l})))}$. Then $\operatorname{mk'}$ applied to $t$, $s$ and $\mathrm{create}$ is an element of $\operatorname{IsLimit}$ applied to $t$.

Assume that for all forks $s$ of $f$ and $g$, $\mathrm{ExistsUnique}$ holds for the function that maps $l$ to the proposition that the composition of $l$ and the inclusion of $t$ is equal to the inclusion of $s$. Then $\operatorname{ofExistsUnique}$ applied to $\mathrm{hs}$ is an element of $\operatorname{IsLimit}$ applied to $t$.

the equivalence of x1 and x2 (from the name)

Let $x_{1}$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $x_{2}$ be an isomorphism of $Y$ and $\mathrm{Y'}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{1}$ and $\mathrm{f'}$ is equal to the composition of $f$ and the homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_equivOfIsos\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{1}$ and $\mathrm{g'}$ is equal to the composition of $g$ and the homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_equivOfIsos\_\_\_auto\_3}$. Then the equivalence of $x_{1}$ and $x_{2}$ is an equivalence of the set of forks of $f$ and $g$ and the set of forks of $\mathrm{f'}$ and $\mathrm{g'}$.

the extension of i and w (from the name)

Let $i$ be an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $i$ and the inclusion of $t$ is equal to the inclusion of $s$ and $\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_ext\_\_\_auto\_1}$. Then the extension of $i$ and $w$ is an isomorphism of $s$ and $t$.

Let $c$ be a fork of $f$ and $g$. Let $\mathrm{c'}$ be a fork of $\mathrm{f'}$ and $\mathrm{g'}$. Let $x_{1}$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $x_{2}$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $\mathrm{c'}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{1}$ and $\mathrm{f'}$ is equal to the composition of $f$ and the homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_isLimitEquivOfIsos\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{1}$ and $\mathrm{g'}$ is equal to the composition of $g$ and the homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_isLimitEquivOfIsos\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $e$ and the inclusion of $\mathrm{c'}$ is equal to the composition of the inclusion of $c$ and the homomorphism of $x_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_isLimitEquivOfIsos\_\_\_auto\_5}$. Then $\operatorname{isLimitEquivOfIsos}$ applied to $c$, $\mathrm{c'}$, $x_{1}$, $x_{2}$, $e$, $h$, $h_{1}$ and $h_{2}$ is an element of $\EquivMACRoAE {\operatorname{IsLimit} (c)}{\operatorname{IsLimit} (\mathrm{c'})}$.

Let $c$ be a fork of $f$ and $g$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{c'}$ be a fork of $\mathrm{f'}$ and $\mathrm{g'}$. Let $x_{1}$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $x_{2}$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $\mathrm{c'}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{1}$ and $\mathrm{f'}$ is equal to the composition of $f$ and the homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_isLimitOfIsos\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{1}$ and $\mathrm{g'}$ is equal to the composition of $g$ and the homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_isLimitOfIsos\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $e$ and the inclusion of $\mathrm{c'}$ is equal to the composition of the inclusion of $c$ and the homomorphism of $x_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_isLimitOfIsos\_\_\_auto\_5}$. Then $\operatorname{isLimitOfIsos}$ applied to $c$, $\mathrm{hc}$, $\mathrm{c'}$, $x_{1}$, $x_{2}$, $e$, $h$, $h_{1}$ and $h_{2}$ is an element of $\operatorname{IsLimit}$ applied to $\mathrm{c'}$.

the isomorphism fork of c (from the name)

Let $c$ be a fork of $f$ and $g$. Then the isomorphism fork of $c$ is an isomorphism of $c$ and the inclusion of the inclusion of $c$ and $\operatorname{condition}$ applied to $c$.

the homomorphism of k and w (from the name)

Let $k$ be a homomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ such that the composition of $k$ and the inclusion of $t$ is equal to the inclusion of $s$. Then the homomorphism of $k$ and $w$ is a homomorphism of $s$ and $t$.

the fork of t (from the name)

Let $t$ be a cone of $F$. Then the fork of $t$ is a fork of the map of $F$ and the left and the map of $F$ and the right.

the inclusion of x1 and w (from the name)

Let $x_{1}$ be a homomorphism of $P$ and $X$ such that the composition of $x_{1}$ and $f$ is equal to the composition of $x_{1}$ and $g$. Then the inclusion of $x_{1}$ and $w$ is a fork of $f$ and $g$.

the inclusion of t (from the name)

Let $t$ be a fork of $f$ and $g$. Then the inclusion of $t$ is a homomorphism of $\operatorname{pt}$ applied to $t$ and $X$ defined as the component of the projection of $t$ and the zero.

the extension of h and #3 (from the name)

Assume that the composition of $x_{1}$ and $f$ is equal to the composition of $x_{1}$ and $g$. Assume that the composition of $x_{2}$ and $f$ is equal to the composition of $x_{2}$ and $g$. Assume that $\EqtMACRoH {x_{1}}{x_{2}}$. Then the extension of $\mathrm{w'}$ and $h$ is an isomorphism of the inclusion of $x_{1}$ and $w$ and the inclusion of $x_{2}$ and $\mathrm{w'}$.

Let $f$ and $g$ be homomorphisms of $Y$ and $X$. Then $\operatorname{HasCoequalizer}$ holds for $f$ and $g$, if the parallel pair of $f$ and $g$ has colimits.

C has coequalizers (from the name)

Let $C$ be a set. Then $C$ has coequalizers, if $\operatorname{HasColimitsOfShape}$ holds for the set of walking parallel pairs and $C$.

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then $\operatorname{HasEqualizer}$ holds for $f$ and $g$, if the parallel pair of $f$ and $g$ has limits.

C has equalizers (from the name)

Let $C$ be a set. Then $C$ has equalizers, if $\operatorname{HasLimitsOfShape}$ holds for the set of walking parallel pairs and $C$.

walking parallel pair (from the name)

The walking parallel pairs are a basic type.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the one.

the walking parallel pair of x (from the name)

Let $x$ be a natural number. Then the walking parallel pair of $x$ is a walking parallel pair defined as $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $0$, the zero and the one.

the one (from the name)

The one is a walking parallel pair.

the zero (from the name)

The zero is a walking parallel pair.

walking parallel pair homomorphism of x and x1 (from the name)

Let $x$ and $x_{1}$ be walking parallel pairs. Then the walking parallel pair homomorphisms of $x$ and $x_{1}$ are a basic type.

the composition of x and x1 (from the name)

Let $x$ be a walking parallel pair homomorphism of $X$ and $Y$. Let $x_{1}$ be a walking parallel pair homomorphism of $Y$ and $Z$. Then the composition of $x$ and $x_{1}$ is a walking parallel pair homomorphism of $X$ and $Z$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero, the one and the left and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero, the one and the right and $\mathrm{PULift}$ applied to the set of functions from walking parallel pairs $X$ to elements of $\mathrm{motive}$ applied to $X$, $X$ and the identity of $X$.

the identity of X (from the name)

Let $X$ be a walking parallel pair. Then the identity of $X$ is a walking parallel pair homomorphism of $X$ and $X$.

the left (from the name)

The left is a walking parallel pair homomorphism of the zero and the one.

the right (from the name)

The right is a walking parallel pair homomorphism of the zero and the one.

the cocone of f (from the name)

Let $f$ be a homomorphism of $Y$ and $X$. Then the cocone of $f$ is a cofork of the identity morphism of $Y$ and the composition of $f$ and the chosen section of $f$.

the coequalizer of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $Y$ and $X$. Then the coequalizer of $f$ and $g$ is an element of $C$ defined as the colimit of the parallel pair of $f$ and $g$.

the cofork of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $Y$ and $X$. Then the cofork of $f$ and $g$ is a cofork of $f$ and $g$ defined as the cocone of the parallel pair of $f$ and $g$.

Let $k$ be a homomorphism of $X$ and $W$ such that the composition of $f$ and $k$ is equal to the composition of $g$ and $k$. Then $\operatorname{desc}$ applied to $k$ and $h_{1}$ is a homomorphism of the coequalizer of $f$ and $g$ and $W$ defined as $\operatorname{desc}$ applied to the parallel pair of $f$ and $g$ and the projection of $k$ and $h_{1}$.

Let $k$ be a homomorphism of $X$ and $W$ such that $\EqtMACRoH {\operatorname{comp} (f , k)}{\operatorname{comp} (g , k)}$. Then $\operatorname{desc'}$ applied to $k$ and $h_{1}$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (\mathrm{CategoryTheory\_\_Limits\_\_coequalizer\_\_\_u3c0\_} (f , g), l)}{k})}$ defined as $\operatorname{desc}$ applied to $k$ and $h_{1}$.

the coequalizer of f (from the docstring)

Let $f$ be a homomorphism of $Y$ and $X$. Then the coequalizer of $f$ is an isomorphism of the coequalizer of $f$ and $f$ and $X$ defined as $\operatorname{asIso'}$ applied to the projection of $f$ and $f$.

the projection of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $Y$ and $X$. Then the projection of $f$ and $g$ is a homomorphism of $X$ and the coequalizer of $f$ and $g$ defined as the inclusion of the parallel pair of $f$ and $g$ and the one.

the comparison morphism for the coequalizer of f (from the docstring)

Let $f$ and $g$ be homomorphisms of $Y$ and $X$. Let $G$ be a functor of $C$ and $D$. Then the comparison morphism for the coequalizer of $f$ is a homomorphism of the coequalizer of the map of $G$ and $f$ and the map of $G$ and $g$ and the action of $G$ and the coequalizer of $f$ and $g$.

Let $f$ and $g$ be homomorphisms of $Y$ and $X$. Then $\operatorname{coequalizerIsCoequalizer}$ applied to $f$ and $g$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $f$ and $g$ and $\operatorname{condition}$ applied to $f$ and $g$.

the cone of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the cone of $f$ is a fork of the identity morphism of $Y$ and the composition of the chosen retraction of $f$ and $f$.

the diagram isomorphism parallel pair of F (from the name)

Let $F$ be a functor of the set of walking parallel pairs and $C$. Then the diagram isomorphism parallel pair of $F$ is an isomorphism of $F$ and the parallel pair of the map of $F$ and the left and the map of $F$ and the right.

the equalizer of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the equalizer of $f$ and $g$ is an element of $C$ defined as the limit of the parallel pair of $f$ and $g$.

the fork of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the fork of $f$ and $g$ is a fork of $f$ and $g$ defined as the cone of the parallel pair of $f$ and $g$.

the equalizer of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the equalizer of $f$ is an isomorphism of the equalizer of $f$ and $f$ and $X$ defined as $\operatorname{asIso}$ applied to the inclusion of $f$ and $f$.

the lift of k and h1 (from the name)

Let $k$ be a homomorphism of $W$ and $X$ such that the composition of $k$ and $f$ is equal to the composition of $k$ and $g$. Then the lift of $k$ and $h_{1}$ is a homomorphism of $W$ and the equalizer of $f$ and $g$ defined as the lift of the parallel pair of $f$ and $g$ and the inclusion of $k$ and $h_{1}$.

the lift of k and h1 (from the name)

Let $k$ be a homomorphism of $W$ and $X$ such that $\EqtMACRoH {\operatorname{comp} (k , f)}{\operatorname{comp} (k , g)}$. Then the lift of $k$ and $h_{1}$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , \mathrm{CategoryTheory\_\_Limits\_\_equalizer\_\_\_u3b9\_} (f , g))}{k})}$ defined as the lift of $k$ and $h_{1}$.

the inclusion of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the inclusion of $f$ and $g$ is a homomorphism of the equalizer of $f$ and $g$ and $X$ defined as the projection from the limit object to a value of the functor of the parallel pair of $f$ and $g$ and the zero.

the comparison morphism for the equalizer of f (from the docstring)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Let $G$ be a functor of $C$ and $D$. Then the comparison morphism for the equalizer of $f$ is a homomorphism of the action of $G$ and the equalizer of $f$ and $g$ and the equalizer of the map of $G$ and $f$ and the map of $G$ and $g$.

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then $\operatorname{equalizerIsEqualizer}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $f$ and $g$ and $\operatorname{condition}$ applied to $f$ and $g$.

the identity cofork of h (from the name)

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

the identity fork of h (from the name)

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

the default (from the name)

The default is a walking parallel pair defined as the zero.

Let $i$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $h$ be a homomorphism of $Z$ and $Y$. Then $\operatorname{isCoequalizerEpiComp}$ applied to $i$ and $h$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_isCoequalizerEpiComp\_\_\_proof\_2}$ applied to $h$ and $\mathrm{CategoryTheory\_\_Limits\_\_isCoequalizerEpiComp\_\_\_proof\_1}$ applied to $h$.

Assume that $\EqtMACRoH {f}{g}$. Then $\operatorname{isColimitIdCofork}$ applied to $h$ is an element of $\operatorname{IsColimit}$ applied to the identity cofork of $h$.

Let $i$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $h$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{isEqualizerCompMono}$ applied to $i$ and $h$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_isEqualizerCompMono\_\_\_proof\_2}$ applied to $h$ and $\mathrm{CategoryTheory\_\_Limits\_\_isEqualizerCompMono\_\_\_proof\_1}$ applied to $h$.

Assume that $\EqtMACRoH {f}{g}$. Then $\operatorname{isLimitIdFork}$ applied to $h$ is an element of $\operatorname{IsLimit}$ applied to the identity fork of $h$.

Let $h$ be a homomorphism of $Z$ and $X$. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitPrecompFork}$ applied to $h$, $\mathrm{hs}$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the precomposition fork of $s$ and $c$.

Let $f$ be a homomorphism of $Y$ and $X$. Then $\operatorname{isSplitEpiCoequalizes}$ applied to $f$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $f$ defined as $\operatorname{mk'}$ applied to the cocone of $f$ and the function that maps $s$ to the composition of the chosen section of $f$ and the projection of $s$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isSplitMonoEqualizes}$ applied to $f$ is an element of $\operatorname{IsLimit}$ applied to the cone of $f$ defined as $\operatorname{mk'}$ applied to the cone of $f$ and the function that maps $s$ to the composition of the inclusion of $s$ and the chosen retraction of $f$.

the lift precomposition of hc and #4 (from the name)

Let $h$ be a homomorphism of $Z$ and $X$. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{s'}$ be a fork of the composition of $h$ and $f$ and the composition of $h$ and $g$. Then the lift precomposition of $\mathrm{hc}$ and $\mathrm{s'}$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{s'}$ and $\operatorname{pt}$ applied to the precomposition fork of $s$ and $c$.

the parallel pair of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the parallel pair of $f$ and $g$ is a functor of the set of walking parallel pairs and $C$.

Assume that $\EqtMACRoH {f}{\mathrm{f'}}$. Assume that $\EqtMACRoH {g}{\mathrm{g'}}$. Then $\operatorname{eqOfHomEq}$ applied to $\mathrm{hf}$ and $\mathrm{hg}$ is an isomorphism of the parallel pair of $f$ and $g$ and the parallel pair of $\mathrm{f'}$ and $\mathrm{g'}$.

the extension of zero and one (from the name)

Let $\mathrm{zero}$ be an isomorphism of the action of $F$ and the zero and the action of $G$ and the zero. Let $\mathrm{one}$ be an isomorphism of the action of $F$ and the one and the action of $G$ and the one such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the left and the homomorphism of $\mathrm{one}$ is equal to the composition of the homomorphism of $\mathrm{zero}$ and the map of $G$ and the left and $\mathrm{CategoryTheory\_\_Limits\_\_parallelPair\_\_ext\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the right and the homomorphism of $\mathrm{one}$ is equal to the composition of the homomorphism of $\mathrm{zero}$ and the map of $G$ and the right and $\mathrm{CategoryTheory\_\_Limits\_\_parallelPair\_\_ext\_\_\_auto\_3}$. Then the extension of $\mathrm{zero}$ and $\mathrm{one}$ is an isomorphism of $F$ and $G$.

the parallel pair homomorphism of wf and wg (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Let $\mathrm{f'}$ and $\mathrm{g'}$ be homomorphisms of $\mathrm{X'}$ and $\mathrm{Y'}$. Let $p$ be a homomorphism of $X$ and $\mathrm{X'}$. Let $q$ be a homomorphism of $Y$ and $\mathrm{Y'}$ such that the composition of $f$ and $q$ is equal to the composition of $p$ and $\mathrm{f'}$ and the composition of $g$ and $q$ is equal to the composition of $p$ and $\mathrm{g'}$. Then the parallel pair homomorphism of $p$ and $q$ is a homomorphism of the parallel pair of $f$ and $g$ and the parallel pair of $\mathrm{f'}$ and $\mathrm{g'}$.

the parallel pair homomorphism of p and q (from the name)

Let $p$ be a homomorphism of the action of $F$ and the zero and the action of $G$ and the zero. Let $q$ be a homomorphism of the action of $F$ and the one and the action of $G$ and the one such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the left and $q$ is equal to the composition of $p$ and the map of $G$ and the left and $\mathrm{CategoryTheory\_\_Limits\_\_parallelPairHomMk\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the right and $q$ is equal to the composition of $p$ and the map of $G$ and the right and $\mathrm{CategoryTheory\_\_Limits\_\_parallelPairHomMk\_\_\_auto\_3}$. Then the parallel pair homomorphism of $p$ and $q$ is a homomorphism of $F$ and $G$.

the parallel pair isomorphism of wf and wg (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Let $\mathrm{f'}$ and $\mathrm{g'}$ be homomorphisms of $\mathrm{X'}$ and $\mathrm{Y'}$. Let $p$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $q$ be an isomorphism of $Y$ and $\mathrm{Y'}$ such that the composition of $f$ and the homomorphism of $q$ is equal to the composition of the homomorphism of $p$ and $\mathrm{f'}$ and the composition of $g$ and the homomorphism of $q$ is equal to the composition of the homomorphism of $p$ and $\mathrm{g'}$. Then the parallel pair isomorphism of $p$ and $q$ is an isomorphism of the parallel pair of $f$ and $g$ and the parallel pair of $\mathrm{f'}$ and $\mathrm{g'}$.

the parallel pair isomorphism of p and q (from the name)

Let $p$ be an isomorphism of the action of $F$ and the zero and the action of $G$ and the zero. Let $q$ be an isomorphism of the action of $F$ and the one and the action of $G$ and the one such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the left and the homomorphism of $q$ is equal to the composition of the homomorphism of $p$ and the map of $G$ and the left and $\mathrm{CategoryTheory\_\_Limits\_\_parallelPairIsoMk\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the right and the homomorphism of $q$ is equal to the composition of the homomorphism of $p$ and the map of $G$ and the right and $\mathrm{CategoryTheory\_\_Limits\_\_parallelPairIsoMk\_\_\_auto\_3}$. Then the parallel pair isomorphism of $p$ and $q$ is an isomorphism of $F$ and $G$.

the precomposition fork of s and c (from the name)

Let $h$ be a homomorphism of $Z$ and $X$. Let $s$ be a fork of $f$ and $g$. Let $c$ be a pullback cone of the inclusion of $s$ and $h$. Then the precomposition fork of $s$ and $c$ is a fork of the composition of $h$ and $f$ and the composition of $h$ and $g$.

the split epimorphism of h (from the name)

Let $C$ be a set. Assume that the composition of the composition of $f$ and $r$ and $f$ is equal to $f$. Let $h$ be an element of $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{trans}$ applied to $\mathrm{hr}$ and $\operatorname{symm}$ applied to $\mathrm{CategoryTheory\_\_Category\_\_id\_comp}$ applied to $f$. Then the split epimorphism of $h$ is a split epimorphism of $f$.

the coequalizer of C and hf (from the docstring)

Let $C$ be a set. Assume that the composition of $f$ and $f$ is equal to $f$. Then the coequalizer of $C$ and $\mathrm{hf}$ is a split epimorphism of the projection of the identity morphism of $X$ and $f$ defined as the split epimorphism of $\operatorname{isColimit}$ applied to the parallel pair of the identity morphism of $X$ and $f$.

the split epimorphism of i (from the name)

Let $C$ be a set. Assume that the composition of $f$ and $f$ is equal to $f$. Let $i$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the split epimorphism of $i$ is a split epimorphism of the projection of $c$.

the split monomorphism of h (from the name)

Let $C$ be a set. Assume that the composition of $f$ and the composition of $r$ and $f$ is equal to $f$. Let $h$ be an element of $\operatorname{IsLimit}$ applied to the inclusion of $f$ and $\operatorname{trans}$ applied to $\mathrm{hr}$ and $\operatorname{symm}$ applied to $\mathrm{CategoryTheory\_\_Category\_\_comp\_id}$ applied to $f$. Then the split monomorphism of $h$ is a split monomorphism of $f$.

the equalizer of C and hf (from the docstring)

Let $C$ be a set. Assume that the composition of $f$ and $f$ is equal to $f$. Then the equalizer of $C$ and $\mathrm{hf}$ is a split monomorphism of the inclusion of the identity morphism of $X$ and $f$ defined as the split monomorphism of $\operatorname{isLimit}$ applied to the parallel pair of the identity morphism of $X$ and $f$.

the split monomorphism of i (from the name)

Let $C$ be a set. Assume that the composition of $f$ and $f$ is equal to $f$. Let $i$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the split monomorphism of $i$ is a split monomorphism of the inclusion of $c$.

the walking parallel pair opposite (from the name)

The walking parallel pair opposite is a functor of the set of walking parallel pairs and the set of opposites of the set of walking parallel pairs.

the equivalence (from the docstring)

The equivalence is an equivalence of the set of walking parallel pairs and the set of opposites of the set of walking parallel pairs.

C has finite colimits (from the name)

Let $C$ be a set. Then we can say that $C$ has finite colimits.

C has finite limits (from the name)

Let $C$ be a set. Then we can say that $C$ has finite limits.

C has finite wide pullbacks (from the name)

Let $C$ be a set. Then we can say that $C$ has finite wide pullbacks.

C has finite wide pushouts (from the name)

Let $C$ be a set. Then we can say that $C$ has finite wide pushouts.

Let $J$ be a shape. Then an element of $\operatorname{proxyType}$ applied to $J$ is an element of the function that maps $J$ to $\mathrm{Sum}$ applied to $\operatorname{L}$ applied to $J$ and $\operatorname{R}$ applied to $J$.

Let $J$ be a shape. Then $\operatorname{proxyTypeEquiv}$ applied to $J$ is an equivalence from $\mathrm{Sum}$ applied to $\operatorname{L}$ applied to $J$ and $\operatorname{R}$ applied to $J$ to the set of walking multicospans of $J$.

Let $J$ be a shape. Then an element of $\operatorname{proxyType}$ applied to $J$ is an element of the function that maps $J$ to $\mathrm{Sum}$ applied to $\operatorname{L}$ applied to $J$ and $\operatorname{R}$ applied to $J$.

Let $J$ be a shape. Then $\operatorname{proxyTypeEquiv}$ applied to $J$ is an equivalence from $\mathrm{Sum}$ applied to $\operatorname{L}$ applied to $J$ and $\operatorname{R}$ applied to $J$ to the set of walking multispans of $J$.

C has finite coproducts (from the name)

Let $C$ be a set. Then we can say that $C$ has finite coproducts.

C has finite products (from the name)

Let $C$ be a set. Then we can say that $C$ has finite products.

the binary coproduct cocone of F and G (from the name)

Let $F$ and $G$ be functors of $C$ and the set of sets. Then the binary coproduct cocone of $F$ and $G$ is a binary cofan of $F$ and $G$ defined as $\operatorname{mk}$ applied to the left injection and the right injection.

the colimit cocone of F and G (from the docstring)

Let $F$ and $G$ be functors of $C$ and the set of sets. Then the colimit cocone of $F$ and $G$ is an element of $\operatorname{IsColimit}$ applied to the binary coproduct cocone of $F$ and $G$.

the binary coproduct for F and G (from the docstring)

Let $F$ and $G$ be functors of $C$ and the set of sets. Then the binary coproduct for $F$ and $G$ is a colimit cocone of the pair of $F$ and $G$ defined as $\operatorname{mk}$ applied to the binary coproduct cocone of $F$ and $G$ and the colimit cocone of $F$ and $G$.

the binary coproduct equivalence of G and a (from the name)

Let $F$ and $G$ be functors of $C$ and the set of sets. Let $a$ be an element of $C$. Then the binary coproduct equivalence of $G$ and $a$ is an equivalence from the action of the coproduct of $F$ and $G$ and $a$ to $\mathrm{Sum}$ applied to the action of $F$ and $a$ and the action of $G$ and $a$.

the binary coproduct isomorphism of F and G (from the name)

Let $F$ and $G$ be functors of $C$ and the set of sets. Then the binary coproduct isomorphism of $F$ and $G$ is an isomorphism of the coproduct of $F$ and $G$ and the coproduct of $F$ and $G$ defined as the isomorphism colimit cocone of the binary coproduct for $F$ and $G$.

the binary product cone of F and G (from the name)

Let $F$ and $G$ be functors of $C$ and the set of sets. Then the binary product cone of $F$ and $G$ is an element of $\operatorname{BinaryFan}$ applied to $F$ and $G$ defined as $\operatorname{mk}$ applied to the first component and the second component.

the binary product equivalence of G and a (from the name)

Let $F$ and $G$ be functors of $C$ and the set of sets. Let $a$ be an element of $C$. Then the binary product equivalence of $G$ and $a$ is an equivalence from the action of the product of $F$ and $G$ and $a$ to $\mathrm{Prod}$ applied to the action of $F$ and $a$ and the action of $G$ and $a$.

the binary product isomorphism of F and G (from the name)

Let $F$ and $G$ be functors of $C$ and the set of sets. Then the binary product isomorphism of $F$ and $G$ is an isomorphism of the product of $F$ and $G$ and the product of $F$ and $G$ defined as the isomorphism limit cone of the binary product for $F$ and $G$.

the limit cone of F and G (from the docstring)

Let $F$ and $G$ be functors of $C$ and the set of sets. Then the limit cone of $F$ and $G$ is an element of $\operatorname{IsLimit}$ applied to the binary product cone of $F$ and $G$.

the binary product for F and G (from the docstring)

Let $F$ and $G$ be functors of $C$ and the set of sets. Then the binary product for $F$ and $G$ is a limit cone of the pair of $F$ and $G$ defined as $\operatorname{mk}$ applied to the binary product cone of $F$ and $G$ and the limit cone of $F$ and $G$.

the coproduct of F and G (from the name)

Let $F$ and $G$ be functors of $C$ and the set of sets. Then the coproduct of $F$ and $G$ is a functor of $C$ and the set of sets.

Let $x_{3}$ be a homomorphism of $x_{1}$ and $F$. Let $x_{4}$ be a homomorphism of $x_{2}$ and $F$. Then $\operatorname{desc}$ applied to $x_{3}$ and $x_{4}$ is a homomorphism of the coproduct of $x_{1}$ and $x_{2}$ and $F$.

the left injection (from the name)

The left injection is a homomorphism of $F$ and the coproduct of $F$ and $G$.

the right injection (from the name)

The right injection is a homomorphism of $G$ and the coproduct of $F$ and $G$.

the coproduct left injection of x1 (from the name)

Let $x_{1}$ be an element of the action of $F$ and $a$. Then the coproduct left injection of $x_{1}$ is an element of the action of the coproduct of $F$ and $G$ and $a$ defined as $\operatorname{hom}$ applied to the component of the inverse of the binary coproduct isomorphism of $F$ and $G$ and $a$ and $\operatorname{inl}$ applied to $x_{1}$.

the coproduct right injection of x1 (from the name)

Let $x_{1}$ be an element of the action of $G$ and $a$. Then the coproduct right injection of $x_{1}$ is an element of the action of the coproduct of $F$ and $G$ and $a$ defined as $\operatorname{hom}$ applied to the component of the inverse of the binary coproduct isomorphism of $F$ and $G$ and $a$ and $\operatorname{inr}$ applied to $x_{1}$.

the product of F and G (from the name)

Let $F$ and $G$ be functors of $C$ and the set of sets. Then the product of $F$ and $G$ is a functor of $C$ and the set of sets.

the first component (from the name)

The first component is a homomorphism of the product of $F$ and $G$ and $F$.

the lift of x3 and x4 (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $x_{1}$. Let $x_{4}$ be a homomorphism of $F$ and $x_{2}$. Then the lift of $x_{3}$ and $x_{4}$ is a homomorphism of $F$ and the product of $x_{1}$ and $x_{2}$.

the second component (from the name)

The second component is a homomorphism of the product of $F$ and $G$ and $G$.

the product of x1 and y (from the name)

Let $x_{1}$ be an element of the action of $F$ and $a$. Let $y$ be an element of the action of $G$ and $a$. Then the product of $x_{1}$ and $y$ is an element of the action of the product of $F$ and $G$ and $a$ defined as $\operatorname{hom}$ applied to the component of the inverse of the binary product isomorphism of $F$ and $G$ and $a$ and $\ProdmkMACRoU {x_{1}}{y}$.

the cocone fiberwise colimit of c (from the name)

Let $c$ be a cocone of $G$. Then the cocone fiberwise colimit of $c$ is a cocone of the fiberwise colimit of $G$.

the cocone of c (from the name)

Let $c$ be a cocone of the fiberwise colimit of $G$. Then the cocone of $c$ is a cocone of $G$.

the colimit fiberwise colimit isomorphism of G (from the name)

Let $G$ be a functor of $\operatorname{Grothendieck}$ applied to $F$ and $H$. Then the colimit fiberwise colimit isomorphism of $G$ is an isomorphism of the colimit of the fiberwise colimit of $G$ and the colimit of $G$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the fiberwise colimit of $G$ and $\operatorname{isColimitCoconeFiberwiseColimitOfCocone}$ applied to $\operatorname{isColimit}$ applied to $G$.

the fiberwise colimit of F and H (from the name)

Let $F$ be a functor of $C$ and the set of categories. Let $H$ be a set. Then the fiberwise colimit of $F$ and $H$ is a functor of the set of functors of $\operatorname{Grothendieck}$ applied to $F$ and $H$ and the set of functors of $C$ and $H$.

the isomorphism (from the docstring)

The isomorphism is an isomorphism of the composition of the fiberwise colimit of $F$ and $H$ and the colimit and the colimit.

the fiberwise colimit composition evaluation isomorphism of c (from the name)

Let $c$ be an element of $C$. Then the fiberwise colimit composition evaluation isomorphism of $c$ is an isomorphism of the composition of the fiberwise colimit of $F$ and $H$ and the action of the evaluation of $C$ and $H$ and $c$ and the composition of the action of the left whiskering of $\operatorname{Grothendieck}$ applied to $F$ and $H$ and the inclusion of $F$ and $c$ and the colimit defined as the identity of the composition of the fiberwise colimit of $F$ and $H$ and the action of the evaluation of $C$ and $H$ and $c$.

the fiberwise colimit of G (from the name)

Let $G$ be a functor of $\operatorname{Grothendieck}$ applied to $F$ and $H$. Then the fiberwise colimit of $G$ is a functor of $C$ and $H$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitCoconeFiberwiseColimitOfCocone}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the cocone fiberwise colimit of $c$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitCoconeOfFiberwiseCocone}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $c$.

Let $G$ be a functor of $\operatorname{Grothendieck}$ applied to $F$ and $H$. Then $\operatorname{natTransIntoForgetCompFiberwiseColimit}$ applied to $G$ is a homomorphism of $G$ and the composition of $\operatorname{forget}$ applied to $F$ and the fiberwise colimit of $G$.

f has images (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ has images.

sq has image maps (from the name)

Let $\mathrm{sq}$ be a homomorphism of $f$ and $g$. Then we can say that $\mathrm{sq}$ has image maps.

the image map of sq (from the name)

Let $\mathrm{sq}$ be a homomorphism of $f$ and $g$. Then the image map of $\mathrm{sq}$ is an image map of $\mathrm{sq}$ defined as $\operatorname{choice}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_HasImageMap\_\_has\_image\_map}$.

C has image maps (from the name)

Let $C$ be a set. Then we can say that $C$ has image maps.

C has images (from the name)

Let $C$ be a set. Then we can say that $C$ has images.

C has strong epimorphism images (from the name)

Let $C$ be a set. Then we can say that $C$ has strong epimorphism images.

C has strong epimorphism monomorphism factorisations (from the name)

Let $C$ be a set. Then we can say that $C$ has strong epimorphism monomorphism factorisations.

the image factorisation of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the image factorisation of $f$ is an image factorisation of $f$ defined as $\operatorname{choice}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_HasImage\_\_exists\_image}$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isImage}$ applied to $f$ is an element of $\operatorname{IsImage}$ applied to the monomorphism factorisation of $f$ defined as $\operatorname{isImage}$ applied to the image factorisation of $f$.

the monomorphism factorisation of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the monomorphism factorisation of $f$ is a monomorphism factorisation of $f$ defined as $\operatorname{F}$ applied to the image factorisation of $f$.

image factorisation of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the image factorisations of $f$ are a basic type.

Let $\mathrm{self}$ be an image factorisation of $f$. Then $\operatorname{F}$ applied to $\mathrm{self}$ is a monomorphism factorisation of $f$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the copy of m and e (from the name)

Let $F$ be an image factorisation of $f$. Let $m$ be a homomorphism of $\operatorname{I}$ applied to $\operatorname{F}$ applied to $F$ and $Y$. Let $e$ be a homomorphism of $X$ and $\operatorname{I}$ applied to $\operatorname{F}$ applied to $F$. Assume that $\mathrm{autoParam}$ holds for $\EqtMACRoH {m}{\operatorname{m} (\operatorname{F} (F))}$ and $\mathrm{CategoryTheory\_\_Limits\_\_ImageFactorisation\_\_copy\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for $\EqtMACRoH {e}{\operatorname{e} (\operatorname{F} (F))}$ and $\mathrm{CategoryTheory\_\_Limits\_\_ImageFactorisation\_\_copy\_\_\_auto\_3}$. Then the copy of $m$ and $e$ is an image factorisation of $f$.

Let $\mathrm{self}$ be an image factorisation of $f$. Then $\operatorname{isImage}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsImage}$ applied to $\operatorname{F}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the image factorisation of F and sq (from the name)

Let $F$ be an image factorisation of the homomorphism of $f$. Let $\mathrm{sq}$ be a homomorphism of $f$ and $g$. Then the image factorisation of $F$ and $\mathrm{sq}$ is an image factorisation of the homomorphism of $g$ defined as $\operatorname{mk}$ applied to the monomorphism factorisation of $\operatorname{F}$ applied to $F$ and $\mathrm{sq}$ and $\operatorname{ofArrowIso}$ applied to $\operatorname{isImage}$ applied to $F$ and $\mathrm{sq}$.

the image factorisation of F and e (from the name)

Let $F$ be an image factorisation of $f$. Let $e$ be an isomorphism of $\operatorname{I}$ applied to $\operatorname{F}$ applied to $F$ and $\mathrm{I'}$. Then the image factorisation of $F$ and $e$ is an image factorisation of $f$ defined as $\operatorname{mk}$ applied to the monomorphism factorisation of $\operatorname{F}$ applied to $F$ and $e$ and $\operatorname{ofIsoI}$ applied to $\operatorname{isImage}$ applied to $F$ and $e$.

image map of sq (from the name)

Let $\mathrm{sq}$ be a homomorphism of $f$ and $g$. Then the image maps of $\mathrm{sq}$ are a basic type.

the map of self (from the name)

Let $\mathrm{self}$ be an image map of $\mathrm{sq}$. Then the map of $\mathrm{self}$ is a homomorphism of the categorical image of the homomorphism of $f$ and the categorical image of the homomorphism of $g$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the transport of F and h2 (from the name)

Let $\mathrm{sq}$ be a homomorphism of $f$ and $g$. Let $F$ be a monomorphism factorisation of the homomorphism of $f$. Let $\mathrm{hF'}$ be an element of $\operatorname{IsImage}$ applied to $\mathrm{F'}$. Assume that the composition of $\mathrm{map}$ and $\operatorname{m}$ applied to $\mathrm{F'}$ is equal to the composition of $\operatorname{m}$ applied to $F$ and the right part of $\mathrm{sq}$. Then the transport of $F$ and $\mathrm{hF'}$ is an image map of $\mathrm{sq}$.

Let $F$ be a monomorphism factorisation of $f$. Then the elements of $\operatorname{IsImage}$ applied to $F$ are a basic type.

the copy of m and e (from the name)

Let $\mathrm{hF}$ be an element of $\operatorname{IsImage}$ applied to $F$. Let $m$ be a homomorphism of $\operatorname{I}$ applied to $F$ and $Y$. Let $e$ be a homomorphism of $X$ and $\operatorname{I}$ applied to $F$. Assume that $\mathrm{autoParam}$ holds for $\EqtMACRoH {m}{\operatorname{m} (F)}$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsImage\_\_copy\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for $\EqtMACRoH {e}{\operatorname{e} (F)}$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsImage\_\_copy\_\_\_auto\_3}$. Then the copy of $m$ and $e$ is an element of $\operatorname{IsImage}$ applied to the copy of $m$ and $e$.

the isomorphism extension of hF and #2 (from the name)

Let $\mathrm{hF}$ be an element of $\operatorname{IsImage}$ applied to $F$. Let $\mathrm{hF'}$ be an element of $\operatorname{IsImage}$ applied to $\mathrm{F'}$. Then the isomorphism extension of $\mathrm{hF}$ and $\mathrm{hF'}$ is an isomorphism of $\operatorname{I}$ applied to $F$ and $\operatorname{I}$ applied to $\mathrm{F'}$.

the lift of self and #2 (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{IsImage}$ applied to $F$. Let $\mathrm{F'}$ be a monomorphism factorisation of $f$. Then the lift of $\mathrm{self}$ and $\mathrm{F'}$ is a homomorphism of $\operatorname{I}$ applied to $F$ and $\operatorname{I}$ applied to $\mathrm{F'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $\mathrm{F'}$.

Let $\mathrm{hF}$ be an element of $\operatorname{IsImage}$ applied to $F$. Let $\mathrm{sq}$ be a homomorphism of $f$ and $g$. Then $\operatorname{ofArrowIso}$ applied to $\mathrm{hF}$ and $\mathrm{sq}$ is an element of $\operatorname{IsImage}$ applied to the monomorphism factorisation of $F$ and $\mathrm{sq}$.

Let $\mathrm{hF}$ be an element of $\operatorname{IsImage}$ applied to $F$. Let $e$ be an isomorphism of $\operatorname{I}$ applied to $F$ and $\mathrm{I'}$. Then $\operatorname{ofIsoI}$ applied to $\mathrm{hF}$ and $e$ is an element of $\operatorname{IsImage}$ applied to the monomorphism factorisation of $F$ and $e$.

the self of f (from the name)

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

monomorphism factorisation of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the monomorphism factorisations of $f$ are a basic type.

Let $\mathrm{self}$ be a monomorphism factorisation of $f$. Then $\operatorname{I}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the composition monomorphism of F and g (from the name)

Let $F$ be a monomorphism factorisation of $f$. Let $g$ be a homomorphism of $Y$ and $\mathrm{Y'}$. Then the composition monomorphism of $F$ and $g$ is a monomorphism factorisation of the composition of $f$ and $g$.

the copy of m and e (from the name)

Let $F$ be a monomorphism factorisation of $f$. Let $m$ be a homomorphism of $\operatorname{I}$ applied to $F$ and $Y$. Let $e$ be a homomorphism of $X$ and $\operatorname{I}$ applied to $F$. Assume that $\mathrm{autoParam}$ holds for $\EqtMACRoH {m}{\operatorname{m} (F)}$ and $\mathrm{CategoryTheory\_\_Limits\_\_MonoFactorisation\_\_copy\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for $\EqtMACRoH {e}{\operatorname{e} (F)}$ and $\mathrm{CategoryTheory\_\_Limits\_\_MonoFactorisation\_\_copy\_\_\_auto\_3}$. Then the copy of $m$ and $e$ is a monomorphism factorisation of $f$.

Let $\mathrm{self}$ be a monomorphism factorisation of $f$. Then $\operatorname{e}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $\operatorname{I}$ applied to $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the isomorphism composition of F and g (from the name)

Let $F$ be a monomorphism factorisation of $f$. Let $g$ be a homomorphism of $\mathrm{X'}$ and $X$. Then the isomorphism composition of $F$ and $g$ is a monomorphism factorisation of the composition of $g$ and $f$.

Let $\mathrm{self}$ be a monomorphism factorisation of $f$. Then $\operatorname{m}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{I}$ applied to $\mathrm{self}$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the monomorphism factorisation of F and sq (from the name)

Let $F$ be a monomorphism factorisation of the homomorphism of $f$. Let $\mathrm{sq}$ be a homomorphism of $f$ and $g$. Then the monomorphism factorisation of $F$ and $\mathrm{sq}$ is a monomorphism factorisation of the homomorphism of $g$.

the monomorphism factorisation of F (from the name)

Let $F$ be a monomorphism factorisation of the composition of $f$ and $g$. Then the monomorphism factorisation of $F$ is a monomorphism factorisation of $f$.

the monomorphism factorisation of g and F (from the name)

Let $g$ be a homomorphism of $\mathrm{X'}$ and $X$. Let $F$ be a monomorphism factorisation of the composition of $g$ and $f$. Then the monomorphism factorisation of $g$ and $F$ is a monomorphism factorisation of $f$.

the monomorphism factorisation of F and e (from the name)

Let $F$ be a monomorphism factorisation of $f$. Let $e$ be an isomorphism of $\operatorname{I}$ applied to $F$ and $\mathrm{I'}$. Then the monomorphism factorisation of $F$ and $e$ is a monomorphism factorisation of $f$.

the self of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the self of $f$ is a monomorphism factorisation of $f$.

strong epimorphism monomorphism factorisation of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the strong epimorphism monomorphism factorisations of $f$ are a basic type.

Let $F$ be a strong epimorphism monomorphism factorisation of $f$. Then $\operatorname{toMonoIsImage}$ applied to $F$ is an element of $\operatorname{IsImage}$ applied to $\operatorname{toMonoFactorisation}$ applied to $F$.

the map from the source to the image of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map from the source to the image of $f$ is a homomorphism of $X$ and the categorical image of $f$ defined as $\operatorname{e}$ applied to the monomorphism factorisation of $f$.

the functorial epimorphism monomorphism factorization data of C (from the name)

Let $C$ be a set. Then the functorial epimorphism monomorphism factorization data of $C$ is a functorial factorization data of the epimorphism of $C$ and the monomorphism of $C$.

the imaginary part (from the name)

The imaginary part is a functor of the set of arrows of $C$ and $C$.

the categorical image of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the categorical image of $f$ is an element of $C$ defined as $\operatorname{I}$ applied to the monomorphism factorisation of $f$.

the composition isomorphism 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 isomorphism of $f$ and $g$ is an isomorphism of the categorical image of $f$ and the categorical image of the composition of $f$ and $g$.

Assume that $\EqtMACRoH {f}{\mathrm{f'}}$. Then $\operatorname{eqToHom}$ applied to $h_{2}$ is a homomorphism of the categorical image of $f$ and the categorical image of $\mathrm{f'}$.

Assume that $\EqtMACRoH {f}{\mathrm{f'}}$. Then $\operatorname{eqToIso}$ applied to $h_{2}$ is an isomorphism of the categorical image of $f$ and the categorical image of $\mathrm{f'}$ defined as $\operatorname{asIso}$ applied to $\operatorname{eqToHom}$ applied to $h_{2}$.

the isomorphism strong epimorphism monomorphism of e and m (from the name)

Let $e$ be a homomorphism of $X$ and $\mathrm{I'}$. Let $m$ be a homomorphism of $\mathrm{I'}$ and $Y$ such that the composition of $e$ and $m$ is equal to $f$. Then the isomorphism strong epimorphism monomorphism of $e$ and $m$ is an isomorphism of $\mathrm{I'}$ and the categorical image of $f$.

the lift of #1 (from the name)

Let $\mathrm{F'}$ be a monomorphism factorisation of $f$. Then the lift of $\mathrm{F'}$ is a homomorphism of the categorical image of $f$ and $\operatorname{I}$ applied to $\mathrm{F'}$ defined as the lift of $\operatorname{isImage}$ applied to $f$ and $\mathrm{F'}$.

the map of sq (from the name)

Let $\mathrm{sq}$ be a homomorphism of $f$ and $g$. Then the map of $\mathrm{sq}$ is a homomorphism of the categorical image of the homomorphism of $f$ and the categorical image of the homomorphism of $g$ defined as the map of the image map of $\mathrm{sq}$.

the comparison map of f and g (from the docstring)

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

the inclusion of the image of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the inclusion of the image of $f$ is a homomorphism of the categorical image of $f$ and $Y$ defined as $\operatorname{m}$ applied to the monomorphism factorisation of $f$.

the image map composition of sq and #2 (from the name)

Let $\mathrm{sq}$ be a homomorphism of $f$ and $g$. Let $\mathrm{sq'}$ be a homomorphism of $g$ and $h_{3}$. Then the image map composition of $\mathrm{sq}$ and $\mathrm{sq'}$ is an image map of the composition of $\mathrm{sq}$ and $\mathrm{sq'}$.

the identity of f (from the docstring)

Let $f$ be an arrow of $C$. Then the identity of $f$ is an image map of the identity morphism of $f$.

the image of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the image of $f$ is an isomorphism of the categorical image of $f$ and $X$ defined as the isomorphism extension of $\operatorname{isImage}$ applied to $f$ and the self of $f$.

Let $C$ be a set. Let $\mathrm{hX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Then $\operatorname{isInitialConst}$ applied to $C$ and $\mathrm{hX}$ is an element of $\operatorname{IsInitial}$ applied to the action of the constant of $C$ and $X$.

Let $C$ be a set. Let $\mathrm{hX}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then $\operatorname{isTerminalConst}$ applied to $C$ and $\mathrm{hX}$ is an element of $\operatorname{IsTerminal}$ applied to the action of the constant of $C$ and $X$.

C is a initial monomorphism class (from the name)

Let $C$ be a set. Then we can say that $C$ is an initial monomorphism class.

Let $X$ be an element of $C$. Then an element of $\operatorname{IsInitial}$ applied to $X$ is an element of the function that maps $X$ to $\operatorname{IsColimit}$ applied to $\operatorname{asEmptyCocone}$ applied to $X$.

the equivalence of e (from the name)

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

Let $\mathrm{hY}$ be an element of $\operatorname{IsInitial}$ applied to $Y$. Let $i$ be an isomorphism of $Y$ and $Z$. Then $\operatorname{ofIso}$ applied to $\mathrm{hY}$ and $i$ is an element of $\operatorname{IsInitial}$ applied to $Z$.

Let $X$ be an element of $C$. Then $\operatorname{ofUnique}$ applied to $X$ is an element of $\operatorname{IsInitial}$ applied to $X$.

Let $h$ be a function from elements $Y_{1}$ of $C$ to homomorphisms of $X$ and $Y_{1}$ such that for all elements $Y$ of $C$, for all homomorphisms $m$ of $X$ and $Y$, $\EqtMACRoH {m}{h (Y)}$. Then $\operatorname{ofUniqueHom}$ applied to $Y_{1}$, $h$ and $\mathrm{uniq}$ is an element of $\operatorname{IsInitial}$ applied to $X$ defined as the function that maps $\mathrm{uniq}$ to $\operatorname{ofUnique}$ applied to $X$ and $\mathrm{uniq}$.

the opposite of C and hX (from the name)

Let $C$ be a set. Let $\mathrm{hX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Then the opposite of $C$ and $\mathrm{hX}$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{op}$ applied to $X$.

Let $t$ be an element of $\operatorname{IsInitial}$ applied to $X$. Let $Y$ be an element of $C$. Then $\operatorname{to}$ applied to $t$ and $Y$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{desc}$ applied to $t$ and $\operatorname{asEmptyCocone}$ applied to $Y$.

Let $\mathrm{hT}$ be an element of $\operatorname{IsInitial}$ applied to $T$. Let $\mathrm{hT'}$ be an element of $\operatorname{IsInitial}$ applied to $\mathrm{T'}$. Then $\operatorname{uniqueUpToIso}$ applied to $\mathrm{hT}$ and $\mathrm{hT'}$ is an isomorphism of $T$ and $\mathrm{T'}$.

the opposite of C and hX (from the name)

Let $C$ be a set. Let $\mathrm{hX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Then the opposite of $C$ and $\mathrm{hX}$ is an element of $\operatorname{IsTerminal}$ applied to the opposite of $X$.

Let $X$ be an element of $C$. Then an element of $\operatorname{IsTerminal}$ applied to $X$ is an element of the function that maps $X$ to $\operatorname{IsLimit}$ applied to $\operatorname{asEmptyCone}$ applied to $X$.

the equivalence of e (from the name)

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

Let $t$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Let $Y$ be an element of $C$. Then $\operatorname{from}$ applied to $t$ and $Y$ is a homomorphism of $Y$ and $X$ defined as the lift of $t$ and $\operatorname{asEmptyCone}$ applied to $Y$.

Let $\mathrm{hY}$ be an element of $\operatorname{IsTerminal}$ applied to $Y$. Let $i$ be an isomorphism of $Y$ and $Z$. Then $\operatorname{ofIso}$ applied to $\mathrm{hY}$ and $i$ is an element of $\operatorname{IsTerminal}$ applied to $Z$.

Let $X$ be an element of $C$. Then $\operatorname{ofUnique}$ applied to $X$ is an element of $\operatorname{IsTerminal}$ applied to $X$.

Let $h$ be a function from elements $Y_{1}$ of $C$ to homomorphisms of $Y_{1}$ and $X$ such that for all elements $Y$ of $C$, for all homomorphisms $m$ of $Y$ and $X$, $\EqtMACRoH {m}{h (Y)}$. Then $\operatorname{ofUniqueHom}$ applied to $Y_{1}$, $h$ and $\mathrm{uniq}$ is an element of $\operatorname{IsTerminal}$ applied to $X$ defined as the function that maps $\mathrm{uniq}$ to $\operatorname{ofUnique}$ applied to $X$ and $\mathrm{uniq}$.

the opposite of C and hX (from the name)

Let $C$ be a set. Let $\mathrm{hX}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then the opposite of $C$ and $\mathrm{hX}$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{op}$ applied to $X$.

Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Let $\mathrm{hT'}$ be an element of $\operatorname{IsTerminal}$ applied to $\mathrm{T'}$. Then $\operatorname{uniqueUpToIso}$ applied to $\mathrm{hT}$ and $\mathrm{hT'}$ is an isomorphism of $T$ and $\mathrm{T'}$.

the opposite of C and hX (from the name)

Let $C$ be a set. Let $\mathrm{hX}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then the opposite of $C$ and $\mathrm{hX}$ is an element of $\operatorname{IsInitial}$ applied to the opposite of $X$.

Let $X$ be an element of $C$. Then $\operatorname{asEmptyCocone}$ applied to $X$ is a cocone of $\operatorname{empty}$ applied to $C$.

Let $X$ be an element of $C$. Then $\operatorname{asEmptyCone}$ applied to $X$ is a cone of $\operatorname{empty}$ applied to $C$.

the cocone of hX and F (from the name)

Let $\mathrm{hX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Let $F$ be a functor of $J$ and $C$. Then the cocone of $\mathrm{hX}$ and $F$ is a cocone of $F$.

the cocone of tX and F (from the name)

Let $\mathrm{tX}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Let $F$ be a functor of $J$ and $C$. Then the cocone of $\mathrm{tX}$ and $F$ is a cocone of $F$.

the colimit of hX and F (from the name)

Let $\mathrm{hX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Let $F$ be a functor of $J$ and $C$. Then the colimit of $\mathrm{hX}$ and $F$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $\mathrm{hX}$ and $F$.

the colimit of tX and F (from the name)

Let $\mathrm{tX}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Let $F$ be a functor of $J$ and $C$. Then the colimit of $\mathrm{tX}$ and $F$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $\mathrm{tX}$ and $F$.

the cone of tX and F (from the name)

Let $\mathrm{tX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Let $F$ be a functor of $J$ and $C$. Then the cone of $\mathrm{tX}$ and $F$ is a cone of $F$.

the cone of hX and F (from the name)

Let $\mathrm{hX}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Let $F$ be a functor of $J$ and $C$. Then the cone of $\mathrm{hX}$ and $F$ is a cone of $F$.

the initial opposite of t (from the name)

Let $t$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then the initial opposite of $t$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{op}$ applied to $X$.

the initial opposite of t (from the name)

Let $t$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then the initial opposite of $t$ is an element of $\operatorname{IsInitial}$ applied to the opposite of $X$.

Let $C$ be a set. Let $\mathrm{hl}$ be an element of $\operatorname{IsColimit}$ applied to $x_{3}$. Let $x_{4}$ be a cocone of $x_{2}$. Let $\mathrm{hi}$ be an isomorphism of $\operatorname{pt}$ applied to $x_{3}$ and $\operatorname{pt}$ applied to $x_{4}$. Then $\operatorname{isColimitChangeEmptyCocone}$ applied to $C$, $\mathrm{hl}$, $x_{4}$ and $\mathrm{hi}$ is an element of $\operatorname{IsColimit}$ applied to $x_{4}$.

Let $C$ be a set. Let $x_{3}$ be a cocone of $x_{1}$. Let $x_{4}$ be a cocone of $x_{2}$. Let $h$ be an isomorphism of $\operatorname{pt}$ applied to $x_{3}$ and $\operatorname{pt}$ applied to $x_{4}$. Then $\operatorname{isColimitEmptyCoconeEquiv}$ applied to $C$, $x_{3}$, $x_{4}$ and $h$ is an element of $\EquivMACRoAE {\operatorname{IsColimit} (x_{3})}{\operatorname{IsColimit} (x_{4})}$.

Let $C$ be a set. Let $c$ be a cocone of $F$. Then $\operatorname{isColimitEquivIsInitialOfIsEmpty}$ applied to $C$ and $c$ is an element of $\EquivMACRoAE {\operatorname{IsColimit} (c)}{\operatorname{IsInitial} (\operatorname{pt} (c))}$ defined as the composition of the whisker equivalence equivalence of the equivalence of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $J$ and $\operatorname{isColimitEmptyCoconeEquiv}$ applied to $C$, the whisker of the functor of the equivalence of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $J$ and $c$, $\operatorname{asEmptyCocone}$ applied to $\operatorname{pt}$ applied to $c$ and the identity of $\operatorname{pt}$ applied to the whisker of the functor of the equivalence of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $J$ and $c$.

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

Let $F$ be a functor of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $C$. Let $Y$ be an element of $C$. Then $\operatorname{isInitialEquivUnique}$ applied to $F$ and $Y$ is an equivalence from $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $Y$ and $\operatorname{mk}$ applied to the function that maps $X$ to $\mathrm{id}$ applied to $\operatorname{casesOn}$ applied to $X$ and the function that maps $\mathrm{as}$ to $\mathrm{falseE}$ applied to the set of homomorphisms of the action of $F$ and $\operatorname{mk}$ applied to $\mathrm{as}$ and $Y$ and $\mathrm{Aesop\_\_BuiltinRules\_\_pEmpty\_false}$ applied to $\mathrm{as}$ and $\mathrm{CategoryTheory\_\_NatTrans\_\_mk\_\_\_proof\_2}$ applied to the function that maps $X_{1}$ to $\mathrm{id}$ applied to $\operatorname{casesOn}$ applied to $X_{1}$ and the function that maps $\mathrm{as1}$ to $\mathrm{falseE}$ applied to the set of homomorphisms of the action of $F$ and $\operatorname{mk}$ applied to $\mathrm{as1}$ and $Y$ and $\mathrm{Aesop\_\_BuiltinRules\_\_pEmpty\_false}$ applied to $\mathrm{as1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_isInitialEquivUnique\_\_\_proof\_2}$ applied to $F$ and $Y$ to the set of functions from elements $X_{2}$ of $C$ to elements of $\mathrm{Unique}$ applied to the set of homomorphisms of $Y$ and $X_{2}$.

Let $C$ be a set. Let $\mathrm{hl}$ be an element of $\operatorname{IsLimit}$ applied to $x_{3}$. Let $x_{4}$ be a cone of $x_{2}$. Let $\mathrm{hi}$ be an isomorphism of $\operatorname{pt}$ applied to $x_{3}$ and $\operatorname{pt}$ applied to $x_{4}$. Then $\operatorname{isLimitChangeEmptyCone}$ applied to $C$, $\mathrm{hl}$, $x_{4}$ and $\mathrm{hi}$ is an element of $\operatorname{IsLimit}$ applied to $x_{4}$.

Let $C$ be a set. Let $x_{3}$ be a cone of $x_{1}$. Let $x_{4}$ be a cone of $x_{2}$. Let $h$ be an isomorphism of $\operatorname{pt}$ applied to $x_{3}$ and $\operatorname{pt}$ applied to $x_{4}$. Then $\operatorname{isLimitEmptyConeEquiv}$ applied to $C$, $x_{3}$, $x_{4}$ and $h$ is an element of $\EquivMACRoAE {\operatorname{IsLimit} (x_{3})}{\operatorname{IsLimit} (x_{4})}$.

Let $C$ be a set. Let $c$ be a cone of $F$. Then $\operatorname{isLimitEquivIsTerminalOfIsEmpty}$ applied to $C$ and $c$ is an element of $\EquivMACRoAE {\operatorname{IsLimit} (c)}{\operatorname{IsTerminal} (\operatorname{pt} (c))}$ defined as the composition of the whisker equivalence equivalence of the equivalence of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $J$ and $\operatorname{isLimitEmptyConeEquiv}$ applied to $C$, the whisker of the functor of the equivalence of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $J$ and $c$, $\operatorname{asEmptyCone}$ applied to $\operatorname{pt}$ applied to $c$ and the identity of $\operatorname{pt}$ applied to the whisker of the functor of the equivalence of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $J$ and $c$.

Let $F$ be a functor of $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $C$. Let $Y$ be an element of $C$. Then $\operatorname{isTerminalEquivUnique}$ applied to $F$ and $Y$ is an equivalence from $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $Y$ and $\operatorname{mk}$ applied to the function that maps $X$ to $\mathrm{id}$ applied to $\operatorname{casesOn}$ applied to $X$ and the function that maps $\mathrm{as}$ to $\mathrm{falseE}$ applied to the set of homomorphisms of $Y$ and the action of $F$ and $\operatorname{mk}$ applied to $\mathrm{as}$ and $\mathrm{Aesop\_\_BuiltinRules\_\_pEmpty\_false}$ applied to $\mathrm{as}$ and $\mathrm{CategoryTheory\_\_Limits\_\_isTerminalEquivUnique\_\_\_proof\_2}$ applied to $F$ and $Y$ to the set of functions from elements $X_{1}$ of $C$ to elements of $\mathrm{Unique}$ applied to the set of homomorphisms of $X_{1}$ and $Y$.

$\operatorname{isTerminalTop}$ is an element of $\operatorname{IsTerminal}$ applied to the top defined as $\operatorname{ofUnique}$ applied to the top.

the limit of tX and F (from the name)

Let $\mathrm{tX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Let $F$ be a functor of $J$ and $C$. Then the limit of $\mathrm{tX}$ and $F$ is an element of $\operatorname{IsLimit}$ applied to the cone of $\mathrm{tX}$ and $F$.

the limit of hX and F (from the name)

Let $\mathrm{hX}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Let $F$ be a functor of $J$ and $C$. Then the limit of $\mathrm{hX}$ and $F$ is an element of $\operatorname{IsLimit}$ applied to the cone of $\mathrm{hX}$ and $F$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $a$ and $b$ be homomorphisms of $R$ and $X$. Then $\operatorname{IsKernelPair}$ holds for $f$, $a$ and $b$, if $\operatorname{IsPullback}$ holds for $a$, $b$, $f$ and $f$.

the lift of p and q (from the name)

Assume that $\operatorname{IsKernelPair}$ holds for $f$, $a$ and $b$. Let $p$ and $q$ be homomorphisms of $S$ and $X$ such that the composition of $p$ and $f$ is equal to the composition of $q$ and $f$. Then the lift of $p$ and $q$ is a homomorphism of $S$ and $R$ defined as the lift of $p$ and $q$.

the lift of p and q (from the name)

Assume that $\operatorname{IsKernelPair}$ holds for $f$, $a$ and $b$. Let $p$ and $q$ be homomorphisms of $S$ and $X$ such that $\EqtMACRoH {\operatorname{comp} (p , f)}{\operatorname{comp} (q , f)}$. Then the lift of $p$ and $q$ is an element of $\SubtypeSet {t}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (t , a)}{p}, \EqtMACRoH {\operatorname{comp} (t , b)}{q})}$ defined as the lift of $p$ and $q$.

the coequalizer of k and r (from the name)

Assume that $\operatorname{IsKernelPair}$ holds for $f$, $a$ and $b$. Let $r$ be a regular epimorphism of $f$. Then the coequalizer of $k$ and $r$ is an element of $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{w}$ applied to $\operatorname{toCommSq}$ applied to $k$.

the coequalizer of k (from the name)

Assume that $\operatorname{IsKernelPair}$ holds for $f$, $a$ and $b$. Then the coequalizer of $k$ is an element of $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{w}$ applied to $\operatorname{toCommSq}$ applied to $k$ defined as the coequalizer of $k$ and $\operatorname{getStruct}$ applied to $f$.

cokernel cofork of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then a cokernel cofork of $f$ is an element of the function that maps $f$ to the set of coforks of $f$ and $0$.

Let $\mathrm{hs}$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $k$ be a homomorphism of $Y$ and $W$ such that $\EqtMACRoH {\operatorname{comp} (f , k)}{0}$. Then $\operatorname{desc'}$ applied to $\mathrm{hs}$, $k$ and $h$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_\_u3c0\_} (s), l)}{k})}$ defined as $\operatorname{desc}$ applied to $\mathrm{hs}$ and the projection of $k$ and $h$.

Let $c$ be a cokernel cofork of $f$. Assume that $f$ is an epimorphism. Assume that $\operatorname{pt}$ applied to $c$ is a zero. Then $\operatorname{ofEpiOfIsZero}$ applied to $c$, $\mathrm{hf}$ and $h$ is an element of $\operatorname{IsColimit}$ applied to $c$.

Let $f$ be a homomorphism of $X$ and $Y$ such that $\EqtMACRoH {f}{0}$. Then $\operatorname{ofId}$ applied to $f$ and $\mathrm{hf}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the identity morphism of $Y$ and $\mathrm{CategoryTheory\_\_Limits\_\_CokernelCofork\_\_IsColimit\_\_ofId\_\_\_proof\_1}$ applied to $f$ and $\mathrm{hf}$.

the projection of g and desc (from the name)

Let $g$ be a homomorphism of $Y$ and $Z$ such that the composition of $f$ and $g$ is equal to $0$. Let $\mathrm{desc}$ be a function from elements $\mathrm{Z'2}$ of $C$ and homomorphisms $\mathrm{g'2}$ of $Y$ and $\mathrm{Z'2}$ and elements of $\mathrm{Proof}$ applied to the proposition that the composition of $f$ and $\mathrm{g'2}$ is equal to $0$ to homomorphisms of $Z$ and $\mathrm{Z'2}$ such that for all elements $\mathrm{Z'1}$ of $C$, for all homomorphisms $\mathrm{g'1}$ of $Y$ and $\mathrm{Z'1}$, for all elements $\mathrm{eq'1}$ of $\mathrm{Proof}$ applied to the proposition that the composition of $f$ and $\mathrm{g'1}$ is equal to $0$, the composition of $g$ and $\mathrm{desc}$ applied to $\mathrm{Z'1}$, $\mathrm{g'1}$ and $\mathrm{eq'1}$ is equal to $\mathrm{g'1}$ and for all elements $\mathrm{Z'}$ of $C$, for all homomorphisms $\mathrm{g'}$ of $Y$ and $\mathrm{Z'}$, for all elements $\mathrm{eq'}$ of $\mathrm{Proof}$ applied to the proposition that the composition of $f$ and $\mathrm{g'}$ is equal to $0$, for all homomorphisms $m$ of $Z$ and $\mathrm{Z'}$, if the composition of $g$ and $m$ is equal to $\mathrm{g'}$, then $\EqtMACRoH {m}{\mathrm{desc} (\mathrm{Z'} , \mathrm{g'} , \mathrm{eq'})}$. Then the projection of $g$ and $\mathrm{Z'2}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $g$ and $\mathrm{eq}$.

the projection of p and h (from the name)

Let $p$ be a homomorphism of $Y$ and $Q$ such that $\EqtMACRoH {\operatorname{comp} (f , p)}{0}$. Let $h$ be a function from elements $A$ of $C$ and homomorphisms $k$ of $Y$ and $A$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{comp} (f , k)}{0}$ to elements of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (p , l)}{k})}$. Then the projection of $p$ and $A$ is an element of $\operatorname{IsColimit}$ applied to the projection of $p$ and $w$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{f'}$ be a homomorphism of $\mathrm{X'}$ and $\mathrm{Y'}$. Let $e$ be an isomorphism of $\mathrm{Y'}$ and $Y$ such that for all elements $W$ of $C$, for all homomorphisms $x_{2}$ of $Y$ and $W$, the composition of $f$ and $x_{2}$ is equal to $0$, if and only if the composition of $\mathrm{f'}$ and the composition of the homomorphism of $e$ and $x_{2}$ is equal to $0$. Then $\operatorname{isColimitOfIsColimitOfIff}$ applied to $\mathrm{hc}$, $\mathrm{f'}$, $e$ and $\mathrm{iff}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the composition of the homomorphism of $e$ and the projection of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_CokernelCofork\_\_isColimitOfIsColimitOfIff\_\_\_proof\_1}$ applied to $\mathrm{f'}$, $e$ and $\mathrm{iff}$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{f'}$ be a homomorphism of $\mathrm{X'}$ and $Y$ such that for all elements $W$ of $C$, for all homomorphisms $x_{2}$ of $Y$ and $W$, the composition of $f$ and $x_{2}$ is equal to $0$, if and only if the composition of $\mathrm{f'}$ and $x_{2}$ is equal to $0$. Then $\operatorname{isColimitOfIsColimitOfIff'}$ applied to $\mathrm{hc}$, $\mathrm{f'}$ and $\mathrm{iff}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_CokernelCofork\_\_isColimitOfIsColimitOfIff'\_\_\_proof\_1}$ applied to $\mathrm{f'}$ and $\mathrm{iff}$.

the map isomorphism of x2 and #3 (from the name)

Let $\mathrm{hf}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Let $\mathrm{hf'}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc'}$. Let $x_{2}$ be an isomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $\mathrm{f'}$. Then the map isomorphism of $\mathrm{hf'}$ and $x_{2}$ is an isomorphism of $\operatorname{pt}$ applied to $\mathrm{cc}$ and $\operatorname{pt}$ applied to $\mathrm{cc'}$.

the map of x2 and #3 (from the name)

Let $\mathrm{hf}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cc}$. Let $\mathrm{cc'}$ be a cokernel cofork of $\mathrm{f'}$. Let $x_{2}$ be a homomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $\mathrm{f'}$. Then the map of $\mathrm{cc'}$ and $x_{2}$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{cc}$ and $\operatorname{pt}$ applied to $\mathrm{cc'}$.

the projection of x2 and w (from the name)

Let $x_{2}$ be a homomorphism of $Y$ and $Z$ such that the composition of $f$ and $x_{2}$ is equal to $0$. Then the projection of $x_{2}$ and $w$ is a cokernel cofork of $f$.

f has cokernels (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then $f$ has cokernels, if the parallel pair of $f$ and $0$ has colimits.

C has cokernels (from the name)

Let $C$ be a set. Then we can say that $C$ has cokernels.

f has kernels (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then $f$ has kernels, if the parallel pair of $f$ and $0$ has limits.

C has kernels (from the name)

Let $C$ be a set. Then we can say that $C$ has kernels.

the cokernel isomorphism of hs and i (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $l$ be a homomorphism of $Y$ and $Z$. Let $\mathrm{hs}$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $i$ be an isomorphism of $\operatorname{pt}$ applied to $s$ and $Z$ such that the composition of the projection of $s$ and the homomorphism of $i$ is equal to $l$. Then the cokernel isomorphism of $\mathrm{hs}$ and $i$ is an element of $\operatorname{IsColimit}$ applied to the projection of $l$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsCokernel\_\_cokernelIso\_\_\_proof\_1}$ applied to $f$, $l$, $i$ and $h$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $\mathrm{hs}$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $\mathrm{s'}$ be a cokernel cofork of $\mathrm{f'}$. Let $\mathrm{eX}$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $\mathrm{eY}$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $\mathrm{s'}$. Assume that the composition of the homomorphism of $\mathrm{eX}$ and $\mathrm{f'}$ is equal to the composition of $f$ and the homomorphism of $\mathrm{eY}$. Assume that the composition of the homomorphism of $\mathrm{eY}$ and the projection of $\mathrm{s'}$ is equal to the composition of the projection of $s$ and the homomorphism of $e$. Then $\operatorname{ofIso}$ applied to $f$, $\mathrm{hs}$, $\mathrm{s'}$, $\mathrm{eX}$, $\mathrm{eY}$, $e$, $H$ and $\mathrm{H'}$ is an element of $\operatorname{IsColimit}$ applied to $\mathrm{s'}$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $l$ be a homomorphism of $Z$ and $Y$. Let $i$ be an isomorphism of $X$ and $Z$ such that the composition of the homomorphism of $i$ and $l$ is equal to $f$. Let $\mathrm{hs}$ be an element of $\operatorname{IsColimit}$ applied to $s$. Then $\operatorname{ofIsoComp}$ applied to $f$, $l$, $i$, $h$ and $\mathrm{hs}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $s$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsCokernel\_\_ofIsoComp\_\_\_proof\_1}$ applied to $f$, $l$, $i$ and $h$.

the isomorphism kernel of hs and i (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $l$ be a homomorphism of $Z$ and $X$. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $i$ be an isomorphism of $Z$ and $\operatorname{pt}$ applied to $s$ such that the composition of the homomorphism of $i$ and the inclusion of $s$ is equal to $l$. Then the isomorphism kernel of $\mathrm{hs}$ and $i$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $l$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsKernel\_\_isoKernel\_\_\_proof\_1}$ applied to $f$, $l$, $i$ and $h$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $l$ be a homomorphism of $X$ and $Z$. Let $i$ be an isomorphism of $Z$ and $Y$ such that the composition of $l$ and the homomorphism of $i$ is equal to $f$. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then $\operatorname{ofCompIso}$ applied to $f$, $l$, $i$, $h$ and $\mathrm{hs}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $s$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsKernel\_\_ofCompIso\_\_\_proof\_1}$ applied to $f$, $l$, $i$ and $h$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $\mathrm{s'}$ be a kernel fork of $\mathrm{f'}$. Let $\mathrm{eX}$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $\mathrm{eY}$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $\mathrm{s'}$. Assume that the composition of the homomorphism of $\mathrm{eX}$ and $\mathrm{f'}$ is equal to the composition of $f$ and the homomorphism of $\mathrm{eY}$. Assume that the composition of the homomorphism of $e$ and the inclusion of $\mathrm{s'}$ is equal to the composition of the inclusion of $s$ and the homomorphism of $\mathrm{eX}$. Then $\operatorname{ofIso}$ applied to $f$, $\mathrm{hs}$, $\mathrm{s'}$, $\mathrm{eX}$, $\mathrm{eY}$, $e$, $H$ and $\mathrm{H'}$ is an element of $\operatorname{IsLimit}$ applied to $\mathrm{s'}$.

kernel fork of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then a kernel fork of $f$ is an element of the function that maps $f$ to the set of forks of $f$ and $0$.

the lift of hs and k (from the name)

Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $k$ be a homomorphism of $W$ and $X$ such that $\EqtMACRoH {\operatorname{comp} (k , f)}{0}$. Then the lift of $\mathrm{hs}$ and $k$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , \mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_\_u3b9\_} (s))}{k})}$ defined as the lift of $\mathrm{hs}$ and the inclusion of $k$ and $h$.

Let $f$ be a homomorphism of $X$ and $Y$ such that $\EqtMACRoH {f}{0}$. Then $\operatorname{ofId}$ applied to $f$ and $\mathrm{hf}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the identity morphism of $X$ and $\mathrm{CategoryTheory\_\_Limits\_\_KernelFork\_\_IsLimit\_\_ofId\_\_\_proof\_1}$ applied to $f$ and $\mathrm{hf}$.

Let $c$ be a kernel fork of $f$. Assume that $f$ is a monomorphism. Assume that $\operatorname{pt}$ applied to $c$ is a zero. Then $\operatorname{ofMonoOfIsZero}$ applied to $c$, $\mathrm{hf}$ and $h$ is an element of $\operatorname{IsLimit}$ applied to $c$.

the inclusion of g and lift (from the name)

Let $g$ be a homomorphism of $W$ and $X$ such that the composition of $g$ and $f$ is equal to $0$. Let $\mathrm{lift}$ be a function from elements $\mathrm{W'2}$ of $C$ and homomorphisms $\mathrm{g'2}$ of $\mathrm{W'2}$ and $X$ and elements of $\mathrm{Proof}$ applied to the proposition that the composition of $\mathrm{g'2}$ and $f$ is equal to $0$ to homomorphisms of $\mathrm{W'2}$ and $W$ such that for all elements $\mathrm{W'1}$ of $C$, for all homomorphisms $\mathrm{g'1}$ of $\mathrm{W'1}$ and $X$, for all elements $\mathrm{eq'1}$ of $\mathrm{Proof}$ applied to the proposition that the composition of $\mathrm{g'1}$ and $f$ is equal to $0$, the composition of $\mathrm{lift}$ applied to $\mathrm{W'1}$, $\mathrm{g'1}$ and $\mathrm{eq'1}$ and $g$ is equal to $\mathrm{g'1}$ and for all elements $\mathrm{W'}$ of $C$, for all homomorphisms $\mathrm{g'}$ of $\mathrm{W'}$ and $X$, for all elements $\mathrm{eq'}$ of $\mathrm{Proof}$ applied to the proposition that the composition of $\mathrm{g'}$ and $f$ is equal to $0$, for all homomorphisms $m$ of $\mathrm{W'}$ and $W$, if the composition of $m$ and $g$ is equal to $\mathrm{g'}$, then $\EqtMACRoH {m}{\mathrm{lift} (\mathrm{W'} , \mathrm{g'} , \mathrm{eq'})}$. Then the inclusion of $g$ and $\mathrm{W'2}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $g$ and $\mathrm{eq}$.

the inclusion of i and h (from the name)

Let $i$ be a homomorphism of $K$ and $X$ such that $\EqtMACRoH {\operatorname{comp} (i , f)}{0}$. Let $h$ be a function from elements $A$ of $C$ and homomorphisms $k$ of $A$ and $X$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{comp} (k , f)}{0}$ to elements of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , i)}{k})}$. Then the inclusion of $i$ and $A$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $i$ and $w$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{g'}$ be a homomorphism of $\mathrm{X'}$ and $\mathrm{Y'}$. Let $e$ be an isomorphism of $X$ and $\mathrm{X'}$ such that for all elements $W$ of $C$, for all homomorphisms $x_{2}$ of $W$ and $X$, the composition of $x_{2}$ and $g$ is equal to $0$, if and only if the composition of $x_{2}$ and the composition of the homomorphism of $e$ and $\mathrm{g'}$ is equal to $0$. Then $\operatorname{isLimitOfIsLimitOfIff}$ applied to $\mathrm{hc}$, $\mathrm{g'}$, $e$ and $\mathrm{iff}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the composition of the inclusion of $c$ and the homomorphism of $e$ and $\mathrm{CategoryTheory\_\_Limits\_\_KernelFork\_\_isLimitOfIsLimitOfIff\_\_\_proof\_1}$ applied to $\mathrm{g'}$, $e$ and $\mathrm{iff}$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{g'}$ be a homomorphism of $X$ and $\mathrm{Y'}$ such that for all elements $W$ of $C$, for all homomorphisms $x_{2}$ of $W$ and $X$, the composition of $x_{2}$ and $g$ is equal to $0$, if and only if the composition of $x_{2}$ and $\mathrm{g'}$ is equal to $0$. Then $\operatorname{isLimitOfIsLimitOfIff'}$ applied to $\mathrm{hc}$, $\mathrm{g'}$ and $\mathrm{iff}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_KernelFork\_\_isLimitOfIsLimitOfIff'\_\_\_proof\_1}$ applied to $\mathrm{g'}$ and $\mathrm{iff}$.

the map isomorphism of x2 and #3 (from the name)

Let $\mathrm{hf}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf}$. Let $\mathrm{hf'}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf'}$. Let $x_{2}$ be an isomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $\mathrm{f'}$. Then the map isomorphism of $\mathrm{hf'}$ and $x_{2}$ is an isomorphism of $\operatorname{pt}$ applied to $\mathrm{kf}$ and $\operatorname{pt}$ applied to $\mathrm{kf'}$.

the map of x2 and #3 (from the name)

Let $\mathrm{kf}$ be a kernel fork of $f$. Let $\mathrm{hf'}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{kf'}$. Let $x_{2}$ be a homomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $\mathrm{f'}$. Then the map of $\mathrm{hf'}$ and $x_{2}$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{kf}$ and $\operatorname{pt}$ applied to $\mathrm{kf'}$.

the inclusion of x2 and w (from the name)

Let $x_{2}$ be a homomorphism of $Z$ and $X$ such that the composition of $x_{2}$ and $f$ is equal to $0$. Then the inclusion of $x_{2}$ and $w$ is a kernel fork of $f$.

the cokernel of C (from the docstring)

Let $C$ be a set. Then the cokernel of $C$ is a functor of the set of arrows of $C$ and $C$.

the cokernel projection of C (from the docstring)

Let $C$ be a set. Then the cokernel projection of $C$ is a homomorphism of the right function and the cokernel of $C$.

the cokernel of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the cokernel of $f$ is an element of $C$ defined as the coequalizer of $f$ and $0$.

the cokernel isomorphism of l and i (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $l$ be a homomorphism of $Y$ and $Z$. Let $i$ be an isomorphism of the cokernel of $f$ and $Z$ such that the composition of the projection of $f$ and the homomorphism of $i$ is equal to $l$. Then the cokernel isomorphism of $l$ and $i$ is an element of $\operatorname{IsColimit}$ applied to the projection of $l$ and $\mathrm{CategoryTheory\_\_Limits\_\_cokernel\_\_cokernelIso\_\_\_proof\_1}$ applied to $f$, $l$, $i$ and $h_{1}$ defined as the cokernel isomorphism of $\operatorname{isColimit}$ applied to the parallel pair of $f$ and $0$ and $i$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $k$ be a homomorphism of $Y$ and $W$ such that the composition of $f$ and $k$ is equal to $0$. Then $\operatorname{desc}$ applied to $f$, $k$ and $h_{1}$ is a homomorphism of the cokernel of $f$ and $W$ defined as $\operatorname{desc}$ applied to $\operatorname{cokernelIsCokernel}$ applied to $f$ and the projection of $k$ and $h_{1}$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $k$ be a homomorphism of $Y$ and $W$ such that $\EqtMACRoH {\operatorname{comp} (f , k)}{0}$. Then $\operatorname{desc'}$ applied to $f$, $k$ and $h_{1}$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (\mathrm{CategoryTheory\_\_Limits\_\_cokernel\_\_\_u3c0\_} (f), l)}{k})}$ defined as $\operatorname{desc}$ applied to $f$, $k$ and $h_{1}$.

the morphism to the zero object of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the morphism to the zero object of $f$ is an element of $\operatorname{IsColimit}$ applied to the zero cokernel cofork of $f$.

the map of q and w (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $\mathrm{f'}$ be a homomorphism of $\mathrm{X'}$ and $\mathrm{Y'}$. Let $p$ be a homomorphism of $X$ and $\mathrm{X'}$. Let $q$ be a homomorphism of $Y$ and $\mathrm{Y'}$ such that the composition of $f$ and $q$ is equal to the composition of $p$ and $\mathrm{f'}$. Then the map of $p$ and $q$ is a homomorphism of the cokernel of $f$ and the cokernel of $\mathrm{f'}$.

the map isomorphism of q and w (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $\mathrm{f'}$ be a homomorphism of $\mathrm{X'}$ and $\mathrm{Y'}$. Let $p$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $q$ be an isomorphism of $Y$ and $\mathrm{Y'}$ such that the composition of $f$ and the homomorphism of $q$ is equal to the composition of the homomorphism of $p$ and $\mathrm{f'}$. Then the map isomorphism of $p$ and $q$ is an isomorphism of the cokernel of $f$ and the cokernel of $\mathrm{f'}$.

the cokernel of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the cokernel of $f$ is an isomorphism of the cokernel of $f$ and $0$ defined as the map isomorphism of $\operatorname{forget}$ applied to the parallel pair of $f$ and $0$ and $\operatorname{uniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the parallel pair of $f$ and $0$ and the morphism to the zero object of $f$.

the cokernel of l and i (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $l$ be a homomorphism of $Z$ and $Y$. Let $i$ be an isomorphism of $X$ and $Z$ such that the composition of the homomorphism of $i$ and $l$ is equal to $f$. Then the cokernel of $l$ and $i$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $f$ and $\mathrm{CategoryTheory\_\_Limits\_\_cokernel\_\_ofIsoComp\_\_\_proof\_1}$ applied to $f$, $l$, $i$ and $h_{1}$ defined as $\operatorname{ofIsoComp}$ applied to $f$, $l$, $i$, $h_{1}$ and $\operatorname{isColimit}$ applied to the parallel pair of $f$ and $0$.

the zero cokernel cofork of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the zero cokernel cofork of $f$ is a cokernel cofork of $f$.

the projection of f (from the name)

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

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{cokernelCompIsIso}$ applied to $f$ and $g$ is an isomorphism of the cokernel of the composition of $f$ and $g$ and the cokernel of $f$.

the cokernel comparison of f and G (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $G$ be a functor of $C$ and $D$. Then the cokernel comparison of $f$ and $G$ is a homomorphism of the cokernel of the map of $G$ and $f$ and the action of $G$ and the cokernel of $f$.

the cokernel epimorphism 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 cokernel epimorphism composition of $f$ and $g$ is an isomorphism of the cokernel of the composition of $f$ and $g$ and the cokernel of $g$.

the cokernel of the image inclusion of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the cokernel of the image inclusion of $f$ is an isomorphism of the cokernel of the inclusion of the image of $f$ and the cokernel of $f$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{cokernelIsCokernel}$ applied to $f$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $f$ and $\operatorname{trans}$ applied to $\operatorname{condition}$ applied to $f$ and $\operatorname{symm}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_zero\_comp}$.

the cokernel isomorphism of h2 (from the name)

Assume that $\EqtMACRoH {f}{g}$. Then the cokernel isomorphism of $h_{2}$ is an isomorphism of the cokernel of $f$ and the cokernel of $g$.

the cokernel (from the docstring)

The cokernel is an isomorphism of the cokernel of $0$ and $Y$ defined as the coequalizer of $0$.

the composition natural isomorphism of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the composition natural isomorphism of $F$ is an isomorphism of the composition of the parallel pair of $f$ and $0$ and $F$ and the parallel pair of the map of $F$ and $f$ and $0$.

Let $i$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $g$ be a homomorphism of $W$ and $X$ such that $h$ is equal to the composition of $g$ and $f$. Then $\operatorname{isCokernelEpiComp}$ applied to $i$, $g$ and $\mathrm{hh}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_isCokernelEpiComp\_\_\_proof\_1}$ applied to $g$ and $\mathrm{hh}$.

Let $g$ be a homomorphism of $W$ and $X$. Let $h$ be a homomorphism of $W$ and $Y$. Let $i$ be an element of $\operatorname{IsColimit}$ applied to $c$. Assume that the composition of $f$ and the projection of $c$ is equal to $0$. Assume that the composition of $g$ and $f$ is equal to $h$. Then $\operatorname{isCokernelOfComp}$ applied to $g$, $h$, $i$, $\mathrm{hf}$ and $\mathrm{hfg}$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $c$ and $\mathrm{hf}$.

Let $i$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $g$ be a homomorphism of $Y$ and $Z$ such that $h$ is equal to the composition of $f$ and $g$. Then $\operatorname{isKernelCompMono}$ applied to $i$, $g$ and $\mathrm{hh}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_isKernelCompMono\_\_\_proof\_1}$ applied to $g$ and $\mathrm{hh}$.

Let $g$ be a homomorphism of $Y$ and $W$. Let $h$ be a homomorphism of $X$ and $W$. Let $i$ be an element of $\operatorname{IsLimit}$ applied to $c$. Assume that the composition of the inclusion of $c$ and $f$ is equal to $0$. Assume that the composition of $f$ and $g$ is equal to $h$. Then $\operatorname{isKernelOfComp}$ applied to $g$, $h$, $i$, $\mathrm{hf}$ and $\mathrm{hfg}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $c$ and $\mathrm{hf}$.

the isomorphism of s (from the name)

Let $s$ be a fork of $f$ and $0$. Then the isomorphism of $s$ is an isomorphism of $s$ and the inclusion of the inclusion of $s$ and $\operatorname{condition}$ applied to $s$.

the isomorphism of s (from the name)

Let $s$ be a cofork of $f$ and $0$. Then the isomorphism of $s$ is an isomorphism of $s$ and the projection of the projection of $s$ and $\operatorname{condition}$ applied to $s$.

the kernel of C (from the docstring)

Let $C$ be a set. Then the kernel of $C$ is a functor of the set of arrows of $C$ and $C$.

the kernel inclusion of C (from the docstring)

Let $C$ be a set. Then the kernel inclusion of $C$ is a homomorphism of the kernel of $C$ and the left function.

the kernel of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the kernel of $f$ is an element of $C$ defined as the equalizer of $f$ and $0$.

the map from the zero object of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map from the zero object of $f$ is an element of $\operatorname{IsLimit}$ applied to the zero kernel fork of $f$.

the isomorphism kernel of l and i (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $l$ be a homomorphism of $Z$ and $X$. Let $i$ be an isomorphism of $Z$ and the kernel of $f$ such that the composition of the homomorphism of $i$ and the inclusion of $f$ is equal to $l$. Then the isomorphism kernel of $l$ and $i$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $l$ and $\mathrm{CategoryTheory\_\_Limits\_\_kernel\_\_isoKernel\_\_\_proof\_1}$ applied to $f$, $l$, $i$ and $h_{1}$ defined as the isomorphism kernel of $\operatorname{isLimit}$ applied to the parallel pair of $f$ and $0$ and $i$.

the lift of f and k (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $k$ be a homomorphism of $W$ and $X$ such that the composition of $k$ and $f$ is equal to $0$. Then the lift of $f$ and $k$ is a homomorphism of $W$ and the kernel of $f$ defined as the lift of $\operatorname{kernelIsKernel}$ applied to $f$ and the inclusion of $k$ and $h_{1}$.

the lift of f and k (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $k$ be a homomorphism of $W$ and $X$ such that $\EqtMACRoH {\operatorname{comp} (k , f)}{0}$. Then the lift of $f$ and $k$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , \mathrm{CategoryTheory\_\_Limits\_\_kernel\_\_\_u3b9\_} (f))}{k})}$ defined as the lift of $f$ and $k$.

the map of q and w (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $\mathrm{f'}$ be a homomorphism of $\mathrm{X'}$ and $\mathrm{Y'}$. Let $p$ be a homomorphism of $X$ and $\mathrm{X'}$. Let $q$ be a homomorphism of $Y$ and $\mathrm{Y'}$ such that the composition of $f$ and $q$ is equal to the composition of $p$ and $\mathrm{f'}$. Then the map of $p$ and $q$ is a homomorphism of the kernel of $f$ and the kernel of $\mathrm{f'}$.

the map isomorphism of q and w (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $\mathrm{f'}$ be a homomorphism of $\mathrm{X'}$ and $\mathrm{Y'}$. Let $p$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $q$ be an isomorphism of $Y$ and $\mathrm{Y'}$ such that the composition of $f$ and the homomorphism of $q$ is equal to the composition of the homomorphism of $p$ and $\mathrm{f'}$. Then the map isomorphism of $p$ and $q$ is an isomorphism of the kernel of $f$ and the kernel of $\mathrm{f'}$.

the kernel of l and i (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $l$ be a homomorphism of $X$ and $Z$. Let $i$ be an isomorphism of $Z$ and $Y$ such that the composition of $l$ and the homomorphism of $i$ is equal to $f$. Then the kernel of $l$ and $i$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $f$ and $\mathrm{CategoryTheory\_\_Limits\_\_kernel\_\_ofCompIso\_\_\_proof\_1}$ applied to $f$, $l$, $i$ and $h_{1}$ defined as $\operatorname{ofCompIso}$ applied to $f$, $l$, $i$, $h_{1}$ and $\operatorname{isLimit}$ applied to the parallel pair of $f$ and $0$.

the kernel of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the kernel of $f$ is an isomorphism of the kernel of $f$ and $0$ defined as the map isomorphism of $\operatorname{forget}$ applied to the parallel pair of $f$ and $0$ and $\operatorname{uniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to the parallel pair of $f$ and $0$ and the map from the zero object of $f$.

the zero kernel fork of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the zero kernel fork of $f$ is a kernel fork of $f$.

the inclusion of f (from the name)

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

the kernel composition monomorphism 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 kernel composition monomorphism of $f$ and $g$ is an isomorphism of the kernel of the composition of $f$ and $g$ and the kernel of $f$.

the kernel comparison of f and G (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $G$ be a functor of $C$ and $D$. Then the kernel comparison of $f$ and $G$ is a homomorphism of the action of $G$ and the kernel of $f$ and the kernel of the map of $G$ and $f$.

the kernel of the morphism of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the kernel of the morphism of $f$ is an isomorphism of the kernel of the map from the source to the image of $f$ and the kernel of $f$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{kernelIsIsoComp}$ applied to $f$ and $g$ is an isomorphism of the kernel of the composition of $f$ and $g$ and the kernel of $g$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{kernelIsKernel}$ applied to $f$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $f$ and $\operatorname{trans}$ applied to $\operatorname{condition}$ applied to $f$ and $\operatorname{symm}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_comp\_zero}$.

the kernel isomorphism of h2 (from the name)

Assume that $\EqtMACRoH {f}{g}$. Then the kernel isomorphism of $h_{2}$ is an isomorphism of the kernel of $f$ and the kernel of $g$.

the kernel (from the docstring)

The kernel is an isomorphism of the kernel of $0$ and $X$ defined as the equalizer of $0$.

the inclusion congruence of h (from the name)

Assume that $\EqtMACRoH {x_{2}}{x_{3}}$. Then the inclusion congruence of $h$ is an isomorphism of the inclusion of $x_{2}$ and $w$ and the inclusion of $x_{3}$ and $\mathrm{CategoryTheory\_\_Limits\_\_of\_u3b9\_Congr\_\_\_proof\_1}$ applied to $h$.

the projection congruence of h (from the name)

Assume that $\EqtMACRoH {x_{2}}{x_{3}}$. Then the projection congruence of $h$ is an isomorphism of the projection of $x_{2}$ and $w$ and the projection of $x_{3}$ and $\mathrm{CategoryTheory\_\_Limits\_\_of\_u3c0\_Congr\_\_\_proof\_1}$ applied to $h$.

the zero cokernel of f and hf (from the name)

Let $f$ be a homomorphism of $X$ and $Y$ such that for all elements $Z$ of $C$, for all homomorphisms $g$ of $Y$ and $Z$, if the composition of $f$ and $g$ is equal to $0$, then $\EqtMACRoH {g}{0}$. Then the zero cokernel of $f$ and $\mathrm{hf}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $0$ and $\mathrm{CategoryTheory\_\_Limits\_\_zeroCokernelOfZeroCancel\_\_\_proof\_1}$ applied to $f$.

the zero kernel of f and hf (from the name)

Let $f$ be a homomorphism of $X$ and $Y$ such that for all elements $Z$ of $C$, for all homomorphisms $g$ of $Z$ and $X$, if the composition of $g$ and $f$ is equal to $0$, then $\EqtMACRoH {g}{0}$. Then the zero kernel of $f$ and $\mathrm{hf}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $0$ and $\mathrm{CategoryTheory\_\_Limits\_\_zeroKernelOfCancelZero\_\_\_proof\_1}$ applied to $f$.