Definitions: Mathlib.CategoryTheory, part 9 of 25

the cocone of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the cocone of $F$ is a functor of $C$ and the set of sets defined as the composition of the constant of $J$ and the action of the Coyoneda and $\operatorname{op}$ applied to $F$.

the cone of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the cone of $F$ is a functor of the set of opposites of $C$ and the set of sets defined as the composition of the opposite of the constant of $J$ and the action of the Yoneda and $F$.

the functoriality composition postcomposition of x3 (from the name)

Let $x_{3}$ be an isomorphism of $H$ and $\mathrm{H'}$. Then the functoriality composition postcomposition of $x_{3}$ is an isomorphism of the composition of the functoriality of $F$ and $H$ and the postcomposition of the left whisker of $F$ and the homomorphism of $x_{3}$ and the functoriality of $F$ and $\mathrm{H'}$.

the functoriality composition precomposition of x3 (from the name)

Let $x_{3}$ be an isomorphism of $H$ and $\mathrm{H'}$. Then the functoriality composition precomposition of $x_{3}$ is an isomorphism of the composition of the functoriality of $F$ and $H$ and the precomposition of the left whisker of $F$ and the inverse of $x_{3}$ and the functoriality of $F$ and $\mathrm{H'}$.

the map cocone of H and c (from the name)

Let $H$ be a functor of $C$ and $D$. Let $c$ be a cocone of $F$. Then the map cocone of $H$ and $c$ is a cocone of the composition of $F$ and $H$ defined as the action of the functoriality of $F$ and $H$ and $c$.

the map cocone inverse of H and c (from the name)

Let $H$ be a functor of $C$ and $D$. Let $c$ be a cocone of the composition of $F$ and $H$. Then the map cocone inverse of $H$ and $c$ is a cocone of $F$ defined as the action of the inverse of the functoriality equivalence of $F$ and $\operatorname{asEquivalence}$ applied to $H$ and $c$.

the map cocone inverse map cocone of H and c (from the name)

Let $H$ be a functor of $D$ and $C$. Let $c$ be a cocone of $F$. Then the map cocone inverse map cocone of $H$ and $c$ is an isomorphism of the map cocone inverse of $H$ and the map cocone of $H$ and $c$ and $c$ defined as the application of the inverse of the unit isomorphism of the functoriality equivalence of $F$ and $\operatorname{asEquivalence}$ applied to $H$ and $c$.

the map cocone map cocone of c (from the name)

Let $c$ be a cocone of $F$. Then the map cocone map cocone of $c$ is an isomorphism of the map cocone of $\mathrm{H'}$ and the map cocone of $H$ and $c$ and the map cocone of the composition of $H$ and $\mathrm{H'}$ and $c$.

the map cocone map cocone inverse of H and c (from the name)

Let $H$ be a functor of $D$ and $C$. Let $c$ be a cocone of the composition of $F$ and $H$. Then the map cocone map cocone inverse of $H$ and $c$ is an isomorphism of the map cocone of $H$ and the map cocone inverse of $H$ and $c$ and $c$ defined as the application of the counit isomorphism of the functoriality equivalence of $F$ and $\operatorname{asEquivalence}$ applied to $H$ and $c$.

the map cocone morphism of H and f (from the name)

Let $H$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $\mathrm{c'}$ and $c$. Then the map cocone morphism of $H$ and $f$ is a homomorphism of the map cocone of $H$ and $\mathrm{c'}$ and the map cocone of $H$ and $c$ defined as the map of the functoriality of $F$ and $H$ and $f$.

the opposite cone of the image of G and t (from the docstring)

Let $G$ be a functor of $C$ and $D$. Let $t$ be a cocone of $F$. Then the opposite cone of the image of $G$ and $t$ is an isomorphism of the opposite of the map cocone of $G$ and $t$ and the map cone of the opposite of $G$ and the opposite of $t$.

the map cocone precomposition of H (from the name)

Let $H$ be a functor of $C$ and $D$. Then the map cocone precomposition of $H$ is an isomorphism of the map cocone of $H$ and the action of the precomposition of $x_{3}$ and $c$ and the action of the precomposition of the right whisker of $x_{3}$ and $H$ and the map cocone of $H$ and $c$.

the map cocone precomposition equivalence functor of H (from the name)

Let $H$ be a functor of $C$ and $D$. Then the map cocone precomposition equivalence functor of $H$ is an isomorphism of the map cocone of $H$ and the action of the functor of the precomposition equivalence of $x_{3}$ and $c$ and the action of the functor of the precomposition equivalence of the right isomorphism whisker of $x_{3}$ and $H$ and the map cocone of $H$ and $c$.

the map cocone whisker of H (from the name)

Let $H$ be a functor of $C$ and $D$. Then the map cocone whisker of $H$ is an isomorphism of the map cocone of $H$ and the whisker of $E$ and $c$ and the whisker of $E$ and the map cocone of $H$ and $c$.

the map cone of H and c (from the name)

Let $H$ be a functor of $C$ and $D$. Let $c$ be a cone of $F$. Then the map cone of $H$ and $c$ is a cone of the composition of $F$ and $H$ defined as the action of the functoriality of $F$ and $H$ and $c$.

the map cone inverse of H and c (from the name)

Let $H$ be a functor of $C$ and $D$. Let $c$ be a cone of the composition of $F$ and $H$. Then the map cone inverse of $H$ and $c$ is a cone of $F$ defined as the action of the inverse of the functoriality equivalence of $F$ and $\operatorname{asEquivalence}$ applied to $H$ and $c$.

the map cone inverse map cone of H and c (from the name)

Let $H$ be a functor of $D$ and $C$. Let $c$ be a cone of $F$. Then the map cone inverse map cone of $H$ and $c$ is an isomorphism of the map cone inverse of $H$ and the map cone of $H$ and $c$ and $c$ defined as the application of the inverse of the unit isomorphism of the functoriality equivalence of $F$ and $\operatorname{asEquivalence}$ applied to $H$ and $c$.

the map cone map cone of c (from the name)

Let $c$ be a cone of $F$. Then the map cone map cone of $c$ is an isomorphism of the map cone of $\mathrm{H'}$ and the map cone of $H$ and $c$ and the map cone of the composition of $H$ and $\mathrm{H'}$ and $c$.

the map cone map cone inverse of H and c (from the name)

Let $H$ be a functor of $D$ and $C$. Let $c$ be a cone of the composition of $F$ and $H$. Then the map cone map cone inverse of $H$ and $c$ is an isomorphism of the map cone of $H$ and the map cone inverse of $H$ and $c$ and $c$ defined as the application of the counit isomorphism of the functoriality equivalence of $F$ and $\operatorname{asEquivalence}$ applied to $H$ and $c$.

the map cone morphism of H and f (from the name)

Let $H$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $c$ and $\mathrm{c'}$. Then the map cone morphism of $H$ and $f$ is a homomorphism of the map cone of $H$ and $c$ and the map cone of $H$ and $\mathrm{c'}$ defined as the map of the functoriality of $F$ and $H$ and $f$.

the opposite cocone of the image of G and t (from the docstring)

Let $G$ be a functor of $C$ and $D$. Let $t$ be a cone of $F$. Then the opposite cocone of the image of $G$ and $t$ is an isomorphism of the opposite of the map cone of $G$ and $t$ and the map cocone of the opposite of $G$ and the opposite of $t$.

the map cone postcomposition of H (from the name)

Let $H$ be a functor of $C$ and $D$. Then the map cone postcomposition of $H$ is an isomorphism of the map cone of $H$ and the action of the postcomposition of $x_{3}$ and $c$ and the action of the postcomposition of the right whisker of $x_{3}$ and $H$ and the map cone of $H$ and $c$.

the map cone postcomposition equivalence functor of H (from the name)

Let $H$ be a functor of $C$ and $D$. Then the map cone postcomposition equivalence functor of $H$ is an isomorphism of the map cone of $H$ and the action of the functor of the postcomposition equivalence of $x_{3}$ and $c$ and the action of the functor of the postcomposition equivalence of the right isomorphism whisker of $x_{3}$ and $H$ and the map cone of $H$ and $c$.

the map cone whisker of H (from the name)

Let $H$ be a functor of $C$ and $D$. Then the map cone whisker of $H$ is an isomorphism of the map cone of $H$ and the whisker of $E$ and $c$ and the whisker of $E$ and the map cone of $H$ and $c$.

the postcomposition whisker left map cone of x3 and c (from the name)

Let $x_{3}$ be an isomorphism of $H$ and $\mathrm{H'}$. Let $c$ be a cone of $F$. Then the postcomposition whisker left map cone of $x_{3}$ and $c$ is an isomorphism of the action of the postcomposition of the left whisker of $F$ and the homomorphism of $x_{3}$ and the map cone of $H$ and $c$ and the map cone of $\mathrm{H'}$ and $c$ defined as the application of the functoriality composition postcomposition of $x_{3}$ and $c$.

the precomposition whisker left map cocone of x3 and c (from the name)

Let $x_{3}$ be an isomorphism of $H$ and $\mathrm{H'}$. Let $c$ be a cocone of $F$. Then the precomposition whisker left map cocone of $x_{3}$ and $c$ is an isomorphism of the action of the precomposition of the left whisker of $F$ and the inverse of $x_{3}$ and the map cocone of $H$ and $c$ and the map cocone of $\mathrm{H'}$ and $c$ defined as the application of the functoriality composition precomposition of $x_{3}$ and $c$.

cocone of F (from the name)

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

the equivalence of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the equivalence of $F$ is an isomorphism of the set of cocones of $F$ and $\Sigma$ applied to the function that maps $X$ to the action of the cocone of $F$ and $X$.

the equivalence of e and x3 (from the name)

Let $e$ be an equivalence of $K$ and $J$. Let $x_{3}$ be an isomorphism of the composition of the functor of $e$ and $F$ and $G$. Then the equivalence of $e$ and $x_{3}$ is an equivalence of the set of cocones of $F$ and the set of cocones of $G$ defined as the composition of the whiskering equivalence of $e$ and the precomposition equivalence of $x_{3}$.

Let $c$ be a cocone of $F$. Then $\operatorname{eta}$ applied to $c$ is an isomorphism of $c$ and $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and the inclusion of $c$.

the extension of x2 and w (from the name)

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

Let $c$ be a cocone of $F$. Let $f$ be a homomorphism of $\operatorname{pt}$ applied to $c$ and $X$. Then $\operatorname{extend}$ applied to $c$ and $f$ is a cocone of $F$ defined as $\operatorname{mk}$ applied to $X$ and the composition of the inclusion of $c$ and the map of the constant of $J$ and $f$.

Let $s$ be a cocone of $F$. Let $g$ be a homomorphism of $\operatorname{pt}$ applied to $s$ and $Y$. Let $f$ be a homomorphism of $Y$ and $X$. Then $\operatorname{extendComp}$ applied to $s$, $g$ and $f$ is an isomorphism of $\operatorname{extend}$ applied to $s$ and the composition of $g$ and $f$ and $\operatorname{extend}$ applied to $\operatorname{extend}$ applied to $s$ and $g$ and $f$.

Let $s$ be a cocone of $F$. Let $f$ be a homomorphism of $\operatorname{pt}$ applied to $s$ and $X$. Then $\operatorname{extendHom}$ applied to $s$ and $f$ is a homomorphism of $s$ and $\operatorname{extend}$ applied to $s$ and $f$.

Let $s$ be a cocone of $F$. Then $\operatorname{extendId}$ applied to $s$ is an isomorphism of $\operatorname{extend}$ applied to $s$ and the identity morphism of $\operatorname{pt}$ applied to $s$ and $s$.

Let $s$ be a cocone of $F$. Let $f$ be an isomorphism of $\operatorname{pt}$ applied to $s$ and $X$. Then $\operatorname{extendIso}$ applied to $s$ and $f$ is an isomorphism of $s$ and $\operatorname{extend}$ applied to $s$ and the homomorphism of $f$.

the extension of c (from the name)

Let $c$ be a cocone of $F$. Then the extension of $c$ is a homomorphism of the composition of the action of the Coyoneda and $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ and the functor embedding and the cocone of $F$.

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

the functoriality of F and G (from the name)

Let $F$ be a functor of $J$ and $C$. Let $G$ be a functor of $C$ and $D$. Then the functoriality of $F$ and $G$ is a functor of the set of cocones of $F$ and the set of cocones of the composition of $F$ and $G$.

the functoriality composition functoriality of G and H (from the name)

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

the functoriality equivalence of F and e (from the name)

Let $F$ be a functor of $J$ and $C$. Let $e$ be an equivalence of $C$ and $D$. Then the functoriality equivalence of $F$ and $e$ is an equivalence of the set of cocones of $F$ and the set of cocones of the composition of $F$ and the functor of $e$.

the opposite of c (from the name)

Let $c$ be a cocone of $F$. Then the opposite of $c$ is a cone of the opposite of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ and the opposite of the inclusion of $c$.

the precomposition of x2 (from the name)

Let $x_{2}$ be a homomorphism of $G$ and $F$. Then the precomposition of $x_{2}$ is a functor of the set of cocones of $F$ and the set of cocones of $G$.

the precomposition composition of x2 and x3 (from the name)

Let $x_{2}$ be a homomorphism of $H$ and $G$. Let $x_{3}$ be a homomorphism of $G$ and $F$. Then the precomposition composition of $x_{2}$ and $x_{3}$ is an isomorphism of the precomposition of the composition of $x_{2}$ and $x_{3}$ and the composition of the precomposition of $x_{3}$ and the precomposition of $x_{2}$.

the precomposition equivalence of x2 (from the name)

Let $x_{2}$ be an isomorphism of $F$ and $G$. Then the precomposition equivalence of $x_{2}$ is an equivalence of the set of cocones of $F$ and the set of cocones of $G$.

the precomposition identity (from the name)

The precomposition identity is an isomorphism of the precomposition of the identity morphism of $F$ and the identity of the set of cocones of $F$.

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

the opposite of c (from the name)

Let $c$ be a cocone of the opposite of $F$. Then the opposite of $c$ is a cone of $F$ defined as $\operatorname{mk}$ applied to the opposite of $\operatorname{pt}$ applied to $c$ and $\operatorname{removeOp}$ applied to the inclusion of $c$.

the whisker of E and c (from the name)

Let $E$ be a functor of $K$ and $J$. Let $c$ be a cocone of $F$. Then the whisker of $E$ and $c$ is a cocone of the composition of $E$ and $F$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and the left whisker of $E$ and the inclusion of $c$.

the whiskering of E (from the name)

Let $E$ be a functor of $K$ and $J$. Then the whiskering of $E$ is a functor of the set of cocones of $F$ and the set of cocones of the composition of $E$ and $F$.

the whiskering equivalence of e (from the name)

Let $e$ be an equivalence of $K$ and $J$. Then the whiskering equivalence of $e$ is an equivalence of the set of cocones of $F$ and the set of cocones of the composition of the functor of $e$ and $F$.

the inclusion of self (from the name)

Let $\mathrm{self}$ be a cocone of $F$. Then the inclusion of $\mathrm{self}$ is a homomorphism of $F$ and the action of the constant of $J$ and $\operatorname{pt}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

cocone morphism of A and B (from the name)

Let $A$ and $B$ be cocones of $F$. Then the cocone morphisms of $A$ and $B$ are a basic type.

the homomorphism of self (from the name)

Let $\mathrm{self}$ be a cocone morphism of $A$ and $B$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to $A$ and $\operatorname{pt}$ applied to $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

cone of F (from the name)

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

the equivalence of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the equivalence of $F$ is an isomorphism of the set of cones of $F$ and $\Sigma$ applied to the function that maps $X$ to the set of homomorphisms of the action of the constant of $J$ and the opposite of $X$ and $F$.

