Definitions: Mathlib.CategoryTheory, part 10 of 25

the colimit composition flip isomorphism whisker colimit (from the name)

The colimit composition flip isomorphism whisker colimit is an isomorphism of the composition of the flip functor of $J$ and $C$ and the colimit and the action of the right whiskering of the set of functors of $J$ and $C$ and $C$ and the colimit.

the colimit isomorphism flip composition whisker colimit (from the name)

The colimit isomorphism flip composition whisker colimit is an isomorphism of the colimit and the composition of the flip functor of $K$ and $C$ and the action of the right whiskering of the set of functors of $J$ and $C$ and $C$ and the colimit.

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

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Let $G$ be a functor of $D$ and $K$. Then the colimit composition whiskering left isomorphism composition colimit of $F$ and $G$ is an isomorphism of the colimit of the composition of $F$ and the action of the left whiskering of $K$ and $C$ and $G$ and the composition of $G$ and the colimit of $F$.

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

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

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 $F$ and the composition of the flip of $F$ and the colimit.

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

Let $G$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the colimit isomorphism swap composition colimit of $G$ is an isomorphism of the colimit of $G$ and the composition of the action of the curry and the composition of the swap of $K$ and $J$ and the action of $\operatorname{uncurry}$ and $G$ and the colimit defined as the composition of the colimit of $G$ and the right isomorphism whisker of $\operatorname{flipIsoCurrySwapUncurry}$ applied to $G$ and the colimit.

the colimit object isomorphism colimit composition evaluation of F and k (from the name)

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Let $k$ be an element of $K$. Then the colimit object isomorphism colimit composition evaluation of $F$ and $k$ is an isomorphism of the action of the colimit of $F$ and $k$ and the colimit of the composition of $F$ and the action of the evaluation of $K$ and $C$ and $k$ defined as $\operatorname{preservesColimitIso}$ applied to the action of the evaluation of $K$ and $C$ and $k$ and $F$.

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Let $c$ be a function from elements $k$ of $K$ to colimit cocones of the action of the flip of $F$ and $k$. Then $\operatorname{combineCocones}$ applied to $F$, $k$ and $c$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Let $c$ be a function from elements $k$ of $K$ to limit cones of the action of the flip of $F$ and $k$. Then $\operatorname{combineCones}$ applied to $F$, $k$ and $c$ is a cone of $F$.

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Let $c$ be a function from elements $k$ of $K$ to colimit cocones of the action of the flip of $F$ and $k$. Then $\operatorname{combinedIsColimit}$ applied to $F$, $k$ and $c$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{combineCocones}$ applied to $F$ and $c$ defined as the function that maps $c$ to $\operatorname{evaluationJointlyReflectsColimits}$ applied to $\operatorname{combineCocones}$ applied to $F$ and $k$, the function that maps $k$ to $\operatorname{ofIsoColimit}$ applied to $\operatorname{isColimit}$ applied to $k$ applied to $k$ and the inverse of $\operatorname{evaluateCombinedCocones}$ applied to $F$, $k$ and $k$ and $c$.

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Let $c$ be a function from elements $k$ of $K$ to limit cones of the action of the flip of $F$ and $k$. Then $\operatorname{combinedIsLimit}$ applied to $F$, $k$ and $c$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{combineCones}$ applied to $F$ and $c$ defined as the function that maps $c$ to $\operatorname{evaluationJointlyReflectsLimits}$ applied to $\operatorname{combineCones}$ applied to $F$ and $k$, the function that maps $k$ to $\operatorname{ofIsoLimit}$ applied to $\operatorname{isLimit}$ applied to $k$ applied to $k$ and the inverse of $\operatorname{evaluateCombinedCones}$ applied to $F$, $k$ and $k$ and $c$.

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Let $c$ be a function from elements $k_{1}$ of $K$ to colimit cocones of the action of the flip of $F$ and $k_{1}$. Let $k$ be an element of $K$. Then $\operatorname{evaluateCombinedCocones}$ applied to $F$, $k_{1}$, $c$ and $k$ is an isomorphism of the map cocone of the action of the evaluation of $K$ and $C$ and $k$ and $\operatorname{combineCocones}$ applied to $F$ and $c$ and the cocone of $c$ applied to $k$.

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Let $c$ be a function from elements $k_{1}$ of $K$ to limit cones of the action of the flip of $F$ and $k_{1}$. Let $k$ be an element of $K$. Then $\operatorname{evaluateCombinedCones}$ applied to $F$, $k_{1}$, $c$ and $k$ is an isomorphism of the map cone of the action of the evaluation of $K$ and $C$ and $k$ and $\operatorname{combineCones}$ applied to $F$ and $c$ and the cone of $c$ applied to $k$.

Let $c$ be a cocone of $F$. Let $t$ be a function from elements $k$ of $K$ to elements of $\operatorname{IsColimit}$ applied to the map cocone of the action of the evaluation of $K$ and $C$ and $k$ and $c$. Then $\operatorname{evaluationJointlyReflectsColimits}$ applied to $c$, $k$ and $t$ is an element of $\operatorname{IsColimit}$ applied to $c$.

Let $c$ be a cone of $F$. Let $t$ be a function from elements $k$ of $K$ to elements of $\operatorname{IsLimit}$ applied to the map cone of the action of the evaluation of $K$ and $C$ and $k$ and $c$. Then $\operatorname{evaluationJointlyReflectsLimits}$ applied to $c$, $k$ and $t$ is an element of $\operatorname{IsLimit}$ applied to $c$.

the limit composition flip isomorphism whisker limit (from the name)

The limit composition flip isomorphism whisker limit is an isomorphism of the composition of the flip functor of $J$ and $C$ and the limit and the action of the right whiskering of the set of functors of $J$ and $C$ and $C$ and the limit.

the limit isomorphism flip composition whisker limit (from the name)

The limit isomorphism flip composition whisker limit is an isomorphism of the limit and the composition of the flip functor of $K$ and $C$ and the action of the right whiskering of the set of functors of $J$ and $C$ and $C$ and the limit.

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

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Let $G$ be a functor of $D$ and $K$. Then the limit composition whiskering left isomorphism composition limit of $F$ and $G$ is an isomorphism of the limit of the composition of $F$ and the action of the left whiskering of $K$ and $C$ and $G$ and the composition of $G$ and the limit of $F$.

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

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

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 $F$ and the composition of the flip of $F$ and the limit.

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

Let $G$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the limit isomorphism swap composition limit of $G$ is an isomorphism of the limit of $G$ and the composition of the action of the curry and the composition of the swap of $K$ and $J$ and the action of $\operatorname{uncurry}$ and $G$ and the limit defined as the composition of the limit of $G$ and the right isomorphism whisker of $\operatorname{flipIsoCurrySwapUncurry}$ applied to $G$ and the limit.

the limit object isomorphism limit composition evaluation of F and k (from the name)

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Let $k$ be an element of $K$. Then the limit object isomorphism limit composition evaluation of $F$ and $k$ is an isomorphism of the action of the limit of $F$ and $k$ and the limit of the composition of $F$ and the action of the evaluation of $K$ and $C$ and $k$ defined as $\operatorname{preservesLimitIso}$ applied to the action of the evaluation of $K$ and $C$ and $k$ and $F$.

