Definitions: Mathlib.CategoryTheory, part 14 of 25

There is a morphism property of the set of functors of $J$ and $C$. Proof. Let $F$ be arbitrary. Let $G$ be arbitrary. Let $x_{2}$ be arbitrary. By J. Let $i$ be arbitrary. By J. Let $j$ be arbitrary. By i. By j. By Quiver__Hom. Let $f$ be arbitrary. By F. By f. By CategoryTheory__Functor__map. By x2. By i. By CategoryTheory__NatTrans__app. By x2. By j. By CategoryTheory__NatTrans__app. By G. By f. By CategoryTheory__Functor__map. By CategoryTheory__IsPushout. By forall. By forall. By forall.

There is a morphism property of the set of functors of $J$ and $C$. Proof. Let $F$ be arbitrary. Let $G$ be arbitrary. Let $x_{2}$ be arbitrary. By J. Let $i$ be arbitrary. By J. Let $j$ be arbitrary. By i. By j. By Quiver__Hom. Let $f$ be arbitrary. By F. By f. By CategoryTheory__Functor__map. By x2. By i. By CategoryTheory__NatTrans__app. By x2. By j. By CategoryTheory__NatTrans__app. By G. By f. By CategoryTheory__Functor__map. By CategoryTheory__IsPullback. By forall. By forall. By forall.

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{HasPullback}$ holds for $f$ and $g$, if the cospan of $f$ and $g$ has limits.

C has pullbacks (from the name)

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

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{HasPullbacksAlong}$ holds for $f$, if for all elements $W$ of $C$, for all homomorphisms $h$ of $W$ and $Y$, $\operatorname{HasPullback}$ holds for $h$ and $f$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then $\operatorname{HasPushout}$ holds for $f$ and $g$, if the span of $f$ and $g$ has colimits.

C has pushouts (from the name)

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

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{HasPushoutsAlong}$ holds for $f$, if for all elements $W$ of $C$, for all homomorphisms $h$ of $X$ and $W$, $\operatorname{HasPushout}$ holds for $h$ and $f$.

the pullback 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 pullback of $f$ and $g$ is an element of $C$ defined as the limit of the cospan of $f$ and $g$.

the cone 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 cone of $f$ and $g$ is a pullback cone of $f$ and $g$ defined as the cone of the cospan of $f$ and $g$.

the congruence homomorphism of h and h1 (from the name)

Assume that $\EqtMACRoH {x_{1}}{x_{2}}$. Assume that $\EqtMACRoH {x_{3}}{x_{4}}$. Then the congruence homomorphism of $h$ and $h_{1}$ is an isomorphism of the pullback of $x_{1}$ and $x_{3}$ and the pullback of $x_{2}$ and $x_{4}$.