the equivalence of e and x3 (from the name)

Let $e$ be an equivalence of $K$ and $J$. Let $x_{3}$ be an isomorphism of the composition of the functor of $e$ and $F$ and $G$. Then the equivalence of $e$ and $x_{3}$ is an equivalence of the set of cones of $F$ and the set of cones of $G$ defined as the composition of the whiskering equivalence of $e$ and the postcomposition equivalence of $x_{3}$.

Let $c$ be a cone of $F$. Then $\operatorname{eta}$ applied to $c$ is an isomorphism of $c$ and $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and the projection of $c$.

the extension of x2 and w (from the name)

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

Let $c$ be a cone of $F$. Let $f$ be a homomorphism of $X$ and $\operatorname{pt}$ applied to $c$. Then $\operatorname{extend}$ applied to $c$ and $f$ is a cone of $F$ defined as $\operatorname{mk}$ applied to $X$ and the composition of the map of the constant of $J$ and $f$ and the projection of $c$.

Let $s$ be a cone of $F$. Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $\operatorname{pt}$ applied to $s$. Then $\operatorname{extendComp}$ applied to $s$, $f$ and $g$ is an isomorphism of $\operatorname{extend}$ applied to $s$ and the composition of $f$ and $g$ and $\operatorname{extend}$ applied to $\operatorname{extend}$ applied to $s$ and $g$ and $f$.

Let $s$ be a cone of $F$. Let $f$ be a homomorphism of $X$ and $\operatorname{pt}$ applied to $s$. Then $\operatorname{extendHom}$ applied to $s$ and $f$ is a homomorphism of $\operatorname{extend}$ applied to $s$ and $f$ and $s$.

Let $s$ be a cone of $F$. Then $\operatorname{extendId}$ applied to $s$ is an isomorphism of $\operatorname{extend}$ applied to $s$ and the identity morphism of $\operatorname{pt}$ applied to $s$ and $s$.

Let $s$ be a cone of $F$. Let $f$ be an isomorphism of $\operatorname{pt}$ applied to $s$ and $X$. Then $\operatorname{extendIso}$ applied to $s$ and $f$ is an isomorphism of $s$ and $\operatorname{extend}$ applied to $s$ and the inverse of $f$.

the extension of c (from the name)

Let $c$ be a cone of $F$. Then the extension of $c$ is a homomorphism of the action of the lift Yoneda and $\operatorname{pt}$ applied to $c$ and the cone of $F$.

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

the functoriality of F and G (from the name)

Let $F$ be a functor of $J$ and $C$. Let $G$ be a functor of $C$ and $D$. Then the functoriality of $F$ and $G$ is a functor of the set of cones of $F$ and the set of cones of the composition of $F$ and $G$.

the functoriality composition functoriality of G and H (from the name)

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

the functoriality equivalence of F and e (from the name)

Let $F$ be a functor of $J$ and $C$. Let $e$ be an equivalence of $C$ and $D$. Then the functoriality equivalence of $F$ and $e$ is an equivalence of the set of cones of $F$ and the set of cones of the composition of $F$ and the functor of $e$.

the opposite of c (from the name)

Let $c$ be a cone of $F$. Then the opposite of $c$ is a cocone of the opposite of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ and the opposite of the projection of $c$.

the postcomposition of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the postcomposition of $x_{2}$ is a functor of the set of cones of $F$ and the set of cones of $G$.

the postcomposition composition of x2 and x3 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a homomorphism of $G$ and $H$. Then the postcomposition composition of $x_{2}$ and $x_{3}$ is an isomorphism of the postcomposition of the composition of $x_{2}$ and $x_{3}$ and the composition of the postcomposition of $x_{2}$ and the postcomposition of $x_{3}$.

the postcomposition equivalence of x2 (from the name)

Let $x_{2}$ be an isomorphism of $F$ and $G$. Then the postcomposition equivalence of $x_{2}$ is an equivalence of the set of cones of $F$ and the set of cones of $G$.

the postcomposition identity (from the name)

The postcomposition identity is an isomorphism of the postcomposition of the identity morphism of $F$ and the identity of the set of cones of $F$.

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

the opposite of c (from the name)

Let $c$ be a cone of the opposite of $F$. Then the opposite of $c$ is a cocone of $F$ defined as $\operatorname{mk}$ applied to the opposite of $\operatorname{pt}$ applied to $c$ and $\operatorname{removeOp}$ applied to the projection of $c$.

the whisker of E and c (from the name)

Let $E$ be a functor of $K$ and $J$. Let $c$ be a cone of $F$. Then the whisker of $E$ and $c$ is a cone of the composition of $E$ and $F$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and the left whisker of $E$ and the projection of $c$.

the whiskering of E (from the name)

Let $E$ be a functor of $K$ and $J$. Then the whiskering of $E$ is a functor of the set of cones of $F$ and the set of cones of the composition of $E$ and $F$.

the whiskering equivalence of e (from the name)

Let $e$ be an equivalence of $K$ and $J$. Then the whiskering equivalence of $e$ is an equivalence of the set of cones of $F$ and the set of cones of the composition of the functor of $e$ and $F$.

the projection of self (from the name)

Let $\mathrm{self}$ be a cone of $F$. Then the projection of $\mathrm{self}$ is a homomorphism of the action of the constant of $J$ and $\operatorname{pt}$ applied to $\mathrm{self}$ and $F$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

cone morphism of A and B (from the name)

Let $A$ and $B$ be cones of $F$. Then the cone morphisms of $A$ and $B$ are a basic type.

the homomorphism of self (from the name)

Let $\mathrm{self}$ be a cone morphism of $A$ and $B$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to $A$ and $\operatorname{pt}$ applied to $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the cocone equivalence opposite cone opposite of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the cocone equivalence opposite cone opposite of $F$ is an equivalence of the set of cocones of $F$ and the set of opposites of the set of cones of the opposite of $F$.

the cocone left opposite of c (from the name)

Let $c$ be a cone of $F$. Then the cocone left opposite of $c$ is a cocone of the left opposite of $F$ defined as $\operatorname{mk}$ applied to the opposite of $\operatorname{pt}$ applied to $c$ and the left opposite of the projection of $c$.

the cocone left opposite (from the name)

The cocone left opposite is an equivalence of the set of opposites of the set of cones of $F$ and the set of cocones of the left opposite of $F$.

the cocone of c (from the name)

Let $c$ be a cone of the left opposite of $F$. Then the cocone of $c$ is a cocone of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{removeLeftOp}$ applied to the projection of $c$.

the cocone of c (from the name)

Let $c$ be a cone of the right opposite of $F$. Then the cocone of $c$ is a cocone of $F$ defined as $\operatorname{mk}$ applied to the opposite of $\operatorname{pt}$ applied to $c$ and $\operatorname{removeRightOp}$ applied to the projection of $c$.

the cocone of c (from the name)

Let $c$ be a cone of the opposite of $F$. Then the cocone of $c$ is a cocone of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{removeUnop}$ applied to the projection of $c$.

the cocone opposite equivalence (from the name)

The cocone opposite equivalence is an equivalence of the set of opposites of the set of cocones of $F$ and the set of cones of the opposite of $F$.

the cocone right opposite of c (from the name)

Let $c$ be a cone of $F$. Then the cocone right opposite of $c$ is a cocone of the right opposite of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ and the right opposite of the projection of $c$.

the cocone right opposite (from the name)

The cocone right opposite is an equivalence of the set of opposites of the set of cones of $F$ and the set of cocones of the right opposite of $F$.

the cocone opposite of c (from the name)

Let $c$ be a cone of $F$. Then the cocone opposite of $c$ is a cocone of the opposite of $F$ defined as $\operatorname{mk}$ applied to the opposite of $\operatorname{pt}$ applied to $c$ and the opposite of the projection of $c$.

the cocone opposite (from the name)

The cocone opposite is an equivalence of the set of opposites of the set of cones of $F$ and the set of cocones of the opposite of $F$.

the cone equivalence opposite cocone opposite of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the cone equivalence opposite cocone opposite of $F$ is an equivalence of the set of cones of $F$ and the set of opposites of the set of cocones of the opposite of $F$.

the cone left opposite of c (from the name)

Let $c$ be a cocone of $F$. Then the cone left opposite of $c$ is a cone of the left opposite of $F$ defined as $\operatorname{mk}$ applied to the opposite of $\operatorname{pt}$ applied to $c$ and the left opposite of the inclusion of $c$.

the cone left opposite (from the name)

The cone left opposite is an equivalence of the set of opposites of the set of cocones of $F$ and the set of cones of the left opposite of $F$.

the cone of c (from the name)

Let $c$ be a cocone of the left opposite of $F$. Then the cone of $c$ is a cone of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{removeLeftOp}$ applied to the inclusion of $c$.

the cone of c (from the name)

Let $c$ be a cocone of the right opposite of $F$. Then the cone of $c$ is a cone of $F$ defined as $\operatorname{mk}$ applied to the opposite of $\operatorname{pt}$ applied to $c$ and $\operatorname{removeRightOp}$ applied to the inclusion of $c$.

the cone of c (from the name)

Let $c$ be a cocone of the opposite of $F$. Then the cone of $c$ is a cone of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{removeUnop}$ applied to the inclusion of $c$.

the cone opposite equivalence (from the name)

The cone opposite equivalence is an equivalence of the set of opposites of the set of cones of $F$ and the set of cocones of the opposite of $F$.

the cone right opposite of c (from the name)

Let $c$ be a cocone of $F$. Then the cone right opposite of $c$ is a cone of the right opposite of $F$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ and the right opposite of the inclusion of $c$.

the cone right opposite (from the name)

The cone right opposite is an equivalence of the set of opposites of the set of cocones of $F$ and the set of cones of the right opposite of $F$.

the cone opposite of c (from the name)

Let $c$ be a cocone of $F$. Then the cone opposite of $c$ is a cone of the opposite of $F$ defined as $\operatorname{mk}$ applied to the opposite of $\operatorname{pt}$ applied to $c$ and the opposite of the inclusion of $c$.

the cone opposite (from the name)

The cone opposite is an equivalence of the set of opposites of the set of cocones of $F$ and the set of cones of the opposite of $F$.

the cocone of J and C (from the name)

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

the cone of J and C (from the name)

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

Let $c$ be a cocone of $F$. Then $\mathrm{CategoryTheory\_\_Limits\_\_Cocone\_\_isColimitOfIsIsoColimMap\_u3b9\_}$ applied to $c$ is an element of $\operatorname{IsColimit}$ applied to $c$.

Let $c$ be a cone of $F$. Then $\mathrm{CategoryTheory\_\_Limits\_\_Cone\_\_isLimitOfIsIsoLimMap\_u3c0\_}$ applied to $c$ is an element of $\operatorname{IsLimit}$ applied to $c$.

the obvious cocone of J and X (from the docstring)

Let $J$ be a set. Let $X$ be an element of $C$. Then the obvious cocone of $J$ and $X$ is a cocone of the action of the constant of $J$ and $X$ defined as $\operatorname{mk}$ applied to $X$ and the identity morphism of the action of the constant of $J$ and $X$.

the obvious cone of J and X (from the docstring)

Let $J$ be a set. Let $X$ be an element of $C$. Then the obvious cone of $J$ and $X$ is a cone of the action of the constant of $J$ and $X$ defined as $\operatorname{mk}$ applied to $X$ and the identity morphism of the action of the constant of $J$ and $X$.

Let $J$ be a set. Let $X$ be an element of $C$. Then $\operatorname{isColimitConstCocone}$ applied to $J$ and $X$ is an element of $\operatorname{IsColimit}$ applied to the obvious cocone of $J$ and $X$.

Let $J$ be a set. Let $X$ be an element of $C$. Then $\operatorname{isLimitConstCone}$ applied to $J$ and $X$ is an element of $\operatorname{IsLimit}$ applied to the obvious cone of $J$ and $X$.

Let $s$ be a cone of the composition of $K$ and the action of the binary product functor and $X$. Then $\operatorname{forgetCone}$ applied to $s$ is a cone of $K$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $s$ and the composition of the projection of $s$ and $\mathrm{CategoryTheory\_\_ProdPreservesConnectedLimits\_\_\_u3b3\_\_u2082\_}$ applied to $X$.

Let $X$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_ProdPreservesConnectedLimits\_\_\_u3b3\_\_u2081\_}$ applied to $X$ is a homomorphism of the composition of $K$ and the action of the binary product functor and $X$ and the action of the constant of $J$ and $X$.

Let $X$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_ProdPreservesConnectedLimits\_\_\_u3b3\_\_u2082\_}$ applied to $X$ is a homomorphism of the composition of $K$ and the action of the binary product functor and $X$ and $K$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $\operatorname{Discrete}$ applied to the set of walking pairs and $C$. Then the colimit cocone of $F$ is a colimit cocone of $F$.

the coproduct isomorphism pushout of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the coproduct isomorphism pushout of $X$ and $Y$ is an isomorphism of the coproduct of $X$ and $Y$ and the pushout of $\operatorname{to}$ applied to $X$ and $\operatorname{to}$ applied to $Y$ defined as the isomorphism colimit cocone of the colimit cocone of the pair of $X$ and $Y$.

Let $F$ be a functor of $\operatorname{Discrete}$ applied to the set of walking pairs and $C$. Let $c$ be a cocone of $F$. Let $\mathrm{hX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Let $f$ be a homomorphism of $X$ and the action of $F$ and $\operatorname{mk}$ applied to the left. Let $g$ be a homomorphism of $X$ and the action of $F$ and $\operatorname{mk}$ applied to the right. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the component of the inclusion of $c$ and $\operatorname{mk}$ applied to the left, the component of the inclusion of $c$ and $\operatorname{mk}$ applied to the right and $\mathrm{CategoryTheory\_\_Limits\_\_IsInitial\_\_hom\_ext}$ applied to $\mathrm{hX}$, the composition of $f$ and the component of the inclusion of $c$ and $\operatorname{mk}$ applied to the left and the composition of $g$ and the component of the inclusion of $c$ and $\operatorname{mk}$ applied to the right. Then $\mathrm{isBinaryCoproductOfIsInitialIsPushout}$ applied to $F$, $c$, $\mathrm{hX}$, $f$, $g$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $c$.

Let $F$ be a functor of $\operatorname{Discrete}$ applied to the set of walking pairs and $C$. Let $c$ be a cone of $F$. Let $\mathrm{hX}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Let $f$ be a homomorphism of the action of $F$ and $\operatorname{mk}$ applied to the left and $X$. Let $g$ be a homomorphism of the action of $F$ and $\operatorname{mk}$ applied to the right and $X$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the component of the projection of $c$ and $\operatorname{mk}$ applied to the left, the component of the projection of $c$ and $\operatorname{mk}$ applied to the right and $\mathrm{CategoryTheory\_\_Limits\_\_IsTerminal\_\_hom\_ext}$ applied to $\mathrm{hX}$, the composition of the component of the projection of $c$ and $\operatorname{mk}$ applied to the left and $f$ and the composition of the component of the projection of $c$ and $\operatorname{mk}$ applied to the right and $g$. Then $\mathrm{isBinaryProductOfIsTerminalIsPullback}$ applied to $F$, $c$, $\mathrm{hX}$, $f$, $g$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$.

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 $X$. Let $k$ be a homomorphism of $W$ and $Y$. Let $x_{1}$ be an element of $\operatorname{IsInitial}$ applied to $W$. Let $x_{2}$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $f$, $g$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsInitial\_\_hom\_ext}$ applied to $x_{1}$, the composition of $h$ and $f$ and the composition of $k$ and $g$. Then $\mathrm{isCoproductOfIsInitialIsPushout}$ applied to $f$, $g$, $h$, $k$, $x_{1}$ and $x_{2}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $f$ and $g$ defined as $\mathrm{isBinaryCoproductOfIsInitialIsPushout}$ applied to the pair of $X$ and $Y$, $\operatorname{mk}$ applied to $f$ and $g$, $x_{1}$, $h$, $k$ and $x_{2}$.

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 $X$. Let $k$ be a homomorphism of $W$ and $Y$. Let $x_{1}$ be an element of $\operatorname{IsTerminal}$ applied to $Z$. Let $x_{2}$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsTerminal\_\_hom\_ext}$ applied to $x_{1}$, the composition of $h$ and $f$ and the composition of $k$ and $g$. Then $\mathrm{isProductOfIsTerminalIsPullback}$ applied to $f$, $g$, $h$, $k$, $x_{1}$ and $x_{2}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $h$ and $k$ defined as $\mathrm{isBinaryProductOfIsTerminalIsPullback}$ applied to the pair of $X$ and $Y$, $\operatorname{mk}$ applied to $h$ and $k$, $x_{1}$, $f$, $g$ and $x_{2}$.

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 $X$. Let $k$ be a homomorphism of $W$ and $Y$. Let $x_{1}$ be an element of $\operatorname{IsTerminal}$ applied to $Z$. Let $x_{2}$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $h$ and $k$. Then $\mathrm{isPullbackOfIsTerminalIsProduct}$ applied to $f$, $g$, $h$, $k$, $x_{1}$ and $x_{2}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsTerminal\_\_hom\_ext}$ applied to $x_{1}$, the composition of $h$ and $f$ and the composition of $k$ and $g$.

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 $X$. Let $k$ be a homomorphism of $W$ and $Y$. Let $x_{1}$ be an element of $\operatorname{IsInitial}$ applied to $W$. Let $x_{2}$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $f$ and $g$. Then $\mathrm{isPushoutOfIsInitialIsCoproduct}$ applied to $f$, $g$, $h$, $k$, $x_{1}$ and $x_{2}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $f$, $g$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsInitial\_\_hom\_ext}$ applied to $x_{1}$, the composition of $h$ and $f$ and the composition of $k$ and $g$.