the pointwise cocone of F (from the name)

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the pointwise cocone of $F$ is a cocone of $F$.

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then $\operatorname{pointwiseIsColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the pointwise cocone of $F$.

the pointwise binary bicone of F and G (from the name)

Let $F$ and $G$ be functors of $D$ and $C$. Then the pointwise binary bicone of $F$ and $G$ is a binary bicone of $F$ and $G$.

Let $F$ and $G$ be functors of $D$ and $C$. Then $\operatorname{isBilimit}$ applied to $F$ and $G$ is an element of $\operatorname{IsBilimit}$ applied to the pointwise binary bicone of $F$ and $G$.

the pointwise binary biproduct data of F and G (from the name)

Let $F$ and $G$ be functors of $D$ and $C$. Then the pointwise binary biproduct data of $F$ and $G$ is a binary biproduct data of $F$ and $G$ defined as $\operatorname{mk}$ applied to the pointwise binary bicone of $F$ and $G$ and $\operatorname{isBilimit}$ applied to $F$ and $G$.

the monomorphism factorisation of f (from the name)

Let $f$ be a homomorphism of $F$ and $G$. Then the monomorphism factorisation of $f$ is a monomorphism factorisation of $f$.

the image of f (from the docstring)

Let $f$ be a homomorphism of $F$ and $G$. Then the image of $f$ is an element of $\operatorname{IsImage}$ applied to the monomorphism factorisation of $f$.

the cokernel projection of C (from the docstring)

Let $C$ be a set. Then the cokernel projection of $C$ is an element of $\operatorname{IsColimit}$ applied to the projection of the cokernel projection of $C$ and $\operatorname{condition}$ applied to $C$.

the kernel inclusion of C (from the docstring)

Let $C$ be a set. Then the kernel inclusion of $C$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the kernel inclusion of $C$ and $\operatorname{condition}$ applied to $C$.

the product object isomorphism of f and d (from the name)

Let $f$ be a function from elements of $x_{2}$ to functors of $D$ and $C$. Let $d$ be an element of $D$. Then the product object isomorphism of $f$ and $d$ is an isomorphism of the action of the product object of $f$ and $d$ and the product object of the function that maps $s$ to the action of $f$ applied to $s$ and $d$ defined as the composition of the limit object isomorphism limit composition evaluation of the functor of $f$ and $d$ and the isomorphism of $\operatorname{compNatIsoDiscrete}$ applied to $f$ and the action of the evaluation of $D$ and $C$ and $d$.

the sigma object isomorphism of f and d (from the name)

Let $f$ be a function from elements of $x_{2}$ to functors of $D$ and $C$. Let $d$ be an element of $D$. Then the sigma object isomorphism of $f$ and $d$ is an isomorphism of the action of the sigma object of $f$ and $d$ and the sigma object of the function that maps $s$ to the action of $f$ applied to $s$ and $d$ defined as the composition of the colimit object isomorphism colimit composition evaluation of the functor of $f$ and $d$ and the isomorphism of $\operatorname{compNatIsoDiscrete}$ applied to $f$ and the action of the evaluation of $D$ and $C$ and $d$.

Let $f$ be a homomorphism of $F$ and $H$. Let $g$ be a homomorphism of $G$ and $H$. Let $c$ be a function from elements $X_{1}$ of $D$ to pullback cones of the component of $f$ and $X_{1}$ and the component of $g$ and $X_{1}$. Let $\mathrm{hc}$ be a function from elements $X$ of $D$ to elements of $\operatorname{IsLimit}$ applied to $c$ applied to $X$. Then $\operatorname{combine}$ applied to $f$, $g$, $X_{1}$, $c$, $X$ and $\mathrm{hc}$ is a pullback cone of $f$ and $g$.

Let $f$ be a homomorphism of $F$ and $H$. Let $g$ be a homomorphism of $G$ and $H$. Let $c$ be a function from elements $X_{1}$ of $D$ to pullback cones of the component of $f$ and $X_{1}$ and the component of $g$ and $X_{1}$. Let $\mathrm{hc}$ be a function from elements $X$ of $D$ to elements of $\operatorname{IsLimit}$ applied to $c$ applied to $X$. Then $\operatorname{combineIsLimit}$ applied to $f$, $g$, $X_{1}$, $c$, $X$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{combine}$ applied to $f$, $g$, $c$ and $\mathrm{hc}$.

the pullback object isomorphism of g and d (from the name)

Let $f$ be a homomorphism of $F$ and $H$. Let $g$ be a homomorphism of $G$ and $H$. Let $d$ be an element of $D$. Then the pullback object isomorphism of $g$ and $d$ is an isomorphism of the action of the pullback of $f$ and $g$ and $d$ and the pullback of the component of $f$ and $d$ and the component of $g$ and $d$ defined as the composition of the limit object isomorphism limit composition evaluation of the cospan of $f$ and $g$ and $d$ and the isomorphism of the diagram isomorphism cospan of the composition of the cospan of $f$ and $g$ and the action of the evaluation of $D$ and $C$ and $d$.

the pushout object isomorphism of g and d (from the name)

Let $f$ be a homomorphism of $F$ and $G$. Let $g$ be a homomorphism of $F$ and $H$. Let $d$ be an element of $D$. Then the pushout object isomorphism of $g$ and $d$ is an isomorphism of the action of the pushout of $f$ and $g$ and $d$ and the pushout of the component of $f$ and $d$ and the component of $g$ and $d$ defined as the composition of the colimit object isomorphism colimit composition evaluation of the span of $f$ and $g$ and $d$ and the isomorphism of the diagram isomorphism span of the composition of the span of $f$ and $g$ and the action of the evaluation of $D$ and $C$ and $d$.

Let $\mathrm{hF}$ be a function from elements $X$ of $C$ to elements of $\operatorname{IsInitial}$ applied to the action of $F$ and $X$. Then $\operatorname{isInitial}$ applied to $X$ and $\mathrm{hF}$ is an element of $\operatorname{IsInitial}$ applied to $F$.

Let $\mathrm{hF}$ be a function from elements $X$ of $C$ to elements of $\operatorname{IsTerminal}$ applied to the action of $F$ and $X$. Then $\operatorname{isTerminal}$ applied to $X$ and $\mathrm{hF}$ is an element of $\operatorname{IsTerminal}$ applied to $F$.

colimit cocone of F (from the name)

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

the cocone of self (from the name)

Let $\mathrm{self}$ be a colimit cocone of $F$. Then the cocone of $\mathrm{self}$ is a cocone of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a colimit cocone of $F$. Then $\operatorname{isColimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

F has colimits (from the name)

Let $F$ be a functor of $J$ and $C$. Then we can say that $F$ has colimits.

the isomorphism of e and w (from the name)

Let $e$ be an equivalence of $J$ and $K$. Let $w$ be an isomorphism of the composition of the functor of $e$ and $G$ and $F$. Then the isomorphism of $e$ and $w$ is an isomorphism of the colimit of $F$ and the colimit of $G$ defined as the cocone point isomorphism of $e$ and $w$.

the isomorphism of w (from the name)

Let $w$ be an isomorphism of $F$ and $G$. Then the isomorphism of $w$ is an isomorphism of the colimit of $F$ and the colimit of $G$ defined as the cocone point isomorphism of $\operatorname{isColimit}$ applied to $G$ and $w$.

C has colimits (from the name)

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

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

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

F has limits (from the name)

Let $F$ be a functor of $J$ and $C$. Then we can say that $F$ has limits.

the isomorphism of e and w (from the name)

Let $e$ be an equivalence of $J$ and $K$. Let $w$ be an isomorphism of the composition of the functor of $e$ and $G$ and $F$. Then the isomorphism of $e$ and $w$ is an isomorphism of the limit of $F$ and the limit of $G$ defined as the cone point isomorphism of $e$ and $w$.

the isomorphism of w (from the name)

Let $w$ be an isomorphism of $F$ and $G$. Then the isomorphism of $w$ is an isomorphism of the limit of $F$ and the limit of $G$ defined as the cone point isomorphism of $\operatorname{isLimit}$ applied to $G$ and $w$.

C has limits (from the name)

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

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

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

the opposite of P (from the name)

Let $P$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then the opposite of $P$ is an element of $\operatorname{IsLimit}$ applied to the opposite of $t$.

the opposite of P (from the name)

Let $P$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then the opposite of $P$ is an element of $\operatorname{IsLimit}$ applied to the opposite of $t$.

the opposite of P (from the name)

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then the opposite of $P$ is an element of $\operatorname{IsColimit}$ applied to the opposite of $t$.

the opposite of P (from the name)

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then the opposite of $P$ is an element of $\operatorname{IsColimit}$ applied to the opposite of $t$.

limit cone of F (from the name)

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

the cone of self (from the name)

Let $\mathrm{self}$ be a limit cone of $F$. Then the cone of $\mathrm{self}$ is a cone of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a limit cone of $F$. Then $\operatorname{isLimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to the cone of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the colimit (from the name)

The colimit is a functor of the set of functors of $J$ and $C$ and $C$.

the inclusion of j (from the name)

Let $j$ be an element of $J$. Then the inclusion of $j$ is a homomorphism of the action of the evaluation of $J$ and $C$ and $j$ and the colimit.

the colimit functor and constant functor (from the docstring)

The colimit functor and constant functor is an adjunction of the colimit and the constant of $J$.

the colimit Coyoneda (from the name)

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

the colimit map of x2 (from the name)

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

the colimit of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the colimit of $F$ is an element of $C$ defined as $\operatorname{pt}$ applied to the cocone of $F$.

the cocone of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the cocone of $F$ is a cocone of $F$ defined as the cocone of $\operatorname{getColimitCocone}$ applied to $F$.

the cocone morphism of c (from the name)

Let $c$ be a cocone of $F$. Then the cocone morphism of $c$ is a homomorphism of the cocone of $F$ and $c$ defined as the universal morphism of $\operatorname{isColimit}$ applied to $F$ and $c$.

Let $F$ be a functor of $J$ and $C$. Let $c$ be a cocone of $F$. Then $\operatorname{desc}$ applied to $F$ and $c$ is a homomorphism of the colimit of $F$ and $\operatorname{pt}$ applied to $c$ defined as $\operatorname{desc}$ applied to $\operatorname{isColimit}$ applied to $F$ and $c$.

the homomorphism isomorphism of F and W (from the name)

Let $F$ be a functor of $J$ and $C$. Let $W$ be an element of $C$. Then the homomorphism isomorphism of $F$ and $W$ is an isomorphism of $\mathrm{ULift}$ applied to the set of homomorphisms of the colimit of $F$ and $W$ and the action of the cocone of $F$ and $W$ defined as the homomorphism isomorphism of $\operatorname{isColimit}$ applied to $F$ and $W$.

the homomorphism isomorphism of F and W (from the name)

Let $F$ be a functor of $J$ and $C$. Let $W$ be an element of $C$. Then the homomorphism isomorphism of $F$ and $W$ is an isomorphism of $\mathrm{ULift}$ applied to the set of homomorphisms of the colimit of $F$ and $W$ and $\SubtypeSet {p}{\mathrm{forall} (J , \lambda j . \mathrm{forall} (J , \lambda \mathrm{j'} . \mathrm{forall} (\operatorname{Hom} (\mathrm{j'} , j), \lambda f . \EqtMACRoH {\operatorname{comp} (\operatorname{map} (F , f), p (j))}{p (\mathrm{j'})})))}$ defined as the homomorphism isomorphism of $\operatorname{isColimit}$ applied to $F$ and $W$.

Let $F$ be a functor of $J$ and $C$. Then $\operatorname{isColimit}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $F$ defined as $\operatorname{isColimit}$ applied to $\operatorname{getColimitCocone}$ applied to $F$.

the isomorphism colimit cocone of t (from the name)

Let $t$ be a colimit cocone of $F$. Then the isomorphism colimit cocone of $t$ is an isomorphism of the colimit of $F$ and $\operatorname{pt}$ applied to the cocone of $t$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to $F$ and $\operatorname{isColimit}$ applied to $t$.

the post 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 post of $F$ and $G$ is a homomorphism of the colimit of the composition of $F$ and $G$ and the action of $G$ and the colimit of $F$ defined as $\operatorname{desc}$ applied to the composition of $F$ and $G$ and the map cocone of $G$ and the cocone of $F$.

Let $F$ be a functor of $J$ and $C$. Let $E$ be a functor of $K$ and $J$. Then $\operatorname{pre}$ applied to $F$ and $E$ is a homomorphism of the colimit of the composition of $E$ and $F$ and the colimit of $F$ defined as $\operatorname{desc}$ applied to the composition of $E$ and $F$ and the whisker of $E$ and the cocone of $F$.

the inclusion of F and j (from the name)

Let $F$ be a functor of $J$ and $C$. Let $j$ be an element of $J$. Then the inclusion of $F$ and $j$ is a homomorphism of the action of $F$ and $j$ and the colimit of $F$ defined as the component of the inclusion of the cocone of $F$ and $j$.

the cone of adj and F (from the name)

Let $\mathrm{adj}$ be an adjunction of the constant of $J$ and $L$. Let $F$ be a functor of $J$ and $C$. Then the cone of $\mathrm{adj}$ and $F$ is a cone of $F$ defined as $\operatorname{mk}$ applied to the action of $L$ and $F$ and the component of the counit of $\mathrm{adj}$ and $F$.

the constant functor and limit functor (from the docstring)

The constant functor and limit functor is an adjunction of the constant of $J$ and the limit.

Let $F$ be a functor of $J$ and $C$. Then $\operatorname{getColimitCocone}$ applied to $F$ is a colimit cocone of $F$ defined as $\operatorname{choice}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_HasColimit\_\_exists\_colimit}$.

Let $F$ be a functor of $J$ and $C$. Then $\operatorname{getLimitCone}$ applied to $F$ is a limit cone of $F$ defined as $\operatorname{choice}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_HasLimit\_\_exists\_limit}$.

$\operatorname{isColimitEquivIsLimitOp}$ is an equivalence from $\operatorname{IsColimit}$ applied to $t$ to $\operatorname{IsLimit}$ applied to the opposite of $t$ defined as the equivalence of $\operatorname{op}$ and $\operatorname{isColimitOfOp}$.

Let $P$ be an element of $\operatorname{IsLimit}$ applied to the opposite of $t$. Then $\operatorname{isColimitOfOp}$ applied to $P$ is an element of $\operatorname{IsColimit}$ applied to $t$ defined as the opposite of $P$.

Let $P$ be an element of $\operatorname{IsLimit}$ applied to the opposite of $t$. Then $\operatorname{isColimitOfUnop}$ applied to $P$ is an element of $\operatorname{IsColimit}$ applied to $t$ defined as the opposite of $P$.

Let $\mathrm{adj}$ be an adjunction of the constant of $J$ and $L$. Let $F$ be a functor of $J$ and $C$. Then $\operatorname{isLimitConeOfAdj}$ applied to $\mathrm{adj}$ and $F$ is an element of $\operatorname{IsLimit}$ applied to the cone of $\mathrm{adj}$ and $F$.

$\operatorname{isLimitEquivIsColimitOp}$ is an equivalence from $\operatorname{IsLimit}$ applied to $t$ to $\operatorname{IsColimit}$ applied to the opposite of $t$ defined as the equivalence of $\operatorname{op}$ and $\operatorname{isLimitOfOp}$.

Let $P$ be an element of $\operatorname{IsColimit}$ applied to the opposite of $t$. Then $\operatorname{isLimitOfOp}$ applied to $P$ is an element of $\operatorname{IsLimit}$ applied to $t$ defined as the opposite of $P$.

Let $P$ be an element of $\operatorname{IsColimit}$ applied to the opposite of $t$. Then $\operatorname{isLimitOfUnop}$ applied to $P$ is an element of $\operatorname{IsLimit}$ applied to $t$ defined as the opposite of $P$.

the limit (from the name)

The limit is a functor of the set of functors of $J$ and $C$ and $C$.

the projection of j (from the name)

Let $j$ be an element of $J$. Then the projection of $j$ is a homomorphism of the limit and the action of the evaluation of $J$ and $C$ and $j$.

the limit map of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the limit map of $x_{2}$ is a homomorphism of the limit of $F$ and the limit of $G$ defined as the map of $\operatorname{isLimit}$ applied to $G$ and $x_{2}$.

the limit Yoneda (from the name)

The limit Yoneda is an isomorphism of the composition of the limit and the composition of the Yoneda and the action of the right whiskering of the set of sets and the set of sets and the functor embedding and the cone of $J$ and $C$.

the limit of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the limit of $F$ is an element of $C$ defined as $\operatorname{pt}$ applied to the cone of $F$.

the cone of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the cone of $F$ is a cone of $F$ defined as the cone of $\operatorname{getLimitCone}$ applied to $F$.

the cone morphism of c (from the docstring)

Let $c$ be a cone of $F$. Then the cone morphism of $c$ is a homomorphism of $c$ and the cone of $F$ defined as the universal morphism of $\operatorname{isLimit}$ applied to $F$ and $c$.

the homomorphism isomorphism of F and W (from the name)

Let $F$ be a functor of $J$ and $C$. Let $W$ be an element of $C$. Then the homomorphism isomorphism of $F$ and $W$ is an isomorphism of $\mathrm{ULift}$ applied to the set of homomorphisms of $W$ and the limit of $F$ and the action of the cone of $F$ and $\operatorname{op}$ applied to $W$ defined as the homomorphism isomorphism of $\operatorname{isLimit}$ applied to $F$ and $W$.

the homomorphism isomorphism of F and W (from the name)

Let $F$ be a functor of $J$ and $C$. Let $W$ be an element of $C$. Then the homomorphism isomorphism of $F$ and $W$ is an isomorphism of $\mathrm{ULift}$ applied to the set of homomorphisms of $W$ and the limit of $F$ and $\SubtypeSet {p}{\mathrm{forall} (J , \lambda j . \mathrm{forall} (J , \lambda \mathrm{j'} . \mathrm{forall} (\operatorname{Hom} (j , \mathrm{j'}), \lambda f . \EqtMACRoH {\operatorname{comp} (p (j), \operatorname{map} (F , f))}{p (\mathrm{j'})})))}$ defined as the homomorphism isomorphism of $\operatorname{isLimit}$ applied to $F$ and $W$.

Let $F$ be a functor of $J$ and $C$. Then $\operatorname{isLimit}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the cone of $F$ defined as $\operatorname{isLimit}$ applied to $\operatorname{getLimitCone}$ applied to $F$.

the isomorphism limit cone of t (from the name)

Let $t$ be a limit cone of $F$. Then the isomorphism limit cone of $t$ is an isomorphism of the limit of $F$ and $\operatorname{pt}$ applied to the cone of $t$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to $F$ and $\operatorname{isLimit}$ applied to $t$.

the lift of F and c (from the name)

Let $F$ be a functor of $J$ and $C$. Let $c$ be a cone of $F$. Then the lift of $F$ and $c$ is a homomorphism of $\operatorname{pt}$ applied to $c$ and the limit of $F$ defined as the lift of $\operatorname{isLimit}$ applied to $F$ and $c$.

the post 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 post of $F$ and $G$ is a homomorphism of the action of $G$ and the limit of $F$ and the limit of the composition of $F$ and $G$ defined as the lift of the composition of $F$ and $G$ and the map cone of $G$ and the cone of $F$.

Let $F$ be a functor of $J$ and $C$. Let $E$ be a functor of $K$ and $J$. Then $\operatorname{pre}$ applied to $F$ and $E$ is a homomorphism of the limit of $F$ and the limit of the composition of $E$ and $F$ defined as the lift of the composition of $E$ and $F$ and the whisker of $E$ and the cone of $F$.

the projection from the limit object to a value of the functor of F and j (from the docstring)

Let $F$ be a functor of $J$ and $C$. Let $j$ be an element of $J$. Then the projection from the limit object to a value of the functor of $F$ and $j$ is a homomorphism of the limit of $F$ and the action of $F$ and $j$ defined as the component of the projection of the cone of $F$ and $j$.

the colimit Coyoneda homomorphism isomorphism limit of D and F (from the name)

Let $D$ be a functor of the set of opposites of $I$ and $C$. Let $F$ be a functor of $C$ and the set of sets. Then the colimit Coyoneda homomorphism isomorphism limit of $D$ and $F$ is an isomorphism of the set of homomorphisms of the colimit of the composition of the right opposite of $D$ and the Coyoneda and $F$ and the limit of the composition of $D$ and the composition of $F$ and the functor embedding defined as the composition of the colimit homomorphism isomorphism limit Yoneda of the composition of the right opposite of $D$ and the Coyoneda and $F$ and the isomorphism of the left isomorphism whisker of the composition of $D$ and $\operatorname{sectL}$ applied to $C$ and $F$ and the Coyoneda lemma of $C$.

the colimit Coyoneda homomorphism isomorphism limit of D and F (from the name)

Let $D$ be a functor of $I$ and $C$. Let $F$ be a functor of $C$ and the set of sets. Then the colimit Coyoneda homomorphism isomorphism limit of $D$ and $F$ is an isomorphism of the set of homomorphisms of the colimit of the composition of the opposite of $D$ and the Coyoneda and $F$ and the limit of the composition of $D$ and the composition of $F$ and the functor embedding defined as the composition of the colimit homomorphism isomorphism limit Yoneda of the composition of the opposite of $D$ and the Coyoneda and $F$ and the isomorphism of the left isomorphism whisker of the composition of $D$ and $\operatorname{sectL}$ applied to $C$ and $F$ and the Coyoneda lemma of $C$.

the colimit Coyoneda homomorphism isomorphism limit left opposite of D and F (from the name)

Let $D$ be a functor of $I$ and the set of opposites of $C$. Let $F$ be a functor of $C$ and the set of sets. Then the colimit Coyoneda homomorphism isomorphism limit left opposite of $D$ and $F$ is an isomorphism of the set of homomorphisms of the colimit of the composition of $D$ and the Coyoneda and $F$ and the limit of the composition of the left opposite of $D$ and the composition of $F$ and the functor embedding defined as the colimit Coyoneda homomorphism isomorphism limit of the left opposite of $D$ and $F$.

the colimit Coyoneda homomorphism isomorphism limit opposite of D and F (from the name)

Let $D$ be a functor of the set of opposites of $I$ and the set of opposites of $C$. Let $F$ be a functor of $C$ and the set of sets. Then the colimit Coyoneda homomorphism isomorphism limit opposite of $D$ and $F$ is an isomorphism of the set of homomorphisms of the colimit of the composition of $D$ and the Coyoneda and $F$ and the limit of the composition of the opposite of $D$ and the composition of $F$ and the functor embedding defined as the colimit Coyoneda homomorphism isomorphism limit of the opposite of $D$ and $F$.

the colimit homomorphism isomorphism limit Yoneda of F and A (from the name)

Let $F$ be a functor of $I$ and $C$. Let $A$ be an element of $C$. Then the colimit homomorphism isomorphism limit Yoneda of $F$ and $A$ is an isomorphism of the set of homomorphisms of the colimit of $F$ and $A$ and the limit of the composition of the opposite of $F$ and the action of the Yoneda and $A$ defined as the composition of the application of the Coyoneda opposite colimit isomorphism limit Coyoneda of $F$ and $A$ and the limit object isomorphism limit composition evaluation of the composition of the opposite of $F$ and the Coyoneda and $A$.

the colimit homomorphism isomorphism limit Yoneda of F and A (from the name)

Let $F$ be a functor of the set of opposites of $I$ and $C$. Let $A$ be an element of $C$. Then the colimit homomorphism isomorphism limit Yoneda of $F$ and $A$ is an isomorphism of the set of homomorphisms of the colimit of $F$ and $A$ and the limit of the composition of the right opposite of $F$ and the action of the Yoneda and $A$ defined as the composition of the application of the Coyoneda opposite colimit isomorphism limit Coyoneda of $F$ and $A$ and the limit object isomorphism limit composition evaluation of the composition of the right opposite of $F$ and the Coyoneda and $A$.

the colimit Yoneda homomorphism isomorphism limit of D and F (from the name)

Let $D$ be a functor of the set of opposites of $I$ and the set of opposites of $C$. Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the colimit Yoneda homomorphism isomorphism limit of $D$ and $F$ is an isomorphism of the set of homomorphisms of the colimit of the composition of the opposite of $D$ and the Yoneda and $F$ and the limit of the composition of $D$ and the composition of $F$ and the functor embedding defined as the composition of the colimit homomorphism isomorphism limit Yoneda of the composition of the opposite of $D$ and the Yoneda and $F$ and the isomorphism of the left isomorphism whisker of the composition of $D$ and $\operatorname{sectL}$ applied to the set of opposites of $C$ and $F$ and the Yoneda lemma of $C$.

the colimit Yoneda homomorphism isomorphism limit of D and F (from the name)

Let $D$ be a functor of $I$ and the set of opposites of $C$. Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the colimit Yoneda homomorphism isomorphism limit of $D$ and $F$ is an isomorphism of the set of homomorphisms of the colimit of the composition of the left opposite of $D$ and the Yoneda and $F$ and the limit of the composition of $D$ and the composition of $F$ and the functor embedding defined as the composition of the colimit homomorphism isomorphism limit Yoneda of the composition of the left opposite of $D$ and the Yoneda and $F$ and the isomorphism of the left isomorphism whisker of the composition of $D$ and $\operatorname{sectL}$ applied to the set of opposites of $C$ and $F$ and the Yoneda lemma of $C$.

the colimit Yoneda homomorphism isomorphism limit opposite of D and F (from the name)

Let $D$ be a functor of $I$ and $C$. Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the colimit Yoneda homomorphism isomorphism limit opposite of $D$ and $F$ is an isomorphism of the set of homomorphisms of the colimit of the composition of $D$ and the Yoneda and $F$ and the limit of the composition of the opposite of $D$ and the composition of $F$ and the functor embedding defined as the colimit Yoneda homomorphism isomorphism limit of the opposite of $D$ and $F$.

the colimit Yoneda homomorphism isomorphism limit right opposite of D and F (from the name)

Let $D$ be a functor of the set of opposites of $I$ and $C$. Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the colimit Yoneda homomorphism isomorphism limit right opposite of $D$ and $F$ is an isomorphism of the set of homomorphisms of the colimit of the composition of $D$ and the Yoneda and $F$ and the limit of the composition of the right opposite of $D$ and the composition of $F$ and the functor embedding defined as the colimit Yoneda homomorphism isomorphism limit of the right opposite of $D$ and $F$.

the Coyoneda opposite colimit isomorphism limit Coyoneda of F (from the name)

Let $F$ be a functor of $I$ and $C$. Then the Coyoneda opposite colimit isomorphism limit Coyoneda of $F$ is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to the colimit of $F$ and the limit of the composition of the opposite of $F$ and the Coyoneda defined as the composition of the map isomorphism of the Coyoneda and the inverse of the limit of $F$ and $\operatorname{preservesLimitIso}$ applied to the Coyoneda and the opposite of $F$.

the Coyoneda opposite colimit isomorphism limit Coyoneda of F (from the name)

Let $F$ be a functor of the set of opposites of $I$ and $C$. Then the Coyoneda opposite colimit isomorphism limit Coyoneda of $F$ is an isomorphism of the action of the Coyoneda and $\operatorname{op}$ applied to the colimit of $F$ and the limit of the composition of the right opposite of $F$ and the Coyoneda defined as the composition of the map isomorphism of the Coyoneda and the inverse of the limit of $F$ and $\operatorname{preservesLimitIso}$ applied to the Coyoneda and the right opposite of $F$.

ind of C (from the name)

Let $C$ be a set. Then an ind of $C$ is an element of the function that maps $C$ to the set of shrink homs of the set of full subcategories of the proposition that $\operatorname{IsIndObject}$.

the colimit presentation composition Yoneda of X (from the name)

Let $X$ be an ind of $C$. Then the colimit presentation composition Yoneda of $X$ is an isomorphism of the colimit of the composition of $\operatorname{F}$ applied to the presentation of $X$ and the Yoneda and $X$ defined as $\operatorname{symm}$ applied to the equivalence of $\operatorname{fullyFaithful}$ and $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{preservesColimitIso}$ applied to the inclusion of $C$ and the composition of $\operatorname{F}$ applied to the presentation of $X$ and the Yoneda and the isomorphism of the left isomorphism whisker of $\operatorname{F}$ applied to the presentation of $X$ and the composition and $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the composition of $\operatorname{F}$ applied to the presentation of $X$ and the Yoneda and $\operatorname{isColimit}$ applied to the presentation of $X$.

the equivalence of C (from the name)

Let $C$ be a set. Then the equivalence of $C$ is an equivalence of the set of inds of $C$ and the set of full subcategories of the proposition that $\operatorname{IsIndObject}$ defined as the inverse of the equivalence of the set of full subcategories of the proposition that $\operatorname{IsIndObject}$.

the inclusion of C (from the name)

Let $C$ be a set. Then the inclusion of $C$ is a functor of the set of inds of $C$ and the set of functors of the set of opposites of $C$ and the set of sets defined as the composition of the functor of the equivalence of $C$ and the inclusion of the proposition that $\operatorname{IsIndObject}$.

$\operatorname{fullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the inclusion of $C$ defined as $\operatorname{ofFullyFaithful}$ applied to the inclusion of $C$.

the left exact functor equivalence of C (from the name)

Let $C$ be a set. Then the left exact functor equivalence of $C$ is an equivalence of the set of inds of $C$ and the set of left exact functors of the set of opposites of $C$ and the set of sets.

the limit of I (from the name)

Let $I$ be a set. Then the limit of $I$ is a functor of the set of functors of $I$ and $C$ and the set of inds of $C$ defined as the composition of the action of the right whiskering of $C$ and the set of inds of $C$ and the Yoneda and the colimit.

the limit composition inclusion (from the name)

The limit composition inclusion is an isomorphism of the composition of the limit of $I$ and the inclusion of $C$ and the composition of the action of the right whiskering of $C$ and the set of functors of the set of opposites of $C$ and the set of sets and the Yoneda and the colimit defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the associator of the colimit and the inclusion of $C$ and the left isomorphism whisker of the action of the right whiskering of $C$ and the set of inds of $C$ and the Yoneda and $\operatorname{preservesColimitNatIso}$ applied to the inclusion of $C$ and the inverse of the associator of the action of the right whiskering of the set of inds of $C$ and the set of functors of the set of opposites of $C$ and the set of sets and the inclusion of $C$ and the colimit and the right isomorphism whisker of the whiskering right object composition isomorphism of the Yoneda and the inclusion of $C$ and the colimit and the right isomorphism whisker of the map isomorphism of the right whiskering of $C$ and the set of functors of the set of opposites of $C$ and the set of sets and the composition and the colimit.

the presentation of X (from the name)

Let $X$ be an ind of $C$. Then the presentation of $X$ is an ind object presentation of the action of the inclusion of $C$ and $X$ defined as the presentation of $\mathrm{CategoryTheory\_\_Ind\_\_isIndObject\_inclusion\_obj}$ applied to $X$.

the Yoneda (from the name)

The Yoneda is a functor of $C$ and the set of inds of $C$ defined as the composition of the lift of the proposition that $\operatorname{IsIndObject}$ and the Yoneda and the inverse of the equivalence of $C$.

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

the composition (from the docstring)

The composition is an isomorphism of the composition of the Yoneda and the inclusion of $C$ and the Yoneda defined as the left isomorphism whisker of the lift of the proposition that $\operatorname{IsIndObject}$ and the Yoneda and the right isomorphism whisker of the counit isomorphism of the equivalence of $C$ and the inclusion of the proposition that $\operatorname{IsIndObject}$.

the parallel pair isomorphism parallel pair composition ind Yoneda of P (from the name)

Let $P$ be an ind parallel pair presentation of the map of the inclusion of $C$ and $f$ and the map of the inclusion of $C$ and $g$. Then the parallel pair isomorphism parallel pair composition ind Yoneda of $P$ is an isomorphism of the parallel pair of $f$ and $g$ and the composition of the parallel pair of $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_\_u3c6\_}$ applied to $P$ and $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_\_u3c8\_}$ applied to $P$ and the limit of $\operatorname{I}$ applied to $P$ defined as the preimage isomorphism of the action of the right whiskering of the set of inds of $C$ and the set of functors of the set of opposites of $C$ and the set of sets and the inclusion of $C$ and the composition of the diagram isomorphism parallel pair of the action of the action of the right whiskering of the set of inds of $C$ and the set of functors of the set of opposites of $C$ and the set of sets and the inclusion of $C$ and the parallel pair of $f$ and $g$ and the composition of the parallel pair isomorphism parallel pair composition Yoneda of $P$ and the left isomorphism whisker of the parallel pair of $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_\_u3c6\_}$ applied to $P$ and $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_\_u3c8\_}$ applied to $P$ and the inverse of the limit composition inclusion.

the composition Yoneda colimit isomorphism colimit composition Yoneda of G and H (from the name)

Let $F$ be a functor of $I$ and the set of functors of the set of opposites of $C$ and the set of sets. Let $G$ be a functor of $J$ and the set of costructured arrows of the Yoneda and the colimit of $F$. Let $H$ be a functor of $K$ and $\operatorname{Over}$ applied to the colimit of $F$. Then the composition Yoneda colimit isomorphism colimit composition Yoneda of $G$ and $H$ is an isomorphism of the composition of the composition of the opposite of $G$ and the opposite of $\operatorname{toOver}$ applied to the Yoneda and the colimit of $F$ and the action of the Yoneda and the colimit of $H$ and the colimit of the composition of $H$ and the composition of the Yoneda and the action of the left whiskering of the set of opposites of $\operatorname{Over}$ applied to the colimit of $F$ and the set of sets and the composition of the opposite of $G$ and the opposite of $\operatorname{toOver}$ applied to the Yoneda and the colimit of $F$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the left isomorphism whisker of the opposite of $G$ and $\operatorname{toOverCompYonedaColimit}$ applied to $H$ and the left isomorphism whisker of the composition of the opposite of $G$ and the opposite of $\operatorname{toOver}$ applied to the Yoneda and the colimit of $F$ and the colimit of the composition of $H$ and the Yoneda and the identity of the composition of the composition of the opposite of $G$ and the opposite of $\operatorname{toOver}$ applied to the Yoneda and the colimit of $F$ and the composition of the flip of the composition of $H$ and the Yoneda and the colimit and the inverse of the colimit of the composition of $H$ and the composition of the Yoneda and the action of the left whiskering of the set of opposites of $\operatorname{Over}$ applied to the colimit of $F$ and the set of sets and the composition of the opposite of $G$ and the opposite of $\operatorname{toOver}$ applied to the Yoneda and the colimit of $F$.

ind object presentation of A (from the name)

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Then the ind object presentations of $A$ are a basic type.

Let $\mathrm{self}$ be an ind object presentation of $A$. Then $\operatorname{F}$ applied to $\mathrm{self}$ is a functor of $\operatorname{I}$ applied to $\mathrm{self}$ and $C$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an ind object presentation of $A$. 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 cocone of P (from the name)

Let $P$ be an ind object presentation of $A$. Then the cocone of $P$ is a cocone of the composition of $\operatorname{F}$ applied to $P$ and the Yoneda defined as $\operatorname{mk}$ applied to $A$ and the inclusion of $P$.

the colimit cocone of P (from the docstring)

Let $P$ be an ind object presentation of $A$. Then the colimit cocone of $P$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $P$ defined as $\operatorname{isColimit}$ applied to $P$.

Let $P$ be an ind object presentation of $A$. Let $x_{1}$ be a homomorphism of $A$ and $B$. Then $\operatorname{extend}$ applied to $P$ and $x_{1}$ is an ind object presentation of $B$ defined as the ind object presentation of $\operatorname{extend}$ applied to the cocone of $P$ and $x_{1}$ and $\operatorname{extendIso}$ applied to $x_{1}$ and the colimit cocone of $P$.

Let $\mathrm{self}$ be an ind object presentation of $A$. Then $\operatorname{isColimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $A$ and the inclusion of $\mathrm{self}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

the ind object presentation of c and hc (from the name)

Let $c$ be a cocone of the composition of $F$ and the Yoneda. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the ind object presentation of $c$ and $\mathrm{hc}$ is an ind object presentation of $\operatorname{pt}$ applied to $c$ defined as $\operatorname{mk}$ applied to $I$, $F$, the inclusion of $c$ and $\mathrm{hc}$.

the costructured arrow of P (from the name)

Let $P$ be an ind object presentation of $A$. Then the costructured arrow of $P$ is a functor of $\operatorname{I}$ applied to $P$ and the set of costructured arrows of the Yoneda and $A$ defined as the composition of the costructured arrow of the cocone of $P$ and $\operatorname{pre}$ applied to $\operatorname{F}$ applied to $P$, the Yoneda and $\operatorname{pt}$ applied to the cocone of $P$.

the Yoneda of X (from the name)

Let $X$ be an element of $C$. Then the Yoneda of $X$ is an ind object presentation of the action of the Yoneda and $X$.

the inclusion of self (from the name)

Let $\mathrm{self}$ be an ind object presentation of $A$. Then the inclusion of $\mathrm{self}$ is a homomorphism of the composition of $\operatorname{F}$ applied to $\mathrm{self}$ and the Yoneda and the action of the constant of $\operatorname{I}$ applied to $\mathrm{self}$ and $A$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

A is a ind object (from the name)

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Then we can say that $A$ is an ind object.

the presentation of h (from the name)

Assume that $A$ is an ind object. Then the presentation of $h$ is an ind object presentation of $A$.

the colimit Yoneda homomorphism equivalence of F and G (from the name)

Let $F$ be a functor of $I$ and $C$. Let $G$ be a functor of the set of opposites of $C$ and the set of sets. Then the colimit Yoneda homomorphism equivalence of $F$ and $G$ is an equivalence from the set of homomorphisms of the colimit of the composition of $F$ and the Yoneda and $G$ to the limit of the composition of the opposite of $F$ and $G$ defined as the inverse of the composition of the inverse of the lift and the inverse of the equivalence of $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the colimit Yoneda homomorphism isomorphism limit opposite of $F$ and $G$ and the isomorphism of the inverse of the associator of $G$ and the functor embedding and the inverse of $\operatorname{preservesLimitIso}$ applied to the functor embedding and the composition of the opposite of $F$ and $G$.

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

Let $f$ and $g$ be homomorphisms of $A$ and $B$. Then the ind parallel pair presentations of $f$ and $g$ are a basic type.

Let $\mathrm{self}$ be an ind parallel pair presentation of $f$ and $g$. Then $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_F\_u2081\_}$ applied to $\mathrm{self}$ is a functor of $\operatorname{I}$ applied to $\mathrm{self}$ and $C$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an ind parallel pair presentation of $f$ and $g$. Then $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_F\_u2082\_}$ applied to $\mathrm{self}$ is a functor of $\operatorname{I}$ applied to $\mathrm{self}$ and $C$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an ind parallel pair presentation of $f$ and $g$. 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}$.

Let $\mathrm{self}$ be an ind parallel pair presentation of $f$ and $g$. Then $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_isColimit\_u2081\_}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $A$ and the inclusion of $\mathrm{self}$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an ind parallel pair presentation of $f$ and $g$. Then $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_isColimit\_u2082\_}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $B$ and the inclusion of $\mathrm{self}$ defined as $\operatorname{proj8}$ applied to $\mathrm{self}$.

the parallel pair isomorphism parallel pair composition Yoneda of P (from the name)

Let $P$ be an ind parallel pair presentation of $f$ and $g$. Then the parallel pair isomorphism parallel pair composition Yoneda of $P$ is an isomorphism of the parallel pair of $f$ and $g$ and the composition of the parallel pair of $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_\_u3c6\_}$ applied to $P$ and $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_\_u3c8\_}$ applied to $P$ and the composition of the action of the right whiskering of $C$ and the set of functors of the set of opposites of $C$ and the set of sets and the Yoneda and the colimit.

the inclusion of self (from the name)

Let $\mathrm{self}$ be an ind parallel pair presentation of $f$ and $g$. Then the inclusion of $\mathrm{self}$ is a homomorphism of the composition of $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_F\_u2081\_}$ applied to $\mathrm{self}$ and the Yoneda and the action of the constant of $\operatorname{I}$ applied to $\mathrm{self}$ and $A$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

the inclusion of self (from the name)

Let $\mathrm{self}$ be an ind parallel pair presentation of $f$ and $g$. Then the inclusion of $\mathrm{self}$ is a homomorphism of the composition of $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_F\_u2082\_}$ applied to $\mathrm{self}$ and the Yoneda and the action of the constant of $\operatorname{I}$ applied to $\mathrm{self}$ and $B$ defined as $\operatorname{proj7}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an ind parallel pair presentation of $f$ and $g$. Then $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_\_u3c6\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_F\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_F\_u2082\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj9}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an ind parallel pair presentation of $f$ and $g$. Then $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_\_u3c8\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_F\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_IndParallelPairPresentation\_\_F\_u2082\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj10}$ applied to $\mathrm{self}$.