the first projection of the pullback of f and g (from the docstring)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the first projection of the pullback of $f$ and $g$ is a homomorphism of the pullback of $f$ and $g$ and $X$ defined as the projection from the limit object to a value of the functor of the cospan of $f$ and $g$ and the left point of the walking cospan.

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{isLimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the cone of $f$ and $g$ defined as $\operatorname{isLimit}$ applied to the cospan of $f$ and $g$.

the lift of h1 and k (from the name)

Let $h_{1}$ be a homomorphism of $W$ and $X$. Let $k$ be a homomorphism of $W$ and $Y$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $h_{1}$ and $f$ is equal to the composition of $k$ and $g$ and $\mathrm{CategoryTheory\_\_Limits\_\_pullback\_\_lift\_\_\_auto\_1}$. Then the lift of $h_{1}$ and $k$ is a homomorphism of $W$ and the pullback of $f$ and $g$ defined as the lift of the cospan of $f$ and $g$ and $\operatorname{mk}$ applied to $h_{1}$, $k$ and $w$.

the lift of h1 and k (from the name)

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

the map of x6 and x7 (from the name)

Let $x_{1}$ be a homomorphism of $W$ and $S$. Let $x_{2}$ be a homomorphism of $X$ and $S$. Let $x_{3}$ be a homomorphism of $Y$ and $T$. Let $x_{4}$ be a homomorphism of $Z$ and $T$. Let $x_{5}$ be a homomorphism of $W$ and $Y$. Let $x_{6}$ be a homomorphism of $X$ and $Z$. Let $x_{7}$ be a homomorphism of $S$ and $T$ such that the composition of $x_{1}$ and $x_{7}$ is equal to the composition of $x_{5}$ and $x_{3}$ and the composition of $x_{2}$ and $x_{7}$ is equal to the composition of $x_{6}$ and $x_{4}$. Then the map of $x_{6}$ and $x_{7}$ is a homomorphism of the pullback of $x_{1}$ and $x_{2}$ and the pullback of $x_{3}$ and $x_{4}$.

Let $f$ be a homomorphism of $X$ and $S$. Let $g$ be a homomorphism of $Y$ and $S$. Let $i$ be a homomorphism of $S$ and $T$. Then $\operatorname{mapDesc}$ applied to $f$, $g$ and $i$ is a homomorphism of the pullback of $f$ and $g$ and the pullback of the composition of $f$ and $i$ and the composition of $g$ and $i$.

the second projection of the pullback of f and g (from the docstring)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the second projection of the pullback of $f$ and $g$ is a homomorphism of the pullback of $f$ and $g$ and $Y$ defined as the projection from the limit object to a value of the functor of the cospan of $f$ and $g$ and the right point of the walking cospan.

the comparison morphism for the pullback of G (from the docstring)

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

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{pullbackIsPullback}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the first projection of the pullback of $f$ and $g$, the second projection of the pullback of $f$ and $g$ and $\operatorname{condition}$ defined as $\operatorname{mkSelfIsLimit}$ applied to $\operatorname{isLimit}$ applied to $f$ and $g$.

the pullback product first component isomorphism product of f and Z (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $Z$ be an element of $C$. Then the pullback product first component isomorphism product of $f$ and $Z$ is an isomorphism of the pullback of $f$ and the projection map to the first component of the product and the product of $X$ and $Z$.

the pullback product second component isomorphism product of f and Z (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $Z$ be an element of $C$. Then the pullback product second component isomorphism product of $f$ and $Z$ is an isomorphism of the pullback of the projection map to the second component of the product and $f$ and the product of $Z$ and $X$.

the pullback symmetry 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 pullback symmetry of $f$ and $g$ is an isomorphism of the pullback of $f$ and $g$ and the pullback of $g$ and $f$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to the flip of $\operatorname{pullbackIsPullback}$ applied to $f$ and $g$ and $\operatorname{isLimit}$ applied to the cospan of $g$ and $f$.

the pushout of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the pushout of $f$ and $g$ is an element of $C$ defined as the colimit of the span of $f$ and $g$.

the cocone of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the cocone of $f$ and $g$ is a pushout cocone of $f$ and $g$ defined as the cocone of the span of $f$ and $g$.

the congruence homomorphism of h and h1 (from the name)

Assume that $\EqtMACRoH {x_{1}}{x_{2}}$. Assume that $\EqtMACRoH {x_{3}}{x_{4}}$. Then the congruence homomorphism of $h$ and $h_{1}$ is an isomorphism of the pushout of $x_{1}$ and $x_{3}$ and the pushout of $x_{2}$ and $x_{4}$.

Let $h_{1}$ be a homomorphism of $Y$ and $W$. Let $k$ be a homomorphism of $Z$ and $W$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $f$ and $h_{1}$ is equal to the composition of $g$ and $k$ and $\mathrm{CategoryTheory\_\_Limits\_\_pushout\_\_desc\_\_\_auto\_1}$. Then $\operatorname{desc}$ applied to $h_{1}$, $k$ and $w$ is a homomorphism of the pushout of $f$ and $g$ and $W$ defined as $\operatorname{desc}$ applied to the span of $f$ and $g$ and $\operatorname{mk}$ applied to $h_{1}$, $k$ and $w$.

Let $h_{1}$ be a homomorphism of $Y$ and $W$. Let $k$ be a homomorphism of $Z$ and $W$ such that $\EqtMACRoH {\operatorname{comp} (f , h_{1})}{\operatorname{comp} (g , k)}$. Then $\operatorname{desc'}$ applied to $h_{1}$, $k$ and $w$ is an element of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (\operatorname{inl} (f , g), l)}{h_{1}}, \EqtMACRoH {\operatorname{comp} (\operatorname{inr} (f , g), l)}{k})}$ defined as $\operatorname{desc}$ applied to $h_{1}$, $k$ and $w$.

the left injection of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the left injection of $f$ and $g$ is a homomorphism of $Y$ and the pushout of $f$ and $g$ defined as the inclusion of the span of $f$ and $g$ and the left point of the walking span.

the right injection of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the right injection of $f$ and $g$ is a homomorphism of $Z$ and the pushout of $f$ and $g$ defined as the inclusion of the span of $f$ and $g$ and the right point of the walking span.

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then $\operatorname{isColimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $f$ and $g$ defined as $\operatorname{isColimit}$ applied to the span of $f$ and $g$.

the map of x6 and x7 (from the name)

Let $x_{1}$ be a homomorphism of $S$ and $W$. Let $x_{2}$ be a homomorphism of $S$ and $X$. Let $x_{3}$ be a homomorphism of $T$ and $Y$. Let $x_{4}$ be a homomorphism of $T$ and $Z$. Let $x_{5}$ be a homomorphism of $W$ and $Y$. Let $x_{6}$ be a homomorphism of $X$ and $Z$. Let $x_{7}$ be a homomorphism of $S$ and $T$ such that the composition of $x_{1}$ and $x_{5}$ is equal to the composition of $x_{7}$ and $x_{3}$ and the composition of $x_{2}$ and $x_{6}$ is equal to the composition of $x_{7}$ and $x_{4}$. Then the map of $x_{6}$ and $x_{7}$ is a homomorphism of the pushout of $x_{1}$ and $x_{2}$ and the pushout of $x_{3}$ and $x_{4}$.

the map lift of g and i (from the name)

Let $f$ be a homomorphism of $T$ and $X$. Let $g$ be a homomorphism of $T$ and $Y$. Let $i$ be a homomorphism of $S$ and $T$. Then the map lift of $g$ and $i$ is a homomorphism of the pushout of the composition of $i$ and $f$ and the composition of $i$ and $g$ and the pushout of $f$ and $g$.

the comparison morphism for the pushout of G (from the docstring)

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

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then $\operatorname{pushoutIsPushout}$ applied to $f$ and $g$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the left injection of $f$ and $g$, the right injection of $f$ and $g$ and $\operatorname{condition}$.

the pushout symmetry of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the pushout symmetry of $f$ and $g$ is an isomorphism of the pushout of $f$ and $g$ and the pushout of $g$ and $f$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to the flip of $\operatorname{pushoutIsPushout}$ applied to $f$ and $g$ and $\operatorname{isColimit}$ applied to the span of $g$ and $f$.

the duality equivalence (from the docstring)

The duality equivalence is an equivalence of the set of opposites of the set of walking cospans and the set of walking spans defined as the duality equivalence of the set of walking pairs.

the duality equivalence (from the docstring)

The duality equivalence is an equivalence of the set of opposites of the set of walking spans and the set of walking cospans defined as the duality equivalence of the set of walking pairs.

Assume that $\operatorname{IsPullback}$ holds for $f$, $f$, $g$ and $\mathrm{g'}$. Then $\operatorname{isLimitFork}$ applied to $H$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $f$ and $\operatorname{w}$ applied to $\operatorname{toCommSq}$ applied to $H$.

the isomorphism over pullback of h1 (from the name)

Assume that $\operatorname{IsPullback}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$. Then the isomorphism over pullback of $h_{1}$ is an isomorphism of $\operatorname{mk}$ applied to $\mathrm{fst}$ and $\operatorname{mk}$ applied to the first projection of the pullback of $f$ and $g$.

Assume that $\operatorname{IsPushout}$ holds for $t$, $l$, $r$ and $b$. Let $x_{6}$ be a cocone of $x_{2}$. Let $x_{7}$ be a cocone of $x_{3}$. Let $x_{8}$ be a cocone of $x_{4}$. Let $x_{9}$ be a cocone of $x_{5}$. Let $x_{10}$ be an element of $\operatorname{IsColimit}$ applied to $x_{6}$. Let $x_{11}$ be an element of $\operatorname{IsColimit}$ applied to $x_{7}$. Let $x_{12}$ be an element of $\operatorname{IsColimit}$ applied to $x_{8}$. Assume that $\operatorname{IsPushout}$ holds for $\mathrm{t'}$, $\mathrm{l'}$, $\mathrm{r'}$ and $\mathrm{b'}$. Assume that $\mathrm{autoParam}$ holds for the proposition that for all elements $j_{3}$ of $J$, the composition of the component of the inclusion of $x_{6}$ and $j_{3}$ and $\mathrm{t'}$ is equal to the composition of the component of $t$ and $j_{3}$ and the component of the inclusion of $x_{7}$ and $j_{3}$ and $\mathrm{CategoryTheory\_\_IsPushout\_\_isColimitOfIsColimitOfIsPushout\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that for all elements $j_{2}$ of $J$, the composition of the component of the inclusion of $x_{6}$ and $j_{2}$ and $\mathrm{l'}$ is equal to the composition of the component of $l$ and $j_{2}$ and the component of the inclusion of $x_{8}$ and $j_{2}$ and $\mathrm{CategoryTheory\_\_IsPushout\_\_isColimitOfIsColimitOfIsPushout\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that for all elements $j_{1}$ of $J$, the composition of the component of the inclusion of $x_{7}$ and $j_{1}$ and $\mathrm{r'}$ is equal to the composition of the component of $r$ and $j_{1}$ and the component of the inclusion of $x_{9}$ and $j_{1}$ and $\mathrm{CategoryTheory\_\_IsPushout\_\_isColimitOfIsColimitOfIsPushout\_\_\_auto\_5}$. Assume that $\mathrm{autoParam}$ holds for the proposition that for all elements $j$ of $J$, the composition of the component of the inclusion of $x_{8}$ and $j$ and $\mathrm{b'}$ is equal to the composition of the component of $b$ and $j$ and the component of the inclusion of $x_{9}$ and $j$ and $\mathrm{CategoryTheory\_\_IsPushout\_\_isColimitOfIsColimitOfIsPushout\_\_\_auto\_7}$. Then $\operatorname{isColimitOfIsColimitOfIsPushout}$ applied to $\mathrm{sq}$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $x_{12}$, $\mathrm{sq'}$, $\mathrm{ht'}$, $\mathrm{hl'}$, $\mathrm{hr'}$ and $\mathrm{hb'}$ is an element of $\operatorname{IsColimit}$ applied to $x_{9}$.

Assume that $\operatorname{IsPushout}$ holds for $f$, $\mathrm{f'}$, $g$ and $g$. Then $\operatorname{isLimitFork}$ applied to $H$ is an element of $\operatorname{IsColimit}$ applied to the projection of $g$ and $\operatorname{w}$ applied to $\operatorname{toCommSq}$ applied to $H$.

Let $f$ be a homomorphism of $W$ and $X$. Let $g$ be a homomorphism of $W$ and $Y$. Let $h$ be a homomorphism of $X$ and $Z$. Let $i$ be a homomorphism of $Y$ and $Z$. Then we can say that $\operatorname{BicartesianSq}$ holds for $f$, $g$, $h$ and $i$.

the pullback biproduct left injection biproduct right injection (from the name)

The pullback biproduct left injection biproduct right injection is an isomorphism of the pullback of the left injection and the right injection and $0$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the cone of $\mathrm{CategoryTheory\_\_IsPullback\_\_of\_hasBinaryBiproduct}$ applied to $X$ and $Y$ and $\operatorname{isLimit}$ applied to $\mathrm{CategoryTheory\_\_IsPullback\_\_of\_hasBinaryBiproduct}$ applied to $X$ and $Y$.

the pushout biproduct first component biproduct second component (from the name)

The pushout biproduct first component biproduct second component is an isomorphism of the pushout of the projection onto the first summand and the projection onto the second summand and $0$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the cocone of $\mathrm{CategoryTheory\_\_IsPushout\_\_of\_hasBinaryBiproduct}$ applied to $X$ and $Y$ and $\operatorname{isColimit}$ applied to $\mathrm{CategoryTheory\_\_IsPushout\_\_of\_hasBinaryBiproduct}$ applied to $X$ and $Y$.

Let $\mathrm{fst}$ be a homomorphism of $P$ and $X$. Let $\mathrm{snd}$ be a homomorphism of $P$ and $Y$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then we can say that $\operatorname{IsPullback}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$.

the cone of h (from the name)

Assume that $\operatorname{IsPullback}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$. Then the cone of $h$ is a pullback cone of $f$ and $g$ defined as the cone of $\operatorname{toCommSq}$ applied to $h$.

Assume that $\operatorname{IsPullback}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$. Then $\operatorname{isLimit}$ applied to $h$ is an element of $\operatorname{IsLimit}$ applied to the cone of $h$ defined as $\operatorname{some}$ applied to $\operatorname{isLimit'}$ applied to $h$.

Let $X$ and $Y$ be elements of $C$. Assume that $\operatorname{IsPullback}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$. Assume that $\operatorname{IsPullback}$ holds for $\mathrm{fst'}$, $\mathrm{snd'}$, $f$ and $g$. Then $\operatorname{isoIsPullback}$ applied to $X$, $Y$, $h$ and $\mathrm{h'}$ is an isomorphism of $P$ and $\mathrm{P'}$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to $h$ and $\operatorname{isLimit}$ applied to $\mathrm{h'}$.

the isomorphism pullback of h (from the name)

Assume that $\operatorname{IsPullback}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$. Then the isomorphism pullback of $h$ is an isomorphism of $P$ and the pullback of $f$ and $g$ defined as the inverse of the isomorphism limit cone of $\operatorname{mk}$ applied to the cone of $h$ and $\operatorname{isLimit}$ applied to $h$.

the lift of h and k (from the name)

Assume that $\operatorname{IsPullback}$ holds for $\mathrm{fst}$, $\mathrm{snd}$, $f$ and $g$. Let $h$ be a homomorphism of $W$ and $X$. Let $k$ be a homomorphism of $W$ and $Y$ such that the composition of $h$ and $f$ is equal to the composition of $k$ and $g$. Then the lift of $h$ and $k$ is a homomorphism of $W$ and $P$ defined as the lift of $h$ and $k$.

Let $f$ be a homomorphism of $Z$ and $X$. Let $g$ be a homomorphism of $Z$ and $Y$. Let $\mathrm{inl}$ be a homomorphism of $X$ and $P$. Let $\mathrm{inr}$ be a homomorphism of $Y$ and $P$. Then we can say that $\operatorname{IsPushout}$ holds for $f$, $g$, $\mathrm{inl}$ and $\mathrm{inr}$.

the cocone of h (from the name)

Assume that $\operatorname{IsPushout}$ holds for $f$, $g$, $\mathrm{inl}$ and $\mathrm{inr}$. Then the cocone of $h$ is a pushout cocone of $f$ and $g$ defined as the cocone of $\operatorname{toCommSq}$ applied to $h$.

Assume that $\operatorname{IsPushout}$ holds for $f$, $g$, $\mathrm{inl}$ and $\mathrm{inr}$. Let $h$ be a homomorphism of $X$ and $W$. Let $k$ be a homomorphism of $Y$ and $W$ such that the composition of $f$ and $h$ is equal to the composition of $g$ and $k$. Then $\operatorname{desc}$ applied to $\mathrm{hP}$, $h$, $k$ and $w$ is a homomorphism of $P$ and $W$ defined as $\operatorname{desc}$ applied to $\operatorname{isColimit}$ applied to $\mathrm{hP}$, $h$, $k$ and $w$.

Assume that $\operatorname{IsPushout}$ holds for $f$, $g$, $\mathrm{inl}$ and $\mathrm{inr}$. Then $\operatorname{isColimit}$ applied to $h$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $h$ defined as $\operatorname{some}$ applied to $\operatorname{isColimit'}$ applied to $h$.

Let $X$ and $Y$ be elements of $C$. Assume that $\operatorname{IsPushout}$ holds for $f$, $g$, $\mathrm{inl}$ and $\mathrm{inr}$. Assume that $\operatorname{IsPushout}$ holds for $f$, $g$, $\mathrm{inl'}$ and $\mathrm{inr'}$. Then $\operatorname{isoIsPushout}$ applied to $X$, $Y$, $h$ and $\mathrm{h'}$ is an isomorphism of $P$ and $\mathrm{P'}$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to $h$ and $\operatorname{isColimit}$ applied to $\mathrm{h'}$.

the isomorphism pushout of h (from the name)

Assume that $\operatorname{IsPushout}$ holds for $f$, $g$, $\mathrm{inl}$ and $\mathrm{inr}$. Then the isomorphism pushout of $h$ is an isomorphism of $P$ and the pushout of $f$ and $g$ defined as the inverse of the isomorphism colimit cocone of $\operatorname{mk}$ applied to the cocone of $h$ and $\operatorname{isColimit}$ applied to $h$.

the pullback cone 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 pullback cone of $f$ and $g$ is a pullback cone of $f$ and $g$.

the pullback cone 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 pullback cone of $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone of $f$ and $g$ defined as $\operatorname{isLimitAux'}$ applied to the pullback cone of $f$ and $g$ and the function that maps $s$ to the second projection of $s$.

the pullback cone 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 pullback cone of $f$ and $g$ is a pullback cone of $f$ and $g$.

the pullback cone 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 pullback cone of $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone of $f$ and $g$ defined as $\operatorname{isLimitAux'}$ applied to the pullback cone of $f$ and $g$ and the function that maps $s$ to the first projection of $s$.

the pushout cocone of f and g (from the name)

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

the pushout cocone of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the pushout cocone of $f$ and $g$ is an element of $\operatorname{IsColimit}$ applied to the pushout cocone of $f$ and $g$ defined as $\operatorname{isColimitAux'}$ applied to the pushout cocone of $f$ and $g$ and the function that maps $s$ to the right injection of $s$.

the pushout cocone of f and g (from the name)

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

the pushout cocone of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the pushout cocone of $f$ and $g$ is an element of $\operatorname{IsColimit}$ applied to the pushout cocone of $f$ and $g$ defined as $\operatorname{isColimitAux'}$ applied to the pushout cocone of $f$ and $g$ and the function that maps $s$ to the left injection of $s$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isLimitMkIdId}$ applied to $f$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the identity morphism of $X$, the identity morphism of $X$ and $\mathrm{rfl}$.

Let $f$ be a homomorphism of $X$ and $W$. Let $g$ be a homomorphism of $Y$ and $W$. Let $i$ be a homomorphism of $W$ and $Z$. Let $s$ be a pullback cone of $f$ and $g$. Let $H$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then $\operatorname{isLimitOfCompMono}$ applied to $f$, $g$, $i$, $s$ and $H$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the first projection of $s$, the second projection of $s$ and $\mathrm{CategoryTheory\_\_Limits\_\_PullbackCone\_\_isLimitOfCompMono\_\_\_proof\_1}$ applied to $f$, $g$, $i$ and $s$.

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $h$ be a homomorphism of $W$ and $Z$. Let $x_{1}$ be a homomorphism of $X$ and $W$. Let $y$ be a homomorphism of $Y$ and $W$. Assume that the composition of $x_{1}$ and $h$ is equal to $f$. Assume that the composition of $y$ and $h$ is equal to $g$. Let $s$ be a pullback cone of $f$ and $g$. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then $\operatorname{isLimitOfFactors}$ applied to $f$, $g$, $h$, $x_{1}$, $y$, $\mathrm{hxh}$, $\mathrm{hyh}$, $s$ and $\mathrm{hs}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the first projection of $s$, the second projection of $s$ and $\mathrm{iffEl}$ applied to the proposition that the composition of the composition of the first projection of $s$ and $x_{1}$ and $h$ is equal to the composition of the composition of the second projection of $s$ and $y$ and $h$, the proposition that the composition of the first projection of $s$ and $x_{1}$ is equal to the composition of the second projection of $s$ and $y$, $\mathrm{CategoryTheory\_\_cancel\_mono}$ applied to $h$ and $\mathrm{CategoryTheory\_\_Limits\_\_PullbackCone\_\_isLimitOfFactors\_\_\_proof\_1}$ applied to $f$, $g$, $h$, $x_{1}$, $y$, $\mathrm{hxh}$, $\mathrm{hyh}$ and $s$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isColimitMkIdId}$ applied to $f$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the identity morphism of $Y$, the identity morphism of $Y$ and $\mathrm{rfl}$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Let $h$ be a homomorphism of $W$ and $X$. Let $s$ be a pushout cocone of $f$ and $g$. Let $H$ be an element of $\operatorname{IsColimit}$ applied to $s$. Then $\operatorname{isColimitOfEpiComp}$ applied to $f$, $g$, $h$, $s$ and $H$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the left injection of $s$, the right injection of $s$ and $\mathrm{CategoryTheory\_\_Limits\_\_PushoutCocone\_\_isColimitOfEpiComp\_\_\_proof\_1}$ applied to $f$, $g$, $h$ and $s$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Let $h$ be a homomorphism of $X$ and $W$. Let $x_{1}$ be a homomorphism of $W$ and $Y$. Let $y$ be a homomorphism of $W$ and $Z$. Assume that the composition of $h$ and $x_{1}$ is equal to $f$. Assume that the composition of $h$ and $y$ is equal to $g$. Let $s$ be a pushout cocone of $f$ and $g$. Let $\mathrm{hs}$ be an element of $\operatorname{IsColimit}$ applied to $s$. Then $\operatorname{isColimitOfFactors}$ applied to $f$, $g$, $h$, $x_{1}$, $y$, $\mathrm{hhx}$, $\mathrm{hhy}$, $s$ and $\mathrm{hs}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the left injection of $s$, the right injection of $s$ and $\mathrm{iffEl}$ applied to the proposition that the composition of $h$ and the composition of $x_{1}$ and the left injection of $s$ is equal to the composition of $h$ and the composition of $y$ and the right injection of $s$, the proposition that the composition of $x_{1}$ and the left injection of $s$ is equal to the composition of $y$ and the right injection of $s$, $\mathrm{CategoryTheory\_\_cancel\_epi}$ applied to $h$ and $\mathrm{CategoryTheory\_\_Limits\_\_PushoutCocone\_\_isColimitOfFactors\_\_\_proof\_3}$ applied to $f$, $g$, $h$, $x_{1}$, $y$, $s$, $\mathrm{CategoryTheory\_\_Limits\_\_PushoutCocone\_\_isColimitOfFactors\_\_\_proof\_1}$ applied to $f$, $g$, $h$, $x_{1}$, $\mathrm{hhx}$ and $s$ and $\mathrm{CategoryTheory\_\_Limits\_\_PushoutCocone\_\_isColimitOfFactors\_\_\_proof\_2}$ applied to $f$, $g$, $h$, $y$, $\mathrm{hhy}$ and $s$.

the pullback of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $W$. Let $g$ be a homomorphism of $Y$ and $W$. Let $i$ be a homomorphism of $W$ and $Z$. Then the pullback of $f$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the first projection of the pullback of $f$ and $g$, the second projection of the pullback of $f$ and $g$ and $\mathrm{CategoryTheory\_\_Limits\_\_pullbackIsPullbackOfCompMono\_\_\_proof\_2}$ applied to $f$, $g$ and $i$ defined as $\operatorname{isLimitOfCompMono}$ applied to $f$, $g$, $i$, the cone of the cospan of $f$ and $g$ and $\operatorname{isLimit}$ applied to the cospan of $f$ and $g$.

the pushout of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Let $h$ be a homomorphism of $W$ and $X$. Then the pushout of $f$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the left injection of $f$ and $g$, the right injection of $f$ and $g$ and $\mathrm{CategoryTheory\_\_Limits\_\_pushoutIsPushoutOfEpiComp\_\_\_proof\_1}$ applied to $f$, $g$ and $h$ defined as $\operatorname{isColimitOfEpiComp}$ applied to $f$, $g$, $h$, the cocone of the span of $f$ and $g$ and $\operatorname{isColimit}$ applied to the span of $f$ and $g$.

Let $x_{8}$ be a pullback cone of $x_{6}$ and $x_{7}$. Let $x_{10}$ be a pullback cone of $x_{5}$ and $x_{9}$. Assume that $x_{9}$ is equal to the first projection of $x_{8}$. Then $\operatorname{pasteHoriz}$ applied to $x_{8}$, $x_{10}$ and $h$ is a pullback cone of the composition of $x_{5}$ and $x_{6}$ and $x_{7}$.

Let $x_{8}$ be a pullback cone of $x_{7}$ and $x_{5}$. Let $x_{10}$ be a pullback cone of $x_{9}$ and $x_{6}$. Assume that $x_{9}$ is equal to the second projection of $x_{8}$. Then $\operatorname{pasteVert}$ applied to $x_{8}$, $x_{10}$ and $h$ is a pullback cone of $x_{7}$ and the composition of $x_{6}$ and $x_{5}$.

Let $x_{8}$ be a pullback cone of $x_{7}$ and $x_{5}$. Let $x_{10}$ be a pullback cone of $x_{9}$ and $x_{6}$. Assume that $x_{9}$ is equal to the second projection of $x_{8}$. Then $\operatorname{pasteVertFlip}$ applied to $x_{8}$, $x_{10}$ and $h$ is an isomorphism of the flip of $\operatorname{pasteVert}$ applied to $x_{8}$, $x_{10}$ and $h$ and $\operatorname{pasteHoriz}$ applied to the flip of $x_{8}$, the flip of $x_{10}$ and $h$.

Let $x_{8}$ be a pushout cocone of $x_{7}$ and $x_{5}$. Let $x_{10}$ be a pushout cocone of $x_{9}$ and $x_{6}$. Assume that $x_{9}$ is equal to the right injection of $x_{8}$. Then $\operatorname{pasteHoriz}$ applied to $x_{8}$, $x_{10}$ and $h$ is a pushout cocone of $x_{7}$ and the composition of $x_{5}$ and $x_{6}$.

Let $x_{8}$ be a pushout cocone of $x_{5}$ and $x_{7}$. Let $x_{10}$ be a pushout cocone of $x_{6}$ and $x_{9}$. Assume that $x_{9}$ is equal to the left injection of $x_{8}$. Then $\operatorname{pasteVert}$ applied to $x_{8}$, $x_{10}$ and $h$ is a pushout cocone of the composition of $x_{5}$ and $x_{6}$ and $x_{7}$.

Let $x_{8}$ be a pushout cocone of $x_{5}$ and $x_{7}$. Let $x_{10}$ be a pushout cocone of $x_{6}$ and $x_{9}$. Assume that $x_{9}$ is equal to the left injection of $x_{8}$. Then $\operatorname{pasteVertFlip}$ applied to $x_{8}$, $x_{10}$ and $h$ is an isomorphism of the flip of $\operatorname{pasteVert}$ applied to $x_{8}$, $x_{10}$ and $h$ and $\operatorname{pasteHoriz}$ applied to the flip of $x_{8}$, the flip of $x_{10}$ and $h$.

Let $x_{10}$ be a pushout cocone of $x_{6}$ and $x_{9}$. Assume that $x_{9}$ is equal to the left injection of $x_{8}$. Let $x_{11}$ be an element of $\operatorname{IsColimit}$ applied to $x_{8}$. Let $x_{12}$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{pasteVert}$ applied to $x_{8}$, $x_{10}$ and $h$. Then $\operatorname{botSquareIsPushout}$ applied to $x_{10}$, $h$, $x_{11}$ and $x_{12}$ is an element of $\operatorname{IsColimit}$ applied to $x_{10}$ defined as $\operatorname{isColimitOfFlip}$ applied to $\operatorname{rightSquareIsPushout}$ applied to the flip of $x_{10}$, $h$, the flip of $x_{11}$ and the flip of $x_{12}$.

Let $x_{10}$ be a pullback cone of $x_{5}$ and $x_{9}$. Assume that $x_{9}$ is equal to the first projection of $x_{8}$. Let $H$ be an element of $\operatorname{IsLimit}$ applied to $x_{8}$. Let $\mathrm{H'}$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{pasteHoriz}$ applied to $x_{8}$, $x_{10}$ and $h$. Then $\operatorname{leftSquareIsPullback}$ applied to $x_{10}$, $h$, $H$ and $\mathrm{H'}$ is an element of $\operatorname{IsLimit}$ applied to $x_{10}$.

Assume that $x_{9}$ is equal to the first projection of $x_{8}$. Let $H$ be an element of $\operatorname{IsLimit}$ applied to $x_{8}$. Let $\mathrm{H'}$ be an element of $\operatorname{IsLimit}$ applied to $x_{10}$. Then $\operatorname{pasteHorizIsPullback}$ applied to $h$, $H$ and $\mathrm{H'}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{pasteHoriz}$ applied to $x_{8}$, $x_{10}$ and $h$.

Let $x_{10}$ be a pullback cone of $x_{5}$ and $x_{9}$. Assume that $x_{9}$ is equal to the first projection of $x_{8}$. Let $H$ be an element of $\operatorname{IsLimit}$ applied to $x_{8}$. Then $\operatorname{pasteHorizIsPullbackEquiv}$ applied to $x_{10}$, $h$ and $H$ is an element of $\EquivMACRoAE {\operatorname{IsLimit} (\operatorname{pasteHoriz} (x_{8} , x_{10} , h))}{\operatorname{IsLimit} (x_{10})}$.

Assume that $x_{9}$ is equal to the right injection of $x_{8}$. Let $H$ be an element of $\operatorname{IsColimit}$ applied to $x_{8}$. Let $\mathrm{H'}$ be an element of $\operatorname{IsColimit}$ applied to $x_{10}$. Then $\operatorname{pasteHorizIsPushout}$ applied to $h$, $H$ and $\mathrm{H'}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{pasteHoriz}$ applied to $x_{8}$, $x_{10}$ and $h$.

Let $x_{10}$ be a pushout cocone of $x_{9}$ and $x_{6}$. Assume that $x_{9}$ is equal to the right injection of $x_{8}$. Let $H$ be an element of $\operatorname{IsColimit}$ applied to $x_{8}$. Then $\operatorname{pasteHorizIsPushoutEquiv}$ applied to $x_{10}$, $h$ and $H$ is an element of $\EquivMACRoAE {\operatorname{IsColimit} (\operatorname{pasteHoriz} (x_{8} , x_{10} , h))}{\operatorname{IsColimit} (x_{10})}$.

Assume that $x_{9}$ is equal to the second projection of $x_{8}$. Let $x_{11}$ be an element of $\operatorname{IsLimit}$ applied to $x_{8}$. Let $x_{12}$ be an element of $\operatorname{IsLimit}$ applied to $x_{10}$. Then $\operatorname{pasteVertIsPullback}$ applied to $h$, $x_{11}$ and $x_{12}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{pasteVert}$ applied to $x_{8}$, $x_{10}$ and $h$ defined as $\operatorname{isLimitOfFlip}$ applied to $\operatorname{ofIsoLimit}$ applied to $\operatorname{pasteHorizIsPullback}$ applied to $h$, the flip of $x_{11}$ and the flip of $x_{12}$ and the inverse of $\operatorname{pasteVertFlip}$ applied to $x_{8}$, $x_{10}$ and $h$.

Let $x_{10}$ be a pullback cone of $x_{9}$ and $x_{6}$. Assume that $x_{9}$ is equal to the second projection of $x_{8}$. Let $H$ be an element of $\operatorname{IsLimit}$ applied to $x_{8}$. Then $\operatorname{pasteVertIsPullbackEquiv}$ applied to $x_{10}$, $h$ and $H$ is an element of $\EquivMACRoAE {\operatorname{IsLimit} (\operatorname{pasteVert} (x_{8} , x_{10} , h))}{\operatorname{IsLimit} (x_{10})}$.

Assume that $x_{9}$ is equal to the left injection of $x_{8}$. Let $x_{11}$ be an element of $\operatorname{IsColimit}$ applied to $x_{8}$. Let $x_{12}$ be an element of $\operatorname{IsColimit}$ applied to $x_{10}$. Then $\operatorname{pasteVertIsPushout}$ applied to $h$, $x_{11}$ and $x_{12}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{pasteVert}$ applied to $x_{8}$, $x_{10}$ and $h$ defined as $\operatorname{isColimitOfFlip}$ applied to $\operatorname{ofIsoColimit}$ applied to $\operatorname{pasteHorizIsPushout}$ applied to $h$, the flip of $x_{11}$ and the flip of $x_{12}$ and the inverse of $\operatorname{pasteVertFlip}$ applied to $x_{8}$, $x_{10}$ and $h$.

Let $x_{10}$ be a pushout cocone of $x_{6}$ and $x_{9}$. Assume that $x_{9}$ is equal to the left injection of $x_{8}$. Let $H$ be an element of $\operatorname{IsColimit}$ applied to $x_{8}$. Then $\operatorname{pasteVertIsPushoutEquiv}$ applied to $x_{10}$, $h$ and $H$ is an element of $\EquivMACRoAE {\operatorname{IsColimit} (\operatorname{pasteVert} (x_{8} , x_{10} , h))}{\operatorname{IsColimit} (x_{10})}$.

the pullback left pullback second component isomorphism of g and #3 (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $\mathrm{g'}$ be a homomorphism of $W$ and $Y$. Then the pullback left pullback second component isomorphism of $g$ and $\mathrm{g'}$ is an isomorphism of the pullback of the second projection of the pullback of $f$ and $g$ and $\mathrm{g'}$ and the pullback of $f$ and the composition of $\mathrm{g'}$ and $g$.

the pullback right pullback first component isomorphism of g and #3 (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $\mathrm{f'}$ be a homomorphism of $W$ and $X$. Then the pullback right pullback first component isomorphism of $g$ and $\mathrm{f'}$ is an isomorphism of the pullback of $\mathrm{f'}$ and the first projection of the pullback of $f$ and $g$ and the pullback of the composition of $\mathrm{f'}$ and $f$ and $g$.

the pushout left pushout right injection isomorphism of g and #3 (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Let $\mathrm{g'}$ be a homomorphism of $Z$ and $W$. Then the pushout left pushout right injection isomorphism of $g$ and $\mathrm{g'}$ is an isomorphism of the pushout of the right injection of $f$ and $g$ and $\mathrm{g'}$ and the pushout of $f$ and the composition of $g$ and $\mathrm{g'}$.

the pushout right pushout left injection isomorphism of g and #3 (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Let $\mathrm{f'}$ be a homomorphism of $Y$ and $W$. Then the pushout right pushout left injection isomorphism of $g$ and $\mathrm{f'}$ is an isomorphism of the pushout of $\mathrm{f'}$ and the left injection of $f$ and $g$ and the pushout of the composition of $f$ and $\mathrm{f'}$ and $g$.

Let $x_{10}$ be a pushout cocone of $x_{9}$ and $x_{6}$. Assume that $x_{9}$ is equal to the right injection of $x_{8}$. Let $H$ be an element of $\operatorname{IsColimit}$ applied to $x_{8}$. Let $\mathrm{H'}$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{pasteHoriz}$ applied to $x_{8}$, $x_{10}$ and $h$. Then $\operatorname{rightSquareIsPushout}$ applied to $x_{10}$, $h$, $H$ and $\mathrm{H'}$ is an element of $\operatorname{IsColimit}$ applied to $x_{10}$.

Let $x_{10}$ be a pullback cone of $x_{9}$ and $x_{6}$. Assume that $x_{9}$ is equal to the second projection of $x_{8}$. Let $x_{11}$ be an element of $\operatorname{IsLimit}$ applied to $x_{8}$. Let $x_{12}$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{pasteVert}$ applied to $x_{8}$, $x_{10}$ and $h$. Then $\operatorname{topSquareIsPullback}$ applied to $x_{10}$, $h$, $x_{11}$ and $x_{12}$ is an element of $\operatorname{IsLimit}$ applied to $x_{10}$ defined as $\operatorname{isLimitOfFlip}$ applied to $\operatorname{leftSquareIsPullback}$ applied to the flip of $x_{10}$, $h$, the flip of $x_{11}$ and the flip of $x_{12}$.

the cocone of s (from the name)

Assume that $\operatorname{CommSq}$ holds for $f$, $g$, $h$ and $i$. Then the cocone of $s$ is a pushout cocone of $f$ and $g$ defined as $\operatorname{mk}$ applied to $h$, $i$ and $\operatorname{w}$ applied to $s$.

the cone of s (from the name)

Assume that $\operatorname{CommSq}$ holds for $f$, $g$, $h$ and $i$. Then the cone of $s$ is a pullback cone of $h$ and $i$ defined as $\operatorname{mk}$ applied to $f$, $g$ and $\operatorname{w}$ applied to $s$.

the cocone of t (from the name)

Let $t$ be a pushout cocone of the map of $F$ and the first component and the map of $F$ and the second component. Then the cocone of $t$ is a cocone of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $t$ and the composition of the homomorphism of the diagram isomorphism span of $F$ and the inclusion of $t$.

the cone of t (from the name)

Let $t$ be a pullback cone of the map of $F$ and the left arrow of the walking cospan and the map of $F$ and the right arrow of the walking cospan. Then the cone of $t$ is a cone of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $t$ and the composition of the projection of $t$ and the inverse of the diagram isomorphism cospan of $F$.

pullback cone 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 a pullback cone of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of cones of the cospan of $f$ and $g$.

the lift of h and k (from the name)

Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to $t$. Let $h$ be a homomorphism of $W$ and $X$. Let $k$ be a homomorphism of $W$ and $Y$ such that the composition of $h$ and $f$ is equal to the composition of $k$ and $g$. Then the lift of $h$ and $k$ is a homomorphism of $W$ and $\operatorname{pt}$ applied to $t$ defined as the lift of $\mathrm{ht}$ and $\operatorname{mk}$ applied to $h$, $k$ and $w$.

the lift of h and k (from the name)

Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to $t$. Let $h$ be a homomorphism of $W$ and $X$. Let $k$ be a homomorphism of $W$ and $Y$ such that $\EqtMACRoH {\operatorname{comp} (h , f)}{\operatorname{comp} (k , g)}$. Then the lift of $h$ and $k$ is an element of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (l , \operatorname{fst} (t))}{h}, \EqtMACRoH {\operatorname{comp} (l , \operatorname{snd} (t))}{k})}$ defined as the lift of $h$ and $k$.

Assume that the composition of $\mathrm{fst}$ and $f$ is equal to the composition of $\mathrm{snd}$ and $g$. Let $\mathrm{lift}$ be a function from pullback cones $s_{3}$ of $f$ and $g$ to homomorphisms of $\operatorname{pt}$ applied to $s_{3}$ and $W$ such that for all pullback cones $s_{2}$ of $f$ and $g$, the composition of $\mathrm{lift}$ applied to $s_{2}$ and $\mathrm{fst}$ is equal to the first projection of $s_{2}$, for all pullback cones $s_{1}$ of $f$ and $g$, the composition of $\mathrm{lift}$ applied to $s_{1}$ and $\mathrm{snd}$ is equal to the second projection of $s_{1}$ and for all pullback cones $s$ of $f$ and $g$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $s$ and $W$, if the composition of $m$ and $\mathrm{fst}$ is equal to the first projection of $s$, then if the composition of $m$ and $\mathrm{snd}$ is equal to the second projection of $s$, then $\EqtMACRoH {m}{\mathrm{lift} (s)}$. Then $\operatorname{mk}$ applied to $\mathrm{eq}$, $s_{3}$, $\mathrm{lift}$, $\mathrm{fac\_left}$, $\mathrm{fac\_right}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $\mathrm{fst}$, $\mathrm{snd}$ and $\mathrm{eq}$.

Let $t$ be a pullback cone of $f$ and $g$. Then $\operatorname{eta}$ applied to $t$ is an isomorphism of $t$ and $\operatorname{mk}$ applied to the first projection of $t$, the second projection of $t$ and $\operatorname{condition}$ applied to $t$.

the extension of i (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 first projection of $s$ is equal to the composition of the homomorphism of $i$ and the first projection of $t$ and $\mathrm{CategoryTheory\_\_Limits\_\_PullbackCone\_\_ext\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the second projection of $s$ is equal to the composition of the homomorphism of $i$ and the second projection of $t$ and $\mathrm{CategoryTheory\_\_Limits\_\_PullbackCone\_\_ext\_\_\_auto\_3}$. Then the extension of $i$ is an isomorphism of $s$ and $t$ defined as the extension of $i$.

the flip of t (from the name)

Let $t$ be a pullback cone of $f$ and $g$. Then the flip of $t$ is a pullback cone of $g$ and $f$.

the flip flip isomorphism of t (from the name)

Let $t$ be a pullback cone of $f$ and $g$. Then the flip flip isomorphism of $t$ is an isomorphism of the flip of the flip of $t$ and $t$.

the flip of ht (from the docstring)

Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then the flip of $\mathrm{ht}$ is an element of $\operatorname{IsLimit}$ applied to the flip of $t$.

the first projection of t (from the docstring)

Let $t$ be a pullback cone of $f$ and $g$. Then the first projection of $t$ is a homomorphism of $\operatorname{pt}$ applied to $t$ and $X$ defined as the component of the projection of $t$ and the left point of the walking cospan.

Let $t$ be a pullback cone of $f$ and $g$. Let $\mathrm{create}$ be a function from pullback cones $s$ of $f$ and $g$ to elements of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (l , \operatorname{fst} (t))}{\operatorname{fst} (s)}, \mathrm{and} (\EqtMACRoH {\operatorname{comp} (l , \operatorname{snd} (t))}{\operatorname{snd} (s)}, \mathrm{forall} (\operatorname{Hom} (\operatorname{pt} (s), \operatorname{pt} (t)), \lambda m . \mathrm{if} (\EqtMACRoH {\operatorname{comp} (m , \operatorname{fst} (t))}{\operatorname{fst} (s)}, \mathrm{if} (\EqtMACRoH {\operatorname{comp} (m , \operatorname{snd} (t))}{\operatorname{snd} (s)}, \EqtMACRoH {m}{l})))))}$. Then $\operatorname{isLimitAux'}$ applied to $t$, $s$ and $\mathrm{create}$ is an element of $\operatorname{IsLimit}$ applied to $t$.

Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to the flip of $t$. Then $\operatorname{isLimitOfFlip}$ applied to $\mathrm{ht}$ is an element of $\operatorname{IsLimit}$ applied to $t$ defined as $\operatorname{ofIsoLimit}$ applied to the flip of $\mathrm{ht}$ and the flip flip isomorphism of $t$.

the isomorphism of t (from the name)

Let $t$ be a cone of $F$. Then the isomorphism of $t$ is an isomorphism of the action of the postcomposition of the homomorphism of the diagram isomorphism cospan of $F$ and $t$ and $\operatorname{mk}$ applied to the component of the projection of $t$ and the left point of the walking cospan, the component of the projection of $t$ and the right point of the walking cospan and $\operatorname{trans}$ applied to $\operatorname{symm}$ applied to $\operatorname{naturality}$ applied to the projection of $t$ and the left arrow of the walking cospan and $\operatorname{naturality}$ applied to the projection of $t$ and the right arrow of the walking cospan.

Let $\mathrm{fst}$ be a homomorphism of $W$ and $X$. Let $\mathrm{snd}$ be a homomorphism of $W$ and $Y$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $\mathrm{fst}$ and $f$ is equal to the composition of $\mathrm{snd}$ and $g$ and $\mathrm{CategoryTheory\_\_Limits\_\_PullbackCone\_\_mk\_\_\_auto\_1}$. Then $\operatorname{mk}$ applied to $\mathrm{fst}$, $\mathrm{snd}$ and $\mathrm{eq}$ is a pullback cone of $f$ and $g$.

Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then $\operatorname{mkSelfIsLimit}$ applied to $\mathrm{ht}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the first projection of $t$, the second projection of $t$ and $\operatorname{condition}$ applied to $t$ defined as $\operatorname{ofIsoLimit}$ applied to $\mathrm{ht}$ and $\operatorname{eta}$ applied to $t$.

the pullback cone of t (from the name)

Let $t$ be a cone of $F$. Then the pullback cone of $t$ is a pullback cone of the map of $F$ and the left arrow of the walking cospan and the map of $F$ and the right arrow of the walking cospan defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $t$ and the composition of the projection of $t$ and the homomorphism of the diagram isomorphism cospan of $F$.

the second projection of t (from the docstring)

Let $t$ be a pullback cone of $f$ and $g$. Then the second projection of $t$ is a homomorphism of $\operatorname{pt}$ applied to $t$ and $Y$ defined as the component of the projection of $t$ and the right point of the walking cospan.

pushout cocone of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then a pushout cocone of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of cocones of the span of $f$ and $g$.

Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to $t$. Let $h$ be a homomorphism of $Y$ and $W$. Let $k$ be a homomorphism of $Z$ and $W$ such that the composition of $f$ and $h$ is equal to the composition of $g$ and $k$. Then $\operatorname{desc}$ applied to $\mathrm{ht}$, $h$, $k$ and $w$ is a homomorphism of $\operatorname{pt}$ applied to $t$ and $W$ defined as $\operatorname{desc}$ applied to $\mathrm{ht}$ and $\operatorname{mk}$ applied to $h$, $k$ and $w$.

Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to $t$. Let $h$ be a homomorphism of $Y$ and $W$. Let $k$ be a homomorphism of $Z$ and $W$ such that $\EqtMACRoH {\operatorname{comp} (f , h)}{\operatorname{comp} (g , k)}$. Then $\operatorname{desc'}$ applied to $\mathrm{ht}$, $h$, $k$ and $w$ is an element of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (\operatorname{inl} (t), l)}{h}, \EqtMACRoH {\operatorname{comp} (\operatorname{inr} (t), l)}{k})}$ defined as $\operatorname{desc}$ applied to $\mathrm{ht}$, $h$, $k$ and $w$.

Assume that the composition of $f$ and $\mathrm{inl}$ is equal to the composition of $g$ and $\mathrm{inr}$. Let $\mathrm{desc}$ be a function from pushout cocones $s_{3}$ of $f$ and $g$ to homomorphisms of $W$ and $\operatorname{pt}$ applied to $s_{3}$ such that for all pushout cocones $s_{2}$ of $f$ and $g$, the composition of $\mathrm{inl}$ and $\mathrm{desc}$ applied to $s_{2}$ is equal to the left injection of $s_{2}$, for all pushout cocones $s_{1}$ of $f$ and $g$, the composition of $\mathrm{inr}$ and $\mathrm{desc}$ applied to $s_{1}$ is equal to the right injection of $s_{1}$ and for all pushout cocones $s$ of $f$ and $g$, for all homomorphisms $m$ of $W$ and $\operatorname{pt}$ applied to $s$, if the composition of $\mathrm{inl}$ and $m$ is equal to the left injection of $s$, then if the composition of $\mathrm{inr}$ and $m$ is equal to the right injection of $s$, then $\EqtMACRoH {m}{\mathrm{desc} (s)}$. Then $\operatorname{mk}$ applied to $\mathrm{eq}$, $s_{3}$, $\mathrm{desc}$, $\mathrm{fac\_left}$, $\mathrm{fac\_right}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $\mathrm{inl}$, $\mathrm{inr}$ and $\mathrm{eq}$.

Let $t$ be a pushout cocone of $f$ and $g$. Then $\operatorname{eta}$ applied to $t$ is an isomorphism of $t$ and $\operatorname{mk}$ applied to the left injection of $t$, the right injection of $t$ and $\operatorname{condition}$ applied to $t$.

the extension of i (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 left injection of $s$ and the homomorphism of $i$ is equal to the left injection of $t$ and $\mathrm{CategoryTheory\_\_Limits\_\_PushoutCocone\_\_ext\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the right injection of $s$ and the homomorphism of $i$ is equal to the right injection of $t$ and $\mathrm{CategoryTheory\_\_Limits\_\_PushoutCocone\_\_ext\_\_\_auto\_3}$. Then the extension of $i$ is an isomorphism of $s$ and $t$ defined as the extension of $i$.

the flip of t (from the name)

Let $t$ be a pushout cocone of $f$ and $g$. Then the flip of $t$ is a pushout cocone of $g$ and $f$.

the flip flip isomorphism of t (from the name)

Let $t$ be a pushout cocone of $f$ and $g$. Then the flip flip isomorphism of $t$ is an isomorphism of the flip of the flip of $t$ and $t$.

the flip of ht (from the docstring)

Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then the flip of $\mathrm{ht}$ is an element of $\operatorname{IsColimit}$ applied to the flip of $t$.

the left injection of t (from the name)

Let $t$ be a pushout cocone of $f$ and $g$. Then the left injection of $t$ is a homomorphism of $Y$ and $\operatorname{pt}$ applied to $t$ defined as the component of the inclusion of $t$ and the left point of the walking span.

the right injection of t (from the name)

Let $t$ be a pushout cocone of $f$ and $g$. Then the right injection of $t$ is a homomorphism of $Z$ and $\operatorname{pt}$ applied to $t$ defined as the component of the inclusion of $t$ and the right point of the walking span.

Let $t$ be a pushout cocone of $f$ and $g$. Let $\mathrm{create}$ be a function from pushout cocones $s$ of $f$ and $g$ to elements of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (\operatorname{inl} (t), l)}{\operatorname{inl} (s)}, \mathrm{and} (\EqtMACRoH {\operatorname{comp} (\operatorname{inr} (t), l)}{\operatorname{inr} (s)}, \mathrm{forall} (\operatorname{Hom} (\operatorname{pt} (t), \operatorname{pt} (s)), \lambda m . \mathrm{if} (\EqtMACRoH {\operatorname{comp} (\operatorname{inl} (t), m)}{\operatorname{inl} (s)}, \mathrm{if} (\EqtMACRoH {\operatorname{comp} (\operatorname{inr} (t), m)}{\operatorname{inr} (s)}, \EqtMACRoH {m}{l})))))}$. Then $\operatorname{isColimitAux'}$ applied to $t$, $s$ and $\mathrm{create}$ is an element of $\operatorname{IsColimit}$ applied to $t$.

Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to the flip of $t$. Then $\operatorname{isColimitOfFlip}$ applied to $\mathrm{ht}$ is an element of $\operatorname{IsColimit}$ applied to $t$ defined as $\operatorname{ofIsoColimit}$ applied to the flip of $\mathrm{ht}$ and the flip flip isomorphism of $t$.

the isomorphism of t (from the name)

Let $t$ be a cocone of $F$. Then the isomorphism of $t$ is an isomorphism of the action of the precomposition of the inverse of the diagram isomorphism span of $F$ and $t$ and $\operatorname{mk}$ applied to the component of the inclusion of $t$ and the left point of the walking span, the component of the inclusion of $t$ and the right point of the walking span and $\operatorname{trans}$ applied to $\operatorname{naturality}$ applied to the inclusion of $t$ and the first component and $\operatorname{symm}$ applied to $\operatorname{naturality}$ applied to the inclusion of $t$ and the second component.

Let $\mathrm{inl}$ be a homomorphism of $Y$ and $W$. Let $\mathrm{inr}$ be a homomorphism of $Z$ and $W$ such that the composition of $f$ and $\mathrm{inl}$ is equal to the composition of $g$ and $\mathrm{inr}$. Then $\operatorname{mk}$ applied to $\mathrm{inl}$, $\mathrm{inr}$ and $\mathrm{eq}$ is a pushout cocone of $f$ and $g$.

Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then $\operatorname{mkSelfIsColimit}$ applied to $\mathrm{ht}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the left injection of $t$, the right injection of $t$ and $\operatorname{condition}$ applied to $t$ defined as $\operatorname{ofIsoColimit}$ applied to $\mathrm{ht}$ and $\operatorname{eta}$ applied to $t$.

the pushout cocone of t (from the name)

Let $t$ be a cocone of $F$. Then the pushout cocone of $t$ is a pushout cocone of the map of $F$ and the first component and the map of $F$ and the second component defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $t$ and the composition of the inverse of the diagram isomorphism span of $F$ and the inclusion of $t$.

the adjoint of x6 and x7 (from the name)

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $G$ be a functor of the set of opposites of $x$ and the set of functors of $x_{2}$ and $x_{1}$. Let $x_{6}$ be a parametrized adjunction of $F$ and $G$. Let $x_{7}$ be an arrow of $x$. Then the adjoint of $x_{6}$ and $x_{7}$ is an adjunction of the action of $\operatorname{leibnizPushout}$ applied to $F$ and $x_{7}$ and the action of $\operatorname{leibnizPullback}$ applied to $G$ and $\operatorname{op}$ applied to $x_{7}$.

pullback object object of x8 and x11 (from the name)

Let $G$ be a functor of the set of opposites of $x$ and the set of functors of $x_{2}$ and $x_{1}$. Let $x_{8}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{9}$ and $x_{10}$. Then the pullback object objects of $x_{8}$ and $x_{11}$ are a basic type.

the first projection of self (from the docstring)

Let $\mathrm{self}$ be a pullback object object of $x_{8}$ and $x_{11}$. Then the first projection of $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{self}$ and the action of the action of $G$ and $\operatorname{op}$ applied to $x_{6}$ and $x_{9}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the left map arrow of x10 and sq (from the name)

Let $x_{9}$ be a pullback object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{8}$. Let $x_{10}$ be a pullback object object of the homomorphism of $x_{7}$ and the homomorphism of $x_{8}$. Let $\mathrm{sq}$ be a homomorphism of $x_{7}$ and $x_{6}$. Then the left map arrow of $x_{10}$ and $\mathrm{sq}$ is a homomorphism of $\operatorname{mk}$ applied to the projection of $x_{9}$ and $\operatorname{mk}$ applied to the projection of $x_{10}$.

the right map arrow of x10 and sq (from the name)

Let $x_{9}$ be a pullback object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{7}$. Let $x_{10}$ be a pullback object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{8}$. Let $\mathrm{sq}$ be a homomorphism of $x_{7}$ and $x_{8}$. Then the right map arrow of $x_{10}$ and $\mathrm{sq}$ is a homomorphism of $\operatorname{mk}$ applied to the projection of $x_{9}$ and $\operatorname{mk}$ applied to the projection of $x_{10}$.

the pullback object object of x8 and x11 (from the name)

Let $G$ be a functor of the set of opposites of $x$ and the set of functors of $x_{2}$ and $x_{1}$. Let $x_{8}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{9}$ and $x_{10}$. Then the pullback object object of $x_{8}$ and $x_{11}$ is a pullback object object of $x_{8}$ and $x_{11}$.

the pullback object object of x11 and h2 (from the name)

Let $G$ be a functor of the set of opposites of $x$ and the set of functors of $x_{2}$ and $x_{1}$. Let $x_{8}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{9}$ and $x_{10}$. Let $h_{2}$ be an element of $\operatorname{IsInitial}$ applied to $x_{6}$. Then the pullback object object of $x_{11}$ and $h_{2}$ is a pullback object object of $x_{8}$ and $x_{11}$.

the pullback object object of x11 and h2 (from the name)

Let $G$ be a functor of the set of opposites of $x$ and the set of functors of $x_{2}$ and $x_{1}$. Let $x_{8}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{9}$ and $x_{10}$. Let $h_{2}$ be an element of $\operatorname{IsTerminal}$ applied to $x_{10}$. Then the pullback object object of $x_{11}$ and $h_{2}$ is a pullback object object of $x_{8}$ and $x_{11}$.

Let $\mathrm{self}$ be a pullback object object of $x_{8}$ and $x_{11}$. Then $\operatorname{pt}$ applied to $\mathrm{self}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the second projection of self (from the docstring)

Let $\mathrm{self}$ be a pullback object object of $x_{8}$ and $x_{11}$. Then the second projection of $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{self}$ and the action of the action of $G$ and $\operatorname{op}$ applied to $x_{7}$ and $x_{10}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the projection of self (from the name)

Let $\mathrm{self}$ be a pullback object object of $x_{8}$ and $x_{11}$. Then the projection of $\mathrm{self}$ is a homomorphism of the action of the action of $G$ and $\operatorname{op}$ applied to $x_{7}$ and $x_{9}$ and $\operatorname{pt}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

the projection isomorphism of x10 and iso (from the name)

Let $x_{9}$ be a pullback object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{8}$. Let $x_{10}$ be a pullback object object of the homomorphism of $x_{7}$ and the homomorphism of $x_{8}$. Let $\mathrm{iso}$ be an isomorphism of $x_{6}$ and $x_{7}$. Then the projection isomorphism of $x_{10}$ and $\mathrm{iso}$ is an isomorphism of $\operatorname{mk}$ applied to the projection of $x_{9}$ and $\operatorname{mk}$ applied to the projection of $x_{10}$.

the projection isomorphism of x10 and iso (from the name)

Let $x_{9}$ be a pullback object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{7}$. Let $x_{10}$ be a pullback object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{8}$. Let $\mathrm{iso}$ be an isomorphism of $x_{7}$ and $x_{8}$. Then the projection isomorphism of $x_{10}$ and $\mathrm{iso}$ is an isomorphism of $\operatorname{mk}$ applied to the projection of $x_{9}$ and $\operatorname{mk}$ applied to the projection of $x_{10}$.

pushout object object of x8 and x11 (from the name)

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $x_{8}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{9}$ and $x_{10}$. Then the pushout object objects of $x_{8}$ and $x_{11}$ are a basic type.

the flip of sq (from the name)

Let $\mathrm{sq}$ be a pushout object object of $x_{8}$ and $x_{11}$. Then the flip of $\mathrm{sq}$ is a pushout object object of $x_{11}$ and $x_{8}$.

the left injection of self (from the name)

Let $\mathrm{self}$ be a pushout object object of $x_{8}$ and $x_{11}$. Then the left injection of $\mathrm{self}$ is a homomorphism of the action of the action of $F$ and $x_{7}$ and $x_{9}$ and $\operatorname{pt}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the right injection of self (from the name)

Let $\mathrm{self}$ be a pushout object object of $x_{8}$ and $x_{11}$. Then the right injection of $\mathrm{self}$ is a homomorphism of the action of the action of $F$ and $x_{6}$ and $x_{10}$ and $\operatorname{pt}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the left map arrow of x10 and sq (from the name)

Let $x_{9}$ be a pushout object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{8}$. Let $x_{10}$ be a pushout object object of the homomorphism of $x_{7}$ and the homomorphism of $x_{8}$. Let $\mathrm{sq}$ be a homomorphism of $x_{6}$ and $x_{7}$. Then the left map arrow of $x_{10}$ and $\mathrm{sq}$ is a homomorphism of $\operatorname{mk}$ applied to the inclusion of $x_{9}$ and $\operatorname{mk}$ applied to the inclusion of $x_{10}$.

the right map arrow of x10 and sq (from the name)

Let $x_{9}$ be a pushout object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{7}$. Let $x_{10}$ be a pushout object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{8}$. Let $\mathrm{sq}$ be a homomorphism of $x_{7}$ and $x_{8}$. Then the right map arrow of $x_{10}$ and $\mathrm{sq}$ is a homomorphism of $\operatorname{mk}$ applied to the inclusion of $x_{9}$ and $\operatorname{mk}$ applied to the inclusion of $x_{10}$.

the pushout object object of x8 and x11 (from the name)

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $x_{8}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{9}$ and $x_{10}$. Then the pushout object object of $x_{8}$ and $x_{11}$ is a pushout object object of $x_{8}$ and $x_{11}$.

the pushout object object of x11 and h2 (from the name)

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $x_{8}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{9}$ and $x_{10}$. Let $h_{2}$ be an element of $\operatorname{IsInitial}$ applied to $x_{6}$. Then the pushout object object of $x_{11}$ and $h_{2}$ is a pushout object object of $x_{8}$ and $x_{11}$.

the pushout object object of x11 and h2 (from the name)

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $x_{8}$ be a homomorphism of $x_{6}$ and $x_{7}$. Let $x_{11}$ be a homomorphism of $x_{9}$ and $x_{10}$. Let $h_{2}$ be an element of $\operatorname{IsInitial}$ applied to $x_{9}$. Then the pushout object object of $x_{11}$ and $h_{2}$ is a pushout object object of $x_{8}$ and $x_{11}$.

the pushout object object of sq and e (from the name)

Let $\mathrm{sq}$ be a pushout object object of $x_{8}$ and $x_{11}$. Let $e$ be an isomorphism of $F$ and $\mathrm{F'}$. Then the pushout object object of $\mathrm{sq}$ and $e$ is a pushout object object of $x_{8}$ and $x_{11}$.

Let $\mathrm{self}$ be a pushout object object of $x_{8}$ and $x_{11}$. Then $\operatorname{pt}$ applied to $\mathrm{self}$ is an element of $x_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the inclusion of self (from the name)

Let $\mathrm{self}$ be a pushout object object of $x_{8}$ and $x_{11}$. Then the inclusion of $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{self}$ and the action of the action of $F$ and $x_{7}$ and $x_{10}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

the inclusion isomorphism of x10 and iso (from the name)

Let $x_{9}$ be a pushout object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{8}$. Let $x_{10}$ be a pushout object object of the homomorphism of $x_{7}$ and the homomorphism of $x_{8}$. Let $\mathrm{iso}$ be an isomorphism of $x_{6}$ and $x_{7}$. Then the inclusion isomorphism of $x_{10}$ and $\mathrm{iso}$ is an isomorphism of $\operatorname{mk}$ applied to the inclusion of $x_{9}$ and $\operatorname{mk}$ applied to the inclusion of $x_{10}$.

the inclusion isomorphism of x10 and iso (from the name)

Let $x_{9}$ be a pushout object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{7}$. Let $x_{10}$ be a pushout object object of the homomorphism of $x_{6}$ and the homomorphism of $x_{8}$. Let $\mathrm{iso}$ be an isomorphism of $x_{7}$ and $x_{8}$. Then the inclusion isomorphism of $x_{10}$ and $\mathrm{iso}$ is an isomorphism of $\operatorname{mk}$ applied to the inclusion of $x_{9}$ and $\operatorname{mk}$ applied to the inclusion of $x_{10}$.

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Let $G$ be a functor of the set of opposites of $x$ and the set of functors of $x_{2}$ and $x_{1}$. Let $x_{6}$ be a parametrized adjunction of $F$ and $G$. Then $\operatorname{leibnizAdjunction}$ applied to $F$, $G$ and $x_{6}$ is a parametrized adjunction of $\operatorname{leibnizPushout}$ applied to $F$ and $\operatorname{leibnizPullback}$ applied to $G$.

Let $G$ be a functor of the set of opposites of $x$ and the set of functors of $x_{2}$ and $x_{1}$. Then $\operatorname{leibnizPullback}$ applied to $G$ is a functor of the set of opposites of the set of arrows of $x$ and the set of functors of the set of arrows of $x_{2}$ and the set of arrows of $x_{1}$.

Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $x_{2}$. Then $\operatorname{leibnizPushout}$ applied to $F$ is a functor of the set of arrows of $x$ and the set of functors of the set of arrows of $x_{1}$ and the set of arrows of $x_{2}$.

sq is a pullback (from the name)

Let $\mathrm{sq}$ be a square of $C$. Then $\mathrm{sq}$ is a pullback, if $\operatorname{IsPullback}$ holds for $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2082\_}$ applied to $\mathrm{sq}$, $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2083\_}$ applied to $\mathrm{sq}$, $\mathrm{CategoryTheory\_\_Square\_\_f\_u2082\_\_u2084\_}$ applied to $\mathrm{sq}$ and $\mathrm{CategoryTheory\_\_Square\_\_f\_u2083\_\_u2084\_}$ applied to $\mathrm{sq}$.

Assume that $\mathrm{sq}$ is a pullback. Then $\operatorname{isLimit}$ applied to $h$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone attached to a commutative square of $\mathrm{sq}$ defined as $\operatorname{isLimit}$ applied to $h$.

sq is a pushout (from the name)

Let $\mathrm{sq}$ be a square of $C$. Then $\mathrm{sq}$ is a pushout, if $\operatorname{IsPushout}$ holds for $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2082\_}$ applied to $\mathrm{sq}$, $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2083\_}$ applied to $\mathrm{sq}$, $\mathrm{CategoryTheory\_\_Square\_\_f\_u2082\_\_u2084\_}$ applied to $\mathrm{sq}$ and $\mathrm{CategoryTheory\_\_Square\_\_f\_u2083\_\_u2084\_}$ applied to $\mathrm{sq}$.

Assume that $\mathrm{sq}$ is a pushout. Then $\operatorname{isColimit}$ applied to $h$ is an element of $\operatorname{IsColimit}$ applied to the pushout cocone attached to a commutative square of $\mathrm{sq}$ defined as $\operatorname{isColimit}$ applied to $h$.

the pullback cone attached to a commutative square of sq (from the docstring)

Let $\mathrm{sq}$ be a square of $C$. Then the pullback cone attached to a commutative square of $\mathrm{sq}$ is a pullback cone of $\mathrm{CategoryTheory\_\_Square\_\_f\_u2082\_\_u2084\_}$ applied to $\mathrm{sq}$ and $\mathrm{CategoryTheory\_\_Square\_\_f\_u2083\_\_u2084\_}$ applied to $\mathrm{sq}$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2082\_}$ applied to $\mathrm{sq}$, $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2083\_}$ applied to $\mathrm{sq}$ and $\operatorname{fac}$ applied to $\mathrm{sq}$.

the pushout cocone attached to a commutative square of sq (from the docstring)

Let $\mathrm{sq}$ be a square of $C$. Then the pushout cocone attached to a commutative square of $\mathrm{sq}$ is a pushout cocone of $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2082\_}$ applied to $\mathrm{sq}$ and $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2083\_}$ applied to $\mathrm{sq}$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_Square\_\_f\_u2082\_\_u2084\_}$ applied to $\mathrm{sq}$, $\mathrm{CategoryTheory\_\_Square\_\_f\_u2083\_\_u2084\_}$ applied to $\mathrm{sq}$ and $\operatorname{fac}$ applied to $\mathrm{sq}$.

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then we can say that $\operatorname{IsCoreflexivePair}$ holds for $f$ and $g$.

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then we can say that $\operatorname{IsReflexivePair}$ holds for $f$ and $g$.

C has coreflexive equalizers (from the name)

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

C has reflexive coequalizers (from the name)

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

reflexive cofork of F (from the name)

Let $F$ be a functor of the set of walking reflexive pairs and $C$. Then a reflexive cofork of $F$ is an element of the function that maps $F$ to the set of cocones of $F$.

Let $F$ be a functor of the set of walking reflexive pairs and $C$. Let $G$ be a reflexive cofork of $F$. Then $\operatorname{isColimitEquiv}$ applied to $F$ and $G$ is an equivalence from $\operatorname{IsColimit}$ applied to the cofork of $G$ to $\operatorname{IsColimit}$ applied to $G$ defined as the composition of the equivalence isomorphism colimit of the inverse of the reflexive cofork equivalence cofork object isomorphism of $F$ and $G$ and the composition of the precomposition homomorphism equivalence of the inverse of the diagram isomorphism parallel pair of the composition of the inclusion walking reflexive pair and $F$ and the whisker of the inclusion walking reflexive pair and $G$ and $\operatorname{isColimitWhiskerEquiv}$ applied to the inclusion walking reflexive pair and $G$.

Let $x_{1}$ be a homomorphism of the action of $F$ and the zero and $X$ such that the composition of the map of $F$ and the left and $x_{1}$ is equal to the composition of the map of $F$ and the right and $x_{1}$. Then $\operatorname{mk}$ applied to $x_{1}$ and $h$ is a reflexive cofork of $F$.

the cofork of G (from the name)

Let $G$ be a reflexive cofork of $F$. Then the cofork of $G$ is a cofork of the map of $F$ and the left and the map of $F$ and the right.

the projection of G (from the name)

Let $G$ be a reflexive cofork of $F$. Then the projection of $G$ is a homomorphism of the action of $F$ and the zero and $\operatorname{pt}$ applied to $G$ defined as the component of the inclusion of $G$ and the zero.

the inclusion walking reflexive pair (from the name)

The inclusion walking reflexive pair is a functor of the set of walking parallel pairs and the set of walking reflexive pairs.

walking reflexive pair (from the name)

The walking reflexive pairs are a basic type.

homomorphism of x and x1 (from the name)

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

the composition of x and x1 (from the name)

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

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the one, the zero 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 one, the zero and the right and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero, the one and the reflexion and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the one, the one and the left composition reflexion and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $4$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the one, the one and the right composition reflexion and $\mathrm{PULift}$ applied to the set of functions from walking reflexive 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 reflexive pair. Then the identity of $X$ is a homomorphism of $X$ and $X$.

the left (from the name)

The left is a homomorphism of the one and the zero.

the left composition reflexion (from the name)

The left composition reflexion is a homomorphism of the one and the one.

the reflexion (from the name)

The reflexion is a homomorphism of the zero and the one.

the right (from the name)

The right is a homomorphism of the one and the zero.

the right composition reflexion (from the name)

The right composition reflexion is a homomorphism of the one and the one.

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 reflexive pair of x (from the name)

Let $x$ be a natural number. Then the walking reflexive pair of $x$ is a walking reflexive 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 reflexive pair.

the zero (from the name)

The zero is a walking reflexive pair.

the coequalizer (from the docstring)

The coequalizer is an isomorphism of the colimit of the limit of $f$ and $g$ and the coequalizer of $f$ and $g$ defined as the reflexive coequalizer isomorphism coequalizer of the limit of $f$ and $g$.

the inclusion walking reflexive pair of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then the inclusion walking reflexive pair of $f$ and $g$ is an isomorphism of the composition of the inclusion walking reflexive pair and the limit of $f$ and $g$ and the parallel pair of $f$ and $g$ defined as the diagram isomorphism parallel pair of the composition of the inclusion walking reflexive pair and the limit of $f$ and $g$.

the default (from the name)

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

the limit of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then the limit of $f$ and $g$ is a functor of the set of walking reflexive pairs and $C$.

the reflexive coequalizer isomorphism coequalizer of F (from the name)

Let $F$ be a functor of the set of walking reflexive pairs and $C$. Then the reflexive coequalizer isomorphism coequalizer of $F$ is an isomorphism of the colimit of $F$ and the coequalizer of the map of $F$ and the left and the map of $F$ and the right defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{symm}$ applied to $\operatorname{isColimitEquiv}$ applied to $F$ and the cocone of $F$ and $\operatorname{isColimit}$ applied to $F$ and $\operatorname{isColimit}$ applied to the parallel pair of the map of $F$ and the left and the map of $F$ and the right.

the reflexive cofork equivalence cofork of F (from the name)

Let $F$ be a functor of the set of walking reflexive pairs and $C$. Then the reflexive cofork equivalence cofork of $F$ is an equivalence of the set of reflexive coforks of $F$ and the set of coforks of the map of $F$ and the left and the map of $F$ and the right defined as the composition of the inverse of the cocone equivalence of the inclusion walking reflexive pair and $F$ and the precomposition equivalence of the diagram isomorphism parallel pair of the composition of the inclusion walking reflexive pair and $F$.

the reflexive cofork equivalence cofork object isomorphism of F and G (from the name)

Let $F$ be a functor of the set of walking reflexive pairs and $C$. Let $G$ be a reflexive cofork of $F$. Then the reflexive cofork equivalence cofork object isomorphism of $F$ and $G$ is an isomorphism of the action of the functor of the reflexive cofork equivalence cofork of $F$ and $G$ and the cofork of $G$.

the reflexive pair of g and s (from the name)

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Let $s$ be a homomorphism of $B$ and $A$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $s$ and $f$ is equal to the identity morphism of $B$ and $\mathrm{CategoryTheory\_\_Limits\_\_reflexivePair\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of $s$ and $g$ is equal to the identity morphism of $B$ and $\mathrm{CategoryTheory\_\_Limits\_\_reflexivePair\_\_\_auto\_3}$. Then the reflexive pair of $g$ and $s$ is a functor of the set of walking reflexive pairs and $C$.

the composition right isomorphism of s and F (from the name)

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Let $s$ be a homomorphism of $B$ and $A$ such that the composition of $s$ and $f$ is equal to the identity morphism of $B$ and the composition of $s$ and $g$ is equal to the identity morphism of $B$. Let $F$ be a functor of $C$ and $D$. Then the composition right isomorphism of $s$ and $F$ is an isomorphism of the composition of the reflexive pair of $g$ and $s$ and $F$ and the reflexive pair of the map of $F$ and $g$ and the map of $F$ and $s$.

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

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

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

Let $x_{1}$ be an isomorphism of the action of $F$ and the zero and the action of $G$ and the zero. Let $x_{2}$ 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 $x_{1}$ is equal to the composition of the homomorphism of $x_{2}$ and the map of $G$ and the left and $\mathrm{CategoryTheory\_\_Limits\_\_reflexivePair\_\_mkNatIso\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the right and the homomorphism of $x_{1}$ is equal to the composition of the homomorphism of $x_{2}$ and the map of $G$ and the right and $\mathrm{CategoryTheory\_\_Limits\_\_reflexivePair\_\_mkNatIso\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the reflexion and the homomorphism of $x_{2}$ is equal to the composition of the homomorphism of $x_{1}$ and the map of $G$ and the reflexion and $\mathrm{CategoryTheory\_\_Limits\_\_reflexivePair\_\_mkNatIso\_\_\_auto\_5}$. Then the natural isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of $F$ and $G$.

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

Let $x_{1}$ be a homomorphism of the action of $F$ and the zero and the action of $G$ and the zero. Let $x_{2}$ 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 $x_{1}$ is equal to the composition of $x_{2}$ and the map of $G$ and the left and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Limits\_\_Shapes\_\_Reflexive\_\_0\_\_\_auto\_143}$, $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the right and $x_{1}$ is equal to the composition of $x_{2}$ and the map of $G$ and the right and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Limits\_\_Shapes\_\_Reflexive\_\_0\_\_\_auto\_145}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the reflexion and $x_{2}$ is equal to the composition of $x_{1}$ and the map of $G$ and the reflexion and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Limits\_\_Shapes\_\_Reflexive\_\_0\_\_\_auto\_147}$. Then the natural transformation of $x_{1}$ and $x_{2}$ is a homomorphism of $F$ and $G$.

the common retraction of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then the common retraction of $f$ and $g$ is a homomorphism of $B$ and $A$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_IsCoreflexivePair\_\_common\_retraction}$ applied to $f$ and $g$.

the common section of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then the common section of $f$ and $g$ is a homomorphism of $B$ and $A$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_IsReflexivePair\_\_common\_section}$ applied to $f$ and $g$.

the regular epimorphism of h (from the name)

Let $h$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the regular epimorphism of $h$ is a regular epimorphism of the projection of $c$ defined as $\operatorname{mk}$ applied to $A$, $x_{1}$, $x_{2}$, $\operatorname{condition}$ applied to $c$ and $\operatorname{ofIsoColimit}$ applied to $h$ and the isomorphism cofork of $c$.

Let $\mathrm{hp}$ be an element of $\operatorname{EffectiveEpiStruct}$ applied to $p$. Assume that $\operatorname{IsPullback}$ holds for $x_{1}$, $x_{2}$, $p$ and $p$. Then $\operatorname{isColimitCoforkOfIsPullback}$ applied to $\mathrm{hp}$ and $\mathrm{sq}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $p$ and $\operatorname{w}$ applied to $\operatorname{toCommSq}$ applied to $\mathrm{sq}$.

the regular monomorphism of h (from the name)

Let $h$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the regular monomorphism of $h$ is a regular monomorphism of the inclusion of $c$ defined as $\operatorname{mk}$ applied to $B$, $x_{1}$, $x_{2}$, $\operatorname{condition}$ applied to $c$ and $\operatorname{ofIsoLimit}$ applied to $h$ and the isomorphism fork of $c$.

f is a regular epimorphism (from the name)

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

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

Let $f$ be a homomorphism of $X$ and $Y$. Let $k$ be a homomorphism of $X$ and $Z$ such that the composition of the left of $f$ and $k$ is equal to the composition of the right of $f$ and $k$. Then $\operatorname{desc}$ applied to $f$, $k$ and $h_{1}$ is a homomorphism of $Y$ and $Z$ defined as $\operatorname{desc}$ applied to $\operatorname{isColimit}$ applied to $f$, $k$ and $h_{1}$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{getStruct}$ applied to $f$ is a regular epimorphism of $f$ defined as $\operatorname{some}$ applied to $\operatorname{regularEpi}$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isColimit}$ applied to $f$ is an element of $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{w}$ applied to $f$ defined as $\operatorname{isColimit}$ applied to $\operatorname{getStruct}$ applied to $f$.

the left of f (from the name)

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

the right of f (from the name)

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

C is a regular epimorphism category (from the name)

Let $C$ be a set. Then we can say that $C$ is a regular epimorphism category.

f is a regular monomorphism (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is a regular monomorphism.

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

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{getStruct}$ applied to $f$ is a regular monomorphism of $f$ defined as $\operatorname{some}$ applied to $\operatorname{regularMono}$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isLimit}$ applied to $f$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $f$ and $\operatorname{w}$ applied to $f$ defined as $\operatorname{isLimit}$ applied to $\operatorname{getStruct}$ applied to $f$.

the left of f (from the name)

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

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 $Y$ such that the composition of $k$ and the left of $f$ is equal to the composition of $k$ and the right of $f$. Then the lift of $f$ and $k$ is a homomorphism of $W$ and $X$ defined as the lift of $\operatorname{isLimit}$ applied to $f$ and $k$.

the right of f (from the name)

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

C is a regular monomorphism category (from the name)

Let $C$ be a set. Then we can say that $C$ is a regular monomorphism category.

the regular epimorphism of C (from the name)

Let $C$ be a set. Then the regular epimorphism of $C$ is a morphism property of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to the proposition that $f$ is a regular epimorphism.

the regular monomorphism of C (from the name)

Let $C$ be a set. Then the regular monomorphism of $C$ is a morphism property of $C$ defined as the function that maps $x_{1}$, $x_{2}$ and $f$ to the proposition that $f$ is a regular monomorphism.

regular epimorphism of f (from the name)

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

Let $\mathrm{self}$ be a regular epimorphism of $f$. Then $\operatorname{W}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{hf}$ be a regular epimorphism of $f$. Let $k$ be a homomorphism of $X$ and $W$ such that $\EqtMACRoH {\operatorname{comp} (\operatorname{left} (\mathrm{hf}), k)}{\operatorname{comp} (\operatorname{right} (\mathrm{hf}), k)}$. Then $\operatorname{desc'}$ applied to $\mathrm{hf}$, $k$ and $h$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (f , l)}{k})}$ defined as $\operatorname{desc'}$ applied to $\operatorname{isColimit}$ applied to $\mathrm{hf}$, $k$ and $h$.

Let $\mathrm{self}$ be a regular epimorphism of $f$. Then $\operatorname{isColimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{w}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

the left of self (from the name)

Let $\mathrm{self}$ be a regular epimorphism of $f$. Then the left of $\mathrm{self}$ is a homomorphism of $\operatorname{W}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the regular epimorphism of e and h (from the name)

Let $e$ be an isomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $g$. Let $h$ be a regular epimorphism of $f$. Then the regular epimorphism of $e$ and $h$ is a regular epimorphism of $g$.

the regular epimorphism of e (from the name)

Let $e$ be an isomorphism of $X$ and $Y$. Then the regular epimorphism of $e$ is a regular epimorphism of the homomorphism of $e$.

the regular epimorphism of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the regular epimorphism of $f$ is a regular epimorphism of $f$.

the opposite of hf (from the name)

Let $\mathrm{hf}$ be a regular epimorphism of $f$. Then the opposite of $\mathrm{hf}$ is a regular monomorphism of the opposite in $f$.

the right of self (from the name)

Let $\mathrm{self}$ be a regular epimorphism of $f$. Then the right of $\mathrm{self}$ is a homomorphism of $\operatorname{W}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the opposite of hf (from the name)

Let $\mathrm{hf}$ be a regular epimorphism of $f$. Then the opposite of $\mathrm{hf}$ is a regular monomorphism of the opposite of $f$.

regular monomorphism of f (from the name)

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

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

the chosen equalizer of g and h (from the docstring)

Let $g$ and $h$ be homomorphisms of $X$ and $Y$. Then the chosen equalizer of $g$ and $h$ is a regular monomorphism of the inclusion of $g$ and $h$.

Let $\mathrm{self}$ be a regular monomorphism of $f$. Then $\operatorname{isLimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $f$ and $\operatorname{w}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

the left of self (from the name)

Let $\mathrm{self}$ be a regular monomorphism of $f$. Then the left of $\mathrm{self}$ is a homomorphism of $Y$ and $\operatorname{Z}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the lift of hf and k (from the name)

Let $\mathrm{hf}$ be a regular monomorphism of $f$. Let $k$ be a homomorphism of $W$ and $Y$ such that $\EqtMACRoH {\operatorname{comp} (k , \operatorname{left} (\mathrm{hf}))}{\operatorname{comp} (k , \operatorname{right} (\mathrm{hf}))}$. Then the lift of $\mathrm{hf}$ and $k$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , f)}{k})}$ defined as the lift of $\operatorname{isLimit}$ applied to $\mathrm{hf}$ and $k$.

the regular monomorphism of e and h (from the name)

Let $e$ be an isomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $g$. Let $h$ be a regular monomorphism of $f$. Then the regular monomorphism of $e$ and $h$ is a regular monomorphism of $g$.

the regular monomorphism of f (from the name)

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

the regular monomorphism of e (from the name)

Let $e$ be an isomorphism of $X$ and $Y$. Then the regular monomorphism of $e$ is a regular monomorphism of the homomorphism of $e$.

the opposite of hf (from the name)

Let $\mathrm{hf}$ be a regular monomorphism of $f$. Then the opposite of $\mathrm{hf}$ is a regular epimorphism of the opposite in $f$.

the right of self (from the name)

Let $\mathrm{self}$ be a regular monomorphism of $f$. Then the right of $\mathrm{self}$ is a homomorphism of $Y$ and $\operatorname{Z}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the opposite of hf (from the name)

Let $\mathrm{hf}$ be a regular monomorphism of $f$. Then the opposite of $\mathrm{hf}$ is a regular epimorphism of the opposite of $f$.

the chosen coequalizer of g and h (from the docstring)

Let $g$ and $h$ be homomorphisms of $X$ and $Y$. Then the chosen coequalizer of $g$ and $h$ is a regular epimorphism of the projection of $g$ and $h$.

Let $\mathrm{hf}$ be a regular epimorphism of $f$. Then $\operatorname{effectiveEpiStructOfRegularEpi}$ applied to $\mathrm{hf}$ is an element of $\operatorname{EffectiveEpiStruct}$ applied to $f$.

Let $f$ be a homomorphism of $X$ and $B$. Let $c$ be a pullback cone of $f$ and $f$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isColimitCoforkOfEffectiveEpi}$ applied to $f$, $c$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{condition}$ applied to $c$.