the limit cone of F (from the name)

Let $F$ be a functor of $\operatorname{Discrete}$ applied to the set of walking pairs and $C$. Then the limit cone of $F$ is a limit cone of $F$.

the product isomorphism pullback of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the product isomorphism pullback of $X$ and $Y$ is an isomorphism of the product of $X$ and $Y$ and the pullback of the map of $X$ and the map of $Y$ defined as the isomorphism limit cone of the limit cone of the pair of $X$ and $Y$.

the coequalizer cocone of F (from the name)

Let $F$ be a functor of the set of walking parallel pairs and $C$. Then the coequalizer cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of the set of walking parallel pairs and $C$. Then $\operatorname{coequalizerCoconeIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the coequalizer cocone of $F$.

the construct coequalizer of F (from the name)

Let $F$ be a functor of the set of walking parallel pairs and $C$. Then the construct coequalizer of $F$ is an element of $C$ defined as the pushout of $\operatorname{desc}$ applied to the identity morphism of the action of $F$ and the one and the map of $F$ and the left and $\operatorname{desc}$ applied to the identity morphism of the action of $F$ and the one and the map of $F$ and the right.

the pushout left injection of F (from the name)

Let $F$ be a functor of the set of walking parallel pairs and $C$. Then the pushout left injection of $F$ is a homomorphism of the action of $F$ and the one and the construct coequalizer of $F$ defined as the left injection of $\operatorname{desc}$ applied to the identity morphism of the action of $F$ and the one and the map of $F$ and the left and $\operatorname{desc}$ applied to the identity morphism of the action of $F$ and the one and the map of $F$ and the right.

the construct equalizer of F (from the name)

Let $F$ be a functor of the set of walking parallel pairs and $C$. Then the construct equalizer of $F$ is an element of $C$ defined as the pullback of the lift of the identity morphism of the action of $F$ and the zero and the map of $F$ and the left and the lift of the identity morphism of the action of $F$ and the zero and the map of $F$ and the right.

the equalizer cone of F (from the name)

Let $F$ be a functor of the set of walking parallel pairs and $C$. Then the equalizer cone of $F$ is a cone of $F$.

Let $F$ be a functor of the set of walking parallel pairs and $C$. Then $\operatorname{equalizerConeIsLimit}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the equalizer cone of $F$.

the pullback first component of F (from the name)

Let $F$ be a functor of the set of walking parallel pairs and $C$. Then the pullback first component of $F$ is a homomorphism of the construct equalizer of $F$ and the action of $F$ and the zero defined as the first projection of the pullback of the lift of the identity morphism of the action of $F$ and the zero and the map of $F$ and the left and the lift of the identity morphism of the action of $F$ and the zero and the map of $F$ and the right.

Let $F$ be a functor of $J$ and $C$. Let $i$ be an element of $J$. Then $\operatorname{IsEventuallyConstantFrom}$ holds for $F$ and $i$, if for all elements $j$ of $J$, for all homomorphisms $f$ of $i$ and $j$, the map of $F$ and $f$ is an isomorphism.

the cocone of h (from the name)

Assume that $\operatorname{IsEventuallyConstantFrom}$ holds for $F$ and $x_{2}$. Then the cocone of $h$ is a cocone of $F$.

Assume that $\operatorname{IsEventuallyConstantFrom}$ holds for $F$ and $x_{2}$. Then $\operatorname{isColimitCocone}$ applied to $h$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $h$.

Assume that $\operatorname{IsEventuallyConstantFrom}$ holds for $F$ and $x_{2}$. Let $c$ be a cocone of $F$. Then $\operatorname{isColimitOfIsIso}$ applied to $h$ and $c$ is an element of $\operatorname{IsColimit}$ applied to $c$.

the isomorphism map of x3 (from the name)

Assume that $\operatorname{IsEventuallyConstantFrom}$ holds for $F$ and $x_{2}$. Let $x_{3}$ be a homomorphism of $i$ and $j$. Assume that $\mathrm{Nonempty}$ holds for the set of homomorphisms of $x_{2}$ and $i$. Then the isomorphism map of $x_{3}$ is an isomorphism of the action of $F$ and $i$ and the action of $F$ and $j$ defined as $\operatorname{asIso}$ applied to the map of $F$ and $x_{3}$.

Let $F$ be a functor of $J$ and $C$. Let $j$ be an element of $J$. Then $\operatorname{IsEventuallyConstantTo}$ holds for $F$ and $j$, if for all elements $i$ of $J$, for all homomorphisms $f$ of $i$ and $j$, the map of $F$ and $f$ is an isomorphism.

the cone of h (from the name)

Assume that $\operatorname{IsEventuallyConstantTo}$ holds for $F$ and $x_{2}$. Then the cone of $h$ is a cone of $F$.

Assume that $\operatorname{IsEventuallyConstantTo}$ holds for $F$ and $x_{2}$. Then $\operatorname{isLimitCone}$ applied to $h$ is an element of $\operatorname{IsLimit}$ applied to the cone of $h$.

Assume that $\operatorname{IsEventuallyConstantTo}$ holds for $F$ and $x_{2}$. Let $c$ be a cone of $F$. Then $\operatorname{isLimitOfIsIso}$ applied to $h$ and $c$ is an element of $\operatorname{IsLimit}$ applied to $c$.

the isomorphism map of x3 (from the name)

Assume that $\operatorname{IsEventuallyConstantTo}$ holds for $F$ and $x_{2}$. Let $x_{3}$ be a homomorphism of $i$ and $j$. Assume that $\mathrm{Nonempty}$ holds for the set of homomorphisms of $j$ and $x_{2}$. Then the isomorphism map of $x_{3}$ is an isomorphism of the action of $F$ and $i$ and the action of $F$ and $j$ defined as $\operatorname{asIso}$ applied to the map of $F$ and $x_{3}$.

F is eventually constant (from the name)

F is eventually constant (from the name)

Let $f$ be a function from elements of $x_{1}$ to elements of $C$. Then $\operatorname{finiteSubcoproductsCocone}$ applied to $f$ is a cocone of the lift to finite set object of the functor of $f$.

Let $f$ be a function from elements of $x_{1}$ to elements of $C$. Then $\operatorname{isColimitFiniteSubproductsCocone}$ applied to $f$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{finiteSubcoproductsCocone}$ applied to $f$.

the lift to finite set of C and x1 (from the name)

Let $C$ and $x_{1}$ be sets. Then the lift to finite set of $C$ and $x_{1}$ is a functor of the set of functors of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$ and the set of functors of the set of finite sets of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$.

the lift to finite set colimit isomorphism (from the name)

The lift to finite set colimit isomorphism is an isomorphism of the composition of the lift to finite set of $C$ and $x_{1}$ and the colimit and the colimit.

the lift to finite set colimit cocone of F (from the name)

Let $F$ be a functor of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$. Then the lift to finite set colimit cocone of $F$ is a colimit cocone of $F$.

the lift to finite set evaluation isomorphism of I (from the name)

Let $I$ be a finite set of $\operatorname{Discrete}$ applied to $x_{1}$. Then the lift to finite set evaluation isomorphism of $I$ is an isomorphism of the composition of the lift to finite set of $C$ and $x_{1}$ and the action of the evaluation of the set of finite sets of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$ and $I$ and the composition of the action of the left whiskering of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$ and the functor of the function that maps $x_{3}$ to $x_{3}$ and the colimit.

the lift to finite set object of F (from the name)

Let $F$ be a functor of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$. Then the lift to finite set object of $F$ is a functor of the set of finite sets of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$.

Let $f$ be a function from elements of $x_{1}$ to elements of $C$. Then $\operatorname{finiteSubproductsCone}$ applied to $f$ is a cone of the lift to finite set object of the functor of $f$.

Let $f$ be a function from elements of $x_{1}$ to elements of $C$. Then $\operatorname{isLimitFiniteSubproductsCone}$ applied to $f$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{finiteSubproductsCone}$ applied to $f$.

the lift to finite set of C and x1 (from the name)

Let $C$ and $x_{1}$ be sets. Then the lift to finite set of $C$ and $x_{1}$ is a functor of the set of functors of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$ and the set of functors of the set of opposites of the set of finite sets of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$.

the lift to finite set evaluation isomorphism of I (from the name)

Let $C$ and $x_{1}$ be sets. Let $I$ be a finite set of $\operatorname{Discrete}$ applied to $x_{1}$. Then the lift to finite set evaluation isomorphism of $I$ is an isomorphism of the composition of the lift to finite set of $C$ and $x_{1}$ and the action of the evaluation of the set of opposites of the set of finite sets of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$ and $\operatorname{op}$ applied to $I$ and the composition of the action of the left whiskering of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$ and the functor of the function that maps $x_{3}$ to $x_{3}$ and the limit.

the lift to finite set limit isomorphism of C and x1 (from the name)

Let $C$ and $x_{1}$ be sets. Then the lift to finite set limit isomorphism of $C$ and $x_{1}$ is an isomorphism of the composition of the lift to finite set of $C$ and $x_{1}$ and the limit and the limit.

the lift to finite set limit cone of F (from the name)

Let $F$ be a functor of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$. Then the lift to finite set limit cone of $F$ is a limit cone of $F$.

the lift to finite set object of F (from the name)

Let $F$ be a functor of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$. Then the lift to finite set object of $F$ is a functor of the set of opposites of the set of finite sets of $\operatorname{Discrete}$ applied to $x_{1}$ and $C$.

Let $x_{1}$ be a cofan of the function that maps $i$ to $f$ applied to $\operatorname{succ}$ applied to $i$. Let $x_{2}$ be a binary cofan of $f$ applied to $0$ and $\operatorname{pt}$ applied to $x_{1}$. Then $\operatorname{extendCofan}$ applied to $x_{1}$ and $x_{2}$ is a cofan of $f$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $x_{2}$ and the function that maps $i$ to $\operatorname{cases}$ applied to the left injection of $x_{2}$, the function that maps $i_{1}$ to the composition of the component of the inclusion of $x_{1}$ and $\operatorname{mk}$ applied to $i_{1}$ and the right injection of $x_{2}$ and $i$.

Let $f$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $C$. Let $x_{3}$ be an element of $\operatorname{IsColimit}$ applied to $x_{1}$. Let $x_{4}$ be an element of $\operatorname{IsColimit}$ applied to $x_{2}$. Then $\operatorname{extendCofanIsColimit}$ applied to $f$, $x_{3}$ and $x_{4}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{extendCofan}$ applied to $x_{1}$ and $x_{2}$.

Let $x_{1}$ be an element of $\operatorname{Fan}$ applied to the function that maps $i$ to $f$ applied to $\operatorname{succ}$ applied to $i$. Let $x_{2}$ be an element of $\operatorname{BinaryFan}$ applied to $f$ applied to $0$ and $\operatorname{pt}$ applied to $x_{1}$. Then $\operatorname{extendFan}$ applied to $x_{1}$ and $x_{2}$ is an element of $\operatorname{Fan}$ applied to $f$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $x_{2}$ and the function that maps $i$ to $\operatorname{cases}$ applied to the first projection of $x_{2}$, the function that maps $i_{1}$ to the composition of the second projection of $x_{2}$ and the component of the projection of $x_{1}$ and $\operatorname{mk}$ applied to $i_{1}$ and $i$.

Let $f$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $C$. Let $x_{3}$ be an element of $\operatorname{IsLimit}$ applied to $x_{1}$. Let $x_{4}$ be an element of $\operatorname{IsLimit}$ applied to $x_{2}$. Then $\operatorname{extendFanIsLimit}$ applied to $f$, $x_{3}$ and $x_{4}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{extendFan}$ applied to $x_{1}$ and $x_{2}$.

Let $s$ and $t$ be homomorphisms of $\operatorname{pt}$ applied to $x_{2}$ and $\operatorname{pt}$ applied to $x_{3}$ such that for all elements $f_{2}$ of $\Sigma$ applied to the function that maps $p_{1}$ to the set of homomorphisms of $\ProdfstMACRoZ {p_{1}}$ and $\ProdsndMACRoAA {p_{1}}$, the composition of the component of the inclusion of $x_{2}$ and $\operatorname{mk}$ applied to $f_{2}$ and $s$ is equal to the composition of the map of $F$ and $\operatorname{snd}$ applied to $f_{2}$ and the component of the inclusion of $x_{3}$ and $\operatorname{mk}$ applied to $\ProdsndMACRoAA {\operatorname{fst} (f_{2})}$ and for all elements $f$ of $\Sigma$ applied to the function that maps $p$ to the set of homomorphisms of $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$, the composition of the component of the inclusion of $x_{2}$ and $\operatorname{mk}$ applied to $f$ and $t$ is equal to the component of the inclusion of $x_{3}$ and $\operatorname{mk}$ applied to $\ProdfstMACRoZ {\operatorname{fst} (f)}$. Let $i$ be a cofork of $s$ and $t$. Then $\operatorname{buildColimit}$ applied to $s$, $t$, $\mathrm{hs}$, $\mathrm{ht}$ and $i$ is a cocone of $F$.

Let $s$ and $t$ be homomorphisms of $\operatorname{pt}$ applied to $x_{2}$ and $\operatorname{pt}$ applied to $x_{3}$ such that for all elements $f_{2}$ of $\Sigma$ applied to the function that maps $p_{1}$ to the set of homomorphisms of $\ProdfstMACRoZ {p_{1}}$ and $\ProdsndMACRoAA {p_{1}}$, the composition of the component of the inclusion of $x_{2}$ and $\operatorname{mk}$ applied to $f_{2}$ and $s$ is equal to the composition of the map of $F$ and $\operatorname{snd}$ applied to $f_{2}$ and the component of the inclusion of $x_{3}$ and $\operatorname{mk}$ applied to $\ProdsndMACRoAA {\operatorname{fst} (f_{2})}$ and for all elements $f$ of $\Sigma$ applied to the function that maps $p$ to the set of homomorphisms of $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$, the composition of the component of the inclusion of $x_{2}$ and $\operatorname{mk}$ applied to $f$ and $t$ is equal to the component of the inclusion of $x_{3}$ and $\operatorname{mk}$ applied to $\ProdfstMACRoZ {\operatorname{fst} (f)}$. Let $x_{4}$ be an element of $\operatorname{IsColimit}$ applied to $x_{2}$. Let $x_{5}$ be an element of $\operatorname{IsColimit}$ applied to $x_{3}$. Let $\mathrm{hi}$ be an element of $\operatorname{IsColimit}$ applied to $i$. Then $\operatorname{buildIsColimit}$ applied to $s$, $t$, $\mathrm{hs}$, $\mathrm{ht}$, $x_{4}$, $x_{5}$ and $\mathrm{hi}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{buildColimit}$ applied to $s$, $t$, $\mathrm{hs}$, $\mathrm{ht}$ and $i$.

Let $s$ and $t$ be homomorphisms of $\operatorname{pt}$ applied to $x_{2}$ and $\operatorname{pt}$ applied to $x_{3}$ such that for all elements $f_{2}$ of $\Sigma$ applied to the function that maps $p_{1}$ to the set of homomorphisms of $\ProdfstMACRoZ {p_{1}}$ and $\ProdsndMACRoAA {p_{1}}$, the composition of $s$ and the component of the projection of $x_{3}$ and $\operatorname{mk}$ applied to $f_{2}$ is equal to the composition of the component of the projection of $x_{2}$ and $\operatorname{mk}$ applied to $\ProdfstMACRoZ {\operatorname{fst} (f_{2})}$ and the map of $F$ and $\operatorname{snd}$ applied to $f_{2}$ and for all elements $f$ of $\Sigma$ applied to the function that maps $p$ to the set of homomorphisms of $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$, the composition of $t$ and the component of the projection of $x_{3}$ and $\operatorname{mk}$ applied to $f$ is equal to the component of the projection of $x_{2}$ and $\operatorname{mk}$ applied to $\ProdsndMACRoAA {\operatorname{fst} (f)}$. Let $x_{4}$ be an element of $\operatorname{IsLimit}$ applied to $x_{2}$. Let $x_{5}$ be an element of $\operatorname{IsLimit}$ applied to $x_{3}$. Let $\mathrm{hi}$ be an element of $\operatorname{IsLimit}$ applied to $i$. Then $\operatorname{buildIsLimit}$ applied to $s$, $t$, $\mathrm{hs}$, $\mathrm{ht}$, $x_{4}$, $x_{5}$ and $\mathrm{hi}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{buildLimit}$ applied to $s$, $t$, $\mathrm{hs}$, $\mathrm{ht}$ and $i$.

Let $s$ and $t$ be homomorphisms of $\operatorname{pt}$ applied to $x_{2}$ and $\operatorname{pt}$ applied to $x_{3}$ such that for all elements $f_{2}$ of $\Sigma$ applied to the function that maps $p_{1}$ to the set of homomorphisms of $\ProdfstMACRoZ {p_{1}}$ and $\ProdsndMACRoAA {p_{1}}$, the composition of $s$ and the component of the projection of $x_{3}$ and $\operatorname{mk}$ applied to $f_{2}$ is equal to the composition of the component of the projection of $x_{2}$ and $\operatorname{mk}$ applied to $\ProdfstMACRoZ {\operatorname{fst} (f_{2})}$ and the map of $F$ and $\operatorname{snd}$ applied to $f_{2}$ and for all elements $f$ of $\Sigma$ applied to the function that maps $p$ to the set of homomorphisms of $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$, the composition of $t$ and the component of the projection of $x_{3}$ and $\operatorname{mk}$ applied to $f$ is equal to the component of the projection of $x_{2}$ and $\operatorname{mk}$ applied to $\ProdsndMACRoAA {\operatorname{fst} (f)}$. Let $i$ be a fork of $s$ and $t$. Then $\operatorname{buildLimit}$ applied to $s$, $t$, $\mathrm{hs}$, $\mathrm{ht}$ and $i$ is a cone of $F$.

the colimit cocone of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the colimit cocone of $F$ is a colimit cocone of $F$.

the colimit quotient coproduct of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the colimit quotient coproduct of $F$ is a homomorphism of the sigma object of the function that maps $j$ to the action of $F$ and $j$ and the colimit of $F$ defined as the composition of the projection of $\operatorname{desc}$ applied to the function that maps $f$ to the composition of the map of $F$ and $\operatorname{snd}$ applied to $f$ and the inclusion of the functor of $\operatorname{obj}$ applied to $F$ and $\operatorname{mk}$ applied to $\ProdsndMACRoAA {\operatorname{fst} (f)}$ and $\operatorname{desc}$ applied to the function that maps $f_{1}$ to the inclusion of the functor of $\operatorname{obj}$ applied to $F$ and $\operatorname{mk}$ applied to $\ProdfstMACRoZ {\operatorname{fst} (f_{1})}$ and the inverse of the isomorphism colimit cocone of the colimit cocone of $F$.

the limit cone of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the limit cone of $F$ is a limit cone of $F$.

the limit subobject product of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the limit subobject product of $F$ is a homomorphism of the limit of $F$ and the product object of the function that maps $j$ to the action of $F$ and $j$ defined as the composition of the homomorphism of the isomorphism limit cone of the limit cone of $F$ and the inclusion of the lift of the function that maps $f$ to the composition of the projection from the limit object to a value of the functor of the functor of $\operatorname{obj}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{proj0}$ applied to $\operatorname{fst}$ applied to $f$ and the map of $F$ and $\operatorname{snd}$ applied to $f$ and the lift of the function that maps $f_{1}$ to the projection from the limit object to a value of the functor of the functor of $\operatorname{obj}$ applied to $F$ and $\operatorname{mk}$ applied to $\ProdsndMACRoAA {\operatorname{fst} (f_{1})}$.

Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitRaiseCone}$ applied to $t$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{raiseCone}$ applied to $c$.