the colimit constant unit isomorphism unit of C (from the name)

Let $C$ be a set. Then the colimit constant unit isomorphism unit of $C$ is an isomorphism of the colimit of the constant unit functor of $C$ and $\mathrm{PUnit}$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the constant unit functor of $C$ and $\operatorname{isColimitPUnitCocone}$ applied to $C$.

the constant unit functor of C (from the name)

Let $C$ be a set. Then the constant unit functor of $C$ is a functor of $C$ and the set of sets defined as the action of the constant of $C$ and $\mathrm{PUnit}$.

Let $C$ be a set. Then $\operatorname{isColimitPUnitCocone}$ applied to $C$ is an element of $\operatorname{IsColimit}$ applied to the unit cocone of $C$.

the unit cocone of C (from the name)

Let $C$ be a set. Then the unit cocone of $C$ is a cocone of the constant unit functor of $C$ defined as $\operatorname{mk}$ applied to $\mathrm{PUnit}$ and the identity morphism of the constant unit functor of $C$.

Let $t$ be a cocone of $F$. Then the elements of $\operatorname{IsColimit}$ applied to $t$ are a basic type.

the cocone of h and f (from the name)

Let $h$ be an element of $\operatorname{CorepresentableBy}$ applied to the cocone of $F$ and $X$. Let $f$ be a homomorphism of $X$ and $Y$. Then the cocone of $h$ and $f$ is a cocone of $F$ defined as $\operatorname{mk}$ applied to $Y$ and $\operatorname{homEquiv}$ applied to $h$ and $f$.