the regular epimorphism of f (from the name)

Let $f$ be a homomorphism of $X$ and $B$. Then the regular epimorphism of $f$ is a regular epimorphism of $f$ defined as $\operatorname{mk}$ applied to the pullback of $f$ and $f$, the first projection of the pullback of $f$ and $f$, the second projection of the pullback of $f$ and $f$, $\operatorname{condition}$ and $\operatorname{isColimitCoforkOfEffectiveEpi}$ applied to $f$, the cone of the cospan of $f$ and $f$ and $\operatorname{isLimit}$ applied to $f$ and $f$.

the regular epimorphism of f (from the name)

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

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

Let $f$ be a homomorphism of $X$ and $B$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{condition}$. Then the regular epimorphism of $f$ and $\mathrm{hc}$ is a regular epimorphism of $f$ defined as $\operatorname{mk}$ applied to the pullback of $f$ and $f$, the first projection of the pullback of $f$ and $f$, the second projection of the pullback of $f$ and $f$, $\operatorname{condition}$ and $\mathrm{hc}$.

the regular monomorphism of f (from the name)

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

the regular of hk and t (from the name)

Let $\mathrm{hk}$ be a regular monomorphism of $k$. Assume that the composition of $f$ and $h$ is equal to the composition of $g$ and $k$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $f$, $g$ and $\mathrm{comm}$. Then the regular of $\mathrm{hk}$ and $t$ is a regular monomorphism of $f$.