the natural transformation in costructured arrow of F (from the name)

Let $F$ be a functor of $J$ and the set of costructured arrows of $K$ and $B$. Then the natural transformation in costructured arrow of $F$ is a homomorphism of the composition of $F$ and the composition of the projection of $K$ and $B$ and $K$ and the action of the constant of $J$ and $B$.

Let $c$ be a cone of the composition of $F$ and the projection of $K$ and $B$. Then $\operatorname{raiseCone}$ applied to $c$ is a cone of $F$.

the cone post of F and i (from the name)

Let $F$ be a functor of $J$ and $C$. Let $i$ be an element of $J$. Then the cone post of $F$ and $i$ is a functor of the set of cones of $F$ and the set of cones of the post of $F$.

the cone post isomorphism of F and i (from the name)

Let $F$ be a functor of $J$ and $C$. Let $i$ be an element of $J$. Then the cone post isomorphism of $F$ and $i$ is an isomorphism of the composition of the cone post of $F$ and $i$ and the functoriality of the post of $F$ and $\operatorname{forget}$ applied to the action of $F$ and $i$ and the whiskering of $\operatorname{forget}$ applied to $i$ defined as the identity of the composition of the cone post of $F$ and $i$ and the functoriality of the post of $F$ and $\operatorname{forget}$ applied to the action of $F$ and $i$.

Let $i$ be an element of $J$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitConePost}$ applied to $i$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the action of the cone post of $F$ and $i$ and $c$ defined as $\operatorname{isLimitOfReflects}$ applied to $\operatorname{forget}$ applied to the action of $F$ and $i$ and $\operatorname{symm}$ applied to $\operatorname{isLimitWhiskerEquiv}$ applied to $\operatorname{forget}$ applied to $i$ and $c$ and $\mathrm{hc}$.

the pushout cocone equivalence binary cofan functor of hc (from the name)

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the pushout cocone equivalence binary cofan functor of $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the action of the functor of the pushout cocone equivalence binary cofan and $c$.

the pushout cocone equivalence binary cofan inverse of hc (from the name)

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the pushout cocone equivalence binary cofan inverse of $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the action of the inverse of the pushout cocone equivalence binary cofan and $c$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{pullbackConeEquivBinaryFanFunctor}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the action of the functor of $\operatorname{pullbackConeEquivBinaryFan}$ and $c$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{pullbackConeEquivBinaryFanInverse}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the action of the inverse of $\operatorname{pullbackConeEquivBinaryFan}$ and $c$.

$\operatorname{pullbackConeEquivBinaryFan}$ is an equivalence of the set of pullback cones of $f$ and $g$ and $\operatorname{BinaryFan}$ applied to $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $g$.

the pushout cocone equivalence binary cofan (from the name)

The pushout cocone equivalence binary cofan is an equivalence of the set of pushout cocones of $f$ and $g$ and the set of binary cofans of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $g$.

the cone equivalence of B and F (from the name)

Let $B$ be an element of $C$. Let $F$ be a functor of $\operatorname{Discrete}$ applied to $J$ and $\operatorname{Over}$ applied to $B$. Then the cone equivalence of $B$ and $F$ is an equivalence of the set of cones of the wide pullback diagram of $B$ and $F$ and the set of cones of $F$.

the cone equivalence counit isomorphism of B and F (from the name)

Let $B$ be an element of $C$. Let $F$ be a functor of $\operatorname{Discrete}$ applied to $J$ and $\operatorname{Over}$ applied to $B$. Then the cone equivalence counit isomorphism of $B$ and $F$ is an isomorphism of the composition of the cone equivalence inverse of $B$ and $F$ and the cone equivalence functor of $B$ and $F$ and the identity of the set of cones of $F$.

the cone equivalence functor of B and F (from the name)

Let $B$ be an element of $C$. Let $F$ be a functor of $\operatorname{Discrete}$ applied to $J$ and $\operatorname{Over}$ applied to $B$. Then the cone equivalence functor of $B$ and $F$ is a functor of the set of cones of the wide pullback diagram of $B$ and $F$ and the set of cones of $F$.

the cone equivalence inverse of B and F (from the name)

Let $B$ be an element of $C$. Let $F$ be a functor of $\operatorname{Discrete}$ applied to $J$ and $\operatorname{Over}$ applied to $B$. Then the cone equivalence inverse of $B$ and $F$ is a functor of the set of cones of $F$ and the set of cones of the wide pullback diagram of $B$ and $F$.

the cone equivalence inverse object of F and c (from the name)

Let $B$ be an element of $C$. Let $F$ be a functor of $\operatorname{Discrete}$ applied to $J$ and $\operatorname{Over}$ applied to $B$. Let $c$ be a cone of $F$. Then the cone equivalence inverse object of $F$ and $c$ is a cone of the wide pullback diagram of $B$ and $F$.

the cone equivalence unit isomorphism of B and F (from the name)

Let $B$ be an element of $C$. Let $F$ be a functor of $\operatorname{Discrete}$ applied to $J$ and $\operatorname{Over}$ applied to $B$. Then the cone equivalence unit isomorphism of $B$ and $F$ is an isomorphism of the identity of the set of cones of the wide pullback diagram of $B$ and $F$ and the composition of the cone equivalence functor of $B$ and $F$ and the cone equivalence inverse of $B$ and $F$.

the wide pullback diagram of B and F (from the name)

Let $B$ be an element of $C$. Let $F$ be a functor of $\operatorname{Discrete}$ applied to $J$ and $\operatorname{Over}$ applied to $B$. Then the wide pullback diagram of $B$ and $F$ is a functor of the set of wide pullback shapes of $J$ and $C$ defined as the wide cospan of the function that maps $j$ to the left of the action of $F$ and $\operatorname{mk}$ applied to $j$ and the function that maps $j_{1}$ to the homomorphism of the action of $F$ and $\operatorname{mk}$ applied to $j_{1}$.

the product left isomorphism pullback of Y and Z (from the name)

Let $Y$ and $Z$ be elements of $\operatorname{Over}$ applied to $X$. Then the product left isomorphism pullback of $Y$ and $Z$ is an isomorphism of the left of the product of $Y$ and $Z$ and the pullback of the homomorphism of $Y$ and the homomorphism of $Z$.

Let $\mathrm{arrows}$ be a function from elements $j$ of $x_{1}$ to homomorphisms of $\mathrm{objs}$ applied to $j$ and $B$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{hB}$ be an element of $\operatorname{IsTerminal}$ applied to $B$. Then $\operatorname{isLimitOfFan}$ applied to $j$, $\mathrm{arrows}$, $\mathrm{hc}$ and $\mathrm{hB}$ is an element of $\operatorname{IsLimit}$ applied to the wide pullback cone of $c$ and $\mathrm{hB}$.

the wide pullback cone of j and c (from the name)

Let $\mathrm{arrows}$ be a function from elements $j$ of $x_{1}$ to homomorphisms of $\mathrm{objs}$ applied to $j$ and $B$. Let $c$ be an element of $\operatorname{Fan}$ applied to $\mathrm{objs}$. Let $\mathrm{hB}$ be an element of $\operatorname{IsTerminal}$ applied to $B$. Then the wide pullback cone of $\mathrm{arrows}$ and $c$ is a wide pullback cone of $\mathrm{arrows}$.

Let $\mathrm{arrows}$ be a function from elements $j$ of $x_{1}$ to homomorphisms of $\mathrm{objs}$ applied to $j$ and $B$. Let $s$ be a wide pullback cone of $\mathrm{arrows}$. Then $\operatorname{toFan}$ applied to $j$, $\mathrm{arrows}$ and $s$ is an element of $\operatorname{Fan}$ applied to $\mathrm{objs}$ defined as the function that maps $s$ to $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $\mathrm{arrows}$, $\mathrm{CategoryTheory\_\_Limits\_\_WidePullbackCone\_\_\_u3c0\_}$ applied to $\mathrm{arrows}$ and $s$.

the colimit cocone for the coproduct with a zero object of X (from the docstring)

Let $X$ be an element of $C$. Then the colimit cocone for the coproduct with a zero object of $X$ is a binary cofan of $0$ and $X$ defined as $\operatorname{mk}$ applied to $0$ and the identity morphism of $X$.

the colimit cocone for the coproduct with a zero object of X (from the docstring)

Let $X$ be an element of $C$. Then the colimit cocone for the coproduct with a zero object of $X$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone for the coproduct with a zero object of $X$.

the colimit cocone for the coproduct with a zero object of X (from the docstring)

Let $X$ be an element of $C$. Then the colimit cocone for the coproduct with a zero object of $X$ is a binary cofan of $X$ and $0$ defined as $\operatorname{mk}$ applied to the identity morphism of $X$ and $0$.

the colimit cocone for the coproduct with a zero object of X (from the docstring)

Let $X$ be an element of $C$. Then the colimit cocone for the coproduct with a zero object of $X$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone for the coproduct with a zero object of $X$.

the limit cone for the product with a zero object of X (from the docstring)

Let $X$ be an element of $C$. Then the limit cone for the product with a zero object of $X$ is an element of $\operatorname{BinaryFan}$ applied to $0$ and $X$ defined as $\operatorname{mk}$ applied to $0$ and the identity morphism of $X$.

the limit cone for the product with a zero object of X (from the docstring)

Let $X$ be an element of $C$. Then the limit cone for the product with a zero object of $X$ is an element of $\operatorname{IsLimit}$ applied to the limit cone for the product with a zero object of $X$.