the colimit cocone of h (from the name)

Let $h$ be an element of $\operatorname{CorepresentableBy}$ applied to the cocone of $F$ and $X$. Then the colimit cocone of $h$ is a cocone of $F$ defined as the cocone of $h$ and the identity morphism of $X$.

the homomorphism of h and s (from the name)

Let $h$ be an element of $\operatorname{CorepresentableBy}$ applied to the cocone of $F$ and $X$. Let $s$ be a cocone of $F$. Then the homomorphism of $h$ and $s$ is a homomorphism of $X$ and $\operatorname{pt}$ applied to $s$ defined as $\operatorname{symm}$ applied to the homomorphism equivalence of $h$ and the inclusion of $s$.

Let $P$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $Q$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then $\operatorname{coconePointUniqueUpToIso}$ applied to $P$ and $Q$ is an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ defined as the map isomorphism of $\operatorname{forget}$ applied to $F$ and $\operatorname{uniqueUpToIso}$ applied to $P$ and $Q$.

the cocone point isomorphism of e and w (from the name)

Let $P$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $Q$ be an element of $\operatorname{IsColimit}$ applied to $t$. Let $e$ be an equivalence of $J$ and $K$. Let $w$ be an isomorphism of the composition of the functor of $e$ and $G$ and $F$. Then the cocone point isomorphism of $e$ and $w$ is an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$.

the cocone point isomorphism of Q and w (from the name)

Let $P$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $Q$ be an element of $\operatorname{IsColimit}$ applied to $t$. Let $w$ be an isomorphism of $F$ and $G$. Then the cocone point isomorphism of $Q$ and $w$ is an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then $\operatorname{corepresentableBy}$ applied to $\mathrm{hc}$ is an element of $\operatorname{CorepresentableBy}$ applied to the cocone of $F$ and $\operatorname{pt}$ applied to $t$.

Let $\mathrm{self}$ be an element of $\operatorname{IsColimit}$ applied to $t$. Let $s$ be a cocone of $F$. Then $\operatorname{desc}$ applied to $\mathrm{self}$ and $s$ is a homomorphism of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $s$.

the universal morphism of h and s (from the docstring)

Let $h$ be an element of $\operatorname{IsColimit}$ applied to $t$. Let $s$ be a cocone of $F$. Then the universal morphism of $h$ and $s$ is a homomorphism of $t$ and $s$.

the equivalence isomorphism colimit of i (from the name)

Let $i$ be an isomorphism of $r$ and $t$. Then the equivalence isomorphism colimit of $i$ is an element of $\EquivMACRoAE {\operatorname{IsColimit} (r)}{\operatorname{IsColimit} (t)}$.

the equivalence of d and w (from the name)

Let $x_{2}$ be an isomorphism of $F$ and $G$. Let $c$ be a cocone of $F$. Let $d$ be a cocone of $G$. Let $w$ be an isomorphism of the action of the precomposition of the inverse of $x_{2}$ and $c$ and $d$. Then the equivalence of $d$ and $w$ is an element of $\EquivMACRoAE {\operatorname{IsColimit} (c)}{\operatorname{IsColimit} (d)}$ defined as the composition of the inverse of the precomposition inverse equivalence of $x_{2}$ and $c$ and the equivalence isomorphism colimit of $w$.

Let $i$ be a homomorphism of $\operatorname{pt}$ applied to $s$ and $X$. Let $\mathrm{hs}$ be an element of $\operatorname{IsColimit}$ applied to $s$. Then $\operatorname{extendIso}$ applied to $i$ and $\mathrm{hs}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{extend}$ applied to $s$ and $i$ defined as $\operatorname{ofIsoColimit}$ applied to $\mathrm{hs}$ and $\operatorname{extendIso}$ applied to $s$ and $\operatorname{asIso}$ applied to $i$.

Let $i$ be a homomorphism of $\operatorname{pt}$ applied to $s$ and $X$. Then $\operatorname{extendIsoEquiv}$ applied to $i$ is an element of $\EquivMACRoAE {\operatorname{IsColimit} (s)}{\operatorname{IsColimit} (\operatorname{extend} (s , i))}$ defined as the equivalence of $\operatorname{extendIso}$ applied to $i$ and $\operatorname{ofExtendIso}$ applied to $i$.

the homomorphism equivalence of h (from the name)

Let $h$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then the homomorphism equivalence of $h$ is an equivalence from the set of homomorphisms of $\operatorname{pt}$ applied to $t$ and $W$ to the set of homomorphisms of $F$ and the action of the constant of $J$ and $W$.

the homomorphism isomorphism of h and W (from the name)

Let $h$ be an element of $\operatorname{IsColimit}$ applied to $t$. Let $W$ be an element of $C$. Then the homomorphism isomorphism of $h$ and $W$ is an isomorphism of $\mathrm{ULift}$ applied to the set of homomorphisms of $\operatorname{pt}$ applied to $t$ and $W$ and the set of homomorphisms of $F$ and the action of the constant of $J$ and $W$ defined as the isomorphism of the composition of the lift and the homomorphism equivalence of $h$.

the homomorphism isomorphism of h and W (from the name)