the regular of hr and t (from the name)

Let $\mathrm{hr}$ be a regular monomorphism of $h$. Assume that the composition of $f$ and $h$ is equal to the composition of $g$ and $k$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $f$, $g$ and $\mathrm{comm}$. Then the regular of $\mathrm{hr}$ and $t$ is a regular monomorphism of $g$.

the regular of hf and t (from the name)

Let $\mathrm{hf}$ be a regular epimorphism of $f$. Assume that the composition of $f$ and $h$ is equal to the composition of $g$ and $k$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{comm}$. Then the regular of $\mathrm{hf}$ and $t$ is a regular epimorphism of $k$.

the regular of gr and t (from the name)

Let $\mathrm{gr}$ be a regular epimorphism of $g$. Assume that the composition of $f$ and $h$ is equal to the composition of $g$ and $k$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{comm}$. Then the regular of $\mathrm{gr}$ and $t$ is a regular epimorphism of $h$.

the cone over the tower of f (from the docstring)

Let $f$ be a function from natural numbers $n$ to homomorphisms of $M$ applied to $n$ and $N$ applied to $n$. Then the cone over the tower of $n$ is a cone of the functor of $\operatorname{functorMap}$ applied to $f$.

the functor map of f and n1 (from the name)

Let $f$ be a function from natural numbers $n_{1}$ to homomorphisms of $M$ applied to $n_{1}$ and $N$ applied to $n_{1}$. Let $n$ be a natural number. Then the functor map of $n_{1}$ and $f$ is a homomorphism of the functor object of $N$ and $n + 1$ and the functor object of $N$ and $n$.