the limit cone for the product with a zero object of X (from the docstring)

Let $X$ be an element of $C$. Then the limit cone for the product with a zero object of $X$ is an element of $\operatorname{BinaryFan}$ applied to $X$ and $0$ defined as $\operatorname{mk}$ applied to the identity morphism of $X$ and $0$.

the limit cone for the product with a zero object of X (from the docstring)

Let $X$ be an element of $C$. Then the limit cone for the product with a zero object of $X$ is an element of $\operatorname{IsLimit}$ applied to the limit cone for the product with a zero object of $X$.

the coproduct zero isomorphism of X (from the name)

Let $X$ be an element of $C$. Then the coproduct zero isomorphism of $X$ is an isomorphism of the coproduct of $X$ and $0$ and $X$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the colimit cocone for the coproduct with a zero object of $X$ and the colimit cocone for the coproduct with a zero object of $X$.

the product zero isomorphism of X (from the name)

Let $X$ be an element of $C$. Then the product zero isomorphism of $X$ is an isomorphism of the product of $X$ and $0$ and $X$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the limit cone for the product with a zero object of $X$ and the limit cone for the product with a zero object of $X$.

the pullback over the zero object of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $C$. Then the pullback over the zero object of $X$ and $Y$ is an isomorphism of the pullback of $0$ and $0$ and the product of $X$ and $Y$.

the pushout over the zero object of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $C$. Then the pushout over the zero object of $X$ and $Y$ is an isomorphism of the pushout of $0$ and $0$ and the coproduct of $X$ and $Y$.

the zero coproduct isomorphism of X (from the name)

Let $X$ be an element of $C$. Then the zero coproduct isomorphism of $X$ is an isomorphism of the coproduct of $0$ and $X$ and $X$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the colimit cocone for the coproduct with a zero object of $X$ and the colimit cocone for the coproduct with a zero object of $X$.

the zero product isomorphism of X (from the name)

Let $X$ be an element of $C$. Then the zero product isomorphism of $X$ is an isomorphism of the product of $0$ and $X$ and $X$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the limit cone for the product with a zero object of $X$ and the limit cone for the product with a zero object of $X$.

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

the lift of c and x3 (from the name)

Let $c$ be a cocone of the composition of $K$ and $F$. Let $x_{3}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the lift of $c$ and $x_{3}$ is an element of $\operatorname{LiftableCocone}$ applied to $K$, $F$ and $c$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $c$ and $x_{3}$.

Let $F$ be a functor of $C$ and $D$. Then an element of $\operatorname{CreatesColimits}$ applied to $F$ is an element of the function that maps $F$ to $\operatorname{CreatesColimitsOfSize}$ applied to $F$.

F creates colimits of shapes (from the name)

Let $J$ be a set. Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ creates colimits of shapes.

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

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

the lift of c and x3 (from the name)

Let $c$ be a cone of the composition of $K$ and $F$. Let $x_{3}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the lift of $c$ and $x_{3}$ is an element of $\operatorname{LiftableCone}$ applied to $K$, $F$ and $c$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $c$ and $x_{3}$.

Let $F$ be a functor of $C$ and $D$. Then an element of $\operatorname{CreatesLimits}$ applied to $F$ is an element of the function that maps $F$ to $\operatorname{CreatesLimitsOfSize}$ applied to $F$.

F creates limits of shapes (from the name)

Let $J$ be a set. Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ creates limits of shapes.

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

Let $K$ be a functor of $J$ and $C$. Let $F$ be a functor of $C$ and $D$. Let $c$ be a cocone of the composition of $K$ and $F$. Then the elements of $\operatorname{LiftableCocone}$ applied to $K$, $F$ and $c$ are a basic type.

the lifted cocone of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{LiftableCocone}$ applied to $K$, $F$ and $c$. Then the lifted cocone of $\mathrm{self}$ is a cocone of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the valid lift of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{LiftableCocone}$ applied to $K$, $F$ and $c$. Then the valid lift of $\mathrm{self}$ is an isomorphism of the map cocone of $F$ and the lifted cocone of $\mathrm{self}$ and $c$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $K$ be a functor of $J$ and $C$. Let $F$ be a functor of $C$ and $D$. Let $c$ be a cone of the composition of $K$ and $F$. Then the elements of $\operatorname{LiftableCone}$ applied to $K$, $F$ and $c$ are a basic type.

the lifted cone of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{LiftableCone}$ applied to $K$, $F$ and $c$. Then the lifted cone of $\mathrm{self}$ is a cone of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the valid lift of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{LiftableCone}$ applied to $K$, $F$ and $c$. Then the valid lift of $\mathrm{self}$ is an isomorphism of the map cone of $F$ and the lifted cone of $\mathrm{self}$ and $c$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

lift to colimit of c and t (from the name)

Let $K$ be a functor of $J$ and $C$. Let $F$ be a functor of $C$ and $D$. Let $c$ be a cocone of the composition of $K$ and $F$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the lifts to colimit of $c$ and $t$ are a basic type.