Let $h$ be an element of $\operatorname{IsColimit}$ applied to $t$. Let $W$ be an element of $C$. Then the homomorphism isomorphism of $h$ and $W$ is an isomorphism of $\mathrm{ULift}$ applied to the set of homomorphisms of $\operatorname{pt}$ applied to $t$ and $W$ and $\SubtypeSet {p}{\mathrm{forall} (J , \lambda j . \mathrm{forall} (J , \lambda \mathrm{j'} . \mathrm{forall} (\operatorname{Hom} (\mathrm{j'} , j), \lambda f . \EqtMACRoH {\operatorname{comp} (\operatorname{map} (F , f), p (j))}{p (\mathrm{j'})})))}$.

the isomorphism unique cocone morphism (from the name)

The isomorphism unique cocone morphism is an isomorphism of $\operatorname{IsColimit}$ applied to $t$ and the set of functions from cocones $s$ of $F$ to elements of $\mathrm{Unique}$ applied to the set of homomorphisms of $t$ and $s$.

the map of s and x2 (from the name)

Let $P$ be an element of $\operatorname{IsColimit}$ applied to $t$. Let $s$ be a cocone of $F$. Let $x_{2}$ be a homomorphism of $G$ and $F$. Then the map of $s$ and $x_{2}$ is a homomorphism of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s$ defined as $\operatorname{desc}$ applied to $P$ and the action of the precomposition of $x_{2}$ and $s$.

the map cocone equivalence of h and t (from the name)

Let $h$ be an isomorphism of $F$ and $G$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of $F$ and $c$. Then the map cocone equivalence of $h$ and $t$ is an element of $\operatorname{IsColimit}$ applied to the map cocone of $G$ and $c$ defined as $\operatorname{precomposeHomEquiv}$ applied to the left isomorphism whisker of $K$ and $h$, the map cocone of $G$ and $c$ and $\operatorname{ofIsoColimit}$ applied to $t$ and the inverse of the precomposition whisker left map cocone of the inverse of $h$ and $c$.

the cocone morphism of desc and s1 (from the name)

Let $\mathrm{desc}$ be a function from cocones $s_{1}$ of $F$ to homomorphisms of $t$ and $s_{1}$ such that for all cocones $s$ of $F$, for all homomorphisms $m$ of $t$ and $s$, $\EqtMACRoH {m}{\mathrm{desc} (s)}$. Then the cocone morphism of $s_{1}$ and $\mathrm{desc}$ is an element of $\operatorname{IsColimit}$ applied to $t$.

the natural isomorphism of h (from the name)

Let $h$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then the natural isomorphism of $h$ is an isomorphism of the composition of the action of the Coyoneda and $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $t$ and the functor embedding and the cocone of $F$.

Let $h$ be an equivalence of the set of cocones of $G$ and the set of cocones of $F$. Then $\operatorname{ofCoconeEquiv}$ applied to $h$ is an equivalence from $\operatorname{IsColimit}$ applied to the action of the functor of $h$ and $c$ to $\operatorname{IsColimit}$ applied to $c$.

Let $h$ be an element of $\operatorname{CorepresentableBy}$ applied to the cocone of $F$ and $X$. Then $\operatorname{ofCorepresentableBy}$ applied to $h$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $h$.

Assume that for all cocones $s$ of $F$, $\mathrm{ExistsUnique}$ holds for the function that maps $l$ to the proposition that for all elements $j$ of $J$, the composition of the component of the inclusion of $t$ and $j$ and $l$ is equal to the component of the inclusion of $s$ and $j$. Then $\operatorname{ofExistsUnique}$ applied to $\mathrm{ht}$ is an element of $\operatorname{IsColimit}$ applied to $t$.

Let $i$ be a homomorphism of $\operatorname{pt}$ applied to $s$ and $X$. Let $\mathrm{hs}$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{extend}$ applied to $s$ and $i$. Then $\operatorname{ofExtendIso}$ applied to $i$ and $\mathrm{hs}$ is an element of $\operatorname{IsColimit}$ applied to $s$ defined as $\operatorname{ofIsoColimit}$ applied to $\mathrm{hs}$ and the inverse of $\operatorname{extendIso}$ applied to $s$ and $\operatorname{asIso}$ applied to $i$.

Let $G$ be a functor of $C$ and $D$. Let $\mathrm{ht}$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of $G$ and $t$. Let $\mathrm{desc}$ be a function from cocones $s_{1}$ of $F$ to homomorphisms of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s_{1}$ such that for all cocones $s$ of $F$, the map of $G$ and $\mathrm{desc}$ applied to $s$ is equal to $\operatorname{desc}$ applied to $\mathrm{ht}$ and the map cocone of $G$ and $s$. Then $\operatorname{ofFaithful}$ applied to $G$, $\mathrm{ht}$, $s_{1}$, $\mathrm{desc}$ and $h_{1}$ is an element of $\operatorname{IsColimit}$ applied to $t$.

Let $P$ be an element of $\operatorname{IsColimit}$ applied to $r$. Let $i$ be an isomorphism of $r$ and $t$. Then $\operatorname{ofIsoColimit}$ applied to $P$ and $i$ is an element of $\operatorname{IsColimit}$ applied to $t$.

Let $\mathrm{adj}$ be an adjunction of $\mathrm{left}$ and $\mathrm{right}$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{ofLeftAdjoint}$ applied to $\mathrm{adj}$ and $t$ is an element of $\operatorname{IsColimit}$ applied to the action of $\mathrm{left}$ and $c$.

Let $P$ be an element of $\operatorname{IsColimit}$ applied to $r$. Then $\operatorname{ofPointIso}$ applied to $P$ is an element of $\operatorname{IsColimit}$ applied to $t$ defined as $\operatorname{ofIsoColimit}$ applied to $P$ and the inverse of $\operatorname{asIso'}$ applied to the universal morphism of $P$ and $t$.

Let $e$ be an equivalence of $K$ and $J$. Let $P$ be an element of $\operatorname{IsColimit}$ applied to the whisker of the functor of $e$ and $s$. Then $\operatorname{ofWhiskerEquivalence}$ applied to $e$ and $P$ is an element of $\operatorname{IsColimit}$ applied to $s$ defined as $\operatorname{equivIsoColimit}$ applied to the inverse of the application of the unit isomorphism of the whiskering equivalence of $e$ and $s$ and $\operatorname{ofLeftAdjoint}$ applied to the adjunction of the inverse of the whiskering equivalence of $e$ and $P$.

the precomposition homomorphism equivalence of x2 and c (from the name)

Let $x_{2}$ be an isomorphism of $F$ and $G$. Let $c$ be a cocone of $G$. Then the precomposition homomorphism equivalence of $x_{2}$ and $c$ is an equivalence from $\operatorname{IsColimit}$ applied to the action of the precomposition of the homomorphism of $x_{2}$ and $c$ to $\operatorname{IsColimit}$ applied to $c$ defined as the precomposition inverse equivalence of the inverse of $x_{2}$ and $c$.

the precomposition inverse equivalence of x2 and c (from the name)

Let $x_{2}$ be an isomorphism of $F$ and $G$. Let $c$ be a cocone of $F$. Then the precomposition inverse equivalence of $x_{2}$ and $c$ is an equivalence from $\operatorname{IsColimit}$ applied to the action of the precomposition of the inverse of $x_{2}$ and $c$ to $\operatorname{IsColimit}$ applied to $c$ defined as $\operatorname{ofCoconeEquiv}$ applied to the precomposition equivalence of $x_{2}$.

Let $P$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $Q$ be an element of $\operatorname{IsColimit}$ applied to $t$. Then $\operatorname{uniqueUpToIso}$ applied to $P$ and $Q$ is an isomorphism of $s$ and $t$.

the whisker equivalence of P and e (from the name)

Let $P$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $e$ be an equivalence of $K$ and $J$. Then the whisker equivalence of $P$ and $e$ is an element of $\operatorname{IsColimit}$ applied to the whisker of the functor of $e$ and $s$ defined as $\operatorname{ofLeftAdjoint}$ applied to the adjunction of the whiskering equivalence of $e$ and $P$.

the whisker equivalence equivalence of e (from the name)

Let $e$ be an equivalence of $K$ and $J$. Then the whisker equivalence equivalence of $e$ is an equivalence from $\operatorname{IsColimit}$ applied to $s$ to $\operatorname{IsColimit}$ applied to the whisker of the functor of $e$ and $s$.

Let $t$ be a cone of $F$. Then the elements of $\operatorname{IsLimit}$ applied to $t$ are a basic type.

the cone of h and f (from the name)

Let $h$ be an element of $\operatorname{RepresentableBy}$ applied to the cone of $F$ and $X$. Let $f$ be a homomorphism of $Y$ and $X$. Then the cone of $h$ and $f$ is a cone of $F$ defined as $\operatorname{mk}$ applied to $Y$ and $\operatorname{homEquiv}$ applied to $h$ and $f$.

the homomorphism of h and s (from the name)

Let $h$ be an element of $\operatorname{RepresentableBy}$ applied to the cone of $F$ and $X$. Let $s$ be a cone of $F$. Then the homomorphism of $h$ and $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $X$ defined as $\operatorname{symm}$ applied to the homomorphism equivalence of $h$ and the projection of $s$.

the limit cone of h (from the name)

Let $h$ be an element of $\operatorname{RepresentableBy}$ applied to the cone of $F$ and $X$. Then the limit cone of $h$ is a cone of $F$ defined as the cone of $h$ and the identity morphism of $X$.

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $Q$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then $\operatorname{conePointUniqueUpToIso}$ applied to $P$ and $Q$ is an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ defined as the map isomorphism of $\operatorname{forget}$ applied to $F$ and $\operatorname{uniqueUpToIso}$ applied to $P$ and $Q$.

the cone point isomorphism of e and w (from the name)

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $Q$ be an element of $\operatorname{IsLimit}$ applied to $t$. Let $e$ be an equivalence of $J$ and $K$. Let $w$ be an isomorphism of the composition of the functor of $e$ and $G$ and $F$. Then the cone point isomorphism of $e$ and $w$ is an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$.

the cone point isomorphism of Q and w (from the name)

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $Q$ be an element of $\operatorname{IsLimit}$ applied to $t$. Let $w$ be an isomorphism of $F$ and $G$. Then the cone point isomorphism of $Q$ and $w$ is an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$.

the equivalence isomorphism limit of i (from the name)

Let $i$ be an isomorphism of $r$ and $t$. Then the equivalence isomorphism limit of $i$ is an element of $\EquivMACRoAE {\operatorname{IsLimit} (r)}{\operatorname{IsLimit} (t)}$.

the equivalence of d and w (from the name)

Let $x_{2}$ be an isomorphism of $F$ and $G$. Let $c$ be a cone of $F$. Let $d$ be a cone of $G$. Let $w$ be an isomorphism of the action of the postcomposition of the homomorphism of $x_{2}$ and $c$ and $d$. Then the equivalence of $d$ and $w$ is an element of $\EquivMACRoAE {\operatorname{IsLimit} (c)}{\operatorname{IsLimit} (d)}$ defined as the composition of the inverse of the postcomposition homomorphism equivalence of $x_{2}$ and $c$ and the equivalence isomorphism limit of $w$.

Let $i$ be a homomorphism of $X$ and $\operatorname{pt}$ applied to $s$. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then $\operatorname{extendIso}$ applied to $i$ and $\mathrm{hs}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{extend}$ applied to $s$ and $i$ defined as $\operatorname{ofIsoLimit}$ applied to $\mathrm{hs}$ and $\operatorname{extendIso}$ applied to $s$ and $\operatorname{asIso'}$ applied to $i$.

Let $i$ be a homomorphism of $X$ and $\operatorname{pt}$ applied to $s$. Then $\operatorname{extendIsoEquiv}$ applied to $i$ is an element of $\EquivMACRoAE {\operatorname{IsLimit} (s)}{\operatorname{IsLimit} (\operatorname{extend} (s , i))}$ defined as the equivalence of $\operatorname{extendIso}$ applied to $i$ and $\operatorname{ofExtendIso}$ applied to $i$.

the homomorphism equivalence of h (from the name)

Let $h$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then the homomorphism equivalence of $h$ is an equivalence from the set of homomorphisms of $W$ and $\operatorname{pt}$ applied to $t$ to the set of homomorphisms of the action of the constant of $J$ and $W$ and $F$.

the homomorphism isomorphism of h and W (from the name)

Let $h$ be an element of $\operatorname{IsLimit}$ applied to $t$. Let $W$ be an element of $C$. Then the homomorphism isomorphism of $h$ and $W$ is an isomorphism of $\mathrm{ULift}$ applied to the set of homomorphisms of $W$ and $\operatorname{pt}$ applied to $t$ and the set of homomorphisms of the action of the constant of $J$ and $W$ and $F$ defined as the isomorphism of the composition of the lift and the homomorphism equivalence of $h$.

the homomorphism isomorphism of h and W (from the name)

Let $h$ be an element of $\operatorname{IsLimit}$ applied to $t$. Let $W$ be an element of $C$. Then the homomorphism isomorphism of $h$ and $W$ is an isomorphism of $\mathrm{ULift}$ applied to the set of homomorphisms of $W$ and $\operatorname{pt}$ applied to $t$ and $\SubtypeSet {p}{\mathrm{forall} (J , \lambda j . \mathrm{forall} (J , \lambda \mathrm{j'} . \mathrm{forall} (\operatorname{Hom} (j , \mathrm{j'}), \lambda f . \EqtMACRoH {\operatorname{comp} (p (j), \operatorname{map} (F , f))}{p (\mathrm{j'})})))}$.

the isomorphism unique cone morphism (from the name)

The isomorphism unique cone morphism is an isomorphism of $\operatorname{IsLimit}$ applied to $t$ and the set of functions from cones $s$ of $F$ to elements of $\mathrm{Unique}$ applied to the set of homomorphisms of $s$ and $t$.

the lift of self and s (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{IsLimit}$ applied to $t$. Let $s$ be a cone of $F$. Then the lift of $\mathrm{self}$ and $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $s$.

the universal morphism of h and s (from the docstring)

Let $h$ be an element of $\operatorname{IsLimit}$ applied to $t$. Let $s$ be a cone of $F$. Then the universal morphism of $h$ and $s$ is a homomorphism of $s$ and $t$.

the map of P and x2 (from the name)

Let $s$ be a cone of $F$. Let $P$ be an element of $\operatorname{IsLimit}$ applied to $t$. Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the map of $P$ and $x_{2}$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ defined as the lift of $P$ and the action of the postcomposition of $x_{2}$ and $s$.

the map cone equivalence of h and t (from the name)

Let $h$ be an isomorphism of $F$ and $G$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to the map cone of $F$ and $c$. Then the map cone equivalence of $h$ and $t$ is an element of $\operatorname{IsLimit}$ applied to the map cone of $G$ and $c$ defined as $\operatorname{postcomposeInvEquiv}$ applied to the left isomorphism whisker of $K$ and $h$, the map cone of $G$ and $c$ and $\operatorname{ofIsoLimit}$ applied to $t$ and the inverse of the postcomposition whisker left map cone of the inverse of $h$ and $c$.

the cone morphism of lift and s1 (from the name)

Let $\mathrm{lift}$ be a function from cones $s_{1}$ of $F$ to homomorphisms of $s_{1}$ and $t$ such that for all cones $s$ of $F$, for all homomorphisms $m$ of $s$ and $t$, $\EqtMACRoH {m}{\mathrm{lift} (s)}$. Then the cone morphism of $s_{1}$ and $\mathrm{lift}$ is an element of $\operatorname{IsLimit}$ applied to $t$.

the natural isomorphism of h (from the name)

Let $h$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then the natural isomorphism of $h$ is an isomorphism of the composition of the action of the Yoneda and $\operatorname{pt}$ applied to $t$ and the functor embedding and the cone of $F$.

Let $h$ be an equivalence of the set of cones of $G$ and the set of cones of $F$. Then $\operatorname{ofConeEquiv}$ applied to $h$ is an equivalence from $\operatorname{IsLimit}$ applied to the action of the functor of $h$ and $c$ to $\operatorname{IsLimit}$ applied to $c$.

Assume that for all cones $s$ of $F$, $\mathrm{ExistsUnique}$ holds for the function that maps $l$ to the proposition that for all elements $j$ of $J$, the composition of $l$ and the component of the projection of $t$ and $j$ is equal to the component of the projection of $s$ and $j$. Then $\operatorname{ofExistsUnique}$ applied to $\mathrm{ht}$ is an element of $\operatorname{IsLimit}$ applied to $t$.

Let $i$ be a homomorphism of $X$ and $\operatorname{pt}$ applied to $s$. Let $\mathrm{hs}$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{extend}$ applied to $s$ and $i$. Then $\operatorname{ofExtendIso}$ applied to $i$ and $\mathrm{hs}$ is an element of $\operatorname{IsLimit}$ applied to $s$ defined as $\operatorname{ofIsoLimit}$ applied to $\mathrm{hs}$ and the inverse of $\operatorname{extendIso}$ applied to $s$ and $\operatorname{asIso'}$ applied to $i$.

Let $G$ be a functor of $C$ and $D$. Let $\mathrm{ht}$ be an element of $\operatorname{IsLimit}$ applied to the map cone of $G$ and $t$. Let $\mathrm{lift}$ be a function from cones $s_{1}$ of $F$ to homomorphisms of $\operatorname{pt}$ applied to $s_{1}$ and $\operatorname{pt}$ applied to $t$ such that for all cones $s$ of $F$, the map of $G$ and $\mathrm{lift}$ applied to $s$ is equal to the lift of $\mathrm{ht}$ and the map cone of $G$ and $s$. Then $\operatorname{ofFaithful}$ applied to $G$, $\mathrm{ht}$, $s_{1}$, $\mathrm{lift}$ and $h_{1}$ is an element of $\operatorname{IsLimit}$ applied to $t$.

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $r$. Let $i$ be an isomorphism of $r$ and $t$. Then $\operatorname{ofIsoLimit}$ applied to $P$ and $i$ is an element of $\operatorname{IsLimit}$ applied to $t$.

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $r$. Then $\operatorname{ofPointIso}$ applied to $P$ is an element of $\operatorname{IsLimit}$ applied to $t$ defined as $\operatorname{ofIsoLimit}$ applied to $P$ and the inverse of $\operatorname{asIso}$ applied to the universal morphism of $P$ and $t$.

Let $h$ be an element of $\operatorname{RepresentableBy}$ applied to the cone of $F$ and $X$. Then $\operatorname{ofRepresentableBy}$ applied to $h$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $h$.

Let $\mathrm{adj}$ be an adjunction of $\mathrm{left}$ and $\mathrm{right}$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{ofRightAdjoint}$ applied to $\mathrm{adj}$ and $t$ is an element of $\operatorname{IsLimit}$ applied to the action of $\mathrm{right}$ and $c$.

Let $e$ be an equivalence of $K$ and $J$. Let $P$ be an element of $\operatorname{IsLimit}$ applied to the whisker of the functor of $e$ and $s$. Then $\operatorname{ofWhiskerEquivalence}$ applied to $e$ and $P$ is an element of $\operatorname{IsLimit}$ applied to $s$ defined as $\operatorname{equivIsoLimit}$ applied to the inverse of the application of the unit isomorphism of the whiskering equivalence of $e$ and $s$ and $\operatorname{ofRightAdjoint}$ applied to the adjunction of the whiskering equivalence of $e$ and $P$.

the postcomposition homomorphism equivalence of x2 and c (from the name)

Let $x_{2}$ be an isomorphism of $F$ and $G$. Let $c$ be a cone of $F$. Then the postcomposition homomorphism equivalence of $x_{2}$ and $c$ is an equivalence from $\operatorname{IsLimit}$ applied to the action of the postcomposition of the homomorphism of $x_{2}$ and $c$ to $\operatorname{IsLimit}$ applied to $c$ defined as $\operatorname{ofConeEquiv}$ applied to the postcomposition equivalence of $x_{2}$.

the postcomposition inverse equivalence of x2 and c (from the name)

Let $x_{2}$ be an isomorphism of $F$ and $G$. Let $c$ be a cone of $G$. Then the postcomposition inverse equivalence of $x_{2}$ and $c$ is an equivalence from $\operatorname{IsLimit}$ applied to the action of the postcomposition of the inverse of $x_{2}$ and $c$ to $\operatorname{IsLimit}$ applied to $c$ defined as the postcomposition homomorphism equivalence of the inverse of $x_{2}$ and $c$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then $\operatorname{representableBy}$ applied to $\mathrm{hc}$ is an element of $\operatorname{RepresentableBy}$ applied to the cone of $F$ and $\operatorname{pt}$ applied to $t$.

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $Q$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then $\operatorname{uniqueUpToIso}$ applied to $P$ and $Q$ is an isomorphism of $s$ and $t$.

the whisker equivalence of P and e (from the name)

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $e$ be an equivalence of $K$ and $J$. Then the whisker equivalence of $P$ and $e$ is an element of $\operatorname{IsLimit}$ applied to the whisker of the functor of $e$ and $s$ defined as $\operatorname{ofRightAdjoint}$ applied to the adjunction of the inverse of the whiskering equivalence of $e$ and $P$.

the whisker equivalence equivalence of e (from the name)

Let $e$ be an equivalence of $K$ and $J$. Then the whisker equivalence equivalence of $e$ is an equivalence from $\operatorname{IsLimit}$ applied to $s$ to $\operatorname{IsLimit}$ applied to the whisker of the functor of $e$ and $s$.

the colimit cocone of F (from the docstring)

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

the colimit cocone of F (from the docstring)

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

the limit cone of F (from the docstring)

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

the limit cone of F (from the docstring)

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

C is a monomorphism coproduct (from the name)

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

the binary cofan sum of x5 and x6 (from the name)

Let $c$ be a cofan of $X$. Let $x_{3}$ be a cofan of $\operatorname{comp}$ applied to $X$ and $\operatorname{inl}$. Let $x_{4}$ be a cofan of $\operatorname{comp}$ applied to $X$ and $\operatorname{inr}$. Let $x_{5}$ be an element of $\operatorname{IsColimit}$ applied to $x_{3}$. Let $x_{6}$ be an element of $\operatorname{IsColimit}$ applied to $x_{4}$. Then the binary cofan sum of $x_{5}$ and $x_{6}$ is a binary cofan of $\operatorname{pt}$ applied to $x_{3}$ and $\operatorname{pt}$ applied to $x_{4}$ defined as $\operatorname{mk}$ applied to $\operatorname{desc}$ applied to $x_{5}$ and the function that maps $x_{7}$ to the injection of $c$ and $\operatorname{inl}$ applied to $x_{7}$ and $\operatorname{desc}$ applied to $x_{6}$ and the function that maps $x_{8}$ to the injection of $c$ and $\operatorname{inr}$ applied to $x_{8}$.

Let $c$ be a cofan of $X$. Let $x_{3}$ be a cofan of $\operatorname{comp}$ applied to $X$ and $\operatorname{inl}$. Let $x_{4}$ be a cofan of $\operatorname{comp}$ applied to $X$ and $\operatorname{inr}$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $x_{5}$ be an element of $\operatorname{IsColimit}$ applied to $x_{3}$. Let $x_{6}$ be an element of $\operatorname{IsColimit}$ applied to $x_{4}$. Then $\operatorname{isColimitBinaryCofanSum}$ applied to $c$, $x_{3}$, $x_{4}$, $\mathrm{hc}$, $x_{5}$ and $x_{6}$ is an element of $\operatorname{IsColimit}$ applied to the binary cofan sum of $x_{5}$ and $x_{6}$.

the identity terminal of P and X (from the name)

Let $P$ be a morphism property of $T$. Let $X$ be an element of $T$. Then the identity terminal of $P$ and $X$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{mk}$ applied to the top, the identity morphism of $X$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_id\_mem}$ applied to $P$ and $X$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{mk}$ applied to the top, the identity morphism of $X$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_id\_mem}$ applied to $P$ and $X$.

Let $P$ be a morphism property of $T$. Let $X$ be an element of $T$. Then $\operatorname{mkIdInitial}$ applied to $P$ and $X$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{mk}$ applied to the top, the identity morphism of $X$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_id\_mem}$ applied to $P$ and $X$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{mk}$ applied to the top, the identity morphism of $X$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_id\_mem}$ applied to $P$ and $X$.

the colimit of F (from the docstring)

Let $F$ be a functor of $J$ and the set of opposites of $C$. Then the colimit of $F$ is an isomorphism of the colimit of the left opposite of $F$ and the opposite of the limit of $F$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the cocone left opposite of the cone of $F$ and $\operatorname{isColimitCoconeLeftOpOfCone}$ applied to $F$ and $\operatorname{isLimit}$ applied to $F$.

the colimit of F (from the docstring)

Let $F$ be a functor of $J$ and $C$. Then the colimit of $F$ is an isomorphism of the colimit of the opposite of $F$ and $\operatorname{op}$ applied to the limit of $F$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the opposite of the cone of $F$ and the opposite of $\operatorname{isLimit}$ applied to $F$.

the colimit of F (from the docstring)

Let $F$ be a functor of the set of opposites of $J$ and $C$. Then the colimit of $F$ is an isomorphism of the colimit of the right opposite of $F$ and $\operatorname{op}$ applied to the limit of $F$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the cocone right opposite of the cone of $F$ and $\operatorname{isColimitCoconeRightOpOfCone}$ applied to $F$ and $\operatorname{isLimit}$ applied to $F$.

the colimit of F (from the docstring)

Let $F$ be a functor of the set of opposites of $J$ and the set of opposites of $C$. Then the colimit of $F$ is an isomorphism of the colimit of the opposite of $F$ and the opposite of the limit of $F$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the cocone opposite of the cone of $F$ and $\operatorname{isColimitCoconeUnopOfCone}$ applied to $F$ and $\operatorname{isLimit}$ applied to $F$.

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isColimitCoconeLeftOpOfCone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the cocone left opposite of $c$.

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isColimitCoconeOfConeLeftOp}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $c$.

Let $F$ be a functor of the set of opposites of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isColimitCoconeOfConeRightOp}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $c$.

Let $F$ be a functor of the set of opposites of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isColimitCoconeOfConeUnop}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $c$.

Let $F$ be a functor of the set of opposites of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isColimitCoconeRightOpOfCone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the cocone right opposite of $c$.

Let $F$ be a functor of the set of opposites of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isColimitCoconeUnopOfCone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the cocone opposite of $c$.

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to the cone left opposite of $c$. Then $\operatorname{isColimitOfConeLeftOpOfCocone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $c$ defined as $\operatorname{isColimitCoconeOfConeLeftOp}$ applied to $F$ and $\mathrm{hc}$.

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to the cone of $c$. Then $\operatorname{isColimitOfConeOfCoconeLeftOp}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $c$ defined as $\operatorname{isColimitCoconeLeftOpOfCone}$ applied to $F$ and $\mathrm{hc}$.

Let $F$ be a functor of the set of opposites of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to the cone of $c$. Then $\operatorname{isColimitOfConeOfCoconeRightOp}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $c$ defined as $\operatorname{isColimitCoconeRightOpOfCone}$ applied to $F$ and $\mathrm{hc}$.

Let $F$ be a functor of the set of opposites of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to the cone of $c$. Then $\operatorname{isColimitOfConeOfCoconeUnop}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $c$ defined as $\operatorname{isColimitCoconeUnopOfCone}$ applied to $F$ and $\mathrm{hc}$.

Let $F$ be a functor of the set of opposites of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to the cone right opposite of $c$. Then $\operatorname{isColimitOfConeRightOpOfCocone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $c$ defined as $\operatorname{isColimitCoconeOfConeRightOp}$ applied to $F$ and $\mathrm{hc}$.

Let $F$ be a functor of the set of opposites of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to the cone opposite of $c$. Then $\operatorname{isColimitOfConeUnopOfCocone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $c$ defined as $\operatorname{isColimitCoconeOfConeUnop}$ applied to $F$ and $\mathrm{hc}$.

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isLimitConeLeftOpOfCocone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the cone left opposite of $c$.

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isLimitConeOfCoconeLeftOp}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the cone of $c$.

Let $F$ be a functor of the set of opposites of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isLimitConeOfCoconeRightOp}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the cone of $c$.

Let $F$ be a functor of the set of opposites of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isLimitConeOfCoconeUnop}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the cone of $c$.

Let $F$ be a functor of the set of opposites of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isLimitConeRightOpOfCocone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the cone right opposite of $c$.

Let $F$ be a functor of the set of opposites of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isLimitConeUnopOfCocone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the cone opposite of $c$.

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to the cocone left opposite of $c$. Then $\operatorname{isLimitOfCoconeLeftOpOfCone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$ defined as $\operatorname{isLimitConeOfCoconeLeftOp}$ applied to $F$ and $\mathrm{hc}$.

Let $F$ be a functor of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to the cocone of $c$. Then $\operatorname{isLimitOfCoconeOfConeLeftOp}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$ defined as $\operatorname{isLimitConeLeftOpOfCocone}$ applied to $F$ and $\mathrm{hc}$.

Let $F$ be a functor of the set of opposites of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to the cocone of $c$. Then $\operatorname{isLimitOfCoconeOfConeRightOp}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$ defined as $\operatorname{isLimitConeRightOpOfCocone}$ applied to $F$ and $\mathrm{hc}$.

Let $F$ be a functor of the set of opposites of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to the cocone of $c$. Then $\operatorname{isLimitOfCoconeOfConeUnop}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$ defined as $\operatorname{isLimitConeUnopOfCocone}$ applied to $F$ and $\mathrm{hc}$.

Let $F$ be a functor of the set of opposites of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to the cocone right opposite of $c$. Then $\operatorname{isLimitOfCoconeRightOpOfCone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$ defined as $\operatorname{isLimitConeOfCoconeRightOp}$ applied to $F$ and $\mathrm{hc}$.

Let $F$ be a functor of the set of opposites of $J$ and the set of opposites of $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to the cocone opposite of $c$. Then $\operatorname{isLimitOfCoconeUnopOfCone}$ applied to $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$ defined as $\operatorname{isLimitConeOfCoconeUnop}$ applied to $F$ and $\mathrm{hc}$.

the limit of F (from the docstring)

Let $F$ be a functor of $J$ and the set of opposites of $C$. Then the limit of $F$ is an isomorphism of the limit of the left opposite of $F$ and the opposite of the colimit of $F$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the cone left opposite of the cocone of $F$ and $\operatorname{isLimitConeLeftOpOfCocone}$ applied to $F$ and $\operatorname{isColimit}$ applied to $F$.

the limit of F (from the docstring)

Let $F$ be a functor of $J$ and $C$. Then the limit of $F$ is an isomorphism of the limit of the opposite of $F$ and $\operatorname{op}$ applied to the colimit of $F$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the opposite of the cocone of $F$ and the opposite of $\operatorname{isColimit}$ applied to $F$.

the limit of F (from the docstring)

Let $F$ be a functor of the set of opposites of $J$ and $C$. Then the limit of $F$ is an isomorphism of the limit of the right opposite of $F$ and $\operatorname{op}$ applied to the colimit of $F$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the cone right opposite of the cocone of $F$ and $\operatorname{isLimitConeRightOpOfCocone}$ applied to $F$ and $\operatorname{isColimit}$ applied to $F$.

the limit of F (from the docstring)

Let $F$ be a functor of the set of opposites of $J$ and the set of opposites of $C$. Then the limit of $F$ is an isomorphism of the limit of the opposite of $F$ and the opposite of the colimit of $F$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the cone opposite of the cocone of $F$ and $\operatorname{isLimitConeUnopOfCocone}$ applied to $F$ and $\operatorname{isColimit}$ applied to $F$.

Let $F$ be a functor of $J$ and $C$. Then $\operatorname{isColimitToOver}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{toOver}$ applied to $F$ defined as $\operatorname{isColimitToOver}$ applied to $\operatorname{isColimit}$ applied to $F$.

Let $F$ be a functor of $J$ and $C$. Then $\operatorname{isLimitToOver}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{toUnder}$ applied to $F$ defined as $\operatorname{isLimitToUnder}$ applied to $\operatorname{isLimit}$ applied to $F$.

Let $c$ be a cocone of $F$. Let $f$ be a homomorphism of $\operatorname{pt}$ applied to $c$ and $X$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitLiftCocone}$ applied to $c$, $f$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the lift cocone of $c$ and $f$ defined as $\operatorname{isColimitOfReflects}$ applied to $\operatorname{forget}$ applied to $X$ and $\mathrm{hc}$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitToOver}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{toOver}$ applied to $c$ defined as $\operatorname{isColimitOfReflects}$ applied to $\operatorname{forget}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{equivIsoColimit}$ applied to the inverse of $\operatorname{mapCoconeToOver}$ applied to $c$ and $\mathrm{hc}$.

the lift cocone of c and f (from the name)

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

Let $c$ be a cone of $F$. Let $f$ be a homomorphism of $X$ and $\operatorname{pt}$ applied to $c$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitLiftCone}$ applied to $c$, $f$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the lift cone of $c$ and $f$ defined as $\operatorname{isLimitOfReflects}$ applied to $\operatorname{forget}$ applied to $X$ and $\mathrm{hc}$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitToUnder}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{toUnder}$ applied to $c$ defined as $\operatorname{isLimitOfReflects}$ applied to $\operatorname{forget}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{equivIsoLimit}$ applied to the inverse of $\operatorname{mapConeToUnder}$ applied to $c$ and $\mathrm{hc}$.

the lift cone of c and f (from the name)

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

the cocone composition evaluation of c and i (from the name)

Let $c$ be a cocone of $F$. Let $i$ be an element of $I$. Then the cocone composition evaluation of $c$ and $i$ is a cocone of the composition of $F$ and the evaluation of $C$ and $i$.

the cocone of c (from the name)

Let $c$ be a function from elements $i$ of $I$ to cocones of the composition of $F$ and the evaluation of $C$ and $i$. Then the cocone of $i$ is a cocone of $F$.

the cocone of P (from the name)

Let $P$ be a function from elements $i$ of $I$ to elements of $\operatorname{IsColimit}$ applied to $c$ applied to $i$. Then the cocone of $i$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $c$.

the cone composition evaluation of c and i (from the name)

Let $c$ be a cone of $F$. Let $i$ be an element of $I$. Then the cone composition evaluation of $c$ and $i$ is a cone of the composition of $F$ and the evaluation of $C$ and $i$.

the cone of c (from the name)

Let $c$ be a function from elements $i$ of $I$ to cones of the composition of $F$ and the evaluation of $C$ and $i$. Then the cone of $i$ is a cone of $F$.

the cone of P (from the name)

Let $P$ be a function from elements $i$ of $I$ to elements of $\operatorname{IsLimit}$ applied to $c$ applied to $i$. Then the cone of $i$ is an element of $\operatorname{IsLimit}$ applied to the cone of $c$.

the cocone of F and h (from the name)

Let $F$ be a functor of $J$ and $C$ such that $x_{2}$ is an element of the upper bound of the range of $\operatorname{obj}$ applied to $F$. Then the cocone of $F$ and $h$ is a cocone of $F$.

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

Let $F$ be a functor of $J$ and $C$ such that $\mathrm{IsLUB}$ holds for the range of $\operatorname{obj}$ applied to $F$ and $\mathrm{pt}$. Then the colimit cocone of $F$ and $h$ is a colimit cocone of $F$.

the cone of F and h (from the name)

Let $F$ be a functor of $J$ and $C$ such that $x_{2}$ is an element of the lower bound of the range of $\operatorname{obj}$ applied to $F$. Then the cone of $F$ and $h$ is a cone of $F$.

Let $X$ and $Y$ be elements of $C$. Then $\operatorname{isColimitBinaryCofan}$ applied to $X$ and $Y$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the homomorphism of $\mathrm{le\_sup\_left}$ and the homomorphism of $\mathrm{le\_sup\_right}$.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Then $\operatorname{isColimitISup}$ applied to $X$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the supremum of the function that maps $i$ to $X$ applied to $i$ and the function that maps $i_{1}$ to the homomorphism of $\mathrm{le\_iSup}$ applied to $X$ and $i_{1}$.

Let $F$ be a functor of $J$ and $C$. Let $c$ be a cocone of $F$ such that $\mathrm{IsLUB}$ holds for the range of $\operatorname{obj}$ applied to $F$ and $\operatorname{pt}$ applied to $c$. Then $\operatorname{isColimitOfIsLUB}$ applied to $F$, $c$ and $h$ is an element of $\operatorname{IsColimit}$ applied to $c$.

Let $C$ be a set. Then $\operatorname{isInitialBot}$ applied to $C$ is an element of $\operatorname{IsInitial}$ applied to the bottom defined as $\operatorname{ofUnique}$ applied to the bottom.

Let $X$ and $Y$ be elements of $C$. Then $\operatorname{isLimitBinaryFan}$ applied to $X$ and $Y$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the homomorphism of $\mathrm{inf\_le\_left}$ and the homomorphism of $\mathrm{inf\_le\_right}$.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Then $\operatorname{isLimitIInf}$ applied to $X$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the infimum of the function that maps $i$ to $X$ applied to $i$ and the function that maps $i_{1}$ to the homomorphism of $\mathrm{iInf\_le}$ applied to $X$ and $i_{1}$.

Let $F$ be a functor of $J$ and $C$. Let $c$ be a cone of $F$ such that $\mathrm{IsGLB}$ holds for the range of $\operatorname{obj}$ applied to $F$ and $\operatorname{pt}$ applied to $c$. Then $\operatorname{isLimitOfIsGLB}$ applied to $F$, $c$ and $h$ is an element of $\operatorname{IsLimit}$ applied to $c$.

Let $C$ be a set. Then $\operatorname{isTerminalTop}$ applied to $C$ is an element of $\operatorname{IsTerminal}$ applied to the top defined as $\operatorname{ofUnique}$ applied to the top.

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

Let $F$ be a functor of $J$ and $C$ such that $\mathrm{IsGLB}$ holds for the range of $\operatorname{obj}$ applied to $F$ and $\mathrm{pt}$. Then the limit cone of $F$ and $h$ is a limit cone of $F$.

colimit presentation of J and X (from the name)

Let $J$ be a set. Let $X$ be an element of $C$. Then the colimit presentations of $J$ and $X$ are a basic type.

the change diagonal of P and e (from the name)

Let $P$ be a colimit presentation of $J$ and $X$. Let $e$ be an isomorphism of $F$ and the diagram of $P$. Then the change diagonal of $P$ and $e$ is a colimit presentation of $J$ and $X$ defined as $\operatorname{mk}$ applied to $F$, the composition of the homomorphism of $e$ and the inclusion of $P$ and the inverse function of the precomposition homomorphism equivalence of $e$ and $\operatorname{mk}$ applied to $X$ and the inclusion of $P$ and $\operatorname{isColimit}$ applied to $P$.

the cocone of pres (from the name)

Let $\mathrm{pres}$ be a colimit presentation of $J$ and $X$. Then the cocone of $\mathrm{pres}$ is a cocone of the diagram of $\mathrm{pres}$ defined as $\operatorname{mk}$ applied to $X$ and the inclusion of $\mathrm{pres}$.

the colimit of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the colimit of $F$ is a colimit presentation of $J$ and the colimit of $F$ defined as $\operatorname{mk}$ applied to $F$, the inclusion of $\operatorname{proj0}$ applied to $\operatorname{getColimitCocone}$ applied to $F$ and $\operatorname{isColimit}$ applied to $F$.

the diagram of self (from the docstring)

Let $\mathrm{self}$ be a colimit presentation of $J$ and $X$. Then the diagram of $\mathrm{self}$ is a functor of $J$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a colimit presentation of $J$ and $X$. Then $\operatorname{isColimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $X$ and the inclusion of $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the map of P and F (from the name)

Let $P$ be a colimit presentation of $J$ and $X$. Let $F$ be a functor of $C$ and $D$. Then the map of $P$ and $F$ is a colimit presentation of $J$ and the action of $F$ and $X$.

the colimit presentation of P and e (from the name)

Let $P$ be a colimit presentation of $J$ and $X$. Let $e$ be an isomorphism of $X$ and $Y$. Then the colimit presentation of $P$ and $e$ is a colimit presentation of $J$ and $Y$.

the reindexing of P and F (from the name)

Let $P$ be a colimit presentation of $J$ and $X$. Let $F$ be a functor of $\mathrm{J'}$ and $J$. Then the reindexing of $P$ and $F$ is a colimit presentation of $\mathrm{J'}$ and $X$ defined as $\operatorname{mk}$ applied to the composition of $F$ and the diagram of $P$, the left whisker of $F$ and the inclusion of $P$ and $\operatorname{symm}$ applied to $\operatorname{isColimitWhiskerEquiv}$ applied to $F$ and $\operatorname{mk}$ applied to $X$ and the inclusion of $P$ and $\operatorname{isColimit}$ applied to $P$.

the self of X (from the name)

Let $X$ be an element of $C$. Then the self of $X$ is a colimit presentation of $\mathrm{PUnit}$ and $X$ defined as $\operatorname{mk}$ applied to the action of the constant of $\mathrm{PUnit}$ and $X$, the identity morphism of the action of the constant of $\mathrm{PUnit}$ and $X$ and $\operatorname{isColimitConstCocone}$ applied to $\mathrm{PUnit}$ and $X$.

the inclusion of self (from the name)

Let $\mathrm{self}$ be a colimit presentation of $J$ and $X$. Then the inclusion of $\mathrm{self}$ is a homomorphism of the diagram of $\mathrm{self}$ and the action of the constant of $J$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

limit presentation of J and X (from the name)

Let $J$ be a set. Let $X$ be an element of $C$. Then the limit presentations of $J$ and $X$ are a basic type.

the change diagonal of P and e (from the name)

Let $P$ be a limit presentation of $J$ and $X$. Let $e$ be an isomorphism of $F$ and the diagram of $P$. Then the change diagonal of $P$ and $e$ is a limit presentation of $J$ and $X$ defined as $\operatorname{mk}$ applied to $F$, the composition of the projection of $P$ and the inverse of $e$ and the inverse function of the postcomposition homomorphism equivalence of the inverse of $e$ and $\operatorname{mk}$ applied to $X$ and the projection of $P$ and $\operatorname{isLimit}$ applied to $P$.

the cone of pres (from the name)

Let $\mathrm{pres}$ be a limit presentation of $J$ and $X$. Then the cone of $\mathrm{pres}$ is a cone of the diagram of $\mathrm{pres}$ defined as $\operatorname{mk}$ applied to $X$ and the projection of $\mathrm{pres}$.

the diagram of self (from the docstring)

Let $\mathrm{self}$ be a limit presentation of $J$ and $X$. Then the diagram of $\mathrm{self}$ is a functor of $J$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a limit presentation of $J$ and $X$. Then $\operatorname{isLimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $X$ and the projection of $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the limit of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the limit of $F$ is a limit presentation of $J$ and the limit of $F$ defined as $\operatorname{mk}$ applied to $F$, the projection of $\operatorname{proj0}$ applied to $\operatorname{getLimitCone}$ applied to $F$ and $\operatorname{isLimit}$ applied to $F$.

the map of P and F (from the name)

Let $P$ be a limit presentation of $J$ and $X$. Let $F$ be a functor of $C$ and $D$. Then the map of $P$ and $F$ is a limit presentation of $J$ and the action of $F$ and $X$.

the limit presentation of P and e (from the name)

Let $P$ be a limit presentation of $J$ and $X$. Let $e$ be an isomorphism of $X$ and $Y$. Then the limit presentation of $P$ and $e$ is a limit presentation of $J$ and $Y$.

the reindexing of P and F (from the name)

Let $P$ be a limit presentation of $J$ and $X$. Let $F$ be a functor of $\mathrm{J'}$ and $J$. Then the reindexing of $P$ and $F$ is a limit presentation of $\mathrm{J'}$ and $X$ defined as $\operatorname{mk}$ applied to the composition of $F$ and the diagram of $P$, the left whisker of $F$ and the projection of $P$ and $\operatorname{symm}$ applied to $\operatorname{isLimitWhiskerEquiv}$ applied to $F$ and $\operatorname{mk}$ applied to $X$ and the projection of $P$ and $\operatorname{isLimit}$ applied to $P$.

the self of X (from the name)

Let $X$ be an element of $C$. Then the self of $X$ is a limit presentation of $\mathrm{PUnit}$ and $X$ defined as $\operatorname{mk}$ applied to the action of the constant of $\mathrm{PUnit}$ and $X$, the identity morphism of the action of the constant of $\mathrm{PUnit}$ and $X$ and $\operatorname{isLimitConstCone}$ applied to $\mathrm{PUnit}$ and $X$.

the projection of self (from the name)

Let $\mathrm{self}$ be a limit presentation of $J$ and $X$. Then the projection of $\mathrm{self}$ is a homomorphism of the action of the constant of $J$ and $X$ and the diagram of $\mathrm{self}$ 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$. Then we can say that $\operatorname{PreservesColimit}$ holds for $K$ and $F$.

F preserves colimits (from the name)

Let $F$ be a functor of $C$ and $D$. Then $F$ preserves colimits, if $\operatorname{PreservesColimitsOfSize}$ holds for $F$.

F preserves 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$ preserves colimits of shapes.

Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{PreservesColimitsOfSize}$ 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{PreservesLimit}$ holds for $K$ and $F$.

F preserves limits (from the name)

Let $F$ be a functor of $C$ and $D$. Then $F$ preserves limits, if $\operatorname{PreservesLimitsOfSize}$ holds for $F$.

F preserves 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$ preserves limits of shapes.

Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{PreservesLimitsOfSize}$ 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{ReflectsColimit}$ holds for $K$ and $F$.

F reflects colimits (from the name)

Let $F$ be a functor of $C$ and $D$. Then $F$ reflects colimits, if $\operatorname{ReflectsColimitsOfSize}$ holds for $F$.

F reflects 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$ reflects colimits of shapes.

Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{ReflectsColimitsOfSize}$ 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{ReflectsLimit}$ holds for $K$ and $F$.

F reflects limits (from the name)

Let $F$ be a functor of $C$ and $D$. Then $F$ reflects limits, if $\operatorname{ReflectsLimitsOfSize}$ holds for $F$.

F reflects 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$ reflects limits of shapes.

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

Let $F$ be a functor of $C$ and $D$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitOfPreserves}$ applied to $F$ and $t$ is an element of $\operatorname{IsColimit}$ applied to the map cocone of $F$ and $c$ defined as $\operatorname{some}$ applied to $\operatorname{preserves}$ applied to $t$.

Let $F$ be a functor of $C$ and $D$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of $F$ and $c$. Then $\operatorname{isColimitOfReflects}$ applied to $F$ and $t$ is an element of $\operatorname{IsColimit}$ applied to $c$ defined as $\operatorname{some}$ applied to $\operatorname{reflects}$ applied to $t$.

Let $F$ be a functor of $C$ and $D$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitOfPreserves}$ applied to $F$ and $t$ is an element of $\operatorname{IsLimit}$ applied to the map cone of $F$ and $c$ defined as $\operatorname{some}$ applied to $\operatorname{preserves}$ applied to $t$.

Let $F$ be a functor of $C$ and $D$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to the map cone of $F$ and $c$. Then $\operatorname{isLimitOfReflects}$ applied to $F$ and $t$ is an element of $\operatorname{IsLimit}$ applied to $c$ defined as $\operatorname{some}$ applied to $\operatorname{reflects}$ applied to $t$.

the map cocone of x11 and x12 (from the name)

Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and $C$. Let $x_{11}$ be a cocone of $x_{9}$. Let $x_{12}$ be a cocone of $x_{10}$. Then the map cocone of $x_{11}$ and $x_{12}$ is a cocone of the action of $\operatorname{uncurry}$ and the action of the action of the action of the left whiskering of $C$ and $x_{9}$ and $x_{10}$ and $G$.

the map cone of x11 and x12 (from the name)

Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and $C$. Let $x_{11}$ be a cone of $x_{9}$. Let $x_{12}$ be a cone of $x_{10}$. Then the map cone of $x_{11}$ and $x_{12}$ is a cone of the action of $\operatorname{uncurry}$ and the action of the action of the action of the left whiskering of $C$ and $x_{9}$ and $x_{10}$ and $G$.

Let $x_{9}$ be a functor of $x$ and $x_{4}$. Let $x_{10}$ be a functor of $x_{1}$ and $x_{5}$. Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and $C$. Then we can say that $\mathrm{CategoryTheory\_\_Limits\_\_PreservesColimit\_u2082\_}$ holds for $x_{9}$, $x_{10}$ and $G$.

the left isomorphism colimit uncurrying whiskering of x10 and G (from the name)

Let $x_{9}$ be a functor of $x$ and $x_{4}$. Let $x_{10}$ be a functor of $x_{1}$ and $x_{5}$. Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and $C$. Then the left isomorphism colimit uncurrying whiskering of $x_{10}$ and $G$ is an isomorphism of the colimit of the action of $\operatorname{uncurry}$ and the action of the action of the action of the left whiskering of $C$ and $x_{9}$ and $x_{10}$ and $G$ and the action of the action of $G$ and the colimit of $x_{9}$ and the colimit of $x_{10}$ defined as the inverse of the isomorphism object cocone point of $\operatorname{isColimit}$ applied to $x_{10}$ and $\operatorname{isColimit}$ applied to the action of $\operatorname{uncurry}$ and the action of the action of the action of the left whiskering of $C$ and $x_{9}$ and $x_{10}$ and $G$.

the isomorphism object cocone point of x14 and x16 (from the name)

Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and $C$. Let $x_{12}$ be an element of $\operatorname{IsColimit}$ applied to $x_{11}$. Let $x_{14}$ be an element of $\operatorname{IsColimit}$ applied to $x_{13}$. Let $x_{16}$ be an element of $\operatorname{IsColimit}$ applied to $x_{15}$. Then the isomorphism object cocone point of $x_{14}$ and $x_{16}$ is an isomorphism of the action of the action of $G$ and $\operatorname{pt}$ applied to $x_{11}$ and $\operatorname{pt}$ applied to $x_{13}$ and $\operatorname{pt}$ applied to $x_{15}$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_isColimitOfPreserves\_u2082\_}$ applied to $G$, $x_{12}$ and $x_{14}$ and $x_{16}$.

Let $x_{9}$ be a functor of $x$ and $x_{4}$. Let $x_{10}$ be a functor of $x_{1}$ and $x_{5}$. Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and $C$. Then we can say that $\mathrm{CategoryTheory\_\_Limits\_\_PreservesLimit\_u2082\_}$ holds for $x_{9}$, $x_{10}$ and $G$.

the left isomorphism limit uncurrying whiskering of x10 and G (from the name)

Let $x_{9}$ be a functor of $x$ and $x_{4}$. Let $x_{10}$ be a functor of $x_{1}$ and $x_{5}$. Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and $C$. Then the left isomorphism limit uncurrying whiskering of $x_{10}$ and $G$ is an isomorphism of the limit of the action of $\operatorname{uncurry}$ and the action of the action of the action of the left whiskering of $C$ and $x_{9}$ and $x_{10}$ and $G$ and the action of the action of $G$ and the limit of $x_{9}$ and the limit of $x_{10}$ defined as the inverse of the isomorphism object cone point of $\operatorname{isLimit}$ applied to $x_{10}$ and $\operatorname{isLimit}$ applied to the action of $\operatorname{uncurry}$ and the action of the action of the action of the left whiskering of $C$ and $x_{9}$ and $x_{10}$ and $G$.

the isomorphism object cone point of x14 and x16 (from the name)

Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and $C$. Let $x_{12}$ be an element of $\operatorname{IsLimit}$ applied to $x_{11}$. Let $x_{14}$ be an element of $\operatorname{IsLimit}$ applied to $x_{13}$. Let $x_{16}$ be an element of $\operatorname{IsLimit}$ applied to $x_{15}$. Then the isomorphism object cone point of $x_{14}$ and $x_{16}$ is an isomorphism of the action of the action of $G$ and $\operatorname{pt}$ applied to $x_{11}$ and $\operatorname{pt}$ applied to $x_{13}$ and $\operatorname{pt}$ applied to $x_{15}$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_isLimitOfPreserves\_u2082\_}$ applied to $G$, $x_{12}$ and $x_{14}$ and $x_{16}$.

Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and $C$. Let $x_{12}$ be an element of $\operatorname{IsColimit}$ applied to $x_{11}$. Let $x_{14}$ be an element of $\operatorname{IsColimit}$ applied to $x_{13}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_isColimitOfPreserves\_u2082\_}$ applied to $G$, $x_{12}$ and $x_{14}$ is an element of $\operatorname{IsColimit}$ applied to the map cocone of $x_{11}$ and $x_{13}$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_PreservesColimit\_u2082\_\_\_nonempty\_isColimit\_mapCocone\_u2082\_}$ applied to $x_{12}$ and $x_{14}$.

Let $G$ be a functor of $x_{4}$ and the set of functors of $x_{5}$ and $C$. Let $x_{12}$ be an element of $\operatorname{IsLimit}$ applied to $x_{11}$. Let $x_{14}$ be an element of $\operatorname{IsLimit}$ applied to $x_{13}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_isLimitOfPreserves\_u2082\_}$ applied to $G$, $x_{12}$ and $x_{14}$ is an element of $\operatorname{IsLimit}$ applied to the map cone of $x_{11}$ and $x_{13}$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_PreservesLimit\_u2082\_\_\_nonempty\_isLimit\_mapCone\_u2082\_}$ applied to $x_{12}$ and $x_{14}$.