the functor object of N and x1 (from the name)

Let $M$ and $N$ be functions from natural numbers to elements of $C$. Let $x_{1}$ be a natural number. Then the functor object of $N$ and $x_{1}$ is an element of $C$ defined as the product object of the function that maps $m$ to $\mathrm{dite}$ applied to $\mathrm{Lt} (m , x_{1})$, the function that maps $h_{1}$ to $M$ applied to $m$ and the function that maps $h_{2}$ to $N$ applied to $m$.

the functor object projection negation of n and m (from the name)

Let $n$ and $m$ be natural numbers such that $m$ is not less than $n$. Then the functor object projection negation of $n$ and $m$ is a homomorphism of the functor object of $N$ and $n$ and $N$ applied to $m$.

the functor object projection positive part of n and m (from the name)

Let $n$ and $m$ be natural numbers such that $m < n$. Then the functor object projection positive part of $n$ and $m$ is a homomorphism of the functor object of $N$ and $n$ and $M$ applied to $m$.

Let $f$ be a function from natural numbers $n$ to homomorphisms of $M$ applied to $n$ and $N$ applied to $n$. Then $\operatorname{isLimit}$ applied to $n$ and $f$ is an element of $\operatorname{IsLimit}$ applied to the cone over the tower of $f$.

the colimit of J (from the docstring)