Let $\mathrm{self}$ be a lift to colimit of $c$ and $t$. Then $\operatorname{makesColimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to the lifted cocone of $\operatorname{toLiftableCocone}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

lift to limit of c and t (from the name)

Let $K$ be a functor of $J$ and $C$. Let $F$ be a functor of $C$ and $D$. Let $c$ be a cone of the composition of $K$ and $F$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the lifts to limit of $c$ and $t$ are a basic type.

Let $\mathrm{self}$ be a lift to limit of $c$ and $t$. Then $\operatorname{makesLimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to the lifted cone of $\operatorname{toLiftableCone}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the identity lift cocone of c (from the name)

Let $c$ be a cocone of the composition of $K$ and the identity of $C$. Then the identity lift cocone of $c$ is an element of $\operatorname{LiftableCocone}$ applied to $K$, the identity of $C$ and $c$.

the identity lift cone of c (from the name)

Let $c$ be a cone of the composition of $K$ and the identity of $C$. Then the identity lift cone of $c$ is an element of $\operatorname{LiftableCone}$ applied to $K$, the identity of $C$ and $c$.

the lift colimit of t (from the name)

Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the lift colimit of $t$ is a cocone of $K$ defined as the lifted cocone of the lift of $c$ and $t$.

the lift limit of t (from the name)

Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the lift limit of $t$ is a cone of $K$ defined as the lifted cone of the lift of $c$ and $t$.

the lifted cocone of t (from the docstring)

Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the lifted cocone of $t$ is an element of $\operatorname{IsColimit}$ applied to the lift colimit of $t$ defined as $\operatorname{isColimitOfReflects}$ applied to $F$ and $\operatorname{ofIsoColimit}$ applied to $t$ and the inverse of $\operatorname{liftedColimitMapsToOriginal}$ applied to $t$.

Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{liftedColimitMapsToOriginal}$ applied to $t$ is an isomorphism of the map cocone of $F$ and the lift colimit of $t$ and $c$ defined as the valid lift of the lift of $c$ and $t$.

the lifted cone of t (from the docstring)

Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the lifted cone of $t$ is an element of $\operatorname{IsLimit}$ applied to the lift limit of $t$ defined as $\operatorname{isLimitOfReflects}$ applied to $F$ and $\operatorname{ofIsoLimit}$ applied to $t$ and the inverse of $\operatorname{liftedLimitMapsToOriginal}$ applied to $t$.

Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{liftedLimitMapsToOriginal}$ applied to $t$ is an isomorphism of the map cone of $F$ and the lift limit of $t$ and $c$ defined as the valid lift of the lift of $c$ and $t$.

the lift to colimit of c and t (from the name)

Let $K$ be a functor of $J$ and $C$. Let $F$ be a functor of $C$ and $D$. Let $c$ be a cocone of the composition of $K$ and $F$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the lift to colimit of $c$ and $t$ is a lift to colimit of $c$ and $t$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the lift colimit of $t$ and $\operatorname{liftedColimitMapsToOriginal}$ applied to $t$ and the lifted cocone of $t$.

the lift to limit of c and t (from the name)

Let $K$ be a functor of $J$ and $C$. Let $F$ be a functor of $C$ and $D$. Let $c$ be a cone of the composition of $K$ and $F$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the lift to limit of $c$ and $t$ is a lift to limit of $c$ and $t$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the lift limit of $t$ and $\operatorname{liftedLimitMapsToOriginal}$ applied to $t$ and the lifted cone of $t$.

Let $F$ be a functor of $I$ and the set of elements of $A$. Then $\operatorname{isLimit}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the lifted cone of $F$.

Let $F$ be a functor of $I$ and the set of elements of $A$. Then $\operatorname{isValidLift}$ applied to $F$ is an isomorphism of the map cone of the projection of $A$ and the lifted cone of $F$ and the cone of the composition of $F$ and the projection of $A$ defined as the identity of the map cone of the projection of $A$ and the lifted cone of $F$.

the lifted cone of F (from the name)

Let $F$ be a functor of $I$ and the set of elements of $A$. Then the lifted cone of $F$ is a cone of $F$.

the lifted cone element of F (from the name)

Let $F$ be a functor of $I$ and the set of elements of $A$. Then the lifted cone element of $F$ is an element of the action of $A$ and the limit of the composition of $F$ and the projection of $A$ defined as $\operatorname{hom}$ applied to the inverse of $\operatorname{preservesLimitIso}$ applied to $A$ and the composition of $F$ and the projection of $A$ and the lifted cone element of $F$.

the lifted cone element of F (from the name)

Let $F$ be a functor of $I$ and the set of elements of $A$. Then the lifted cone element of $F$ is an element of the limit of the composition of the composition of $F$ and the projection of $A$ and $A$.

Let $\mathrm{he}$ be an element of $\operatorname{IsInitial}$ applied to $E$. Then $\operatorname{corepresentableByOfIsInitial}$ applied to $\mathrm{he}$ is an element of $\operatorname{CorepresentableBy}$ applied to $F$ and the underlying object of $E$.

Let $\mathrm{he}$ be an element of $\operatorname{IsInitial}$ applied to $E$. Then $\operatorname{representableByOfIsInitial}$ applied to $\mathrm{he}$ is an element of $\operatorname{RepresentableBy}$ applied to $F$ and the opposite of the underlying object of $E$.

exact functor of C and D (from the name)

Let $C$ and $D$ be sets. Then an exact functor of $C$ and $D$ is an element of the function that maps $C$ and $D$ to the set of full subcategories of the exact functor of $C$ and $D$.

Let $C$ and $D$ be sets. Then $\operatorname{forget}$ applied to $C$ and $D$ is a functor of the set of exact functors of $C$ and $D$ and the set of functors of $C$ and $D$ defined as the inclusion of the exact functor of $C$ and $D$.

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

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

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

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

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

left exact functor of C and D (from the name)

Let $C$ and $D$ be sets. Then a left exact functor of $C$ and $D$ is an element of the function that maps $C$ and $D$ to the set of full subcategories of the left exact functor of $C$ and $D$.

Let $C$ and $D$ be sets. Then $\operatorname{forget}$ applied to $C$ and $D$ is a functor of the set of left exact functors of $C$ and $D$ and the set of functors of $C$ and $D$ defined as the inclusion of the left exact functor of $C$ and $D$.

Let $C$ and $D$ be sets. Then $\operatorname{fullyFaithful}$ applied to $C$ and $D$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{forget}$ applied to $C$ and $D$ defined as the inclusion of the left exact functor of $C$ and $D$.

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{of}$ applied to $F$ is a left exact functor of $C$ and $D$.

the left exact functor of C and D (from the name)

Let $C$ and $D$ be sets. Then the left exact functor of $C$ and $D$ is a functor of the set of exact functors of $C$ and $D$ and the set of left exact functors of $C$ and $D$ defined as the inclusion of $\mathrm{CategoryTheory\_\_exactFunctor\_le\_leftExactFunctor}$ applied to $C$ and $D$.

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

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

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

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

right exact functor of C and D (from the name)

Let $C$ and $D$ be sets. Then a right exact functor of $C$ and $D$ is an element of the function that maps $C$ and $D$ to the set of full subcategories of the right exact functor of $C$ and $D$.

Let $C$ and $D$ be sets. Then $\operatorname{forget}$ applied to $C$ and $D$ is a functor of the set of right exact functors of $C$ and $D$ and the set of functors of $C$ and $D$ defined as the inclusion of the right exact functor of $C$ and $D$.

Let $C$ and $D$ be sets. Then $\operatorname{fullyFaithful}$ applied to $C$ and $D$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{forget}$ applied to $C$ and $D$ defined as the inclusion of the right exact functor of $C$ and $D$.

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{of}$ applied to $F$ is a right exact functor of $C$ and $D$.

the right exact functor of C and D (from the name)

Let $C$ and $D$ be sets. Then the right exact functor of $C$ and $D$ is a functor of the set of exact functors of $C$ and $D$ and the set of right exact functors of $C$ and $D$ defined as the inclusion of $\mathrm{CategoryTheory\_\_exactFunctor\_le\_rightExactFunctor}$ applied to $C$ and $D$.

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

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

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

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

the exact functor of C and D (from the name)

Let $C$ and $D$ be sets. Then the exact functor of $C$ and $D$ is an object property of the set of functors of $C$ and $D$ defined as the minimum of the left exact functor of $C$ and $D$ and the right exact functor of $C$ and $D$.

the left exact functor of C and D (from the name)

Let $C$ and $D$ be sets. Then the left exact functor of $C$ and $D$ is an object property of the set of functors of $C$ and $D$ defined as the function that maps $F$ to the proposition that $F$ preserves finite limits.

the right exact functor of C and D (from the name)

Let $C$ and $D$ be sets. Then the right exact functor of $C$ and $D$ is an object property of the set of functors of $C$ and $D$ defined as the function that maps $F$ to the proposition that $F$ preserves finite colimits.

C has cofiltered limits (from the name)

Let $C$ be a set. Then $C$ has cofiltered limits, if $\operatorname{HasCofilteredLimitsOfSize}$ holds for $C$.

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

C has filtered colimits (from the name)

Let $C$ be a set. Then $C$ has filtered colimits, if $\operatorname{HasFilteredColimitsOfSize}$ holds for $C$.

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

the colimit limit isomorphism of F (from the name)

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the colimit limit isomorphism of $F$ is an isomorphism of the colimit of the limit of $F$ and the limit of the colimit of the flip of $F$ defined as the composition of $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimitOfPreserves}$ applied to the colimit and $\operatorname{isLimit}$ applied to $F$ and $\operatorname{isLimit}$ applied to the composition of $F$ and the colimit and the isomorphism of the inverse of the colimit flip isomorphism composition colimit of $F$.

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

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

the equivalence of F and i1 (from the name)

Let $F$ be a function from elements $i_{1}$ of $x_{1}$ to functors of $I$ applied to $i_{1}$ and $C$. Let $f$ be an equivalence from $x_{3}$ to $x_{1}$. Then the equivalence of $i_{1}$ and $F$ is an isomorphism of the composition of the inverse of the equivalence of $I$ and $f$ and the pointwise product of the function that maps $i$ to $F$ applied to $f$ applied to $i$ and the pointwise product of $F$.

the cocone pointwise product of c (from the name)

Let $c$ be a function from elements $i$ of $x_{1}$ to cocones of $F$ applied to $i$. Then the cocone pointwise product of $i$ is a cocone of the pointwise product of $F$ defined as the function that maps $c$ to $\operatorname{mk}$ applied to the product object of the function that maps $i$ to $\operatorname{pt}$ applied to $i$ applied to $i$, the composition of the right whisker of the product of the function that maps $i_{1}$ to the inclusion of $i$ applied to $i_{1}$ and the functor of $x_{1}$ and the homomorphism of the constant composition product isomorphism constant of the function that maps $i_{2}$ to $\operatorname{pt}$ applied to $i$ applied to $i_{2}$ and $c$.

the cocone pointwise product isomorphism of F and i1 (from the name)

Let $F$ be a function from elements $i_{1}$ of $x_{1}$ to functors of $I$ applied to $i_{1}$ and $C$. Let $e$ be a function from elements $i$ of $x_{1}$ to isomorphisms of $c$ applied to $i$ and $\mathrm{c'}$ applied to $i$. Then the cocone pointwise product isomorphism of $i_{1}$ and $F$ is an isomorphism of the cocone pointwise product of $c$ and the cocone pointwise product of $\mathrm{c'}$.

the colimit pointwise product to product colimit of F (from the name)

Let $F$ be a function from elements $i$ of $x_{1}$ to functors of $I$ applied to $i$ and $C$. Then the colimit pointwise product to product colimit of $i$ is a homomorphism of the colimit of the pointwise product of $F$ and the product object of the function that maps $s$ to the colimit of $F$ applied to $s$ defined as the function that maps $F$ to $\operatorname{desc}$ applied to the pointwise product of $i$, the cocone pointwise product of the function that maps $s$ to the cocone of $i$ applied to $s$ and $F$.

the evaluation cocone pointwise product isomorphism of i2 and X (from the name)

Let $F$ be a function from elements $i_{2}$ of $x_{2}$ to functors of $I$ applied to $i_{2}$ and the set of functors of $D$ and $C$. Let $X$ be an element of $D$. Let $c$ be a function from elements $i_{1}$ of $x_{2}$ to cocones of $F$ applied to $i_{1}$. Then the evaluation cocone pointwise product isomorphism of $F$ and $X$ is an isomorphism of the map cocone of the action of the evaluation of $D$ and $C$ and $X$ and the cocone pointwise product of $c$ and the action of the precomposition of the homomorphism of the pointwise product composition evaluation of $F$ and $X$ and the cocone pointwise product of the function that maps $i$ to the map cocone of the action of the evaluation of $D$ and $C$ and $X$ and $c$ applied to $i$.

the pointwise product of F (from the name)

Let $F$ be a function from elements $i_{1}$ of $x_{1}$ to functors of $I$ applied to $i_{1}$ and $C$. Then the pointwise product of $i_{1}$ is a functor of the set of functions from elements $i$ of $x_{1}$ to elements of $I$ applied to $i$ and $C$ defined as the function that maps $F$ to the composition of the product of $i_{1}$ and the functor of $x_{1}$.

the pointwise product composition evaluation of F and i (from the name)

Let $F$ be a function from elements $i$ of $x_{2}$ to functors of $I$ applied to $i$ and the set of functors of $D$ and $C$. Let $d$ be an element of $D$. Then the pointwise product composition evaluation of $i$ and $F$ is an isomorphism of the composition of the pointwise product of $F$ and the action of the evaluation of $D$ and $C$ and $d$ and the pointwise product of the function that maps $s$ to the composition of $F$ applied to $s$ and the action of the evaluation of $D$ and $C$ and $d$.

F is final (from the name)

Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ is final.

the cocone equivalence of F and G (from the name)

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the cocone equivalence of $F$ and $G$ is an equivalence of the set of cocones of the composition of $F$ and $G$ and the set of cocones of $G$.

the colimit isomorphism of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the colimit isomorphism of $F$ is an isomorphism of the composition of the action of the left whiskering of $D$ and $E$ and $F$ and the colimit and the colimit.

the colimit cocone composition of F and t (from the name)

Let $F$ be a functor of $C$ and $D$. Let $t$ be a colimit cocone of $G$. Then the colimit cocone composition of $F$ and $t$ is a colimit cocone of the composition of $F$ and $G$ defined as $\operatorname{mk}$ applied to the whisker of $F$ and the cocone of $t$ and $\operatorname{symm}$ applied to $\operatorname{isColimitWhiskerEquiv}$ applied to $F$ and the cocone of $t$ and $\operatorname{isColimit}$ applied to $t$.

the colimit cocone of F and t (from the name)

Let $F$ be a functor of $C$ and $D$. Let $t$ be a colimit cocone of the composition of $F$ and $G$. Then the colimit cocone of $F$ and $t$ is a colimit cocone of $G$ defined as $\operatorname{mk}$ applied to the action of $\operatorname{extendCocone}$ and the cocone of $t$ and $\operatorname{symm}$ applied to $\operatorname{isColimitExtendCoconeEquiv}$ applied to $F$ and the cocone of $t$ and $\operatorname{isColimit}$ applied to $t$.

the colimit composition Coyoneda isomorphism of F and d (from the name)

Let $F$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Then the colimit composition Coyoneda isomorphism of $F$ and $d$ is an isomorphism of the colimit of the composition of $F$ and the action of the Coyoneda and $\operatorname{op}$ applied to $d$ and $\mathrm{PUnit}$ defined as the composition of $\operatorname{asIso}$ applied to $\operatorname{pre}$ applied to the action of the Coyoneda and $\operatorname{op}$ applied to $d$ and $F$ and the colimit of $\operatorname{op}$ applied to $d$.

the colimit isomorphism of F and G (from the name)

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the colimit isomorphism of $F$ and $G$ is an isomorphism of the colimit of the composition of $F$ and $G$ and the colimit of $G$ defined as $\operatorname{asIso}$ applied to $\operatorname{pre}$ applied to $G$ and $F$.

$\operatorname{extendCocone}$ is a functor of the set of cocones of the composition of $F$ and $G$ and the set of cocones of $G$.

the homomorphism to lift of F and d (from the name)

Let $F$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Then the homomorphism to lift of $F$ and $d$ is a homomorphism of $d$ and the action of $F$ and the lift of $F$ and $d$ defined as the homomorphism of $\operatorname{arbitrary}$ applied to the set of structured arrows of $d$ and $F$.

the induction of x2 and x11 (from the name)

Let $F$ be a functor of $C$ and $D$. Let $Z$ be a function from elements $X$ of $C$ and homomorphisms of $d$ and the action of $F$ and $X$ to sets. Let $x_{2}$ be a function from elements $x_{11}$ of $C$ and elements $x_{12}$ of $C$ and homomorphisms $x_{13}$ of $d$ and the action of $F$ and $x_{11}$ and homomorphisms $x_{14}$ of $d$ and the action of $F$ and $x_{12}$ and homomorphisms $f_{1}$ of $x_{11}$ and $x_{12}$ and elements of $\mathrm{Proof}$ applied to the proposition that the composition of $x_{13}$ and the map of $F$ and $f_{1}$ is equal to $x_{14}$ and elements of $Z$ applied to $x_{11}$ and $x_{13}$ to elements of $Z$ applied to $x_{12}$ and $x_{14}$. Let $x_{3}$ be a function from elements $x_{6}$ of $C$ and elements $x_{7}$ of $C$ and homomorphisms $x_{8}$ of $d$ and the action of $F$ and $x_{6}$ and homomorphisms $x_{9}$ of $d$ and the action of $F$ and $x_{7}$ and homomorphisms $f$ of $x_{6}$ and $x_{7}$ and elements of $\mathrm{Proof}$ applied to the proposition that the composition of $x_{8}$ and the map of $F$ and $f$ is equal to $x_{9}$ and elements of $Z$ applied to $x_{7}$ and $x_{9}$ to elements of $Z$ applied to $x_{6}$ and $x_{8}$. Let $z$ be an element of $Z$ applied to $x_{4}$ and $x_{5}$. Then the induction of $x_{11}$ and $x_{12}$ is an element of $Z$ applied to the lift of $F$ and $d$ and the homomorphism to lift of $F$ and $d$.

Let $F$ be a functor of $C$ and $D$. Let $t$ be a cocone of the composition of $F$ and $G$. Then $\operatorname{isColimitExtendCoconeEquiv}$ applied to $F$ and $t$ is an equivalence from $\operatorname{IsColimit}$ applied to the action of $\operatorname{extendCocone}$ and $t$ to $\operatorname{IsColimit}$ applied to $t$ defined as $\operatorname{ofCoconeEquiv}$ applied to the cocone equivalence of $F$ and $G$.

Let $F$ be a functor of $C$ and $D$. Let $t$ be a cocone of $G$. Then $\operatorname{isColimitWhiskerEquiv}$ applied to $F$ and $t$ is an equivalence from $\operatorname{IsColimit}$ applied to the whisker of $F$ and $t$ to $\operatorname{IsColimit}$ applied to $t$ defined as $\operatorname{ofCoconeEquiv}$ applied to the inverse of the cocone equivalence of $F$ and $G$.

the lift of F and d (from the name)

Let $F$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Then the lift of $F$ and $d$ is an element of $C$ defined as the right object of $\operatorname{arbitrary}$ applied to the set of structured arrows of $d$ and $F$.

F is initial (from the name)

Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ is initial.

the cone equivalence of F and G (from the name)

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the cone equivalence of $F$ and $G$ is an equivalence of the set of cones of the composition of $F$ and $G$ and the set of cones of $G$.

$\operatorname{extendCone}$ is a functor of the set of cones of the composition of $F$ and $G$ and the set of cones of $G$.

the homomorphism to lift of F and d (from the name)

Let $F$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Then the homomorphism to lift of $F$ and $d$ is a homomorphism of the action of $F$ and the lift of $F$ and $d$ and $d$ defined as the homomorphism of $\operatorname{arbitrary}$ applied to the set of costructured arrows of $F$ and $d$.

the induction of x2 and x11 (from the name)

Let $F$ be a functor of $C$ and $D$. Let $Z$ be a function from elements $X$ of $C$ and homomorphisms of the action of $F$ and $X$ and $d$ to sets. Let $x_{2}$ be a function from elements $x_{11}$ of $C$ and elements $x_{12}$ of $C$ and homomorphisms $x_{13}$ of the action of $F$ and $x_{11}$ and $d$ and homomorphisms $x_{14}$ of the action of $F$ and $x_{12}$ and $d$ and homomorphisms $f_{1}$ of $x_{11}$ and $x_{12}$ and elements of $\mathrm{Proof}$ applied to the proposition that the composition of the map of $F$ and $f_{1}$ and $x_{14}$ is equal to $x_{13}$ and elements of $Z$ applied to $x_{11}$ and $x_{13}$ to elements of $Z$ applied to $x_{12}$ and $x_{14}$. Let $x_{3}$ be a function from elements $x_{6}$ of $C$ and elements $x_{7}$ of $C$ and homomorphisms $x_{8}$ of the action of $F$ and $x_{6}$ and $d$ and homomorphisms $x_{9}$ of the action of $F$ and $x_{7}$ and $d$ and homomorphisms $f$ of $x_{6}$ and $x_{7}$ and elements of $\mathrm{Proof}$ applied to the proposition that the composition of the map of $F$ and $f$ and $x_{9}$ is equal to $x_{8}$ and elements of $Z$ applied to $x_{7}$ and $x_{9}$ to elements of $Z$ applied to $x_{6}$ and $x_{8}$. Let $z$ be an element of $Z$ applied to $x_{4}$ and $x_{5}$. Then the induction of $x_{11}$ and $x_{12}$ is an element of $Z$ applied to the lift of $F$ and $d$ and the homomorphism to lift of $F$ and $d$.

Let $F$ be a functor of $C$ and $D$. Let $t$ be a cone of the composition of $F$ and $G$. Then $\operatorname{isLimitExtendConeEquiv}$ applied to $F$ and $t$ is an equivalence from $\operatorname{IsLimit}$ applied to the action of $\operatorname{extendCone}$ and $t$ to $\operatorname{IsLimit}$ applied to $t$ defined as $\operatorname{ofConeEquiv}$ applied to the cone equivalence of $F$ and $G$.

Let $F$ be a functor of $C$ and $D$. Let $t$ be a cone of $G$. Then $\operatorname{isLimitWhiskerEquiv}$ applied to $F$ and $t$ is an equivalence from $\operatorname{IsLimit}$ applied to the whisker of $F$ and $t$ to $\operatorname{IsLimit}$ applied to $t$ defined as $\operatorname{ofConeEquiv}$ applied to the inverse of the cone equivalence of $F$ and $G$.

the lift of F and d (from the name)

Let $F$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Then the lift of $F$ and $d$ is an element of $C$ defined as the left object of $\operatorname{arbitrary}$ applied to the set of costructured arrows of $F$ and $d$.

the limit isomorphism of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the limit isomorphism of $F$ is an isomorphism of the composition of the action of the left whiskering of $D$ and $E$ and $F$ and the limit and the limit.

the limit cone composition of F and t (from the name)

Let $F$ be a functor of $C$ and $D$. Let $t$ be a limit cone of $G$. Then the limit cone composition of $F$ and $t$ is a limit cone of the composition of $F$ and $G$ defined as $\operatorname{mk}$ applied to the whisker of $F$ and the cone of $t$ and $\operatorname{symm}$ applied to $\operatorname{isLimitWhiskerEquiv}$ applied to $F$ and the cone of $t$ and $\operatorname{isLimit}$ applied to $t$.

the limit cone of F and t (from the name)

Let $F$ be a functor of $C$ and $D$. Let $t$ be a limit cone of the composition of $F$ and $G$. Then the limit cone of $F$ and $t$ is a limit cone of $G$ defined as $\operatorname{mk}$ applied to the action of $\operatorname{extendCone}$ and the cone of $t$ and $\operatorname{symm}$ applied to $\operatorname{isLimitExtendConeEquiv}$ applied to $F$ and the cone of $t$ and $\operatorname{isLimit}$ applied to $t$.

the limit isomorphism of F and G (from the name)

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the limit isomorphism of $F$ and $G$ is an isomorphism of the limit of the composition of $F$ and $G$ and the limit of $G$ defined as the inverse of $\operatorname{asIso}$ applied to $\operatorname{pre}$ applied to $G$ and $F$.

the fiberwise colimit map composition equivalence of x1 and H (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $G$. Let $H$ be a functor of $\operatorname{Grothendieck}$ applied to $G$ and the set of sets. Then the fiberwise colimit map composition equivalence of $x_{1}$ and $H$ is an isomorphism of the fiberwise colimit of the composition of the map of $x_{1}$ and $H$ and the fiberwise colimit of $H$.

the structured arrow to structured arrow of d and f (from the name)

Let $F$ be a functor of $D$ and the set of categories. Let $G$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Let $f$ be an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of $F$ and $d$. Then the structured arrow to structured arrow of $d$ and $f$ is a prefunctor of the set of structured arrows of $d$ and $G$ and the set of structured arrows of $\operatorname{mk}$ applied to $d$ and $f$ and $\operatorname{pre}$ applied to $F$ and $G$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $j$ be an element of $J$. Then $\operatorname{underPost}$ applied to $\mathrm{hc}$ and $j$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{underPost}$ applied to $c$ and $j$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $j$ be an element of $J$. Then $\operatorname{overPost}$ applied to $\mathrm{hc}$ and $j$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{overPost}$ applied to $c$ and $j$.

the colimit type precomposition of P and x2 (from the name)

Let $F$ be a functor of $C$ and $D$. Let $P$ be a functor of $D$ and the set of sets. Let $x_{2}$ be a colimit type of the composition of $F$ and $P$. Then the colimit type precomposition of $P$ and $x_{2}$ is a colimit type of $P$ defined as $\operatorname{descColimitType}$ applied to the composition of $F$ and $P$, the precomposition of the cocone type of $P$ and $F$ and $x_{2}$.

the section precomposition of F and x2 (from the name)

Let $F$ be a functor of $C$ and $D$. Let $x_{2}$ be an element of the section of $P$. Then the section precomposition of $F$ and $x_{2}$ is an element of the section of the composition of $F$ and $P$ defined as the function that maps $x_{3}$ to the action of $F$ and $x_{3}$.

final model of J (from the name)

Let $J$ be a set. Then a final model of $J$ is an element of the function that maps $J$ to $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_FinallySmall\_\_final\_smallCategory}$.

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

initial model of J (from the name)

Let $J$ be a set. Then an initial model of $J$ is an element of the function that maps $J$ to $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_InitiallySmall\_\_initial\_smallCategory}$.

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