Let $x_{12}$ be an element of $\operatorname{IsColimit}$ applied to $x_{11}$. Let $x_{17}$ be an element of $\operatorname{IsColimit}$ applied to $x_{16}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $C$. Then $\operatorname{isColimitMapBifunctor}$ applied to $x_{12}$, $x_{17}$ and $F$ is an element of $\operatorname{IsColimit}$ applied to the map bifunctor of $x_{16}$ and $F$.

the map bifunctor of x15 and F (from the name)

Let $x_{11}$ be a cokernel cofork of $x_{10}$. Let $x_{15}$ be a cokernel cofork of $x_{14}$. Let $F$ be a functor of $x$ and the set of functors of $x_{1}$ and $C$. Then the map bifunctor of $x_{15}$ and $F$ is a cokernel cofork of $\operatorname{desc}$ applied to the component of the map of $F$ and $x_{10}$ and $x_{13}$ and the map of the action of $F$ and $x_{9}$ and $x_{14}$.

F creates finite colimits (from the name)

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

F creates finite coproducts (from the name)

Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ creates finite coproducts.

F creates finite limits (from the name)

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

F creates finite products (from the name)

Let $F$ be a functor of $C$ and $D$. Then we can say that $F$ creates finite products.

F preserves cofiltered limits (from the name)