Let $J$ be a functor of the set of single objects of $G$ and the set of sets. Then the colimit of $J$ is an equivalence from the colimit of $J$ to the set of quotients of $G$ and the action of $J$ and the star of $G$ defined as the composition of the colimit equivalence colimit type of $J$ and the explicit quotient construction of the colimit of $J$.

the limit of J (from the docstring)

Let $J$ be a functor of the set of single objects of $M$ and the set of sets. Then the limit of $J$ is an equivalence from the limit of $J$ to the set of elements of the fixed point of $M$ and the action of $J$ and the star of $M$ defined as the composition of the limit equivalence section of $J$ and the equivalence fixed point of $J$.

the equivalence fixed point of J (from the name)

Let $J$ be a functor of the set of single objects of $M$ and the set of sets. Then the equivalence fixed point of $J$ is an equivalence from the set of elements of the section of $J$ to the set of elements of the fixed point of $M$ and the action of $J$ and the star of $M$.

the explicit quotient construction of the colimit of J (from the docstring)

Let $J$ be a functor of the set of single objects of $G$ and the set of sets. Then the explicit quotient construction of the colimit of $J$ is an equivalence from the set of colimit types of $J$ to the set of quotients of $G$ and the action of $J$ and the star of $G$.

Let $G$ be a functor of $C$ and $D$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then $\operatorname{IsSplitPair}$ holds for $G$, $f$ and $g$, if $\operatorname{HasSplitCoequalizer}$ holds for the map of $G$ and $f$ and the map of $G$ and $g$.

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then we can say that $\operatorname{HasSplitCoequalizer}$ holds for $f$ and $g$.