Let $J$ be a set. Then $\operatorname{fromFinalModel}$ applied to $J$ is a functor of the set of final models of $J$ and $J$.

Let $J$ be a set. Then $\operatorname{fromInitialModel}$ applied to $J$ is a functor of the set of initial models of $J$ and $J$.

the categorical product in X (from the docstring)

Let $X$ be a function from elements of $x$ to finite type categories. Then the categorical product in $X$ is an equivalence from the object of the product object of $X$ to the set of functions from elements $i$ of $x$ to elements of the object of $X$ applied to $i$ defined as the composition of $\operatorname{symm}$ applied to the equivalence equivalence isomorphism and the isomorphism of the inclusion and the function that maps $i_{7}$ to $X$ applied to $i_{7}$ and the composition of $\operatorname{symm}$ applied to the equivalence equivalence isomorphism and the categorical product in the function that maps $i_{8}$ to the object of $X$ applied to $i_{8}$ and the inverse of the equivalence shrink of the set of functions from elements $i_{9}$ of $x$ to elements of the object of $X$ applied to $i_{9}$.

formal coproduct of C (from the name)

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

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be formal coproducts of $C$. Then the homomorphisms of $X$ and $Y$ are a basic type.

Let $f$ be a homomorphism of the action of the inclusion of $C$ and $X$ and $Y$. Then $\operatorname{asSigma}$ applied to $f$ is an element of $\Sigma$ applied to the function that maps $i$ to the set of homomorphisms of $X$ and the object of $Y$ and $i$ defined as $\operatorname{mk}$ applied to $\operatorname{f}$ applied to $f$ and $\operatorname{unit}$ and $\mathrm{CategoryTheory\_\_Limits\_\_FormalCoproduct\_\_Hom\_\_\_u3c6\_}$ applied to $f$ and $\operatorname{unit}$.

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

Let $i$ be an element of $\operatorname{I}$ applied to $Y$. Let $f$ be a homomorphism of $X$ and the object of $Y$ and $i$. Then $\operatorname{fromIncl}$ applied to $i$ and $f$ is a homomorphism of the action of the inclusion of $C$ and $X$ and $Y$ defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ to $i$ and the function that maps $x_{2}$ to $f$.

Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Let $i$ be an element of $\operatorname{I}$ applied to $X$. Then $\mathrm{CategoryTheory\_\_Limits\_\_FormalCoproduct\_\_Hom\_\_\_u3c6\_}$ applied to $\mathrm{self}$ and $i$ is a homomorphism of the object of $X$ and $i$ and the object of $Y$ and $\operatorname{f}$ applied to $\mathrm{self}$ and $i$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $i$.

Let $\mathrm{self}$ be a formal coproduct of $C$. Then an element of $\operatorname{I}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

the cofan of x1 and f (from the name)

Let $x_{1}$ be a set. Let $f$ be a function from elements of $x_{1}$ to formal coproducts of $C$. Then the cofan of $x_{1}$ and $f$ is a cofan of $f$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\Sigma$ applied to the function that maps $i$ to $\operatorname{I}$ applied to $f$ applied to $i$ and the function that maps $p$ to the object of $f$ applied to $\operatorname{fst}$ applied to $p$ and $\operatorname{snd}$ applied to $p$ and the function that maps $i_{1}$ to $\operatorname{mk}$ applied to the function that maps $x_{2}$ to $\operatorname{mk}$ applied to $i_{1}$ and $x_{2}$ and the function that maps $x_{3}$ to the identity morphism of the object of $f$ applied to $i_{1}$ and $x_{3}$.

the cofan homomorphism equivalence of f and t (from the name)

Let $x_{1}$ be a set. Let $f$ be a function from elements of $x_{1}$ to formal coproducts of $C$. Let $t$ be a formal coproduct of $C$. Then the cofan homomorphism equivalence of $f$ and $t$ is an equivalence from the set of homomorphisms of $\operatorname{pt}$ applied to the cofan of $x_{1}$ and $f$ and $t$ to the set of functions from elements $i$ of $x_{1}$ to homomorphisms of $f$ applied to $i$ and $t$.

Let $X$ be a formal coproduct of $C$. Then $\operatorname{cofanPtIsoSelf}$ applied to $X$ is an isomorphism of $\operatorname{pt}$ applied to the cofan of $\operatorname{I}$ applied to $X$ and $\operatorname{toFun}$ applied to $X$ and $X$ defined as the isomorphism of the sigma unit of $\operatorname{I}$ applied to $X$ and the function that maps $i$ to the identity of the object of $X$ and $\operatorname{fst}$ applied to $i$.

the arbitrary choice of the coproduct of x1 and f (from the docstring)

Let $x_{1}$ be a set. Let $f$ be a function from elements of $x_{1}$ to formal coproducts of $C$. Then the arbitrary choice of the coproduct of $x_{1}$ and $f$ is an isomorphism of the sigma object of $f$ and $\operatorname{pt}$ applied to the cofan of $x_{1}$ and $f$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the cofan of $x_{1}$ and $f$ and $\operatorname{isColimitCofan}$ applied to $x_{1}$ and $f$.

the isomorphism between the coproduct of X (from the docstring)

Let $X$ be a formal coproduct of $C$. Then the isomorphism between the coproduct of $X$ is an isomorphism of the sigma object of $\operatorname{toFun}$ applied to $X$ and $X$ defined as the composition of the arbitrary choice of the coproduct of $\operatorname{I}$ applied to $X$ and $\operatorname{toFun}$ applied to $X$ and $\operatorname{cofanPtIsoSelf}$ applied to $X$.

the evaluation of C and A (from the name)

Let $C$ and $A$ be sets. Then the evaluation of $C$ and $A$ is a functor of the set of functors of $C$ and $A$ and the set of functors of the set of formal coproducts of $C$ and $A$.

the evaluation composition inclusion isomorphism identity of C and A (from the name)

Let $C$ and $A$ be sets. Then the evaluation composition inclusion isomorphism identity of $C$ and $A$ is an isomorphism of the composition of the evaluation of $C$ and $A$ and the action of the left whiskering of the set of formal coproducts of $C$ and $A$ and the inclusion of $C$ and the identity of the set of functors of $C$ and $A$.

the evaluation opposite of C and A (from the name)

Let $C$ and $A$ be sets. Then the evaluation opposite of $C$ and $A$ is a functor of the set of functors of the set of opposites of $C$ and $A$ and the set of functors of the set of opposites of the set of formal coproducts of $C$ and $A$.

the evaluation opposite composition left injection isomorphism identity of C and A (from the name)

Let $C$ and $A$ be sets. Then the evaluation opposite composition left injection isomorphism identity of $C$ and $A$ is an isomorphism of the composition of the evaluation opposite of $C$ and $A$ and the action of the left whiskering of the set of opposites of the set of formal coproducts of $C$ and $A$ and the opposite of the inclusion of $C$ and the identity of the set of functors of the set of opposites of $C$ and $A$.

the fully faithful inclusion (from the name)

the homomorphism of f and x1 (from the name)

Let $X$ be an element of $C$. Let $f$ be a function from elements of $J$ to elements of $C$. Let $x_{1}$ be a function from elements $j$ of $J$ to homomorphisms of $f$ applied to $j$ and $X$. Then the homomorphism of $f$ and $j$ is a homomorphism of $\operatorname{mk}$ applied to $J$ and $f$ and the action of the inclusion of $C$ and $X$ defined as the function that maps $x_{1}$ to $\operatorname{mk}$ applied to the function that maps $x_{2}$ to $\operatorname{unit}$, $j$ and $x_{1}$.

the homomorphism pullback equivalence of i1 and hpb (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $\mathrm{pb}$ be a function from pullbacks $i_{1}$ of $\operatorname{f}$ applied to $f$ and $\operatorname{f}$ applied to $g$ to pullback cones of the composition of $\mathrm{CategoryTheory\_\_Limits\_\_FormalCoproduct\_\_Hom\_\_\_u3c6\_}$ applied to $f$ and $\ProdfstMACRoZ {i_{1}}$ and $\operatorname{eqToHom}$ applied to $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Limits\_\_FormalCoproducts\_\_Basic\_\_0\_\_\_proof\_107}$ applied to $f$, $g$ and $i_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_FormalCoproduct\_\_Hom\_\_\_u3c6\_}$ applied to $g$ and $\ProdsndMACRoAA {i_{1}}$. Let $\mathrm{hpb}$ be a function from pullbacks $i$ of $\operatorname{f}$ applied to $f$ and $\operatorname{f}$ applied to $g$ to elements of $\operatorname{IsLimit}$ applied to $\mathrm{pb}$ applied to $i$. Let $T$ be a formal coproduct of $C$. Then the homomorphism pullback equivalence of $\mathrm{pb}$ and $i$ is an element of $\EquivMACRoAE {\operatorname{Hom} (T , \operatorname{pt} (\operatorname{pullbackCone} (g , \mathrm{pb})))}{(\SubtypeSet {p}{(\EqtMACRoH {\operatorname{comp} (\ProdfstMACRoZ {p}, f)}{\operatorname{comp} (\ProdsndMACRoAA {p}, g)})})}$.

the inclusion of C (from the name)

Let $C$ be a set. Then the inclusion of $C$ is a functor of $C$ and the set of formal coproducts of $C$.

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

Let $X$ be an element of $C$. Let $Y$ be a formal coproduct of $C$. Then the inclusion homomorphism equivalence of $X$ and $Y$ is an equivalence from the set of homomorphisms of the action of the inclusion of $C$ and $X$ and $Y$ to $\Sigma$ applied to the function that maps $i$ to the set of homomorphisms of $X$ and the object of $Y$ and $i$.

Let $x_{1}$ be a set. Let $f$ be a function from elements of $x_{1}$ to formal coproducts of $C$. Then $\operatorname{isColimitCofan}$ applied to $x_{1}$ and $f$ is an element of $\operatorname{IsColimit}$ applied to the cofan of $x_{1}$ and $f$.

Let $J$ be a set. Let $f$ be a function from elements of $J$ to formal coproducts of $C$. Let $F$ be a functor of $C$ and $A$. Then $\operatorname{isColimitEvalMapCoconeCofan}$ applied to $J$, $f$ and $F$ is an element of $\operatorname{IsColimit}$ applied to the map cocone of the action of the evaluation of $C$ and $A$ and $F$ and the cofan of $J$ and $f$.

Let $J$ be a set. Let $f$ be a function from elements of $J$ to formal coproducts of $C$. Let $F$ be a functor of the set of opposites of $C$ and $A$. Then $\operatorname{isLimitEvalMapConeCofanOp}$ applied to $J$, $f$ and $F$ is an element of $\operatorname{IsLimit}$ applied to the map cone of the action of the evaluation opposite of $C$ and $A$ and $F$ and the opposite of the cofan of $J$ and $f$.

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $\mathrm{pb}$ be a function from pullbacks $i_{1}$ of $\operatorname{f}$ applied to $f$ and $\operatorname{f}$ applied to $g$ to pullback cones of the composition of $\mathrm{CategoryTheory\_\_Limits\_\_FormalCoproduct\_\_Hom\_\_\_u3c6\_}$ applied to $f$ and $\ProdfstMACRoZ {i_{1}}$ and $\operatorname{eqToHom}$ applied to $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Limits\_\_FormalCoproducts\_\_Basic\_\_0\_\_\_proof\_107}$ applied to $f$, $g$ and $i_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_FormalCoproduct\_\_Hom\_\_\_u3c6\_}$ applied to $g$ and $\ProdsndMACRoAA {i_{1}}$. Let $\mathrm{hpb}$ be a function from pullbacks $i$ of $\operatorname{f}$ applied to $f$ and $\operatorname{f}$ applied to $g$ to elements of $\operatorname{IsLimit}$ applied to $\mathrm{pb}$ applied to $i$. Then $\operatorname{isLimitPullbackCone}$ applied to $f$, $g$, $i_{1}$, $\mathrm{pb}$, $i$ and $\mathrm{hpb}$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone of $g$ and $\mathrm{pb}$.

Let $T$ be an element of $C$. Let $\mathrm{ht}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then $\operatorname{isTerminalIncl}$ applied to $T$ and $\mathrm{ht}$ is an element of $\operatorname{IsTerminal}$ applied to the action of the inclusion of $C$ and $T$.

the isomorphism of e and h (from the name)

Let $e$ be an element of $\EquivMACRoAE {\operatorname{I} (X)}{\operatorname{I} (Y)}$. Let $h$ be a function from elements $i$ of $\operatorname{I}$ applied to $X$ to isomorphisms of the object of $X$ and $i$ and the object of $Y$ and $e$ applied to $i$. Then the isomorphism of $e$ and $i$ is an isomorphism of $X$ and $Y$.

the object of self and i (from the name)

Let $\mathrm{self}$ be a formal coproduct of $C$. Let $i$ be an element of $\operatorname{I}$ applied to $\mathrm{self}$. Then the object of $\mathrm{self}$ and $i$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $i$.

the object isomorphism of X and hij (from the name)

Let $X$ be a formal coproduct of $C$. Assume that $\EqtMACRoH {i}{j}$. Then the object isomorphism of $X$ and $\mathrm{hij}$ is an isomorphism of the object of $X$ and $i$ and the object of $X$ and $j$.

the pullback cone of g and pb (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $\mathrm{pb}$ be a function from pullbacks $i$ of $\operatorname{f}$ applied to $f$ and $\operatorname{f}$ applied to $g$ to pullback cones of the composition of $\mathrm{CategoryTheory\_\_Limits\_\_FormalCoproduct\_\_Hom\_\_\_u3c6\_}$ applied to $f$ and $\ProdfstMACRoZ {i}$ and $\operatorname{eqToHom}$ applied to $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Limits\_\_FormalCoproducts\_\_Basic\_\_0\_\_\_proof\_107}$ applied to $f$, $g$ and $i$ and $\mathrm{CategoryTheory\_\_Limits\_\_FormalCoproduct\_\_Hom\_\_\_u3c6\_}$ applied to $g$ and $\ProdsndMACRoAA {i}$. Then the pullback cone of $g$ and $i$ is a pullback cone of $f$ and $g$.

the shrink Yoneda (from the name)

The shrink Yoneda is a functor of the set of formal coproducts of $C$ and the set of functors of the set of opposites of $C$ and the set of sets defined as the action of the evaluation of $C$ and the set of functors of the set of opposites of $C$ and the set of sets and the Yoneda embedding.

the formal coproduct of X and x1 (from the name)

Let $X$ be a formal coproduct of $C$. Let $x_{1}$ be an element of $\operatorname{I}$ applied to $X$. Then the formal coproduct of $X$ and $x_{1}$ is a formal coproduct of $C$ defined as $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to the inclusion of $C$, $\operatorname{obj}$ applied to $X$ and $x_{1}$.

the lift Yoneda (from the name)

The lift Yoneda is a functor of the set of formal coproducts of $C$ and the set of functors of the set of opposites of $C$ and the set of sets defined as the action of the evaluation of $C$ and the set of functors of the set of opposites of $C$ and the set of sets and the lift Yoneda.

the Yoneda (from the name)