Let $F$ be a functor of $C$ and $D$. Then $F$ preserves cofiltered limits, if $\operatorname{PreservesCofilteredLimitsOfSize}$ holds for $F$.

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

F preserves filtered colimits (from the name)

Let $F$ be a functor of $C$ and $D$. Then $F$ preserves filtered colimits, if $\operatorname{PreservesFilteredColimitsOfSize}$ holds for $F$.

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

F reflects cofiltered limits (from the name)

Let $F$ be a functor of $C$ and $D$. Then $F$ reflects cofiltered limits, if $\operatorname{ReflectsCofilteredLimitsOfSize}$ holds for $F$.

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

F reflects filtered colimits (from the name)

Let $F$ be a functor of $C$ and $D$. Then $F$ reflects filtered colimits, if $\operatorname{ReflectsFilteredColimitsOfSize}$ holds for $F$.

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

F preserves finite colimits (from the name)

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

F preserves finite coproducts (from the name)

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

F preserves finite limits (from the name)

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

F preserves finite products (from the name)

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

F reflects finite colimits (from the name)

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

F reflects finite coproducts (from the name)

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

F reflects finite limits (from the name)

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

F reflects finite products (from the name)

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

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

Let $F$ be a functor of $D$ and $E$. Let $G$ be a functor of $J$ and the set of functors of $C$ and $D$. Then the colimit composition whiskering right isomorphism colimit composition of $F$ and $G$ is an isomorphism of the colimit of the composition of $G$ and the action of the right whiskering of $D$ and $E$ and $F$ and the composition of the colimit of $G$ and $F$ defined as the inverse of $\operatorname{preservesColimitIso}$ applied to the action of the right whiskering of $D$ and $E$ and $F$ and $G$.

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