the coequalizer of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the coequalizer of $f$ and $g$ is an element of $C$ defined as $\operatorname{choose}$ applied to $\operatorname{splittable}$.

the coequalizer projection of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the coequalizer projection of $f$ and $g$ is a homomorphism of $Y$ and the coequalizer of $f$ and $g$.

the coequalizer morphism of f and g (from the docstring)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the coequalizer morphism of $f$ and $g$ is an element of $\operatorname{IsSplitCoequalizer}$ applied to $f$, $g$ and the coequalizer projection of $f$ and $g$.

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Let $x_{1}$ be a homomorphism of $Y$ and $Z$. Then the elements of $\operatorname{IsSplitCoequalizer}$ applied to $f$, $g$ and $x_{1}$ are a basic type.

Let $t$ be an element of $\operatorname{IsSplitCoequalizer}$ applied to $f$, $g$ and $h$. Then $\operatorname{asCofork}$ applied to $t$ is a cofork of $f$ and $g$ defined as the projection of $h$ and $\operatorname{condition}$ applied to $t$.

the cofork induced by a split coequalizer of t (from the docstring)

Let $t$ be an element of $\operatorname{IsSplitCoequalizer}$ applied to $f$, $g$ and $h$. Then the cofork induced by a split coequalizer of $t$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{asCofork}$ applied to $t$ defined as $\operatorname{mk'}$ applied to $\operatorname{asCofork}$ applied to $t$ and the function that maps $s$ to the composition of the right section of $t$ and the projection of $s$.

the left section of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{IsSplitCoequalizer}$ applied to $f$, $g$ and $x_{1}$. Then the left section of $\mathrm{self}$ is a homomorphism of $Y$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the map of q and F (from the name)

Let $q$ be an element of $\operatorname{IsSplitCoequalizer}$ applied to $f$, $g$ and $x_{2}$. Let $F$ be a functor of $C$ and $D$. Then the map of $q$ and $F$ is an element of $\operatorname{IsSplitCoequalizer}$ applied to the map of $F$ and $f$, the map of $F$ and $g$ and the map of $F$ and $x_{2}$.

the right section of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{IsSplitCoequalizer}$ applied to $f$, $g$ and $x_{1}$. Then the right section of $\mathrm{self}$ is a homomorphism of $Z$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $G$ be a functor of $C$ and $D$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then $\operatorname{IsCosplitPair}$ holds for $G$, $f$ and $g$, if $\operatorname{HasSplitEqualizer}$ holds for the map of $G$ and $f$ and the map of $G$ and $g$.

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then we can say that $\operatorname{HasSplitEqualizer}$ holds for $f$ and $g$.

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 $\operatorname{choose}$ applied to $\operatorname{splittable}$.

the equalizer inclusion of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the equalizer inclusion of $f$ and $g$ is a homomorphism of the equalizer of $f$ and $g$ and $X$.

the equalizer morphism of f and g (from the docstring)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the equalizer morphism of $f$ and $g$ is an element of $\operatorname{IsSplitEqualizer}$ applied to $f$, $g$ and the equalizer inclusion of $f$ and $g$.

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Let $x_{1}$ be a homomorphism of $W$ and $X$. Then the elements of $\operatorname{IsSplitEqualizer}$ applied to $f$, $g$ and $x_{1}$ are a basic type.

Let $t$ be an element of $\operatorname{IsSplitEqualizer}$ applied to $f$, $g$ and $h$. Then $\operatorname{asFork}$ applied to $t$ is a fork of $f$ and $g$ defined as the inclusion of $h$ and $\operatorname{condition}$ applied to $t$.

the fork induced by a split equalizer of t (from the docstring)

Let $t$ be an element of $\operatorname{IsSplitEqualizer}$ applied to $f$, $g$ and $h$. Then the fork induced by a split equalizer of $t$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{asFork}$ applied to $t$ defined as $\operatorname{mk'}$ applied to $\operatorname{asFork}$ applied to $t$ and the function that maps $s$ to the composition of the inclusion of $s$ and the left retraction of $t$.

the left retraction of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{IsSplitEqualizer}$ applied to $f$, $g$ and $x_{1}$. Then the left retraction of $\mathrm{self}$ is a homomorphism of $X$ and $W$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the map of q and F (from the name)

Let $q$ be an element of $\operatorname{IsSplitEqualizer}$ applied to $f$, $g$ and $x_{2}$. Let $F$ be a functor of $C$ and $D$. Then the map of $q$ and $F$ is an element of $\operatorname{IsSplitEqualizer}$ applied to the map of $F$ and $f$, the map of $F$ and $g$ and the map of $F$ and $x_{2}$.

the right retraction of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{IsSplitEqualizer}$ applied to $f$, $g$ and $x_{1}$. Then the right retraction of $\mathrm{self}$ is a homomorphism of $Y$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

C has strict initial objects (from the name)

Let $C$ be a set. Then we can say that $C$ has strict initial objects.

C has strict terminal objects (from the name)

Let $C$ be a set. Then we can say that $C$ has strict terminal objects.

Let $f$ be a homomorphism of $X$ and $Y$. Let $\mathrm{hY}$ be an element of $\operatorname{IsInitial}$ applied to $Y$. Then $\operatorname{ofStrict}$ applied to $f$ and $\mathrm{hY}$ is an element of $\operatorname{IsInitial}$ applied to $X$ defined as $\operatorname{ofIso}$ applied to $\mathrm{hY}$ and the inverse of $\operatorname{asIso}$ applied to $f$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $\mathrm{hY}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then $\operatorname{ofStrict}$ applied to $f$ and $\mathrm{hY}$ is an element of $\operatorname{IsTerminal}$ applied to $Y$ defined as $\operatorname{ofIso}$ applied to $\mathrm{hY}$ and $\operatorname{asIso}$ applied to $f$.

the initial product of X (from the name)

Let $X$ be an element of $C$. Then the initial product of $X$ is an isomorphism of the product of $\operatorname{initial}$ applied to $C$ and $X$ and $\operatorname{initial}$ applied to $C$ defined as $\operatorname{isInitialMul}$ applied to $X$ and $\operatorname{initialIsInitial}$.

Let $X$ be an element of $C$. Let $\mathrm{hI}$ be an element of $\operatorname{IsInitial}$ applied to $I$. Then $\operatorname{isInitialMul}$ applied to $X$ and $\mathrm{hI}$ is an isomorphism of the product of $I$ and $X$ and $I$ defined as $\operatorname{asIso}$ applied to the projection map to the first component of the product.

Let $X$ be an element of $C$. Then $\operatorname{mulInitial}$ applied to $X$ is an isomorphism of the product of $X$ and $\operatorname{initial}$ applied to $C$ and $\operatorname{initial}$ applied to $C$ defined as $\operatorname{mulIsInitial}$ applied to $X$ and $\operatorname{initialIsInitial}$.

Let $X$ be an element of $C$. Let $\mathrm{hI}$ be an element of $\operatorname{IsInitial}$ applied to $I$. Then $\operatorname{mulIsInitial}$ applied to $X$ and $\mathrm{hI}$ is an isomorphism of the product of $X$ and $I$ and $I$ defined as $\operatorname{asIso}$ applied to the projection map to the second component of the product.

f is a strong epimorphism (from the name)

Let $f$ be a homomorphism of $P$ and $Q$. Then we can say that $f$ is a strong epimorphism.

C is a strong epimorphism category (from the name)

Let $C$ be a set. Then we can say that $C$ is a strong epimorphism category.

f is a strong monomorphism (from the name)

Let $f$ be a homomorphism of $P$ and $Q$. Then we can say that $f$ is a strong monomorphism.

C is a strong monomorphism category (from the name)

Let $C$ be a set. Then we can say that $C$ is a strong monomorphism category.

Let $C$ be a set. Then $\operatorname{HasInitial}$ holds for $C$, if $\operatorname{HasColimitsOfShape}$ holds for $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $C$.

C has terminals (from the name)

Let $C$ be a set. Then $C$ has terminals, if $\operatorname{HasLimitsOfShape}$ holds for $\operatorname{Discrete}$ applied to $\mathrm{PEmpty}$ and $C$.

the colimit of the constant (from the docstring)

The colimit of the constant is an isomorphism of the colimit of the action of the constant of $J$ and $\operatorname{initial}$ applied to $C$ and $\operatorname{initial}$ applied to $C$.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the colimit of $F$ is an isomorphism of the colimit of $F$ and the action of $F$ and $\operatorname{initial}$ applied to $J$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to $F$ and the colimit of $\operatorname{initialIsInitial}$ and $F$.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the colimit of $F$ is an isomorphism of the colimit of $F$ and the action of $F$ and $\operatorname{terminal}$ applied to $J$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to $F$ and the colimit of $\operatorname{terminalIsTerminal}$ and $F$.

Let $C$ be a set. Then $\operatorname{initial}$ applied to $C$ is an element of $C$ defined as the colimit of $\operatorname{empty}$ applied to $C$.

Let $P$ be an element of $C$. Then $\operatorname{to}$ applied to $P$ is a homomorphism of $\operatorname{initial}$ applied to $C$ and $P$ defined as $\operatorname{desc}$ applied to $\operatorname{empty}$ applied to $C$ and $\operatorname{asEmptyCocone}$ applied to $P$.

the initial comparison of G (from the name)

Let $G$ be a functor of $C$ and $D$. Then the initial comparison of $G$ is a homomorphism of $\operatorname{initial}$ applied to $D$ and the action of $G$ and $\operatorname{initial}$ applied to $C$ defined as $\operatorname{to}$ applied to the action of $G$ and $\operatorname{initial}$ applied to $C$.

$\operatorname{initialIsInitial}$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{initial}$ applied to $C$.

Let $t$ be an element of $\operatorname{IsInitial}$ applied to $P$. Then $\operatorname{initialIsoIsInitial}$ applied to $t$ is an isomorphism of $\operatorname{initial}$ applied to $C$ and $P$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{initialIsInitial}$ and $t$.

the limit of the constant (from the docstring)

The limit of the constant is an isomorphism of the limit of the action of the constant of $J$ and $\operatorname{terminal}$ applied to $C$ and $\operatorname{terminal}$ applied to $C$.

the limit of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the limit of $F$ is an isomorphism of the limit of $F$ and the action of $F$ and $\operatorname{initial}$ applied to $J$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to $F$ and the limit of $\operatorname{initialIsInitial}$ and $F$.

the limit of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the limit of $F$ is an isomorphism of the limit of $F$ and the action of $F$ and $\operatorname{terminal}$ applied to $J$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to $F$ and the limit of $\operatorname{terminalIsTerminal}$ and $F$.

the map of P (from the docstring)

Let $P$ be an element of $C$. Then the map of $P$ is a homomorphism of $P$ and $\operatorname{terminal}$ applied to $C$ defined as the lift of $\operatorname{empty}$ applied to $C$ and $\operatorname{asEmptyCone}$ applied to $P$.

the cocone of t (from the name)

Let $t$ be an element of $\operatorname{Cotrident}$ applied to the function that maps $j$ to the map of $F$ and the line of $j$. Then the cocone of $t$ is a cocone of $F$.

the cone of t (from the name)

Let $t$ be a trident of the function that maps $j$ to the map of $F$ and the line of $j$. Then the cone of $t$ is a cone of $F$.

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then an element of $\operatorname{Cotrident}$ applied to $f$ is an element of the function that maps $f$ to the set of cocones of the parallel family of $f$.

Let $\mathrm{hs}$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $k$ be a homomorphism of $Y$ and $W$ such that for all elements $x_{1}$ and $x_{2}$ of $J$, $\EqtMACRoH {\operatorname{comp} (f (x_{1}), k)}{\operatorname{comp} (f (x_{2}), k)}$. Then $\operatorname{desc'}$ applied to $\mathrm{hs}$, $k$ and $h_{1}$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (\mathrm{CategoryTheory\_\_Limits\_\_Cotrident\_\_\_u3c0\_} (s), l)}{k})}$ defined as $\operatorname{desc}$ applied to $\mathrm{hs}$ and the projection of $k$ and $h_{1}$.

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_{1}}{\mathrm{forall} (J , \lambda x_{1} . \mathrm{forall} (J , \lambda x_{2} . \EqtMACRoH {\operatorname{comp} (f (x_{1}), h_{1})}{\operatorname{comp} (f (x_{2}), h_{1})}))})}$.