The Yoneda is a functor of the set of formal coproducts of $C$ and the set of functors of the set of opposites of $C$ and the set of sets defined as the action of the evaluation of $C$ and the set of functors of the set of opposites of $C$ and the set of sets and the Yoneda.

the Cech of U (from the name)

Let $U$ be a formal coproduct of $C$. Then the Cech of $U$ is a simplicial object of the set of formal coproducts of $C$.

the functor (from the docstring)

The functor is a functor of the set of formal coproducts of $C$ and the set of simplicial objects of the set of formal coproducts of $C$.

Let $U$ be a formal coproduct of $C$. Let $x_{1}$ be a set. Then $\operatorname{isLimitPowerFan}$ applied to $U$ and $x_{1}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{powerFan}$ applied to $U$ and $x_{1}$.

the map power of U and f (from the name)

Let $U$ be a formal coproduct of $C$. Let $f$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Then the map power of $U$ and $f$ is a homomorphism of the power of $U$ and $x_{2}$ and the power of $U$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to $\operatorname{comp}$ applied to $i$ and $f$ and the function that maps $x_{3}$ to the lift of the function that maps $x_{4}$ to the projection of $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to $U$ and $x_{3}$ and $f$ applied to $x_{4}$.

the power of U and x1 (from the name)

Let $U$ be a formal coproduct of $C$. Let $x_{1}$ be a set. Then the power of $U$ and $x_{1}$ is a formal coproduct of $C$ defined as $\operatorname{mk}$ applied to the set of functions from elements of $x_{1}$ to elements of $\operatorname{I}$ applied to $U$ and the function that maps $i$ to the product object of $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to $U$ and $i$.

the power bifunctor (from the name)

The power bifunctor is a functor of the set of opposites of the set of sets and the set of functors of the set of formal coproducts of $C$ and the set of formal coproducts of $C$.

Let $U$ be a formal coproduct of $C$. Let $x_{1}$ be a set. Then $\operatorname{powerFan}$ applied to $U$ and $x_{1}$ is an element of $\operatorname{Fan}$ applied to the function that maps $x_{2}$ to $U$ defined as $\operatorname{mk}$ applied to the power of $U$ and $x_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_FormalCoproduct\_\_power\_u3c0\_}$ applied to $U$.

the power functor of x1 (from the name)

Let $x_{1}$ be a set. Then the power functor of $x_{1}$ is a functor of the set of formal coproducts of $C$ and the set of formal coproducts of $C$.

the power map of f and x1 (from the name)

Let $f$ be a homomorphism of $U$ and $V$. Let $x_{1}$ be a set. Then the power map of $f$ and $x_{1}$ is a homomorphism of the power of $U$ and $x_{1}$ and the power of $V$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to $\operatorname{comp}$ applied to $\operatorname{f}$ applied to $f$ and $i$ and the function that maps $i_{1}$ to the map of the function that maps $a$ to $\mathrm{CategoryTheory\_\_Limits\_\_FormalCoproduct\_\_Hom\_\_\_u3c6\_}$ applied to $f$ and $i_{1}$ applied to $a$.

the projection of U and a (from the docstring)

Let $U$ be a formal coproduct of $C$. Let $a$ be an element of $x_{1}$. Then the projection of $U$ and $a$ is a homomorphism of the power of $U$ and $x_{1}$ and $U$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to $i$ applied to $a$ and the function that maps $x_{2}$ to the projection of $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to $U$ and $x_{2}$ and $a$.

the Cech isomorphism augmented Cech nerve of U and hT (from the name)

Let $U$ be a formal coproduct of $C$. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then the Cech isomorphism augmented Cech nerve of $U$ and $\mathrm{hT}$ is an isomorphism of $\operatorname{augmentOfIsTerminal}$ applied to the Cech of $U$ and $\operatorname{isTerminalIncl}$ applied to $T$ and $\mathrm{hT}$ and the augmented Cech nerve of $\operatorname{mk}$ applied to $\operatorname{from}$ applied to $\operatorname{isTerminalIncl}$ applied to $T$ and $\mathrm{hT}$ and $U$.

the Cech isomorphism Cech nerve of U and hT (from the name)

Let $U$ be a formal coproduct of $C$. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then the Cech isomorphism Cech nerve of $U$ and $\mathrm{hT}$ is an isomorphism of the Cech of $U$ and the Cech nerve of $\operatorname{mk}$ applied to $\operatorname{from}$ applied to $\operatorname{isTerminalIncl}$ applied to $T$ and $\mathrm{hT}$ and $U$.

the Cech object of U (from the docstring)

Let $U$ be a formal coproduct of $C$. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Let $d$ be a homomorphism of $T$ and the object of $U$ and $x_{1}$. Then the Cech object of $U$ is an extra degeneracy of $\operatorname{augmentOfIsTerminal}$ applied to the Cech of $U$ and $\operatorname{isTerminalIncl}$ applied to $T$ and $\mathrm{hT}$.

diagram of cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the diagrams of cocone of $F$ are a basic type.

the cocone point of D (from the name)

Let $D$ be a diagram of cocone of $F$. Then the cocone point of $D$ is a functor of $J$ and $C$ defined as $\operatorname{mk}$ applied to the function that maps $j$ to $\operatorname{pt}$ applied to the object of $D$ and $j$, the function that maps $x_{3}$, $x_{4}$ and $f$ to the homomorphism of the map of $D$ and $f$, the function that maps $j_{1}$ to $\operatorname{id}$ applied to $D$ and $j_{1}$ and the function that maps $x_{5}$, $x_{6}$, $x_{7}$, $f_{1}$ and $g$ to $\operatorname{comp}$ applied to $D$, $f_{1}$ and $g$.

the map of self and f (from the name)

Let $\mathrm{self}$ be a diagram of cocone of $F$. Let $f$ be a homomorphism of $j$ and $\mathrm{j'}$. Then the map of $\mathrm{self}$ and $f$ is a homomorphism of the object of $\mathrm{self}$ and $j$ and the action of the precomposition of the map of $F$ and $f$ and the object of $\mathrm{self}$ and $\mathrm{j'}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $f$.

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then $\operatorname{mkOfHasColimits}$ applied to $F$ is a diagram of cocone of $F$.

the object of self and j (from the name)

Let $\mathrm{self}$ be a diagram of cocone of $F$. Let $j$ be an element of $J$. Then the object of $\mathrm{self}$ and $j$ is a cocone of the action of $F$ and $j$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $j$.

diagram of cone of F (from the name)

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the diagrams of cone of $F$ are a basic type.

the cone point of D (from the name)

Let $D$ be a diagram of cone of $F$. Then the cone point of $D$ is a functor of $J$ and $C$ defined as $\operatorname{mk}$ applied to the function that maps $j$ to $\operatorname{pt}$ applied to the object of $D$ and $j$, the function that maps $x_{3}$, $x_{4}$ and $f$ to the homomorphism of the map of $D$ and $f$, the function that maps $j_{1}$ to $\operatorname{id}$ applied to $D$ and $j_{1}$ and the function that maps $x_{5}$, $x_{6}$, $x_{7}$, $f_{1}$ and $g$ to $\operatorname{comp}$ applied to $D$, $f_{1}$ and $g$.

the map of self and f (from the name)

Let $\mathrm{self}$ be a diagram of cone of $F$. Let $f$ be a homomorphism of $j$ and $\mathrm{j'}$. Then the map of $\mathrm{self}$ and $f$ is a homomorphism of the action of the postcomposition of the map of $F$ and $f$ and the object of $\mathrm{self}$ and $j$ and the object of $\mathrm{self}$ and $\mathrm{j'}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $f$.

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then $\operatorname{mkOfHasLimits}$ applied to $F$ is a diagram of cone of $F$.

the object of self and j (from the name)

Let $\mathrm{self}$ be a diagram of cone of $F$. Let $j$ be an element of $J$. Then the object of $\mathrm{self}$ and $j$ is a cone of the action of $F$ and $j$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $j$.

Let $Q$ be a function from elements $j$ of $J$ to elements of $\operatorname{IsColimit}$ applied to the object of $D$ and $j$. Let $P$ be an element of $\operatorname{IsColimit}$ applied to the cocone of $Q$ and $c$. Then $\operatorname{ofCoconeUncurry}$ applied to $j$, $Q$ and $P$ is an element of $\operatorname{IsColimit}$ applied to $c$.

Let $Q$ be a function from elements $j$ of $J$ to elements of $\operatorname{IsLimit}$ applied to the object of $D$ and $j$. Let $P$ be an element of $\operatorname{IsLimit}$ applied to the cone of $Q$ and $c$. Then $\operatorname{ofConeOfConeUncurry}$ applied to $j$, $Q$ and $P$ is an element of $\operatorname{IsLimit}$ applied to $c$.

the cocone of Q and j (from the name)

Let $G$ be a functor of $\mathrm{Prod}$ applied to $J$ and $K$ and $C$. Let $Q$ be a function from elements $j$ of $J$ to elements of $\operatorname{IsColimit}$ applied to the object of $D$ and $j$. Let $c$ be a cocone of $G$. Then the cocone of $j$ and $Q$ is a cocone of the cocone point of $D$.

the cocone of Q and j (from the name)

Let $Q$ be a function from elements $j$ of $J$ to elements of $\operatorname{IsColimit}$ applied to the object of $D$ and $j$. Let $c$ be a cocone of the action of $\operatorname{uncurry}$ and $F$. Then the cocone of $j$ and $Q$ is a cocone of the cocone point of $D$.

the cocone of Q and j (from the name)

Let $Q$ be a function from elements $j$ of $J$ to elements of $\operatorname{IsColimit}$ applied to the object of $D$ and $j$. Let $P$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the cocone of $j$ and $Q$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $Q$ and $c$.

the cocone of G (from the name)

Let $G$ be a functor of $\mathrm{Prod}$ applied to $J$ and $K$ and $C$. Then the cocone of $G$ is a cocone of $G$.

the colimit curry swap composition colimit isomorphism colimit curry composition colimit of G (from the name)

Let $G$ be a functor of $\mathrm{Prod}$ applied to $J$ and $K$ and $C$. Then the colimit curry swap composition colimit isomorphism colimit curry composition colimit of $G$ is an isomorphism of the colimit of the composition of the action of the curry and the composition of the swap of $K$ and $J$ and $G$ and the colimit and the colimit of the composition of the action of the curry and $G$ and the colimit defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of the colimit isomorphism colimit curry composition colimit of the composition of the swap of $K$ and $J$ and $G$ and the isomorphism of the braiding of $K$ and $J$ and the identity of the composition of the functor of the braiding of $K$ and $J$ and $G$ and the colimit isomorphism colimit curry composition colimit of $G$.

the colimit of F (from the docstring)

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the colimit of $F$ is an isomorphism of the colimit of the composition of the flip of $F$ and the colimit and the colimit of the composition of $F$ and the colimit.

the colimit isomorphism colimit curry composition colimit of G (from the name)

Let $G$ be a functor of $\mathrm{Prod}$ applied to $J$ and $K$ and $C$. Then the colimit isomorphism colimit curry composition colimit of $G$ is an isomorphism of the colimit of $G$ and the colimit of the composition of the action of the curry and $G$ and the colimit defined as $\operatorname{simple}$ applied to the isomorphism of the application of the unit isomorphism of the inverse of the currying and $G$ and the colimit uncurrying isomorphism colimit composition colimit of the action of the curry and $G$.

the colimit uncurrying isomorphism colimit composition colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the colimit uncurrying isomorphism colimit composition colimit of $F$ is an isomorphism of the colimit of the action of $\operatorname{uncurry}$ and $F$ and the colimit of the composition of $F$ and the colimit defined as $\operatorname{coconePointUniqueUpToIso}$ applied to the cocone of the function that maps $j$ to $\operatorname{isColimit}$ applied to the action of $F$ and $j$ and $\operatorname{isColimit}$ applied to the action of $\operatorname{uncurry}$ and $F$ and $\operatorname{isColimit}$ applied to the composition of $F$ and the colimit.

the cone of Q and j (from the name)

Let $G$ be a functor of $\mathrm{Prod}$ applied to $J$ and $K$ and $C$. Let $Q$ be a function from elements $j$ of $J$ to elements of $\operatorname{IsLimit}$ applied to the object of $D$ and $j$. Let $c$ be a cone of $G$. Then the cone of $j$ and $Q$ is a cone of the cone point of $D$.

the cone of Q and j (from the name)

Let $Q$ be a function from elements $j$ of $J$ to elements of $\operatorname{IsLimit}$ applied to the object of $D$ and $j$. Let $c$ be a cone of the action of $\operatorname{uncurry}$ and $F$. Then the cone of $j$ and $Q$ is a cone of the cone point of $D$.

the cone of Q and j (from the name)

Let $Q$ be a function from elements $j$ of $J$ to elements of $\operatorname{IsLimit}$ applied to the object of $D$ and $j$. Let $P$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the cone of $j$ and $Q$ is an element of $\operatorname{IsLimit}$ applied to the cone of $Q$ and $c$.

the cone of G (from the name)

Let $G$ be a functor of $\mathrm{Prod}$ applied to $J$ and $K$ and $C$. Then the cone of $G$ is a cone of $G$.

Let $G$ be a functor of $\mathrm{Prod}$ applied to $J$ and $K$ and $C$. Then $\operatorname{isColimitCoconeOfHasColimitCurryCompColim}$ applied to $G$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $G$.

Let $G$ be a functor of $\mathrm{Prod}$ applied to $J$ and $K$ and $C$. Then $\operatorname{isLimitConeOfHasLimitCurryCompLim}$ applied to $G$ is an element of $\operatorname{IsLimit}$ applied to the cone of $G$.

the limit curry swap composition limit isomorphism limit curry composition limit of G (from the name)

Let $G$ be a functor of $\mathrm{Prod}$ applied to $J$ and $K$ and $C$. Then the limit curry swap composition limit isomorphism limit curry composition limit of $G$ is an isomorphism of the limit of the composition of the action of the curry and the composition of the swap of $K$ and $J$ and $G$ and the limit and the limit of the composition of the action of the curry and $G$ and the limit defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of the limit isomorphism limit curry composition limit of the composition of the swap of $K$ and $J$ and $G$ and the isomorphism of the braiding of $K$ and $J$ and the identity of the composition of the functor of the braiding of $K$ and $J$ and $G$ and the limit isomorphism limit curry composition limit of $G$.

the limit of F (from the docstring)

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the limit of $F$ is an isomorphism of the limit of the composition of the flip of $F$ and the limit and the limit of the composition of $F$ and the limit.

the limit isomorphism limit curry composition limit of G (from the name)

Let $G$ be a functor of $\mathrm{Prod}$ applied to $J$ and $K$ and $C$. Then the limit isomorphism limit curry composition limit of $G$ is an isomorphism of the limit of $G$ and the limit of the composition of the action of the curry and $G$ and the limit defined as $\operatorname{simple}$ applied to the isomorphism of the application of the unit isomorphism of the inverse of the currying and $G$ and the limit uncurrying isomorphism limit composition limit of the action of the curry and $G$.

the limit uncurrying isomorphism limit composition limit of F (from the name)

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the limit uncurrying isomorphism limit composition limit of $F$ is an isomorphism of the limit of the action of $\operatorname{uncurry}$ and $F$ and the limit of the composition of $F$ and the limit defined as $\operatorname{conePointUniqueUpToIso}$ applied to the cone of the function that maps $j$ to $\operatorname{isLimit}$ applied to the action of $F$ and $j$ and $\operatorname{isLimit}$ applied to the action of $\operatorname{uncurry}$ and $F$ and $\operatorname{isLimit}$ applied to the composition of $F$ and the limit.