Let $F$ be a functor of $D$ and $E$. Let $G$ be a functor of $J$ and the set of functors of $C$ and $D$. Then the limit composition whiskering right isomorphism limit composition of $F$ and $G$ is an isomorphism of the limit of the composition of $G$ and the action of the right whiskering of $D$ and $E$ and $F$ and the composition of the limit of $G$ and $F$ defined as the inverse of $\operatorname{preservesLimitIso}$ applied to the action of the right whiskering of $D$ and $E$ and $F$ and $G$.

the fiberwise colimit limit isomorphism of K (from the name)

Let $K$ be a functor of $J$ and the set of functors of $\operatorname{Grothendieck}$ applied to $F$ and $H$. Then the fiberwise colimit limit isomorphism of $K$ is an isomorphism of the fiberwise colimit of the limit of $K$ and the limit of the composition of $K$ and the fiberwise colimit of $F$ and $H$.

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

Let $G$ be a functor of $C$ and $D$. Then $\operatorname{preservesColimitNatIso}$ applied to $G$ is an isomorphism of the composition of the colimit and $G$ and the composition of the action of the right whiskering of $C$ and $D$ and $G$ and the colimit.

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

Let $G$ be a functor of $C$ and $D$. Then $\operatorname{preservesLimitNatIso}$ applied to $G$ is an isomorphism of the composition of the limit and $G$ and the composition of the action of the right whiskering of $C$ and $D$ and $G$ and the limit.

the flip functor to interchange of A and K (from the name)

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Let $K$ be a functor of $J$ and the set of opposites of $C$. Then the flip functor to interchange of $A$ and $K$ is an isomorphism of the flip of the functor to interchange of $A$ and $K$ and the composition of the composition of the projection of the Yoneda and $A$ and the Yoneda and the action of the left whiskering of the set of opposites of $C$ and the set of sets and $K$ defined as the identity of the flip of the functor to interchange of $A$ and $K$.

the functor to interchange of A and K (from the name)

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Let $K$ be a functor of $J$ and the set of opposites of $C$. Then the functor to interchange of $A$ and $K$ is a functor of $J$ and the set of functors of the set of costructured arrows of the Yoneda and $A$ and the set of sets defined as the composition of $K$ and the composition of the Coyoneda and the action of the left whiskering of $C$ and the set of sets and the projection of the Yoneda and $A$.

the functor to interchange isomorphism of A and K (from the name)

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Let $K$ be a functor of $J$ and the set of opposites of $C$. Then the functor to interchange isomorphism of $A$ and $K$ is an isomorphism of the functor to interchange of $A$ and $K$ and the composition of $K$ and the composition of the Coyoneda and the action of the left whiskering of $C$ and the set of sets and the projection of the Yoneda and $A$ defined as the identity of the functor to interchange of $A$ and $K$.

the isomorphism of A and K (from the name)

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Let $K$ be a functor of $J$ and the set of opposites of $C$. Then the isomorphism of $A$ and $K$ is an isomorphism of the action of $A$ and the limit of $K$ and the limit of the composition of $K$ and $A$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the application of $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimitTautologicalCocone}$ applied to $A$ and $\operatorname{isColimit}$ applied to the composition of the projection of the Yoneda and $A$ and the Yoneda and the limit of $K$ and the colimit object isomorphism colimit composition evaluation of the composition of the projection of the Yoneda and $A$ and the Yoneda and the limit of $K$ and the isomorphism of the associator of the Yoneda and the action of the evaluation of the set of opposites of $C$ and the set of sets and the limit of $K$ and the isomorphism of $\operatorname{isoAux}$ applied to $A$ and $K$ and the isomorphism of $\operatorname{preservesLimitIso}$ applied to the composition of the Coyoneda and the action of the left whiskering of $C$ and the set of sets and the projection of the Yoneda and $A$ and $K$ and the isomorphism of the isomorphism of the inverse of the functor to interchange isomorphism of $A$ and $K$ and the colimit limit isomorphism of the functor to interchange of $A$ and $K$ and the isomorphism of the isomorphism of the flip functor to interchange of $A$ and $K$ and the isomorphism of the colimit composition whiskering left isomorphism composition colimit of the composition of the projection of the Yoneda and $A$ and the Yoneda and $K$ and the isomorphism of the left isomorphism whisker of $K$ and $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the composition of the projection of the Yoneda and $A$ and the Yoneda and $\operatorname{isColimitTautologicalCocone}$ applied to $A$.

the isomorphism of F and f (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the isomorphism of $F$ and $f$ is an isomorphism of the action of $F$ and the coimage of $f$ and the coimage of the map of $F$ and $f$.

the isomorphism of F and f (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the isomorphism of $F$ and $f$ is an isomorphism of $\operatorname{mk}$ applied to the map of $F$ and the canonical map from the abelian coimage to the abelian image of $f$ and $\operatorname{mk}$ applied to the canonical map from the abelian coimage to the abelian image of the map of $F$ and $f$ defined as the isomorphism of the isomorphism of $F$ and $f$ and the isomorphism of $F$ and $f$.

the isomorphism of F and f (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the isomorphism of $F$ and $f$ is an isomorphism of the action of $F$ and the image of $f$ and the image of the map of $F$ and $f$.

the isomorphism of X and Y (from the name)

Let $G$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then the isomorphism of $X$ and $Y$ is an isomorphism of the coproduct of the action of $G$ and $X$ and the action of $G$ and $Y$ and the action of $G$ and the coproduct of $X$ and $Y$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the pair of the action of $G$ and $X$ and the action of $G$ and $Y$ and $\operatorname{isColimitOfHasBinaryCoproductOfPreservesColimit}$ applied to $G$, $X$ and $Y$.

the isomorphism of X and Y (from the name)

Let $G$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then the isomorphism of $X$ and $Y$ is an isomorphism of the action of $G$ and the product of $X$ and $Y$ and the product of the action of $G$ and $X$ and the action of $G$ and $Y$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimitOfHasBinaryProductOfPreservesLimit}$ applied to $G$, $X$ and $Y$ and $\operatorname{isLimit}$ applied to the pair of the action of $G$ and $X$ and the action of $G$ and $Y$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $P$. Let $g$ be a homomorphism of $Y$ and $P$. Then $\operatorname{isColimitMapCoconeBinaryCofanEquiv}$ applied to $G$, $f$ and $g$ is an equivalence from $\operatorname{IsColimit}$ applied to the map cocone of $G$ and $\operatorname{mk}$ applied to $f$ and $g$ to $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $f$ and the map of $G$ and $g$.

Let $G$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then $\operatorname{isColimitOfHasBinaryCoproductOfPreservesColimit}$ applied to $G$, $X$ and $Y$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and the left injection and the map of $G$ and the right injection defined as $\operatorname{mapIsColimitOfPreservesOfIsColimit}$ applied to $G$, the left injection, the right injection and $\operatorname{coprodIsCoprod}$ applied to $X$ and $Y$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $P$. Let $g$ be a homomorphism of $Y$ and $P$. Let $l$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $f$ and the map of $G$ and $g$. Then $\operatorname{isColimitOfReflectsOfMapIsColimit}$ applied to $G$, $f$, $g$ and $l$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $f$ and $g$ defined as $\operatorname{isColimitOfReflects}$ applied to $G$ and $\operatorname{symm}$ applied to $\operatorname{isColimitMapCoconeBinaryCofanEquiv}$ applied to $G$, $f$ and $g$ and $l$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $P$ and $X$. Let $g$ be a homomorphism of $P$ and $Y$. Then $\operatorname{isLimitMapConeBinaryFanEquiv}$ applied to $G$, $f$ and $g$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $G$ and $\operatorname{mk}$ applied to $f$ and $g$ to $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $f$ and the map of $G$ and $g$.

Let $G$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then $\operatorname{isLimitOfHasBinaryProductOfPreservesLimit}$ applied to $G$, $X$ and $Y$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and the projection map to the first component of the product and the map of $G$ and the projection map to the second component of the product defined as $\operatorname{mapIsLimitOfPreservesOfIsLimit}$ applied to $G$, the projection map to the first component of the product, the projection map to the second component of the product and $\operatorname{prodIsProd}$ applied to $X$ and $Y$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $P$ and $X$. Let $g$ be a homomorphism of $P$ and $Y$. Let $l$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $f$ and the map of $G$ and $g$. Then $\operatorname{isLimitOfReflectsOfMapIsLimit}$ applied to $G$, $f$, $g$ and $l$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $f$ and $g$ defined as $\operatorname{isLimitOfReflects}$ applied to $G$ and $\operatorname{symm}$ applied to $\operatorname{isLimitMapConeBinaryFanEquiv}$ applied to $G$, $f$ and $g$ and $l$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $P$. Let $g$ be a homomorphism of $Y$ and $P$. Let $l$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $f$ and $g$. Then $\operatorname{mapIsColimitOfPreservesOfIsColimit}$ applied to $G$, $f$, $g$ and $l$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $f$ and the map of $G$ and $g$ defined as $\operatorname{isColimitMapCoconeBinaryCofanEquiv}$ applied to $G$, $f$, $g$ and $\operatorname{isColimitOfPreserves}$ applied to $G$ and $l$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $P$ and $X$. Let $g$ be a homomorphism of $P$ and $Y$. Let $l$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $f$ and $g$. Then $\operatorname{mapIsLimitOfPreservesOfIsLimit}$ applied to $G$, $f$, $g$ and $l$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $f$ and the map of $G$ and $g$ defined as $\operatorname{isLimitMapConeBinaryFanEquiv}$ applied to $G$, $f$, $g$ and $\operatorname{isLimitOfPreserves}$ applied to $G$ and $l$.