Let $t$ be an element of $\operatorname{Cotrident}$ applied to $f$. Let $\mathrm{desc}$ be a function from elements $s_{2}$ of $\operatorname{Cotrident}$ applied to $f$ to homomorphisms of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s_{2}$ such that for all elements $s_{1}$ of $\operatorname{Cotrident}$ applied to $f$, the composition of the projection of $t$ and $\mathrm{desc}$ applied to $s_{1}$ is equal to the projection of $s_{1}$ and for all elements $s$ of $\operatorname{Cotrident}$ applied to $f$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s$, if for all walking parallel families $j$ of $J$, the composition of the component of the inclusion of $t$ and $j$ and $m$ is equal to the component of the inclusion of $s$ and $j$, then $\EqtMACRoH {m}{\mathrm{desc} (s)}$. Then $\operatorname{mk}$ applied to $t$, $s_{2}$, $\mathrm{desc}$, $\mathrm{fac}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsColimit}$ applied to $t$.

Let $t$ be an element of $\operatorname{Cotrident}$ applied to $f$. Let $\mathrm{create}$ be a function from elements $s$ of $\operatorname{Cotrident}$ applied to $f$ to elements of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (\mathrm{CategoryTheory\_\_Limits\_\_Cotrident\_\_\_u3c0\_} (t), l)}{\mathrm{CategoryTheory\_\_Limits\_\_Cotrident\_\_\_u3c0\_} (s)}, \mathrm{forall} (\operatorname{Hom} (\operatorname{obj} (\operatorname{obj} (\operatorname{const} (\operatorname{WalkingParallelFamily} (J)), \operatorname{pt} (t)), \operatorname{one}), \operatorname{obj} (\operatorname{obj} (\operatorname{const} (\operatorname{WalkingParallelFamily} (J)), \operatorname{pt} (s)), \operatorname{one})), \lambda m . \mathrm{if} (\EqtMACRoH {\operatorname{comp} (\mathrm{CategoryTheory\_\_Limits\_\_Cotrident\_\_\_u3c0\_} (t), m)}{\mathrm{CategoryTheory\_\_Limits\_\_Cotrident\_\_\_u3c0\_} (s)}, \EqtMACRoH {m}{l})))}$. Then $\operatorname{mk'}$ applied to $t$, $s$ and $\mathrm{create}$ 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\_\_Cotrident\_\_ext\_\_\_auto\_1}$. Then the extension of $i$ and $w$ is an isomorphism of $s$ and $t$.

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 $\mathrm{autoParam}$ holds for the proposition that the composition of the projection of $s$ and $k$ is equal to the projection of $t$ and $\mathrm{CategoryTheory\_\_Limits\_\_Cotrident\_\_mkHom\_\_\_auto\_1}$. Then the homomorphism of $k$ and $w$ is a homomorphism of $s$ and $t$.

Let $t$ be a cocone of $F$. Then $\operatorname{ofCocone}$ applied to $t$ is an element of $\operatorname{Cotrident}$ applied to the function that maps $j$ to the map of $F$ and the line of $j$.

the projection of x1 and w (from the name)

Let $x_{1}$ be a homomorphism of $Y$ and $P$ such that for all elements $x_{2}$ and $x_{3}$ of $J$, the composition of $f$ applied to $x_{2}$ and $x_{1}$ is equal to the composition of $f$ applied to $x_{3}$ and $x_{1}$. Then the projection of $x_{1}$ and $w$ is an element of $\operatorname{Cotrident}$ applied to $f$.

the projection of t (from the name)

Let $t$ be an element of $\operatorname{Cotrident}$ applied to $f$. Then the projection of $t$ is a homomorphism of the action of the parallel family of $f$ and the one and the action of the action of the constant of the set of walking parallel families of $J$ and $\operatorname{pt}$ applied to $t$ and the one defined as the component of the inclusion of $t$ and the one.

f has wide coequalizers (from the name)

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then $f$ has wide coequalizers, if the parallel family of $f$ has colimits.

C has wide coequalizers (from the name)

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

f has wide equalizers (from the name)

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then $f$ has wide equalizers, if the parallel family of $f$ has limits.

C has wide equalizers (from the name)

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

trident of f (from the name)

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then a trident of $f$ is an element of the function that maps $f$ to the set of cones of the parallel family of $f$.

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_{1}}{\mathrm{forall} (J , \lambda x_{1} . \mathrm{forall} (J , \lambda x_{2} . \EqtMACRoH {\operatorname{comp} (h_{1} , f (x_{1}))}{\operatorname{comp} (h_{1} , f (x_{2}))}))})}$.

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 for all elements $x_{1}$ and $x_{2}$ of $J$, $\EqtMACRoH {\operatorname{comp} (k , f (x_{1}))}{\operatorname{comp} (k , f (x_{2}))}$. Then the lift of $\mathrm{hs}$ and $k$ is an element of $\SubtypeSet {l}{(\EqtMACRoH {\operatorname{comp} (l , \mathrm{CategoryTheory\_\_Limits\_\_Trident\_\_\_u3b9\_} (s))}{k})}$ defined as the lift of $\mathrm{hs}$ and the inclusion of $k$ and $h_{1}$.

Let $t$ be a trident of $f$. Let $\mathrm{lift}$ be a function from tridents $s_{2}$ of $f$ to homomorphisms of $\operatorname{pt}$ applied to $s_{2}$ and $\operatorname{pt}$ applied to $t$ such that for all tridents $s_{1}$ of $f$, 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 tridents $s$ of $f$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$, if for all walking parallel families $j$ of $J$, the composition of $m$ and the component of the projection of $t$ and $j$ is equal to the component of the projection of $s$ and $j$, 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 trident of $f$. Let $\mathrm{create}$ be a function from tridents $s$ of $f$ to elements of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (l , \mathrm{CategoryTheory\_\_Limits\_\_Trident\_\_\_u3b9\_} (t))}{\mathrm{CategoryTheory\_\_Limits\_\_Trident\_\_\_u3b9\_} (s)}, \mathrm{forall} (\operatorname{Hom} (\operatorname{obj} (\operatorname{obj} (\operatorname{const} (\operatorname{WalkingParallelFamily} (J)), \operatorname{pt} (s)), \operatorname{zero}), \operatorname{obj} (\operatorname{obj} (\operatorname{const} (\operatorname{WalkingParallelFamily} (J)), \operatorname{pt} (t)), \operatorname{zero})), \lambda m . \mathrm{if} (\EqtMACRoH {\operatorname{comp} (m , \mathrm{CategoryTheory\_\_Limits\_\_Trident\_\_\_u3b9\_} (t))}{\mathrm{CategoryTheory\_\_Limits\_\_Trident\_\_\_u3b9\_} (s)}, \EqtMACRoH {m}{l})))}$. Then $\operatorname{mk'}$ applied to $t$, $s$ and $\mathrm{create}$ is an element of $\operatorname{IsLimit}$ 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 homomorphism of $i$ and the inclusion of $t$ is equal to the inclusion of $s$ and $\mathrm{CategoryTheory\_\_Limits\_\_Trident\_\_ext\_\_\_auto\_1}$. Then the extension of $i$ and $w$ is an isomorphism of $s$ and $t$.

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 $\mathrm{autoParam}$ holds for the proposition that the composition of $k$ and the inclusion of $t$ is equal to the inclusion of $s$ and $\mathrm{CategoryTheory\_\_Limits\_\_Trident\_\_mkHom\_\_\_auto\_1}$. Then the homomorphism of $k$ and $w$ is a homomorphism of $s$ and $t$.

the trident of t (from the name)

Let $t$ be a cone of $F$. Then the trident of $t$ is a trident of the function that maps $j$ to the map of $F$ and the line of $j$.

the inclusion of x1 and w (from the name)

Let $x_{1}$ be a homomorphism of $P$ and $X$ such that for all elements $x_{2}$ and $x_{3}$ of $J$, the composition of $x_{1}$ and $f$ applied to $x_{2}$ is equal to the composition of $x_{1}$ and $f$ applied to $x_{3}$. Then the inclusion of $x_{1}$ and $w$ is a trident of $f$.

the inclusion of t (from the name)

Let $t$ be a trident of $f$. Then the inclusion of $t$ is a homomorphism of the action of the action of the constant of the set of walking parallel families of $J$ and $\operatorname{pt}$ applied to $t$ and the zero and the action of the parallel family of $f$ and the zero defined as the component of the projection of $t$ and the zero.

walking parallel family of J (from the name)

Let $J$ be a set. Then the walking parallel families of $J$ are a basic type.

homomorphism of x and x1 (from the name)

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

the composition of x and x1 (from the name)

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

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

the identity of X (from the name)

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

the line of x (from the name)

Let $x$ be an element of $J$. Then the line of $x$ is a homomorphism of the zero and the one.

the arrow equivalence of J (from the name)

Let $J$ be a set. Then the arrow equivalence of $J$ is an equivalence from the set of arrows of the set of walking parallel families of $J$ to $\mathrm{Option}$ applied to $\mathrm{Option}$ applied to $J$.

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 equivalence of e (from the name)

Let $e$ be an equivalence from $J$ to $\mathrm{J'}$. Then the equivalence of $e$ is an equivalence of the set of walking parallel families of $J$ and the set of walking parallel families of $\mathrm{J'}$.

the one (from the name)

The one is a walking parallel family of $J$.

the zero (from the name)

The zero is a walking parallel family of $J$.

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

Let $F$ be a functor of the set of walking parallel families of $J$ and $C$. Then the diagram isomorphism parallel family of $F$ is an isomorphism of $F$ and the parallel family of the function that maps $j$ to the map of $F$ and the line of $j$.

the default (from the name)

The default is a walking parallel family of $J$ defined as the zero.

the parallel family of f (from the name)

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then the parallel family of $f$ is a functor of the set of walking parallel families of $J$ and $C$.

the walking parallel family equivalence walking parallel pair (from the name)

The walking parallel family equivalence walking parallel pair is an equivalence of the set of walking parallel families of $\mathrm{ULift}$ applied to $\mathrm{Bool}$ and the set of walking parallel pairs.

the wide coequalizer of f (from the name)

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then the wide coequalizer of $f$ is an element of $C$ defined as the colimit of the parallel family of $f$.

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then $\operatorname{cotrident}$ applied to $f$ is an element of $\operatorname{Cotrident}$ applied to $f$ defined as the cocone of the parallel family of $f$.

Let $k$ be a homomorphism of $Y$ and $W$ such that for all elements $x_{1}$ and $x_{2}$ of $J$, the composition of $f$ applied to $x_{1}$ and $k$ is equal to the composition of $f$ applied to $x_{2}$ and $k$. Then $\operatorname{desc}$ applied to $k$ and $h_{2}$ is a homomorphism of the wide coequalizer of $f$ and $W$ defined as $\operatorname{desc}$ applied to the parallel family of $f$ and the projection of $k$ and $h_{2}$.

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

the projection of f (from the name)

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then the projection of $f$ is a homomorphism of $Y$ and the wide coequalizer of $f$ defined as the inclusion of the parallel family of $f$ and the one.

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then $\operatorname{wideCoequalizerIsWideCoequalizer}$ applied to $f$ is an element of $\operatorname{IsColimit}$ applied to the projection of the projection of $f$ and $\operatorname{condition}$ applied to $f$.

the wide equalizer of f (from the name)

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then the wide equalizer of $f$ is an element of $C$ defined as the limit of the parallel family of $f$.

the lift of k and h2 (from the name)

Let $k$ be a homomorphism of $W$ and $X$ such that for all elements $x_{1}$ and $x_{2}$ of $J$, the composition of $k$ and $f$ applied to $x_{1}$ is equal to the composition of $k$ and $f$ applied to $x_{2}$. Then the lift of $k$ and $h_{2}$ is a homomorphism of $W$ and the wide equalizer of $f$ defined as the lift of the parallel family of $f$ and the inclusion of $k$ and $h_{2}$.

the lift of k and h2 (from the name)

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

the trident of f (from the name)

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then the trident of $f$ is a trident of $f$ defined as the cone of the parallel family of $f$.

the inclusion of f (from the name)

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

Let $f$ be a function from elements of $J$ to homomorphisms of $X$ and $Y$. Then $\operatorname{wideEqualizerIsWideEqualizer}$ applied to $f$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the inclusion of $f$ and $\operatorname{condition}$ applied to $f$.