Definitions: Mathlib.CategoryTheory, part 11 of 25

the biproduct comparison of X and Y (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then the biproduct comparison of $X$ and $Y$ is a homomorphism of the action of $F$ and the biproduct of $X$ and $Y$ and the biproduct of the action of $F$ and $X$ and the action of $F$ and $Y$ defined as the lift of the map of $F$ and the projection onto the first summand and the map of $F$ and the projection onto the second summand.

the biproduct comparison of X and Y (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then the biproduct comparison of $X$ and $Y$ is a homomorphism of the biproduct of the action of $F$ and $X$ and the action of $F$ and $Y$ and the action of $F$ and the biproduct of $X$ and $Y$ defined as $\operatorname{desc}$ applied to the map of $F$ and the left injection and the map of $F$ and the right injection.

the biproduct comparison of F and f (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Then the biproduct comparison of $F$ and $f$ is a homomorphism of the action of $F$ and the biproduct of $f$ and the biproduct of $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to $F$ and $f$ defined as the lift of the function that maps $j$ to the map of $F$ and the projection onto a summand of $f$ and $j$.

the biproduct comparison of F and f (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Then the biproduct comparison of $F$ and $f$ is a homomorphism of the biproduct of $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to $F$ and $f$ and the action of $F$ and the biproduct of $f$ defined as $\operatorname{desc}$ applied to the function that maps $j$ to the map of $F$ and the inclusion into a summand of $f$ and $j$.

the image of F and b (from the docstring)

Let $F$ be a functor of $C$ and $D$. Let $b$ be a bicone of $f$. Then the image of $F$ and $b$ is a bicone of $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to $F$ and $f$.

the image of F and b (from the docstring)

Let $F$ be a functor of $C$ and $D$. Let $b$ be a binary bicone of $X$ and $Y$. Then the image of $F$ and $b$ is a binary bicone of the action of $F$ and $X$ and the action of $F$ and $Y$ defined as the action of the functoriality of $Y$ and $F$ and $b$.

the map biproduct of X and Y (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then the map biproduct of $X$ and $Y$ is an isomorphism of the action of $F$ and the biproduct of $X$ and $Y$ and the biproduct of the action of $F$ and $X$ and the action of $F$ and $Y$ defined as $\operatorname{uniqueUpToIso}$ applied to the action of $F$ and $X$, the action of $F$ and $Y$ and $\operatorname{isBinaryBilimitOfPreserves}$ applied to $F$ and $\operatorname{isBilimit}$ applied to $X$ and $Y$.

the map biproduct of F and f (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Then the map biproduct of $F$ and $f$ is an isomorphism of the action of $F$ and the biproduct of $f$ and the biproduct of $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to $F$ and $f$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to $F$ and $f$ and $\operatorname{isBilimitOfPreserves}$ applied to $F$ and the bilimit bicone of $f$.

the split epimorphism biproduct comparison of X and Y (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then the split epimorphism biproduct comparison of $X$ and $Y$ is a split epimorphism of the biproduct comparison of $X$ and $Y$.

the split epimorphism of F and f (from the docstring)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Then the split epimorphism of $F$ and $f$ is a split epimorphism of the biproduct comparison of $F$ and $f$.

the split monomorphism biproduct comparison of X and Y (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then the split monomorphism biproduct comparison of $X$ and $Y$ is a split monomorphism of the biproduct comparison of $X$ and $Y$.

the split monomorphism of F and f (from the docstring)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Then the split monomorphism of $F$ and $f$ is a split monomorphism of the biproduct comparison of $F$ and $f$.

Let $X$ and $Y$ be elements of $C$. Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{PreservesBinaryBiproduct}$ holds for $X$, $Y$ and $F$.

F preserves binary biproducts (from the name)

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

Let $f$ be a function from elements of $J$ to elements of $C$. Let $F$ be a functor of $C$ and $D$. Then we can say that $\operatorname{PreservesBiproduct}$ holds for $f$ and $F$.

F preserves biproducts (from the name)

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

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

F preserves finite biproducts (from the name)

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

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hb}$ be an element of $\operatorname{IsBilimit}$ applied to $b$. Then $\operatorname{isBilimitOfPreserves}$ applied to $F$ and $\mathrm{hb}$ is an element of $\operatorname{IsBilimit}$ applied to the image of $F$ and $b$ defined as $\operatorname{some}$ applied to $\operatorname{preserves}$ applied to $\mathrm{hb}$.

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hb}$ be an element of $\operatorname{IsBilimit}$ applied to $b$. Then $\operatorname{isBinaryBilimitOfPreserves}$ applied to $F$ and $\mathrm{hb}$ is an element of $\operatorname{IsBilimit}$ applied to the image of $F$ and $b$ defined as $\operatorname{some}$ applied to $\operatorname{preserves}$ applied to $\mathrm{hb}$.

the isomorphism of f and g (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the isomorphism of $f$ and $g$ is an isomorphism of the coequalizer of the map of $G$ and $f$ and the map of $G$ and $g$ and the action of $G$ and the coequalizer of $f$ and $g$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the parallel pair of the map of $G$ and $f$ and the map of $G$ and $g$ and $\operatorname{isColimitOfHasCoequalizerOfPreservesColimit}$ applied to $G$, $f$ and $g$.

the isomorphism of f and g (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the isomorphism of $f$ and $g$ is an isomorphism of the action of $G$ and the equalizer of $f$ and $g$ and the equalizer of the map of $G$ and $f$ and the map of $G$ and $g$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimitOfHasEqualizerOfPreservesLimit}$ applied to $G$, $f$ and $g$ and $\operatorname{isLimit}$ applied to the parallel pair of the map of $G$ and $f$ and the map of $G$ and $g$.

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $f$ and $h$ is equal to the composition of $g$ and $h$. Let $l$ be an element of $\operatorname{IsColimit}$ applied to the projection of $h$ and $w$. Then $\operatorname{isColimitCoforkMapOfIsColimit}$ applied to $G$, $w$ and $l$ is an element of $\operatorname{IsColimit}$ applied to the projection of the map of $G$ and $h$ and $\mathrm{CategoryTheory\_\_Limits\_\_isColimitMapCoconeCoforkEquiv\_\_\_proof\_1}$ applied to $G$ and $w$ defined as $\operatorname{isColimitMapCoconeCoforkEquiv}$ applied to $G$, $w$ and $\operatorname{isColimitOfPreserves}$ applied to $G$ and $l$.

the map of G and w (from the docstring)

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $f$ and $h$ is equal to the composition of $g$ and $h$. Then the map of $G$ and $w$ is an equivalence from $\operatorname{IsColimit}$ applied to the map cocone of $G$ and the projection of $h$ and $w$ to $\operatorname{IsColimit}$ applied to the projection of the map of $G$ and $h$ and $\mathrm{CategoryTheory\_\_Limits\_\_isColimitMapCoconeCoforkEquiv\_\_\_proof\_1}$ applied to $G$ and $w$.

Let $G$ be a functor of $C$ and $D$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then $\operatorname{isColimitOfHasCoequalizerOfPreservesColimit}$ applied to $G$, $f$ and $g$ is an element of $\operatorname{IsColimit}$ applied to the projection of the map of $G$ and the projection of $f$ and $g$ and $\mathrm{CategoryTheory\_\_Limits\_\_isColimitOfHasCoequalizerOfPreservesColimit\_\_\_proof\_1}$ applied to $G$, $f$ and $g$ defined as $\operatorname{isColimitCoforkMapOfIsColimit}$ applied to $G$, $\operatorname{condition}$ applied to $f$ and $g$ and $\operatorname{coequalizerIsCoequalizer}$ applied to $f$ and $g$.

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $f$ and $h$ is equal to the composition of $g$ and $h$. Let $l$ be an element of $\operatorname{IsColimit}$ applied to the projection of the map of $G$ and $h$ and $\mathrm{CategoryTheory\_\_Limits\_\_isColimitMapCoconeCoforkEquiv\_\_\_proof\_1}$ applied to $G$ and $w$. Then $\operatorname{isColimitOfIsColimitCoforkMap}$ applied to $G$, $w$ and $l$ is an element of $\operatorname{IsColimit}$ applied to the projection of $h$ and $w$ defined as $\operatorname{isColimitOfReflects}$ applied to $G$ and $\operatorname{symm}$ applied to the map of $G$ and $w$ and $l$.

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $h$ and $f$ is equal to the composition of $h$ and $g$. Let $l$ be an element of $\operatorname{IsLimit}$ applied to the inclusion of $h$ and $w$. Then $\operatorname{isLimitForkMapOfIsLimit}$ applied to $G$, $w$ and $l$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the map of $G$ and $h$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitMapConeForkEquiv\_\_\_proof\_1}$ applied to $G$ and $w$ defined as $\operatorname{isLimitMapConeForkEquiv}$ applied to $G$, $w$ and $\operatorname{isLimitOfPreserves}$ applied to $G$ and $l$.

the map of G and w (from the docstring)

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $h$ and $f$ is equal to the composition of $h$ and $g$. Then the map of $G$ and $w$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $G$ and the inclusion of $h$ and $w$ to $\operatorname{IsLimit}$ applied to the inclusion of the map of $G$ and $h$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitMapConeForkEquiv\_\_\_proof\_1}$ applied to $G$ and $w$.

Let $G$ be a functor of $C$ and $D$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then $\operatorname{isLimitOfHasEqualizerOfPreservesLimit}$ applied to $G$, $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the map of $G$ and the inclusion of $f$ and $g$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitOfHasEqualizerOfPreservesLimit\_\_\_proof\_1}$ applied to $G$, $f$ and $g$ defined as $\operatorname{isLimitForkMapOfIsLimit}$ applied to $G$, $\operatorname{condition}$ applied to $f$ and $g$ and $\operatorname{equalizerIsEqualizer}$ applied to $f$ and $g$.

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $h$ and $f$ is equal to the composition of $h$ and $g$. Let $l$ be an element of $\operatorname{IsLimit}$ applied to the inclusion of the map of $G$ and $h$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitMapConeForkEquiv\_\_\_proof\_1}$ applied to $G$ and $w$. Then $\operatorname{isLimitOfIsLimitForkMap}$ applied to $G$, $w$ and $l$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $h$ and $w$ defined as $\operatorname{isLimitOfReflects}$ applied to $G$ and $\operatorname{symm}$ applied to the map of $G$ and $w$ and $l$.

the isomorphism of L and f (from the name)

Let $L$ be a functor of $A$ and $B$. Let $f$ be a homomorphism of $X$ and $Y$. Then the isomorphism of $L$ and $f$ is an isomorphism of the categorical image of the map of $L$ and $f$ and the action of $L$ and the categorical image of $f$.

the underlying cocone of c and G (from the docstring)

Let $c$ be a cokernel cofork of $f$. Let $G$ be a functor of $C$ and $D$. Then the underlying cocone of $c$ and $G$ is an equivalence from $\operatorname{IsColimit}$ applied to the map cocone of $G$ and $c$ to $\operatorname{IsColimit}$ applied to the map of $c$ and $G$.

the map of c and G (from the name)

Let $c$ be a cokernel cofork of $f$. Let $G$ be a functor of $C$ and $D$. Then the map of $c$ and $G$ is a cokernel cofork of the map of $G$ and $f$ defined as the projection of the map of $G$ and the projection of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_CokernelCofork\_\_map\_condition}$ applied to $c$ and $G$.

Let $c$ be a cokernel cofork of $f$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $G$ be a functor of $C$ and $D$. Then $\operatorname{mapIsColimit}$ applied to $c$, $\mathrm{hc}$ and $G$ is an element of $\operatorname{IsColimit}$ applied to the map of $c$ and $G$ defined as $\operatorname{isColimitMapCoconeEquiv}$ applied to $c$, $G$ and $\operatorname{isColimitOfPreserves}$ applied to $G$ and $\mathrm{hc}$.

the underlying cone of c and G (from the docstring)

Let $c$ be a kernel fork of $f$. Let $G$ be a functor of $C$ and $D$. Then the underlying cone of $c$ and $G$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $G$ and $c$ to $\operatorname{IsLimit}$ applied to the map of $c$ and $G$.

the map of c and G (from the name)

Let $c$ be a kernel fork of $f$. Let $G$ be a functor of $C$ and $D$. Then the map of $c$ and $G$ is a kernel fork of the map of $G$ and $f$ defined as the inclusion of the map of $G$ and the inclusion of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_KernelFork\_\_map\_condition}$ applied to $c$ and $G$.

Let $c$ be a kernel fork of $f$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $G$ be a functor of $C$ and $D$. Then $\operatorname{mapIsLimit}$ applied to $c$, $\mathrm{hc}$ and $G$ is an element of $\operatorname{IsLimit}$ applied to the map of $c$ and $G$ defined as $\operatorname{isLimitMapConeEquiv}$ applied to $c$, $G$ and $\operatorname{isLimitOfPreserves}$ applied to $G$ and $\mathrm{hc}$.

the isomorphism of G and f (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the isomorphism of $G$ and $f$ is an isomorphism of the action of $G$ and the cokernel of $f$ and the cokernel of the map of $G$ and $f$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimitOfHasCokernelOfPreservesColimit}$ applied to $G$ and $f$ and $\operatorname{isColimit}$ applied to the parallel pair of the map of $G$ and $f$ and $0$.

the isomorphism of G and f (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the isomorphism of $G$ and $f$ is an isomorphism of the action of $G$ and the kernel of $f$ and the kernel of the map of $G$ and $f$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimitOfHasKernelOfPreservesLimit}$ applied to $G$ and $f$ and $\operatorname{isLimit}$ applied to the parallel pair of the map of $G$ and $f$ and $0$.

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $f$ and $h_{1}$ is equal to $0$. Let $l$ be an element of $\operatorname{IsColimit}$ applied to the projection of $h_{1}$ and $w$. Then $\operatorname{isColimitCoforkMapOfIsColimit'}$ applied to $G$, $w$ and $l$ is an element of $\operatorname{IsColimit}$ applied to the projection of the map of $G$ and $h_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_isColimitMapCoconeCoforkEquiv'\_\_\_proof\_1}$ applied to $G$ and $w$ defined as $\operatorname{isColimitMapCoconeCoforkEquiv'}$ applied to $G$, $w$ and $\operatorname{isColimitOfPreserves}$ applied to $G$ and $l$.

the map of G and w (from the docstring)

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $f$ and $h_{1}$ is equal to $0$. Then the map of $G$ and $w$ is an equivalence from $\operatorname{IsColimit}$ applied to the map cocone of $G$ and the projection of $h_{1}$ and $w$ to $\operatorname{IsColimit}$ applied to the projection of the map of $G$ and $h_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_isColimitMapCoconeCoforkEquiv'\_\_\_proof\_1}$ applied to $G$ and $w$ defined as the underlying cocone of the projection of $h_{1}$ and $w$ and $G$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isColimitOfHasCokernelOfPreservesColimit}$ applied to $G$ and $f$ is an element of $\operatorname{IsColimit}$ applied to the projection of the map of $G$ and the projection of $f$ and $\mathrm{CategoryTheory\_\_Limits\_\_isColimitOfHasCokernelOfPreservesColimit\_\_\_proof\_1}$ applied to $G$ and $f$ defined as $\operatorname{isColimitCoforkMapOfIsColimit'}$ applied to $G$, $\operatorname{condition}$ applied to $f$ and $\operatorname{cokernelIsCokernel}$ applied to $f$.

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $h_{1}$ and $f$ is equal to $0$. Let $l$ be an element of $\operatorname{IsLimit}$ applied to the inclusion of $h_{1}$ and $w$. Then $\operatorname{isLimitForkMapOfIsLimit'}$ applied to $G$, $w$ and $l$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the map of $G$ and $h_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitMapConeForkEquiv'\_\_\_proof\_1}$ applied to $G$ and $w$ defined as $\operatorname{isLimitMapConeForkEquiv'}$ applied to $G$, $w$ and $\operatorname{isLimitOfPreserves}$ applied to $G$ and $l$.

the map of G and w (from the docstring)

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $h_{1}$ and $f$ is equal to $0$. Then the map of $G$ and $w$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $G$ and the inclusion of $h_{1}$ and $w$ to $\operatorname{IsLimit}$ applied to the inclusion of the map of $G$ and $h_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitMapConeForkEquiv'\_\_\_proof\_1}$ applied to $G$ and $w$ defined as the underlying cone of the inclusion of $h_{1}$ and $w$ and $G$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isLimitOfHasKernelOfPreservesLimit}$ applied to $G$ and $f$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the map of $G$ and the inclusion of $f$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitOfHasKernelOfPreservesLimit\_\_\_proof\_1}$ applied to $G$ and $f$ defined as $\operatorname{isLimitForkMapOfIsLimit'}$ applied to $G$, $\operatorname{condition}$ applied to $f$ and $\operatorname{kernelIsKernel}$ applied to $f$.

the map zero cokernel cofork of G and f (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map zero cokernel cofork of $G$ and $f$ is an isomorphism of the map of the zero cokernel cofork of $f$ and $G$ and the zero cokernel cofork of the map of $G$ and $f$.

the map zero kernel fork of G and f (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map zero kernel fork of $G$ and $f$ is an isomorphism of the map of the zero kernel fork of $f$ and $G$ and the zero kernel fork of the map of $G$ and $f$.

Let $c$ be a multicofork of $d$. Let $F$ be a functor of $C$ and $D$. Then $\operatorname{isColimitMapEquiv}$ applied to $c$ and $F$ is an equivalence from $\operatorname{IsColimit}$ applied to the map cocone of $F$ and $c$ to $\operatorname{IsColimit}$ applied to the map of $c$ and $F$.

Let $c$ be a multicofork of $d$. Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitMapOfPreserves}$ applied to $c$, $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the map of $c$ and $F$ defined as $\operatorname{isColimitMapEquiv}$ applied to $c$, $F$ and $\operatorname{isColimitOfPreserves}$ applied to $F$ and $\mathrm{hc}$.

the map of c and F (from the name)

Let $c$ be a multicofork of $d$. Let $F$ be a functor of $C$ and $D$. Then the map of $c$ and $F$ is a multicofork of the map of $d$ and $F$.

the map of d and F (from the name)

Let $d$ be a multicospan index of $J$ and $C$. Let $F$ be a functor of $C$ and $D$. Then the map of $d$ and $F$ is a multicospan index of $J$ and $D$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to the action of $F$ and the left of $d$ and $i$, the function that maps $i_{1}$ to the action of $F$ and the right of $d$ and $i_{1}$, the function that maps $i_{2}$ to the map of $F$ and the first component of $d$ and $i_{2}$ and the function that maps $i_{3}$ to the map of $F$ and the second component of $d$ and $i_{3}$.

the multicospan map isomorphism of d and F (from the name)

Let $d$ be a multicospan index of $J$ and $C$. Let $F$ be a functor of $C$ and $D$. Then the multicospan map isomorphism of $d$ and $F$ is an isomorphism of the multicospan of the map of $d$ and $F$ and the composition of the multicospan of $d$ and $F$.

Let $c$ be a multifork of $d$. Let $F$ be a functor of $C$ and $D$. Then $\operatorname{isLimitMapEquiv}$ applied to $c$ and $F$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $F$ and $c$ to $\operatorname{IsLimit}$ applied to the map of $c$ and $F$.

Let $c$ be a multifork of $d$. Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitMapOfPreserves}$ applied to $c$, $F$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the map of $c$ and $F$ defined as $\operatorname{isLimitMapEquiv}$ applied to $c$, $F$ and $\operatorname{isLimitOfPreserves}$ applied to $F$ and $\mathrm{hc}$.

the map of c and F (from the name)

Let $c$ be a multifork of $d$. Let $F$ be a functor of $C$ and $D$. Then the map of $c$ and $F$ is a multifork of the map of $d$ and $F$.

the map of d and F (from the name)

Let $d$ be a multispan index of $J$ and $C$. Let $F$ be a functor of $C$ and $D$. Then the map of $d$ and $F$ is a multispan index of $J$ and $D$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to the action of $F$ and the left of $d$ and $i$, the function that maps $i_{1}$ to the action of $F$ and the right of $d$ and $i_{1}$, the function that maps $i_{2}$ to the map of $F$ and the first component of $d$ and $i_{2}$ and the function that maps $i_{3}$ to the map of $F$ and the second component of $d$ and $i_{3}$.

the multispan map isomorphism of d and F (from the name)

Let $d$ be a multispan index of $J$ and $C$. Let $F$ be a functor of $C$ and $D$. Then the multispan map isomorphism of $d$ and $F$ is an isomorphism of the multispan of the map of $d$ and $F$ and the composition of the multispan of $d$ and $F$.

Let $J$ be a set. Let $G$ be a functor of $C$ and $D$. Then we can say that $\operatorname{PreservesWellOrderContinuousOfShape}$ holds for $J$ and $G$.

the isomorphism of G and f (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Then the isomorphism of $G$ and $f$ is an isomorphism of the action of $G$ and the sigma object of $f$ and the sigma object of the function that maps $j$ to the action of $G$ and $f$ applied to $j$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimitOfHasCoproductOfPreservesColimit}$ applied to $G$ and $f$ and $\operatorname{isColimit}$ applied to the functor of the function that maps $j$ to the action of $G$ and $f$ applied to $j$.

the isomorphism of G and f (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Then the isomorphism of $G$ and $f$ is an isomorphism of the action of $G$ and the product object of $f$ and the product object of the function that maps $j$ to the action of $G$ and $f$ applied to $j$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimitOfHasProductOfPreservesLimit}$ applied to $G$ and $f$ and $\operatorname{isLimit}$ applied to the functor of the function that maps $j$ to the action of $G$ and $f$ applied to $j$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Let $g$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $f$ applied to $j_{1}$ and $P$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $P$ and $g$. Then $\operatorname{isColimitCofanMkObjOfIsColimit}$ applied to $G$, $f$, $j_{1}$, $g$ and $t$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the action of $G$ and $P$ and the function that maps $j$ to the map of $G$ and $g$ applied to $j$ defined as the function that maps $t$ to $\operatorname{isColimitMapCoconeCofanMkEquiv}$ applied to $G$, $f$, $j_{1}$, $\operatorname{isColimitOfPreserves}$ applied to $G$ and $g$ and $t$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Let $g$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $f$ applied to $j_{1}$ and $P$. Then $\operatorname{isColimitMapCoconeCofanMkEquiv}$ applied to $G$, $f$, $j_{1}$ and $g$ is an equivalence from $\operatorname{IsColimit}$ applied to the map cocone of $G$ and $\operatorname{mk}$ applied to $P$ and $g$ to $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the action of $G$ and $P$ and the function that maps $j$ to the map of $G$ and $g$ applied to $j$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Then $\operatorname{isColimitOfHasCoproductOfPreservesColimit}$ applied to $G$ and $f$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the action of $G$ and the sigma object of $f$ and the function that maps $j$ to the map of $G$ and the inclusion of $f$ and $j$ defined as $\operatorname{isColimitCofanMkObjOfIsColimit}$ applied to $G$, $f$, $\mathrm{CategoryTheory\_\_Limits\_\_Sigma\_\_\_u3b9\_}$ applied to $f$ and $\operatorname{coproductIsCoproduct}$ applied to $f$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Let $g$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $f$ applied to $j_{1}$ and $P$. Let $t$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the action of $G$ and $P$ and the function that maps $j$ to the map of $G$ and $g$ applied to $j$. Then $\operatorname{isColimitOfIsColimitCofanMkObj}$ applied to $G$, $f$, $j_{1}$, $g$ and $t$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $P$ and $g$ defined as the function that maps $t$ to $\operatorname{isColimitOfReflects}$ applied to $G$, $\operatorname{symm}$ applied to $\operatorname{isColimitMapCoconeCofanMkEquiv}$ applied to $G$, $f$ and $j_{1}$ and $g$ and $t$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Let $g$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $P$ and $f$ applied to $j_{1}$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $P$ and $g$. Then $\operatorname{isLimitFanMkObjOfIsLimit}$ applied to $G$, $f$, $j_{1}$, $g$ and $t$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the action of $G$ and $P$ and the function that maps $j$ to the map of $G$ and $g$ applied to $j$ defined as the function that maps $t$ to $\operatorname{isLimitMapConeFanMkEquiv}$ applied to $G$, $f$, $j_{1}$, $\operatorname{isLimitOfPreserves}$ applied to $G$ and $g$ and $t$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Let $g$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $P$ and $f$ applied to $j_{1}$. Then $\operatorname{isLimitMapConeFanMkEquiv}$ applied to $G$, $f$, $j_{1}$ and $g$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $G$ and $\operatorname{mk}$ applied to $P$ and $g$ to $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the action of $G$ and $P$ and the function that maps $j$ to the map of $G$ and $g$ applied to $j$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Then $\operatorname{isLimitOfHasProductOfPreservesLimit}$ applied to $G$ and $f$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the action of $G$ and the product object of $f$ and the function that maps $j$ to the map of $G$ and the projection of $f$ and $j$ defined as $\operatorname{isLimitFanMkObjOfIsLimit}$ applied to $G$, $f$, $\mathrm{CategoryTheory\_\_Limits\_\_Pi\_\_\_u3c0\_}$ applied to $f$ and $\operatorname{productIsProduct}$ applied to $f$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $J$ to elements of $C$. Let $g$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $P$ and $f$ applied to $j_{1}$. Let $t$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the action of $G$ and $P$ and the function that maps $j$ to the map of $G$ and $g$ applied to $j$. Then $\operatorname{isLimitOfIsLimitFanMkObj}$ applied to $G$, $f$, $j_{1}$, $g$ and $t$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $P$ and $g$ defined as the function that maps $t$ to $\operatorname{isLimitOfReflects}$ applied to $G$, $\operatorname{symm}$ applied to $\operatorname{isLimitMapConeFanMkEquiv}$ applied to $G$, $f$ and $j_{1}$ and $g$ and $t$.

the isomorphism of f and g (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the isomorphism of $f$ and $g$ is an isomorphism of the action of $G$ and the pullback of $f$ and $g$ and the pullback of the map of $G$ and $f$ and the map of $G$ and $g$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimitOfHasPullbackOfPreservesLimit}$ applied to $G$, $f$ and $g$ and $\operatorname{isLimit}$ applied to the cospan of the map of $G$ and $f$ and the map of $G$ and $g$.

the isomorphism of f and g (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $W$ and $X$. Let $g$ be a homomorphism of $W$ and $Y$. Then the isomorphism of $f$ and $g$ is an isomorphism of the pushout of the map of $G$ and $f$ and the map of $G$ and $g$ and the action of $G$ and the pushout of $f$ and $g$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the span of the map of $G$ and $f$ and the map of $G$ and $g$ and $\operatorname{isColimitOfHasPushoutOfPreservesColimit}$ applied to $G$, $f$ and $g$.

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $c$ be a pullback cone of $f$ and $g$. Then $\operatorname{isLimitCoyonedaEquiv}$ applied to $f$, $g$ and $c$ is an equivalence from $\operatorname{IsLimit}$ applied to $c$ to the set of functions from opposites $X_{1}$ of $C$ to elements of $\operatorname{IsLimit}$ applied to the map of $c$ and the action of the Coyoneda and $X_{1}$ defined as the composition of $\operatorname{isLimitCoyonedaEquiv}$ applied to $c$ and the right product congruence of the function that maps $X_{1}$ to $\operatorname{isLimitMapConeEquiv}$ applied to $c$ and the action of the Coyoneda and $X_{1}$.

Let $c$ be a pullback cone of $f$ and $g$. Let $G$ be a functor of $C$ and $D$. Then $\operatorname{isLimitMapConeEquiv}$ applied to $c$ and $G$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $G$ and $c$ to $\operatorname{IsLimit}$ applied to the map of $c$ and $G$.

the map of c and G (from the name)

Let $c$ be a pullback cone of $f$ and $g$. Let $G$ be a functor of $C$ and $D$. Then the map of $c$ and $G$ is a pullback cone of the map of $G$ and $f$ and the map of $G$ and $g$.

Let $c$ be a pushout cocone of $f$ and $g$. Let $G$ be a functor of $C$ and $D$. Then $\operatorname{isColimitMapCoconeEquiv}$ applied to $c$ and $G$ is an equivalence from $\operatorname{IsColimit}$ applied to the map cocone of $G$ and $c$ to $\operatorname{IsColimit}$ applied to the map of $c$ and $G$.

Let $c$ be a pushout cocone of $f$ and $g$. Then $\operatorname{isColimitYonedaEquiv}$ applied to $c$ is an equivalence from $\operatorname{IsColimit}$ applied to $c$ to the set of functions from elements $X_{1}$ of $C$ to elements of $\operatorname{IsLimit}$ applied to the map of the opposite of $c$ and the action of the Yoneda and $X_{1}$.

the map of c and G (from the name)

Let $c$ be a pushout cocone of $f$ and $g$. Let $G$ be a functor of $C$ and $D$. Then the map of $c$ and $G$ is a pushout cocone of the map of $G$ and $f$ and the map of $G$ and $g$.

the map of G and comm (from the docstring)

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $f$ and $h$ is equal to the composition of $g$ and $k$. Then the map of $G$ and $\mathrm{comm}$ is an equivalence from $\operatorname{IsColimit}$ applied to the map cocone of $G$ and $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{comm}$ to $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $h$, the map of $G$ and $k$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitMapConePullbackConeEquiv\_\_\_proof\_1}$ applied to $G$ and $\mathrm{comm}$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $W$ and $X$. Let $g$ be a homomorphism of $W$ and $Y$. Then $\operatorname{isColimitOfHasPushoutOfPreservesColimit}$ applied to $G$, $f$ and $g$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and the left injection of $f$ and $g$, the map of $G$ and the right injection of $f$ and $g$ and $\mathrm{CategoryTheory\_\_Limits\_\_isColimitOfHasPushoutOfPreservesColimit\_\_\_proof\_1}$ applied to $G$, $f$ and $g$ defined as $\operatorname{isColimitPushoutCoconeMapOfIsColimit}$ applied to $G$, $\operatorname{condition}$ and $\operatorname{pushoutIsPushout}$ applied to $f$ and $g$.

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $f$ and $h$ is equal to the composition of $g$ and $k$. Let $l$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $h$, the map of $G$ and $k$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitMapConePullbackConeEquiv\_\_\_proof\_1}$ applied to $G$ and $\mathrm{comm}$. Then $\operatorname{isColimitOfIsColimitPushoutCoconeMap}$ applied to $G$, $\mathrm{comm}$ and $l$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{comm}$ defined as $\operatorname{isColimitOfReflects}$ applied to $G$ and $\operatorname{symm}$ applied to the map of $G$ and $\mathrm{comm}$ and $l$.

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $f$ and $h$ is equal to the composition of $g$ and $k$. Let $l$ be an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{comm}$. Then $\operatorname{isColimitPushoutCoconeMapOfIsColimit}$ applied to $G$, $\mathrm{comm}$ and $l$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $h$, the map of $G$ and $k$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitMapConePullbackConeEquiv\_\_\_proof\_1}$ applied to $G$ and $\mathrm{comm}$ defined as $\operatorname{isColimitMapCoconePushoutCoconeEquiv}$ applied to $G$, $\mathrm{comm}$ and $\operatorname{isColimitOfPreserves}$ applied to $G$ and $l$.

the map of G and comm (from the docstring)

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $h$ and $f$ is equal to the composition of $k$ and $g$. Then the map of $G$ and $\mathrm{comm}$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $G$ and $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{comm}$ to $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $h$, the map of $G$ and $k$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitMapConePullbackConeEquiv\_\_\_proof\_1}$ applied to $G$ and $\mathrm{comm}$ defined as $\operatorname{isLimitMapConeEquiv}$ applied to $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{comm}$ and $G$.

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{isLimitOfHasPullbackOfPreservesLimit}$ applied to $G$, $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and the first projection of the pullback of $f$ and $g$, the map of $G$ and the second projection of the pullback of $f$ and $g$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitOfHasPullbackOfPreservesLimit\_\_\_proof\_1}$ applied to $G$, $f$ and $g$ defined as $\operatorname{isLimitPullbackConeMapOfIsLimit}$ applied to $G$, $\operatorname{condition}$ and $\operatorname{pullbackIsPullback}$ applied to $f$ and $g$.

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $h$ and $f$ is equal to the composition of $k$ and $g$. Let $l$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $h$, the map of $G$ and $k$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitMapConePullbackConeEquiv\_\_\_proof\_1}$ applied to $G$ and $\mathrm{comm}$. Then $\operatorname{isLimitOfIsLimitPullbackConeMap}$ applied to $G$, $\mathrm{comm}$ and $l$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{comm}$ defined as $\operatorname{isLimitOfReflects}$ applied to $G$ and the inverse function of $\operatorname{isLimitMapConeEquiv}$ applied to $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{comm}$ and $G$ and $l$.

Let $G$ be a functor of $C$ and $D$. Assume that the composition of $h$ and $f$ is equal to the composition of $k$ and $g$. Let $l$ be an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{comm}$. Then $\operatorname{isLimitPullbackConeMapOfIsLimit}$ applied to $G$, $\mathrm{comm}$ and $l$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the map of $G$ and $h$, the map of $G$ and $k$ and $\mathrm{CategoryTheory\_\_Limits\_\_isLimitMapConePullbackConeEquiv\_\_\_proof\_1}$ applied to $G$ and $\mathrm{comm}$ defined as the forward map of $\operatorname{isLimitMapConeEquiv}$ applied to $\operatorname{mk}$ applied to $h$, $k$ and $\mathrm{comm}$ and $G$ and $\operatorname{isLimitOfPreserves}$ applied to $G$ and $l$.

Let $G$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then $\operatorname{isInitialIffObj}$ applied to $G$ and $X$ is an equivalence from $\operatorname{IsInitial}$ applied to $X$ to $\operatorname{IsInitial}$ applied to the action of $G$ and $X$.

Let $G$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Let $l$ be an element of $\operatorname{IsInitial}$ applied to $X$. Then $\operatorname{isInitialObj}$ applied to $G$, $X$ and $l$ is an element of $\operatorname{IsInitial}$ applied to the action of $G$ and $X$ defined as $\operatorname{isColimitMapCoconeEmptyCoconeEquiv}$ applied to $G$, $X$ and $\operatorname{isColimitOfPreserves}$ applied to $G$ and $l$.

Let $G$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Let $l$ be an element of $\operatorname{IsInitial}$ applied to the action of $G$ and $X$. Then $\operatorname{isInitialOfObj}$ applied to $G$, $X$ and $l$ is an element of $\operatorname{IsInitial}$ applied to $X$ defined as $\operatorname{isColimitOfReflects}$ applied to $G$ and $\operatorname{symm}$ applied to the map of $G$ and $X$ and $l$.

Let $G$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then $\operatorname{isTerminalIffObj}$ applied to $G$ and $X$ is an equivalence from $\operatorname{IsTerminal}$ applied to $X$ to $\operatorname{IsTerminal}$ applied to the action of $G$ and $X$.

Let $G$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Let $l$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then $\operatorname{isTerminalObj}$ applied to $G$, $X$ and $l$ is an element of $\operatorname{IsTerminal}$ applied to the action of $G$ and $X$ defined as $\operatorname{isLimitMapConeEmptyConeEquiv}$ applied to $G$, $X$ and $\operatorname{isLimitOfPreserves}$ applied to $G$ and $l$.

Let $G$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Let $l$ be an element of $\operatorname{IsTerminal}$ applied to the action of $G$ and $X$. Then $\operatorname{isTerminalOfObj}$ applied to $G$, $X$ and $l$ is an element of $\operatorname{IsTerminal}$ applied to $X$ defined as $\operatorname{isLimitOfReflects}$ applied to $G$ and $\operatorname{symm}$ applied to the map of $G$ and $X$ and $l$.

the isomorphism of G (from the name)

Let $G$ be a functor of $C$ and $D$. Then the isomorphism of $G$ is an isomorphism of the action of $G$ and $\operatorname{initial}$ applied to $C$ and $\operatorname{initial}$ applied to $D$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimitOfHasInitialOfPreservesColimit}$ applied to $G$ and $\operatorname{isColimit}$ applied to $\operatorname{empty}$ applied to $D$.

the isomorphism of G (from the name)

Let $G$ be a functor of $C$ and $D$. Then the isomorphism of $G$ is an isomorphism of the action of $G$ and $\operatorname{terminal}$ applied to $C$ and $\operatorname{terminal}$ applied to $D$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimitOfHasTerminalOfPreservesLimit}$ applied to $G$ and $\operatorname{isLimit}$ applied to $\operatorname{empty}$ applied to $D$.

the map of G and X (from the docstring)

Let $G$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then the map of $G$ and $X$ is an equivalence from $\operatorname{IsColimit}$ applied to the map cocone of $G$ and $\operatorname{asEmptyCocone}$ applied to $X$ to $\operatorname{IsInitial}$ applied to the action of $G$ and $X$.

Let $G$ be a functor of $C$ and $D$. Then $\operatorname{isColimitOfHasInitialOfPreservesColimit}$ applied to $G$ is an element of $\operatorname{IsInitial}$ applied to the action of $G$ and $\operatorname{initial}$ applied to $C$ defined as $\operatorname{isInitialObj}$ applied to $G$, $\operatorname{initial}$ applied to $C$ and $\operatorname{initialIsInitial}$.

the map of G and X (from the docstring)

Let $G$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then the map of $G$ and $X$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $G$ and $\operatorname{asEmptyCone}$ applied to $X$ to $\operatorname{IsTerminal}$ applied to the action of $G$ and $X$.

Let $G$ be a functor of $C$ and $D$. Then $\operatorname{isLimitOfHasTerminalOfPreservesLimit}$ applied to $G$ is an element of $\operatorname{IsTerminal}$ applied to the action of $G$ and $\operatorname{terminal}$ applied to $C$ defined as $\operatorname{isTerminalObj}$ applied to $G$, $\operatorname{terminal}$ applied to $C$ and $\operatorname{terminalIsTerminal}$.

F preserves zero morphisms (from the name)

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

the map zero object of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the map zero object of $F$ is an isomorphism of the action of $F$ and $0$ and $0$.

the cokernel of the map of R and f (from the docstring)

Let $R$ be an element of $C$. Let $f$ be a function from elements of $x_{2}$ to elements of $x_{3}$. Then the cokernel of the map of $R$ and $f$ is an element of $\operatorname{IsColimit}$ applied to the sigma constant cokernel cofork of $R$ and $f$.

the sigma constant cokernel cofork of R and f (from the name)

Let $R$ be an element of $C$. Let $f$ be a function from elements of $x_{2}$ to elements of $x_{3}$. Then the sigma constant cokernel cofork of $R$ and $f$ is a cokernel cofork of the map of $f$ and the function that maps $x_{4}$ to the identity morphism of $R$.

the sigma constant object composition isomorphism of F and X (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then the sigma constant object composition isomorphism of $F$ and $X$ is an isomorphism of the composition of the action of the sigma constant and $X$ and $F$ and the action of the sigma constant and the action of $F$ and $X$.

the section equivalence of K (from the name)

Let $K$ be a functor of $J$ and the set of sets. Then the section equivalence of $K$ is an equivalence from the set of elements of the section of $K$ to the set of elements of the section of the composition of $K$ and the functor embedding.

the Yoneda Yoneda colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of functors of the set of opposites of $C$ and the set of sets. Then the Yoneda Yoneda colimit of $F$ is an isomorphism of the composition of the opposite of the Yoneda and the action of the Yoneda and the colimit of $F$ and the composition of the opposite of the Yoneda and the colimit of the composition of $F$ and the Yoneda defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the Yoneda opposite composition Yoneda object of the colimit of $F$ and the right isomorphism whisker of the colimit of $F$ and the functor embedding and the left isomorphism whisker of the flip of $F$ and $\operatorname{preservesColimitNatIso}$ applied to the functor embedding and the right isomorphism whisker of the right isomorphism whisker of the inverse of the curried version of the Yoneda lemma and the action of the left whiskering of the set of functors of the set of opposites of $C$ and the set of sets and the set of sets and $F$ and the colimit and the left isomorphism whisker of the opposite of the Yoneda and the inverse of the colimit of the composition of $F$ and the Yoneda.

the cocone projection opposite composition shrink Yoneda flip of F (from the name)

Let $F$ be a functor of $C$ and the set of sets. Then the cocone projection opposite composition shrink Yoneda flip of $F$ is a cocone of the composition of the opposite of the projection of $F$ and the flip of the Yoneda embedding.

the cocone projection opposite composition shrink Yoneda object of F and X (from the name)

Let $F$ be a functor of $C$ and the set of sets. Let $X$ be an element of $C$. Then the cocone projection opposite composition shrink Yoneda object of $F$ and $X$ is a cocone of the composition of the opposite of the projection of $F$ and the action of the Yoneda embedding and $X$.

Let $F$ be a functor of $C$ and the set of sets. Then $\mathrm{CategoryTheory\_\_Functor\_\_Elements\_\_isColimitCocone\_u3c0\_OpCompShrinkYonedaFlip}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the cocone projection opposite composition shrink Yoneda flip of $F$ defined as $\operatorname{evaluationJointlyReflectsColimits}$ applied to the cocone projection opposite composition shrink Yoneda flip of $F$ and $\mathrm{CategoryTheory\_\_Functor\_\_Elements\_\_isColimitCocone\_u3c0\_OpCompShrinkYonedaObj}$ applied to $F$.

Let $F$ be a functor of $C$ and the set of sets. Let $X$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_Functor\_\_Elements\_\_isColimitCocone\_u3c0\_OpCompShrinkYonedaObj}$ applied to $F$ and $X$ is an element of $\operatorname{IsColimit}$ applied to the cocone projection opposite composition shrink Yoneda object of $F$ and $X$.

Let $X$ be an element of $C$. Then $\operatorname{isInitialElementsMkShrinkYonedaObjObjEquivId}$ applied to $X$ is an element of $\operatorname{IsInitial}$ applied to the element of $X$ and $\operatorname{symm}$ applied to the shrink Yoneda object object equivalence and the identity morphism of $X$.

the shrink Yoneda composition whiskering left object projection composition colimit isomorphism of F (from the name)

Let $F$ be a functor of $C$ and the set of sets. Then the shrink Yoneda composition whiskering left object projection composition colimit isomorphism of $F$ is an isomorphism of the composition of the Yoneda embedding and the composition of the action of the left whiskering of the set of opposites of $C$ and the set of sets and the opposite of the projection of $F$ and the colimit and $F$.

the cocone of P (from the name)

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

the colimit of P (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Then the colimit of $P$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $P$.

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{compULiftYonedaIsoULiftYonedaCompLan}$ applied to $F$ is an isomorphism of the composition of $F$ and the lift Yoneda and the composition of the lift Yoneda and $\operatorname{lan}$ applied to the opposite of $F$.

the extension homomorphism of x2 (from the name)

Let $x_{2}$ be a left extension of the lift Yoneda and the composition of $F$ and the lift Yoneda. Then the extension homomorphism of $x_{2}$ is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{lan}$ applied to the opposite of $F$ and the homomorphism of $\operatorname{compULiftYonedaIsoULiftYonedaCompLan}$ applied to $F$ and $x_{2}$.

the natural transformation of x2 (from the name)

Let $x_{2}$ be a homomorphism of the composition of $F$ and the lift Yoneda and the composition of the lift Yoneda and $G$. Then the natural transformation of $x_{2}$ is a homomorphism of $\operatorname{lan}$ applied to the opposite of $F$ and $G$.

the presheaf homomorphism of x2 and P (from the name)

Let $x_{2}$ be a homomorphism of the composition of $F$ and the lift Yoneda and the composition of the lift Yoneda and $G$. Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Then the presheaf homomorphism of $x_{2}$ and $P$ is a homomorphism of $P$ and the composition of the opposite of $F$ and the action of $G$ and $P$.

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{functorToRepresentables}$ applied to $P$ is a functor of the set of opposites of the set of elements of $P$ and the set of functors of the set of opposites of $C$ and the set of sets defined as the composition of the left opposite of the projection of $P$ and the lift Yoneda.

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{isColimitTautologicalCocone}$ applied to $P$ is an element of $\operatorname{IsColimit}$ applied to the tautological cocone of $P$.

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{isColimitTautologicalCocone'}$ applied to $P$ is an element of $\operatorname{IsColimit}$ applied to the tautological cocone of $P$ defined as the inverse function of the whisker equivalence equivalence of the costructured arrow lift Yoneda equivalence of $P$ and the colimit of $P$.

Let $A$ be a functor of $C$ and $x_{1}$. Then $\operatorname{isExtensionAlongULiftYoneda}$ applied to $A$ is an isomorphism of the composition of the lift Yoneda and the left Kan extension of the lift Yoneda and $A$ and $A$ defined as the inverse of $\operatorname{asIso}$ applied to the unit of the chosen left Kan extension of the lift Yoneda and $A$.

the restricted lift Yoneda of A (from the name)

Let $A$ be a functor of $C$ and $x_{1}$. Then the restricted lift Yoneda of $A$ is a functor of $x_{1}$ and the set of functors of the set of opposites of $C$ and the set of sets defined as the composition of the lift Yoneda and the action of the left whiskering of the set of opposites of $x_{1}$ and the set of sets and the opposite of $A$.

the tautological cocone of P (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Then the tautological cocone of $P$ is a cocone of the composition of the projection of the Yoneda and $P$ and the Yoneda.

the tautological cocone of P (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Then the tautological cocone of $P$ is a cocone of the composition of the projection of the lift Yoneda and $P$ and the lift Yoneda.

the lift Yoneda adjunction of L and x3 (from the name)

Let $L$ be a functor of the set of functors of the set of opposites of $C$ and the set of sets and $x_{1}$. Let $x_{3}$ be a homomorphism of $A$ and the composition of the lift Yoneda and $L$. Then the lift Yoneda adjunction of $L$ and $x_{3}$ is an adjunction of $L$ and the restricted lift Yoneda of $A$.

Let $L$ be a functor of the set of functors of the set of opposites of $C$ and the set of sets and $x_{1}$. Let $e$ be an isomorphism of $A$ and the composition of the lift Yoneda and $L$. Then $\operatorname{uniqueExtensionAlongULiftYoneda}$ applied to $L$ and $e$ is an isomorphism of $L$ and the left Kan extension of the lift Yoneda and $A$ defined as $\operatorname{leftKanExtensionUnique}$ applied to $L$, the homomorphism of $e$, the left Kan extension of the lift Yoneda and $A$ and the unit of the chosen left Kan extension of the lift Yoneda and $A$.

X is indecomposable (from the docstring)

Let $X$ be an element of $C$. Then $X$ is indecomposable, if $X$ is not a zero and for all elements $Y$ of $C$, for all elements $Z$ of $C$, for all isomorphisms $x_{2}$ of $X$ and the biproduct of $Y$ and $Z$, $Y$ is a zero or $Z$ is a zero.

the binary bicone of b (from the name)

Let $b$ be a bicone of $\operatorname{pairFunction}$ applied to $Y$. Then the binary bicone of $b$ is a binary bicone of $X$ and $Y$ defined as the action of the binary bicone functor and $b$.

the binary bicone functor (from the name)

The binary bicone functor is a functor of the set of bicones of $\operatorname{pairFunction}$ applied to $Y$ and the set of binary bicones of $X$ and $Y$.

Let $b$ be a bicone of $\operatorname{pairFunction}$ applied to $Y$. Then $\operatorname{toBinaryBiconeIsBilimit}$ applied to $b$ is an equivalence from $\operatorname{IsBilimit}$ applied to the binary bicone of $b$ to $\operatorname{IsBilimit}$ applied to $b$.

Let $b$ be a bicone of $\operatorname{pairFunction}$ applied to $Y$. Then $\operatorname{toBinaryBiconeIsColimit}$ applied to $b$ is an equivalence from $\operatorname{IsColimit}$ applied to the cocone of the binary bicone of $b$ to $\operatorname{IsColimit}$ applied to the cocone of $b$.

Let $b$ be a bicone of $\operatorname{pairFunction}$ applied to $Y$. Then $\operatorname{toBinaryBiconeIsLimit}$ applied to $b$ is an equivalence from $\operatorname{IsLimit}$ applied to the cone of the binary bicone of $b$ to $\operatorname{IsLimit}$ applied to the cone of $b$.

binary bicone of P and Q (from the name)

Let $P$ and $Q$ be elements of $C$. Then the binary bicones of $P$ and $Q$ are a basic type.

Let $b$ be a binary bicone of $P$ and $Q$. Then the elements of $\operatorname{IsBilimit}$ applied to $b$ are a basic type.

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

Let $\mathrm{self}$ be an element of $\operatorname{IsBilimit}$ applied to $b$. Then $\operatorname{isLimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to the cone of $b$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{hb}$ be an element of $\operatorname{IsBilimit}$ applied to $b$. Let $\mathrm{eP}$ be an isomorphism of $P$ and $\mathrm{P'}$. Let $\mathrm{eQ}$ be an isomorphism of $Q$ and $\mathrm{Q'}$. Then $\operatorname{ofIso}$ applied to $\mathrm{hb}$, $\mathrm{eP}$ and $\mathrm{eQ}$ is an element of $\operatorname{IsBilimit}$ applied to the binary bicone of $\mathrm{eP}$ and $\mathrm{eQ}$.

the opposite of h (from the docstring)

Let $h$ be an element of $\operatorname{IsBilimit}$ applied to $b$. Then the opposite of $h$ is an element of $\operatorname{IsBilimit}$ applied to the opposite of $b$ defined as $\operatorname{mk}$ applied to the opposite of $\operatorname{isColimit}$ applied to $h$ and the opposite of $\operatorname{isLimit}$ applied to $h$.

the first component of self (from the name)

Let $\mathrm{self}$ be a binary bicone of $P$ and $Q$. Then the first component of $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{self}$ and $P$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the first component kernel fork of c (from the name)

Let $c$ be a binary bicone of $X$ and $Y$. Then the first component kernel fork of $c$ is a kernel fork of the first component of $c$ defined as the inclusion of the right injection of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_BinaryBicone\_\_inr\_fst}$ applied to $c$.

the left injection of self (from the name)

Let $\mathrm{self}$ be a binary bicone of $P$ and $Q$. Then the left injection of $\mathrm{self}$ is a homomorphism of $P$ and $\operatorname{pt}$ applied to $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the left injection cokernel cofork of c (from the name)

Let $c$ be a binary bicone of $X$ and $Y$. Then the left injection cokernel cofork of $c$ is a cokernel cofork of the left injection of $c$ defined as the projection of the second component of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_BinaryBicone\_\_inl\_snd}$ applied to $c$.

the right injection of self (from the name)

Let $\mathrm{self}$ be a binary bicone of $P$ and $Q$. Then the right injection of $\mathrm{self}$ is a homomorphism of $Q$ and $\operatorname{pt}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

the right injection cokernel cofork of c (from the name)

Let $c$ be a binary bicone of $X$ and $Y$. Then the right injection cokernel cofork of $c$ is a cokernel cofork of the right injection of $c$ defined as the projection of the first component of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_BinaryBicone\_\_inr\_fst}$ applied to $c$.

Let $i$ be an element of $\operatorname{IsColimit}$ applied to the cocone of $c$. Then $\operatorname{isColimitInlCokernelCofork}$ applied to $i$ is an element of $\operatorname{IsColimit}$ applied to the left injection cokernel cofork of $c$ defined as $\operatorname{mk'}$ applied to the left injection cokernel cofork of $c$ and the function that maps $s$ to the composition of the right injection of $c$ and the projection of $s$.

Let $i$ be an element of $\operatorname{IsColimit}$ applied to the cocone of $c$. Then $\operatorname{isColimitInrCokernelCofork}$ applied to $i$ is an element of $\operatorname{IsColimit}$ applied to the right injection cokernel cofork of $c$ defined as $\operatorname{mk'}$ applied to the right injection cokernel cofork of $c$ and the function that maps $s$ to the composition of the left injection of $c$ and the projection of $s$.

Let $i$ be an element of $\operatorname{IsLimit}$ applied to the cone of $c$. Then $\operatorname{isLimitFstKernelFork}$ applied to $i$ is an element of $\operatorname{IsLimit}$ applied to the first component kernel fork of $c$ defined as $\operatorname{mk'}$ applied to the first component kernel fork of $c$ and the function that maps $s$ to the composition of the inclusion of $s$ and the second component of $c$.

Let $i$ be an element of $\operatorname{IsLimit}$ applied to the cone of $c$. Then $\operatorname{isLimitSndKernelFork}$ applied to $i$ is an element of $\operatorname{IsLimit}$ applied to the second component kernel fork of $c$ defined as $\operatorname{mk'}$ applied to the second component kernel fork of $c$ and the function that maps $s$ to the composition of the inclusion of $s$ and the first component of $c$.

the binary bicone of eP and eQ (from the name)

Let $b$ be a binary bicone of $P$ and $Q$. Let $\mathrm{eP}$ be an isomorphism of $P$ and $\mathrm{P'}$. Let $\mathrm{eQ}$ be an isomorphism of $Q$ and $\mathrm{Q'}$. Then the binary bicone of $\mathrm{eP}$ and $\mathrm{eQ}$ is a binary bicone of $\mathrm{P'}$ and $\mathrm{Q'}$.

the opposite of b (from the docstring)

Let $b$ be a binary bicone of $P$ and $Q$. Then the opposite of $b$ is a binary bicone of $\operatorname{op}$ applied to $P$ and $\operatorname{op}$ applied to $Q$.

Let $\mathrm{self}$ be a binary bicone of $P$ and $Q$. Then $\operatorname{pt}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the retract of c (from the docstring)

Let $c$ be a binary bicone of $P$ and $Q$. Then the retract of $c$ is a retract of $P$ and $\operatorname{pt}$ applied to $c$.

the retract of c (from the docstring)

Let $c$ be a binary bicone of $P$ and $Q$. Then the retract of $c$ is a retract of $Q$ and $\operatorname{pt}$ applied to $c$.

the second component of self (from the name)

Let $\mathrm{self}$ be a binary bicone of $P$ and $Q$. Then the second component of $\mathrm{self}$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{self}$ and $Q$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the second component kernel fork of c (from the name)

Let $c$ be a binary bicone of $X$ and $Y$. Then the second component kernel fork of $c$ is a kernel fork of the second component of $c$ defined as the inclusion of the left injection of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_BinaryBicone\_\_inl\_snd}$ applied to $c$.

the bicone of b (from the name)

Let $b$ be a binary bicone of $X$ and $Y$. Then the bicone of $b$ is a bicone of $\operatorname{pairFunction}$ applied to $Y$ defined as the action of the bicone functor and $b$.

the bicone functor (from the name)

The bicone functor is a functor of the set of binary bicones of $X$ and $Y$ and the set of bicones of $\operatorname{pairFunction}$ applied to $Y$.

Let $b$ be a binary bicone of $X$ and $Y$. Then $\operatorname{toBiconeIsBilimit}$ applied to $b$ is an equivalence from $\operatorname{IsBilimit}$ applied to the bicone of $b$ to $\operatorname{IsBilimit}$ applied to $b$.

Let $b$ be a binary bicone of $X$ and $Y$. Then $\operatorname{toBiconeIsColimit}$ applied to $b$ is an equivalence from $\operatorname{IsColimit}$ applied to the cocone of the bicone of $b$ to $\operatorname{IsColimit}$ applied to the cocone of $b$.

Let $b$ be a binary bicone of $X$ and $Y$. Then $\operatorname{toBiconeIsLimit}$ applied to $b$ is an equivalence from $\operatorname{IsLimit}$ applied to the cone of the bicone of $b$ to $\operatorname{IsLimit}$ applied to the cone of $b$.

the cocone of c (from the name)

Let $c$ be a binary bicone of $P$ and $Q$. Then the cocone of $c$ is a cocone of the pair of $P$ and $Q$ defined as $\operatorname{mk}$ applied to the left injection of $c$ and the right injection of $c$.

the cone of c (from the name)

Let $c$ be a binary bicone of $P$ and $Q$. Then the cone of $c$ is a cone of the pair of $P$ and $Q$ defined as $\operatorname{mk}$ applied to the first component of $c$ and the second component of $c$.

binary bicone morphism of A and B (from the name)

Let $A$ and $B$ be binary bicones of $P$ and $Q$. Then the binary bicone morphisms of $A$ and $B$ are a basic type.

the homomorphism of self (from the name)

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

the extension of x2 (from the name)

Let $x_{2}$ be an isomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $\mathrm{c'}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the left injection of $c$ and the homomorphism of $x_{2}$ is equal to the left injection of $\mathrm{c'}$ and $\mathrm{CategoryTheory\_\_Limits\_\_BinaryBicones\_\_ext\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for the proposition that the composition of the right injection of $c$ and the homomorphism of $x_{2}$ is equal to the right injection of $\mathrm{c'}$ and $\mathrm{CategoryTheory\_\_Limits\_\_BinaryBicones\_\_ext\_\_\_auto\_3}$, $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{2}$ and the first component of $\mathrm{c'}$ is equal to the first component of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_BinaryBicones\_\_ext\_\_\_auto\_5}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{2}$ and the second component of $\mathrm{c'}$ is equal to the second component of $c$ and $\mathrm{CategoryTheory\_\_Limits\_\_BinaryBicones\_\_ext\_\_\_auto\_7}$. Then the extension of $x_{2}$ is an isomorphism of $c$ and $\mathrm{c'}$.

the functoriality of Q and F (from the name)

Let $P$ and $Q$ be elements of $C$. Let $F$ be a functor of $C$ and $D$. Then the functoriality of $Q$ and $F$ is a functor of the set of binary bicones of $P$ and $Q$ and the set of binary bicones of the action of $F$ and $P$ and the action of $F$ and $Q$.

the bicone of P and Q (from the name)

Let $P$ and $Q$ be elements of $C$. Then the bicone of $P$ and $Q$ is a binary bicone of $P$ and $Q$ defined as the bicone of $\operatorname{getBinaryBiproductData}$ applied to $P$ and $Q$.

Let $P$ and $Q$ be elements of $C$. Then $\operatorname{isBilimit}$ applied to $P$ and $Q$ is an element of $\operatorname{IsBilimit}$ applied to the bicone of $P$ and $Q$ defined as $\operatorname{isBilimit}$ applied to $\operatorname{getBinaryBiproductData}$ applied to $P$ and $Q$.

the colimit cocone of P and Q (from the docstring)

Let $P$ and $Q$ be elements of $C$. Then the colimit cocone of $P$ and $Q$ is an element of $\operatorname{IsColimit}$ applied to the cocone of the bicone of $P$ and $Q$ defined as $\operatorname{isColimit}$ applied to $\operatorname{isBilimit}$ applied to $\operatorname{getBinaryBiproductData}$ applied to $P$ and $Q$.

the limit cone of P and Q (from the docstring)

Let $P$ and $Q$ be elements of $C$. Then the limit cone of $P$ and $Q$ is an element of $\operatorname{IsLimit}$ applied to the cone of the bicone of $P$ and $Q$ defined as $\operatorname{isLimit}$ applied to $\operatorname{isBilimit}$ applied to $\operatorname{getBinaryBiproductData}$ applied to $P$ and $Q$.

binary biproduct data of P and Q (from the name)

Let $P$ and $Q$ be elements of $C$. Then the binary biproduct data of $P$ and $Q$ are a basic type.

the bicone of self (from the name)

Let $\mathrm{self}$ be a binary biproduct data of $P$ and $Q$. Then the bicone of $\mathrm{self}$ is a binary bicone of $P$ and $Q$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a binary biproduct data of $P$ and $Q$. Then $\operatorname{isBilimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsBilimit}$ applied to the bicone of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the binary biproduct data of eP and eQ (from the name)

Let $d$ be a binary biproduct data of $P$ and $Q$. Let $\mathrm{eP}$ be an isomorphism of $P$ and $\mathrm{P'}$. Let $\mathrm{eQ}$ be an isomorphism of $Q$ and $\mathrm{Q'}$. Then the binary biproduct data of $\mathrm{eP}$ and $\mathrm{eQ}$ is a binary biproduct data of $\mathrm{P'}$ and $\mathrm{Q'}$ defined as $\operatorname{mk}$ applied to the binary bicone of $\mathrm{eP}$ and $\mathrm{eQ}$ and $\operatorname{ofIso}$ applied to $\operatorname{isBilimit}$ applied to $d$, $\mathrm{eP}$ and $\mathrm{eQ}$.

the opposite of d (from the docstring)

Let $d$ be a binary biproduct data of $P$ and $Q$. Then the opposite of $d$ is a binary biproduct data of $\operatorname{op}$ applied to $P$ and $\operatorname{op}$ applied to $Q$ defined as $\operatorname{mk}$ applied to the opposite of the bicone of $d$ and the opposite of $\operatorname{isBilimit}$ applied to $d$.

Let $P$ and $Q$ be elements of $C$. Then we can say that $\operatorname{HasBinaryBiproduct}$ holds for $P$ and $Q$.

C has binary biproducts (from the name)

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

the biproduct of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the biproduct of $X$ and $Y$ is an element of $C$ defined as $\operatorname{pt}$ applied to the bicone of $X$ and $Y$.

the associator of Q and R (from the name)

Let $P$, $Q$ and $R$ be elements of $C$. Then the associator of $Q$ and $R$ is an isomorphism of the biproduct of the biproduct of $P$ and $Q$ and $R$ and the biproduct of $P$ and the biproduct of $Q$ and $R$.

the braiding of P and Q (from the name)

Let $P$ and $Q$ be elements of $C$. Then the braiding of $P$ and $Q$ is an isomorphism of the biproduct of $P$ and $Q$ and the biproduct of $Q$ and $P$.

the braiding of P and Q (from the name)

Let $P$ and $Q$ be elements of $C$. Then the braiding of $P$ and $Q$ is an isomorphism of the biproduct of $P$ and $Q$ and the biproduct of $Q$ and $P$.

Let $f$ be a homomorphism of $X$ and $W$. Let $g$ be a homomorphism of $Y$ and $W$. Then $\operatorname{desc}$ applied to $f$ and $g$ is a homomorphism of the biproduct of $X$ and $Y$ and $W$ defined as $\operatorname{desc}$ applied to the colimit cocone of $X$ and $Y$, $f$ and $g$.

the projection onto the first summand (from the docstring)

The projection onto the first summand is a homomorphism of the biproduct of $X$ and $Y$ and $X$ defined as the first component of the bicone of $X$ and $Y$.

the first component kernel fork of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the first component kernel fork of $X$ and $Y$ is a kernel fork of the projection onto the first summand defined as the first component kernel fork of the bicone of $X$ and $Y$.

the left injection (from the name)

The left injection is a homomorphism of $X$ and the biproduct of $X$ and $Y$ defined as the left injection of the bicone of $X$ and $Y$.

the left injection cokernel cofork of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the left injection cokernel cofork of $X$ and $Y$ is a cokernel cofork of the left injection defined as the left injection cokernel cofork of the bicone of $X$ and $Y$.

the right injection (from the name)

The right injection is a homomorphism of $Y$ and the biproduct of $X$ and $Y$ defined as the right injection of the bicone of $X$ and $Y$.

the right injection cokernel cofork of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the right injection cokernel cofork of $X$ and $Y$ is a cokernel cofork of the right injection defined as the right injection cokernel cofork of the bicone of $X$ and $Y$.

Let $X$ and $Y$ be elements of $C$. Then $\operatorname{isCokernelInlCokernelFork}$ applied to $X$ and $Y$ is an element of $\operatorname{IsColimit}$ applied to the left injection cokernel cofork of $X$ and $Y$ defined as $\operatorname{isColimitInlCokernelCofork}$ applied to the colimit cocone of $X$ and $Y$.

Let $X$ and $Y$ be elements of $C$. Then $\operatorname{isCokernelInrCokernelFork}$ applied to $X$ and $Y$ is an element of $\operatorname{IsColimit}$ applied to the right injection cokernel cofork of $X$ and $Y$ defined as $\operatorname{isColimitInrCokernelCofork}$ applied to the colimit cocone of $X$ and $Y$.

the fork of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $C$. Then the fork of $X$ and $Y$ is an element of $\operatorname{IsLimit}$ applied to the first component kernel fork of $X$ and $Y$ defined as $\operatorname{isLimitFstKernelFork}$ applied to the limit cone of $X$ and $Y$.

the fork of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $C$. Then the fork of $X$ and $Y$ is an element of $\operatorname{IsLimit}$ applied to the second component kernel fork of $X$ and $Y$ defined as $\operatorname{isLimitSndKernelFork}$ applied to the limit cone of $X$ and $Y$.

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

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

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

Let $X$ and $Y$ be elements of $C$. Then the isomorphism product of $X$ and $Y$ is an isomorphism of the biproduct of $X$ and $Y$ and the product of $X$ and $Y$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to the limit cone of $X$ and $Y$ and $\operatorname{isLimit}$ applied to the pair of $X$ and $Y$.

the lift of f and g (from the name)

Let $f$ be a homomorphism of $W$ and $X$. Let $g$ be a homomorphism of $W$ and $Y$. Then the lift of $f$ and $g$ is a homomorphism of $W$ and the biproduct of $X$ and $Y$ defined as the lift of $f$ and $g$.

the map of f and g (from the name)

Let $f$ be a homomorphism of $W$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the map of $f$ and $g$ is a homomorphism of the biproduct of $W$ and $X$ and the biproduct of $Y$ and $Z$ defined as the map of the limit cone of $Y$ and $Z$ and the map pair of $f$ and $g$.

the map of f and g (from the name)

Let $f$ be a homomorphism of $W$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the map of $f$ and $g$ is a homomorphism of the biproduct of $W$ and $X$ and the biproduct of $Y$ and $Z$ defined as the map of the cocone of the bicone of $Y$ and $Z$ and the map pair of $f$ and $g$.

the map isomorphism of f and g (from the name)

Let $f$ be an isomorphism of $W$ and $Y$. Let $g$ be an isomorphism of $X$ and $Z$. Then the map isomorphism of $f$ and $g$ is an isomorphism of the biproduct of $W$ and $X$ and the biproduct of $Y$ and $Z$.

the isomorphism of P and Q (from the docstring)

Let $P$ and $Q$ be elements of $C$. Then the isomorphism of $P$ and $Q$ is an isomorphism of $\operatorname{op}$ applied to the biproduct of $P$ and $Q$ and the biproduct of $\operatorname{op}$ applied to $P$ and $\operatorname{op}$ applied to $Q$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{op}$ applied to $P$, $\operatorname{op}$ applied to $Q$ and $\operatorname{isBilimit}$ applied to the opposite of $\operatorname{getBinaryBiproductData}$ applied to $P$ and $Q$.

the projection onto the second summand (from the docstring)

The projection onto the second summand is a homomorphism of the biproduct of $X$ and $Y$ and $Y$ defined as the second component of the bicone of $X$ and $Y$.

the second component kernel fork of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the second component kernel fork of $X$ and $Y$ is a kernel fork of the projection onto the second summand defined as the second component kernel fork of the bicone of $X$ and $Y$.

Let $X$ and $Y$ be elements of $C$. Let $\mathrm{hb}$ be an element of $\operatorname{IsBilimit}$ applied to $b$. Then $\operatorname{uniqueUpToIso}$ applied to $X$, $Y$ and $\mathrm{hb}$ is an isomorphism of $\operatorname{pt}$ applied to $b$ and the biproduct of $X$ and $Y$.

the biproduct isomorphism of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the biproduct isomorphism of $X$ and $Y$ is an isomorphism of the product of $X$ and $Y$ and the coproduct of $X$ and $Y$ defined as the composition of $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to the pair of $X$ and $Y$ and the limit cone of $X$ and $Y$ and $\operatorname{coconePointUniqueUpToIso}$ applied to the colimit cocone of $X$ and $Y$ and $\operatorname{isColimit}$ applied to the pair of $X$ and $Y$.

the cokernel biproduct left injection isomorphism (from the name)

The cokernel biproduct left injection isomorphism is an isomorphism of the cokernel of the left injection and $Y$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the left injection cokernel cofork of $X$ and $Y$ and $\operatorname{isCokernelInlCokernelFork}$ applied to $X$ and $Y$.

the cokernel biproduct right injection isomorphism (from the name)

The cokernel biproduct right injection isomorphism is an isomorphism of the cokernel of the right injection and $X$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the right injection cokernel cofork of $X$ and $Y$ and $\operatorname{isCokernelInrCokernelFork}$ applied to $X$ and $Y$.

Let $P$ and $Q$ be elements of $C$. Then $\operatorname{getBinaryBiproductData}$ applied to $P$ and $Q$ is a binary biproduct data of $P$ and $Q$ defined as $\operatorname{choice}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_HasBinaryBiproduct\_\_exists\_binary\_biproduct}$.

the isomorphism biproduct zero of hY (from the name)

Assume that $Y$ is a zero. Then the isomorphism biproduct zero of $\mathrm{hY}$ is an isomorphism of $X$ and the biproduct of $X$ and $Y$.

the isomorphism zero biproduct of hY (from the name)

Assume that $X$ is a zero. Then the isomorphism zero biproduct of $\mathrm{hY}$ is an isomorphism of $Y$ and the biproduct of $X$ and $Y$.

the kernel biproduct first component isomorphism (from the name)

The kernel biproduct first component isomorphism is an isomorphism of the kernel of the projection onto the first summand and $Y$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the first component kernel fork of $X$ and $Y$ and the fork of $X$ and $Y$.

the kernel biproduct second component isomorphism (from the name)

The kernel biproduct second component isomorphism is an isomorphism of the kernel of the projection onto the second summand and $X$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the second component kernel fork of $X$ and $Y$ and the fork of $X$ and $Y$.

binary cofan of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then a binary cofan of $X$ and $Y$ is an element of the function that maps $X$ and $Y$ to the set of cocones of the pair of $X$ and $Y$.

Let $h$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $f$ be a homomorphism of $X$ and $W$. Let $g$ be a homomorphism of $Y$ and $W$. Then $\operatorname{desc}$ applied to $h$, $f$ and $g$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $W$ defined as $\operatorname{desc}$ applied to $h$ and $\operatorname{mk}$ applied to $f$ and $g$.

Let $h$ be an element of $\operatorname{IsColimit}$ applied to $s$. Let $f$ be a homomorphism of $X$ and $W$. Let $g$ be a homomorphism of $Y$ and $W$. Then $\operatorname{desc'}$ applied to $h$, $f$ and $g$ is an element of $\SubtypeSet {l}{\mathrm{and} (\EqtMACRoH {\operatorname{comp} (\operatorname{inl} (s), l)}{f}, \EqtMACRoH {\operatorname{comp} (\operatorname{inr} (s), l)}{g})}$ defined as $\operatorname{desc}$ applied to $h$ and $\operatorname{mk}$ applied to $f$ and $g$.

Let $s$ be a binary cofan of $X$ and $Y$. Let $\mathrm{lift}$ be a function from elements $T_{3}$ of $C$ and homomorphisms of $X$ and $T_{3}$ and homomorphisms of $Y$ and $T_{3}$ to homomorphisms of $\operatorname{pt}$ applied to $s$ and $T_{3}$ such that for all elements $T_{2}$ of $C$, for all homomorphisms $f_{2}$ of $X$ and $T_{2}$, for all homomorphisms $g_{2}$ of $Y$ and $T_{2}$, the composition of the left injection of $s$ and $\mathrm{lift}$ applied to $T_{2}$, $f_{2}$ and $g_{2}$ is equal to $f_{2}$, for all elements $T_{1}$ of $C$, for all homomorphisms $f_{1}$ of $X$ and $T_{1}$, for all homomorphisms $g_{1}$ of $Y$ and $T_{1}$, the composition of the right injection of $s$ and $\mathrm{lift}$ applied to $T_{1}$, $f_{1}$ and $g_{1}$ is equal to $g_{1}$ and for all elements $T$ of $C$, for all homomorphisms $f$ of $X$ and $T$, for all homomorphisms $g$ of $Y$ and $T$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $s$ and $T$, if the composition of the left injection of $s$ and $m$ is equal to $f$, then if the composition of the right injection of $s$ and $m$ is equal to $g$, then $\EqtMACRoH {m}{\mathrm{lift} (T , f , g)}$. Then $\operatorname{mk}$ applied to $s$, $T_{3}$, $\mathrm{lift}$, $h$, $h_{1}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsColimit}$ applied to $s$.

the opposite of hc (from the name)

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

the opposite of hc (from the name)

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

the extension of e (from the name)

Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $\mathrm{c'}$ such that the left injection of $c$ is equal to the composition of the left injection of $\mathrm{c'}$ and the inverse of $e$ and the right injection of $c$ is equal to the composition of the right injection of $\mathrm{c'}$ and the inverse of $e$. Then the extension of $e$ is an isomorphism of $c$ and $\mathrm{c'}$.

the left injection of s (from the name)

Let $s$ be a binary cofan of $X$ and $Y$. Then the left injection of $s$ is a homomorphism of $X$ and $\operatorname{pt}$ applied to $s$ defined as the component of the inclusion of $s$ and $\operatorname{mk}$ applied to the left.

the right injection of s (from the name)

Let $s$ be a binary cofan of $X$ and $Y$. Then the right injection of $s$ is a homomorphism of $Y$ and $\operatorname{pt}$ applied to $s$ defined as the component of the inclusion of $s$ and $\operatorname{mk}$ applied to the right.

Let $c$ be a binary cofan of $X$ and $Y$. Let $f$ be a homomorphism of $\mathrm{X'}$ and $X$. Let $h_{1}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitCompLeftIso}$ applied to $c$, $f$ and $h_{1}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the composition of $f$ and the left injection of $c$ and the right injection of $c$.

Let $c$ be a binary cofan of $X$ and $Y$. Let $f$ be a homomorphism of $\mathrm{Y'}$ and $Y$. Let $h_{1}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitCompRightIso}$ applied to $c$, $f$ and $h_{1}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the left injection of $c$ and the composition of $f$ and the right injection of $c$ defined as $\operatorname{isColimitFlip}$ applied to $\operatorname{isColimitCompLeftIso}$ applied to $\operatorname{mk}$ applied to the right injection of $c$ and the left injection of $c$, $f$ and $\operatorname{isColimitFlip}$ applied to $h_{1}$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitFlip}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the right injection of $c$ and the left injection of $c$.

$\operatorname{isColimitMapCoconeEquiv}$ is an equivalence from $\operatorname{IsColimit}$ applied to the map cocone of $F$ and $s$ to $\operatorname{IsColimit}$ applied to the map of $F$ and $s$.

Let $\mathrm{lift}$ be a function from binary cofans $s_{3}$ of $X$ and $Y$ to homomorphisms of $W$ and $\operatorname{pt}$ applied to $s_{3}$ such that for all binary cofans $s_{2}$ of $X$ and $Y$, the composition of $\mathrm{fst}$ and $\mathrm{lift}$ applied to $s_{2}$ is equal to the left injection of $s_{2}$, for all binary cofans $s_{1}$ of $X$ and $Y$, the composition of $\mathrm{snd}$ and $\mathrm{lift}$ applied to $s_{1}$ is equal to the right injection of $s_{1}$ and for all binary cofans $s$ of $X$ and $Y$, for all homomorphisms $m$ of $W$ and $\operatorname{pt}$ applied to $s$, if the composition of $\mathrm{fst}$ and $m$ is equal to the left injection of $s$, then if the composition of $\mathrm{snd}$ and $m$ is equal to the right injection of $s$, then $\EqtMACRoH {m}{\mathrm{lift} (s)}$. Then $\operatorname{isColimitMk}$ applied to $s_{3}$, $\mathrm{lift}$, $\mathrm{fac\_left}$, $\mathrm{fac\_right}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $\mathrm{fst}$ and $\mathrm{snd}$.

the map of F and s (from the name)

Let $F$ be a functor of $C$ and $D$. Let $s$ be a binary cofan of $X$ and $Y$. Then the map of $F$ and $s$ is a binary cofan of the action of $F$ and $X$ and the action of $F$ and $Y$ defined as $\operatorname{mk}$ applied to the map of $F$ and the left injection of $s$ and the map of $F$ and the right injection of $s$.

Let $x_{1}$ be a homomorphism of $X$ and $P$. Let $x_{2}$ be a homomorphism of $Y$ and $P$. Then $\operatorname{mk}$ applied to $x_{1}$ and $x_{2}$ is a binary cofan of $X$ and $Y$.

the opposite of c (from the name)

Let $c$ be a binary cofan of $X$ and $Y$. Then the opposite of $c$ is an element of $\operatorname{BinaryFan}$ applied to $\operatorname{op}$ applied to $X$ and $\operatorname{op}$ applied to $Y$ defined as $\operatorname{mk}$ applied to the opposite in the left injection of $c$ and the opposite in the right injection of $c$.

the opposite of c (from the name)

Let $c$ be a binary cofan of $\operatorname{op}$ applied to $X$ and $\operatorname{op}$ applied to $Y$. Then the opposite of $c$ is an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$ defined as $\operatorname{mk}$ applied to the opposite of the left injection of $c$ and the opposite of the right injection of $c$.

Let $X$ and $Y$ be elements of $C$. Then an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$ is an element of the function that maps $X$ and $Y$ to the set of cones of the pair of $X$ and $Y$.

the lift of f and g (from the name)

Let $h$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $f$ be a homomorphism of $W$ and $X$. Let $g$ be a homomorphism of $W$ and $Y$. Then the lift of $f$ and $g$ is a homomorphism of $W$ and $\operatorname{pt}$ applied to $s$ defined as the lift of $h$ and $\operatorname{mk}$ applied to $f$ and $g$.

the lift of f and g (from the name)

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

Let $s$ be an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$. Let $\mathrm{lift}$ be a function from elements $T_{3}$ of $C$ and homomorphisms of $T_{3}$ and $X$ and homomorphisms of $T_{3}$ and $Y$ to homomorphisms of $T_{3}$ and $\operatorname{pt}$ applied to $s$ such that for all elements $T_{2}$ of $C$, for all homomorphisms $f_{2}$ of $T_{2}$ and $X$, for all homomorphisms $g_{2}$ of $T_{2}$ and $Y$, the composition of $\mathrm{lift}$ applied to $T_{2}$, $f_{2}$ and $g_{2}$ and the first projection of $s$ is equal to $f_{2}$, for all elements $T_{1}$ of $C$, for all homomorphisms $f_{1}$ of $T_{1}$ and $X$, for all homomorphisms $g_{1}$ of $T_{1}$ and $Y$, the composition of $\mathrm{lift}$ applied to $T_{1}$, $f_{1}$ and $g_{1}$ and the second projection of $s$ is equal to $g_{1}$ and for all elements $T$ of $C$, for all homomorphisms $f$ of $T$ and $X$, for all homomorphisms $g$ of $T$ and $Y$, for all homomorphisms $m$ of $T$ and $\operatorname{pt}$ applied to $s$, if the composition of $m$ and the first projection of $s$ is equal to $f$, then if the composition of $m$ and the second projection of $s$ is equal to $g$, then $\EqtMACRoH {m}{\mathrm{lift} (T , f , g)}$. Then $\operatorname{mk}$ applied to $s$, $T_{3}$, $\mathrm{lift}$, $h$, $h_{1}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsLimit}$ applied to $s$.

the opposite of hc (from the name)

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

the opposite of hc (from the name)

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

the associator of Q and s (from the name)

Let $Q$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{sYZ}$. Let $s$ be an element of $\operatorname{BinaryFan}$ applied to $\operatorname{pt}$ applied to $\mathrm{sXY}$ and $Z$. Then the associator of $Q$ and $s$ is an element of $\operatorname{BinaryFan}$ applied to $X$ and $\operatorname{pt}$ applied to $\mathrm{sYZ}$ defined as $\operatorname{mk}$ applied to the composition of the first projection of $s$ and the first projection of $\mathrm{sXY}$ and the lift of $Q$ and $\operatorname{mk}$ applied to the composition of the first projection of $s$ and the second projection of $\mathrm{sXY}$ and the second projection of $s$.

the associator inverse of P and s (from the name)

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{sXY}$. Let $s$ be an element of $\operatorname{BinaryFan}$ applied to $X$ and $\operatorname{pt}$ applied to $\mathrm{sYZ}$. Then the associator inverse of $P$ and $s$ is an element of $\operatorname{BinaryFan}$ applied to $\operatorname{pt}$ applied to $\mathrm{sXY}$ and $Z$ defined as $\operatorname{mk}$ applied to the lift of the first projection of $s$ and the composition of the second projection of $s$ and the first projection of $\mathrm{sYZ}$ and the composition of the second projection of $s$ and the second projection of $\mathrm{sYZ}$.

the associator of R and S (from the name)

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{sXY}$. Let $Q$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{sYZ}$. Let $R$ be an element of $\operatorname{IsLimit}$ applied to $s$. Let $S$ be an element of $\operatorname{IsLimit}$ applied to $t$. Then the associator of $R$ and $S$ is an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to the associator of $Q$ and $R$ and $S$.

the associator of Y1 and X (from the name)

Let $L$ be a function from elements $X_{1}$ of $C$ and elements $Y_{1}$ of $C$ to limit cones of the pair of $X_{1}$ and $Y_{1}$. Let $X$, $Y$ and $Z$ be elements of $C$. Then the associator of $L$ and $X$ is an isomorphism of $\operatorname{pt}$ applied to the cone of $L$ applied to $\operatorname{pt}$ applied to the cone of $L$ applied to $X$ and $Y$ and $Z$ and $\operatorname{pt}$ applied to the cone of $L$ applied to $X$ and $\operatorname{pt}$ applied to the cone of $L$ applied to $Y$ and $Z$ defined as the function that maps $Y$ and $Z$ to the associator of $\operatorname{isLimit}$ applied to $X_{1}$ applied to $\operatorname{pt}$ applied to the cone of $X_{1}$ applied to $Y_{1}$ and $L$ and $X$ and $\operatorname{isLimit}$ applied to $X_{1}$ applied to $Y_{1}$ and $\operatorname{pt}$ applied to the cone of $X_{1}$ applied to $L$ and $X$.

the braiding of P and Q (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$. Then the braiding of $P$ and $Q$ is an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $P$ and $\operatorname{binaryFanSwap}$ applied to $Q$.

the extension of e (from the name)

Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $\mathrm{c'}$ such that the first projection of $c$ is equal to the composition of the homomorphism of $e$ and the first projection of $\mathrm{c'}$ and the second projection of $c$ is equal to the composition of the homomorphism of $e$ and the second projection of $\mathrm{c'}$. Then the extension of $e$ is an isomorphism of $c$ and $\mathrm{c'}$.

the first projection of s (from the docstring)

Let $s$ be an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$. Then the first projection of $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $X$ defined as the component of the projection of $s$ and $\operatorname{mk}$ applied to the left.

Let $c$ be an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$. Let $f$ be a homomorphism of $X$ and $\mathrm{X'}$. Let $h_{1}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitCompLeftIso}$ applied to $c$, $f$ and $h_{1}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the composition of the first projection of $c$ and $f$ and the second projection of $c$.

Let $c$ be an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$. Let $f$ be a homomorphism of $Y$ and $\mathrm{Y'}$. Let $h_{1}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitCompRightIso}$ applied to $c$, $f$ and $h_{1}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the first projection of $c$ and the composition of the second projection of $c$ and $f$ defined as $\operatorname{isLimitFlip}$ applied to $\operatorname{isLimitCompLeftIso}$ applied to $\operatorname{mk}$ applied to the second projection of $c$ and the first projection of $c$, $f$ and $\operatorname{isLimitFlip}$ applied to $h_{1}$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitFlip}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the second projection of $c$ and the first projection of $c$.

$\operatorname{isLimitMapConeEquiv}$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $F$ and $s$ to $\operatorname{IsLimit}$ applied to the map of $F$ and $s$.

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

the left unitor of P and Q (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$. Then the left unitor of $P$ and $Q$ is an isomorphism of $\operatorname{pt}$ applied to $t$ and $X$.

the map of F and s (from the name)

Let $F$ be a functor of $C$ and $D$. Let $s$ be an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$. Then the map of $F$ and $s$ is an element of $\operatorname{BinaryFan}$ applied to the action of $F$ and $X$ and the action of $F$ and $Y$ defined as $\operatorname{mk}$ applied to the map of $F$ and the first projection of $s$ and the map of $F$ and the second projection of $s$.

Let $x_{1}$ be a homomorphism of $P$ and $X$. Let $x_{2}$ be a homomorphism of $P$ and $Y$. Then $\operatorname{mk}$ applied to $x_{1}$ and $x_{2}$ is an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$.

the opposite of c (from the name)

Let $c$ be an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$. Then the opposite of $c$ is a binary cofan of $\operatorname{op}$ applied to $X$ and $\operatorname{op}$ applied to $Y$ defined as $\operatorname{mk}$ applied to the opposite in the first projection of $c$ and the opposite in the second projection of $c$.

the right unitor of P and Q (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$. Then the right unitor of $P$ and $Q$ is an isomorphism of $\operatorname{pt}$ applied to $t$ and $X$.

the second projection of s (from the docstring)

Let $s$ be an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$. Then the second projection of $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $Y$ defined as the component of the projection of $s$ and $\operatorname{mk}$ applied to the right.

the swap of s (from the name)

Let $s$ be an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$. Then the swap of $s$ is an element of $\operatorname{BinaryFan}$ applied to $Y$ and $X$ defined as $\operatorname{mk}$ applied to the second projection of $s$ and the first projection of $s$.

the opposite of c (from the name)

Let $c$ be an element of $\operatorname{BinaryFan}$ applied to $\operatorname{op}$ applied to $X$ and $\operatorname{op}$ applied to $Y$. Then the opposite of $c$ is a binary cofan of $X$ and $Y$ defined as $\operatorname{mk}$ applied to the opposite of the first projection of $c$ and the opposite of the second projection of $c$.

the associator of Q and R (from the name)

Let $P$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{sXY}$. Let $Q$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{sYZ}$. Let $R$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then the associator of $Q$ and $R$ is an element of $\operatorname{IsLimit}$ applied to the associator of $Q$ and $s$.

Let $I$ be an element of $\operatorname{IsLimit}$ applied to $s$. Then $\operatorname{binaryFanSwap}$ applied to $I$ is an element of $\operatorname{IsLimit}$ applied to the swap of $s$.

the isomorphism binary cofan of c (from the name)

Let $c$ be a binary cofan of $X$ and $Y$. Then the isomorphism binary cofan of $c$ is an isomorphism of $c$ and $\operatorname{mk}$ applied to the left injection of $c$ and the right injection of $c$.

Let $c$ be an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$. Then $\operatorname{isoBinaryFanMk}$ applied to $c$ is an isomorphism of $c$ and $\operatorname{mk}$ applied to the first projection of $c$ and the second projection of $c$.

Let $X$ and $Y$ be elements of $C$. Then $\operatorname{HasBinaryCoproduct}$ holds for $X$ and $Y$, if the pair of $X$ and $Y$ has colimits.

C has binary coproducts (from the name)

Let $C$ be a set. Then $C$ has binary coproducts, if $\operatorname{HasColimitsOfShape}$ holds for $\operatorname{Discrete}$ applied to the set of walking pairs and $C$.

Let $X$ and $Y$ be elements of $C$. Then $\operatorname{HasBinaryProduct}$ holds for $X$ and $Y$, if the pair of $X$ and $Y$ has limits.

C has binary products (from the name)

Let $C$ be a set. Then $C$ has binary products, if $\operatorname{HasLimitsOfShape}$ holds for $\operatorname{Discrete}$ applied to the set of walking pairs and $C$.

Let $X$ be an element of $C$. Then $\operatorname{codiag}$ applied to $X$ is a homomorphism of the coproduct of $X$ and $X$ and $X$ defined as $\operatorname{desc}$ applied to the identity morphism of $X$ and the identity morphism of $X$.

the coproduct of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the coproduct of $X$ and $Y$ is an element of $C$ defined as the colimit of the pair of $X$ and $Y$.

the associator of Q and R (from the name)

Let $P$, $Q$ and $R$ be elements of $C$. Then the associator of $Q$ and $R$ is an isomorphism of the coproduct of the coproduct of $P$ and $Q$ and $R$ and the coproduct of $P$ and the coproduct of $Q$ and $R$.

the braiding of P and Q (from the name)

Let $P$ and $Q$ be elements of $C$. Then the braiding of $P$ and $Q$ is an isomorphism of the coproduct of $P$ and $Q$ and the coproduct of $Q$ and $P$.

Let $f$ be a homomorphism of $X$ and $W$. Let $g$ be a homomorphism of $Y$ and $W$. Then $\operatorname{desc}$ applied to $f$ and $g$ is a homomorphism of the coproduct of $X$ and $Y$ and $W$ defined as $\operatorname{desc}$ applied to the pair of $X$ and $Y$ and $\operatorname{mk}$ applied to $f$ and $g$.

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

the binary coproduct functor (from the docstring)

The binary coproduct functor is a functor of $C$ and the set of functors of $C$ and $C$.

the functor left composition of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the functor left composition of $X$ and $Y$ is an isomorphism of the action of the binary coproduct functor and the coproduct of $X$ and $Y$ and the composition of the action of the binary coproduct functor and $Y$ and the action of the binary coproduct functor and $X$.

the left injection (from the name)

The left injection is a homomorphism of $X$ and the coproduct of $X$ and $Y$ defined as the inclusion of the pair of $X$ and $Y$ and $\operatorname{mk}$ applied to the left.

the right injection (from the name)

The right injection is a homomorphism of $Y$ and the coproduct of $X$ and $Y$ defined as the inclusion of the pair of $X$ and $Y$ and $\operatorname{mk}$ applied to the right.

the left unitor of P (from the name)

Let $P$ be an element of $C$. Then the left unitor of $P$ is an isomorphism of the coproduct of $\operatorname{initial}$ applied to $C$ and $P$ and $P$.

the map of f and g (from the name)

Let $f$ be a homomorphism of $Y$ and $W$. Let $g$ be a homomorphism of $Z$ and $X$. Then the map of $f$ and $g$ is a homomorphism of the coproduct of $Y$ and $Z$ and the coproduct of $W$ and $X$ defined as the colimit map of the map pair of $f$ and $g$.

the map isomorphism of f and g (from the name)

Let $f$ be an isomorphism of $W$ and $Y$. Let $g$ be an isomorphism of $X$ and $Z$. Then the map isomorphism of $f$ and $g$ is an isomorphism of the coproduct of $W$ and $X$ and the coproduct of $Y$ and $Z$.

the right unitor of P (from the name)

Let $P$ be an element of $C$. Then the right unitor of $P$ is an isomorphism of the coproduct of $P$ and $\operatorname{initial}$ applied to $C$ and $P$.

Let $X$ and $Y$ be elements of $C$. Then $\operatorname{coprodIsCoprod}$ applied to $X$ and $Y$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the left injection and the right injection.

the diagonal of X (from the name)

Let $X$ be an element of $C$. Then the diagonal of $X$ is a homomorphism of $X$ and the product of $X$ and $X$ defined as the lift of the identity morphism of $X$ and the identity morphism of $X$.

the product of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the product of $X$ and $Y$ is an element of $C$ defined as the limit of the pair of $X$ and $Y$.

the associator of Q and R (from the name)

Let $P$, $Q$ and $R$ be elements of $C$. Then the associator of $Q$ and $R$ is an isomorphism of the product of the product of $P$ and $Q$ and $R$ and the product of $P$ and the product of $Q$ and $R$.

the braiding of P and Q (from the name)

Let $P$ and $Q$ be elements of $C$. Then the braiding of $P$ and $Q$ is an isomorphism of the product of $P$ and $Q$ and the product of $Q$ and $P$.

the projection map to the first component of the product (from the docstring)

The projection map to the first component of the product is a homomorphism of the product of $X$ and $Y$ and $X$ defined as the projection from the limit object to a value of the functor of the pair of $X$ and $Y$ and $\operatorname{mk}$ applied to the left.

the binary product functor (from the docstring)

The binary product functor is a functor of $C$ and the set of functors of $C$ and $C$.

the functor left composition of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the functor left composition of $X$ and $Y$ is an isomorphism of the action of the binary product functor and the product of $X$ and $Y$ and the composition of the action of the binary product functor and $Y$ and the action of the binary product functor and $X$.

the left unitor of P (from the name)

Let $P$ be an element of $C$. Then the left unitor of $P$ is an isomorphism of the product of $\operatorname{terminal}$ applied to $C$ and $P$ and $P$.

the lift of f and g (from the name)

Let $f$ be a homomorphism of $W$ and $X$. Let $g$ be a homomorphism of $W$ and $Y$. Then the lift of $f$ and $g$ is a homomorphism of $W$ and the product of $X$ and $Y$ defined as the lift of the pair of $X$ and $Y$ and $\operatorname{mk}$ applied to $f$ and $g$.

the lift of f and g (from the name)

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

the map of f and g (from the name)

Let $f$ be a homomorphism of $W$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the map of $f$ and $g$ is a homomorphism of the product of $W$ and $X$ and the product of $Y$ and $Z$ defined as the limit map of the map pair of $f$ and $g$.

the map isomorphism of f and g (from the name)

Let $f$ be an isomorphism of $W$ and $Y$. Let $g$ be an isomorphism of $X$ and $Z$. Then the map isomorphism of $f$ and $g$ is an isomorphism of the product of $W$ and $X$ and the product of $Y$ and $Z$.

the right unitor of P (from the name)

Let $P$ be an element of $C$. Then the right unitor of $P$ is an isomorphism of the product of $P$ and $\operatorname{terminal}$ applied to $C$ and $P$.

the projection map to the second component of the product (from the docstring)

The projection map to the second component of the product is a homomorphism of the product of $X$ and $Y$ and $Y$ defined as the projection from the limit object to a value of the functor of the pair of $X$ and $Y$ and $\operatorname{mk}$ applied to the right.

Let $X$ and $Y$ be elements of $C$. Then $\operatorname{prodIsProd}$ applied to $X$ and $Y$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the projection map to the first component of the product and the projection map to the second component of the product.

the coproduct (from the name)

The coproduct is a functor of $\operatorname{Over}$ applied to $A$ and the set of functors of $\operatorname{Over}$ applied to $A$ and $\operatorname{Over}$ applied to $A$.

the coproduct comparison of A and B (from the name)

Let $F$ be a functor of $C$ and $D$. Let $A$ and $B$ be elements of $C$. Then the coproduct comparison of $A$ and $B$ is a homomorphism of the coproduct of the action of $F$ and $A$ and the action of $F$ and $B$ and the action of $F$ and the coproduct of $A$ and $B$ defined as $\operatorname{desc}$ applied to the map of $F$ and the left injection and the map of $F$ and the right injection.

the natural isomorphism of F and A (from the docstring)

Let $F$ be a functor of $C$ and $D$. Let $A$ be an element of $C$. Then the natural isomorphism of $F$ and $A$ is an isomorphism of the composition of the action of the binary coproduct functor and $A$ and $F$ and the composition of $F$ and the action of the binary coproduct functor and the action of $F$ and $A$.

the coproduct comparison natural transformation of F and A (from the name)

Let $F$ be a functor of $C$ and $D$. Let $A$ be an element of $C$. Then the coproduct comparison natural transformation of $F$ and $A$ is a homomorphism of the composition of $F$ and the action of the binary coproduct functor and the action of $F$ and $A$ and the composition of the action of the binary coproduct functor and $A$ and $F$.

the product comparison of A and B (from the name)

Let $F$ be a functor of $C$ and $D$. Let $A$ and $B$ be elements of $C$. Then the product comparison of $A$ and $B$ is a homomorphism of the action of $F$ and the product of $A$ and $B$ and the product of the action of $F$ and $A$ and the action of $F$ and $B$ defined as the lift of the map of $F$ and the projection map to the first component of the product and the map of $F$ and the projection map to the second component of the product.

the natural isomorphism of F and A (from the docstring)

Let $F$ be a functor of $C$ and $D$. Let $A$ be an element of $C$. Then the natural isomorphism of $F$ and $A$ is an isomorphism of the composition of the action of the binary product functor and $A$ and $F$ and the composition of $F$ and the action of the binary product functor and the action of $F$ and $A$.

the product comparison natural transformation of F and A (from the name)

Let $F$ be a functor of $C$ and $D$. Let $A$ be an element of $C$. Then the product comparison natural transformation of $F$ and $A$ is a homomorphism of the composition of the action of the binary product functor and $A$ and $F$ and the composition of $F$ and the action of the binary product functor and the action of $F$ and $A$.

walking pair (from the name)

The walking pairs are a basic type.

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

the equivalence bool (from the name)

The equivalence bool is an equivalence from the set of walking pairs to $\mathrm{Bool}$.

the left (from the name)

The left is a walking pair.

the walking pair of x (from the name)

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

the right (from the name)

The right is a walking pair.

the swap (from the name)

The swap is an equivalence from the set of walking pairs to the set of walking pairs.

the diagram isomorphism pair of F (from the name)

Let $F$ be a functor of $\operatorname{Discrete}$ applied to the set of walking pairs and $C$. Then the diagram isomorphism pair of $F$ is an isomorphism of $F$ and the pair of the action of $F$ and $\operatorname{mk}$ applied to the left and the action of $F$ and $\operatorname{mk}$ applied to the right defined as the map pair isomorphism of the identity of the action of $F$ and $\operatorname{mk}$ applied to the left and the identity of the action of $F$ and $\operatorname{mk}$ applied to the right.

the default (from the name)

The default is a walking pair defined as the left.

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

Let $f$ be a homomorphism of the action of $F$ and $\operatorname{mk}$ applied to the left and the action of $G$ and $\operatorname{mk}$ applied to the left. Let $g$ be a homomorphism of the action of $F$ and $\operatorname{mk}$ applied to the right and the action of $G$ and $\operatorname{mk}$ applied to the right. Then the map pair of $f$ and $g$ is a homomorphism of $F$ and $G$.

the map pair isomorphism of f and g (from the name)

Let $f$ be an isomorphism of the action of $F$ and $\operatorname{mk}$ applied to the left and the action of $G$ and $\operatorname{mk}$ applied to the left. Let $g$ be an isomorphism of the action of $F$ and $\operatorname{mk}$ applied to the right and the action of $G$ and $\operatorname{mk}$ applied to the right. Then the map pair isomorphism of $f$ and $g$ is an isomorphism of $F$ and $G$.

the pair of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the pair of $X$ and $Y$ is a functor of $\operatorname{Discrete}$ applied to the set of walking pairs and $C$.

the pair composition of Y and F (from the name)

Let $X$ and $Y$ be elements of $C$. Let $F$ be a functor of $C$ and $D$. Then the pair composition of $Y$ and $F$ is an isomorphism of the composition of the pair of $X$ and $Y$ and $F$ and the pair of the action of $F$ and $X$ and the action of $F$ and $Y$ defined as the diagram isomorphism pair of the composition of the pair of $X$ and $Y$ and $F$.

the pair function of Y and x (from the name)

Let $X$ and $Y$ be elements of $C$. Let $x$ be a walking pair. Then the pair function of $Y$ and $x$ is an element of $C$.

bicone of F (from the name)

Let $F$ be a function from elements of $J$ to elements of $C$. Then the bicones of $F$ are a basic type.

Let $B$ be a bicone of $F$. Then the elements of $\operatorname{IsBilimit}$ applied to $B$ are a basic type.

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

Let $\mathrm{self}$ be an element of $\operatorname{IsBilimit}$ applied to $B$. Then $\operatorname{isLimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to the cone of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the bicone of ht (from the name)

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

the bicone of ht (from the name)

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

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

the retract of B and j (from the docstring)

Let $B$ be a bicone of $F$. Let $j$ be an element of $J$. Then the retract of $B$ and $j$ is a retract of $F$ applied to $j$ and $\operatorname{pt}$ applied to $B$.

the cocone of B (from the name)

Let $B$ be a bicone of $F$. Then the cocone of $B$ is a cocone of the functor of $F$ defined as the action of the cocone functor and $B$.

the cocone functor (from the name)

The cocone functor is a functor of the set of bicones of $F$ and the set of cocones of the functor of $F$.

the cone of B (from the name)

Let $B$ be a bicone of $F$. Then the cone of $B$ is a cone of the functor of $F$ defined as the action of the cone functor and $B$.

the cone functor (from the name)

The cone functor is a functor of the set of bicones of $F$ and the set of cones of the functor of $F$.

the whisker of c and g (from the name)

Let $c$ be a bicone of $f$. Let $g$ be an equivalence from $K$ to $J$. Then the whisker of $c$ and $g$ is a bicone of $\operatorname{comp}$ applied to $f$ and $\operatorname{coe}$ applied to $g$.

Let $c$ be a bicone of $f$. Let $g$ be an equivalence from $K$ to $J$. Then $\operatorname{whiskerIsBilimitIff}$ applied to $c$ and $g$ is an equivalence from $\operatorname{IsBilimit}$ applied to the whisker of $c$ and $g$ to $\operatorname{IsBilimit}$ applied to $c$ defined as the equivalence of the function that maps $\mathrm{hc}$ to $\operatorname{mk}$ applied to $\operatorname{ofWhiskerEquivalence}$ applied to the equivalence of $g$ and $\operatorname{postcomposeHomEquiv}$ applied to the inverse of the functor composition of $f$ and $\operatorname{coe}$ applied to $g$, the whisker of the functor of $\operatorname{comp}$ applied to $\operatorname{mk}$ and $\operatorname{coe}$ applied to $g$ and the cone of $c$ and $\operatorname{ofIsoLimit}$ applied to $\operatorname{isLimit}$ applied to $\mathrm{hc}$ and the whisker to cone of $c$ and $g$ and $\operatorname{ofWhiskerEquivalence}$ applied to the equivalence of $g$ and $\operatorname{precomposeHomEquiv}$ applied to the functor composition of $f$ and $\operatorname{coe}$ applied to $g$, the whisker of the functor of $\operatorname{comp}$ applied to $\operatorname{mk}$ and $\operatorname{coe}$ applied to $g$ and the cocone of $c$ and $\operatorname{ofIsoColimit}$ applied to $\operatorname{isColimit}$ applied to $\mathrm{hc}$ and the whisker to cocone of $c$ and $g$ and the function that maps $\mathrm{hc1}$ to $\operatorname{mk}$ applied to $\operatorname{ofIsoLimit}$ applied to $\operatorname{symm}$ applied to the postcomposition homomorphism equivalence of the inverse of the functor composition of $f$ and $\operatorname{coe}$ applied to $g$ and the whisker of the functor of $\operatorname{comp}$ applied to $\operatorname{mk}$ and $\operatorname{coe}$ applied to $g$ and the cone of $c$ and the whisker equivalence of $\operatorname{isLimit}$ applied to $\mathrm{hc1}$ and the equivalence of $g$ and the inverse of the whisker to cone of $c$ and $g$ and $\operatorname{ofIsoColimit}$ applied to $\operatorname{symm}$ applied to the precomposition homomorphism equivalence of the functor composition of $f$ and $\operatorname{coe}$ applied to $g$ and the whisker of the functor of $\operatorname{comp}$ applied to $\operatorname{mk}$ and $\operatorname{coe}$ applied to $g$ and the cocone of $c$ and the whisker equivalence of $\operatorname{isColimit}$ applied to $\mathrm{hc1}$ and the equivalence of $g$ and the inverse of the whisker to cocone of $c$ and $g$.

the whisker to cocone of c and g (from the name)

Let $c$ be a bicone of $f$. Let $g$ be an equivalence from $K$ to $J$. Then the whisker to cocone of $c$ and $g$ is an isomorphism of the cocone of the whisker of $c$ and $g$ and the action of the precomposition of the homomorphism of the functor composition of $f$ and $\operatorname{coe}$ applied to $g$ and the whisker of the functor of $\operatorname{comp}$ applied to $\operatorname{mk}$ and $\operatorname{coe}$ applied to $g$ and the cocone of $c$.

the whisker to cone of c and g (from the name)

Let $c$ be a bicone of $f$. Let $g$ be an equivalence from $K$ to $J$. Then the whisker to cone of $c$ and $g$ is an isomorphism of the cone of the whisker of $c$ and $g$ and the action of the postcomposition of the inverse of the functor composition of $f$ and $\operatorname{coe}$ applied to $g$ and the whisker of the functor of $\operatorname{comp}$ applied to $\operatorname{mk}$ and $\operatorname{coe}$ applied to $g$ and the cone of $c$.

the inclusion of self and j (from the name)

Let $\mathrm{self}$ be a bicone of $F$. Let $j$ be an element of $J$. Then the inclusion of $\mathrm{self}$ and $j$ is a homomorphism of $F$ applied to $j$ and $\operatorname{pt}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $j$.

the projection of self and j (from the name)

Let $\mathrm{self}$ be a bicone of $F$. Let $j$ be an element of $J$. Then the projection of $\mathrm{self}$ and $j$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{self}$ and $F$ applied to $j$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $j$.

bicone morphism of A and B (from the name)

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

the homomorphism of self (from the name)

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

the extension of x2 (from the name)

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

the functoriality of F and G (from the name)

Let $F$ be a function from elements of $J$ to elements of $C$. Let $G$ be a functor of $C$ and $D$. Then the functoriality of $F$ and $G$ is a functor of the set of bicones of $F$ and the set of bicones of $\operatorname{comp}$ applied to $\operatorname{obj}$ applied to $G$ and $F$.

F has biproducts (from the name)

Let $F$ be a function from elements of $J$ to elements of $C$. Then we can say that $F$ has biproducts.

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

the colimit isomorphism limit (from the name)

The colimit isomorphism limit is an isomorphism of the colimit and the limit.

C has finite biproducts (from the name)

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

limit bicone of F (from the name)

Let $F$ be a function from elements of $J$ to elements of $C$. Then the limit bicones of $F$ are a basic type.

the bicone of self (from the name)

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

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

the biproduct of f (from the name)

Let $f$ be a function from elements of $J$ to elements of $C$. Then the biproduct of $f$ is an element of $C$ defined as $\operatorname{pt}$ applied to the bicone of $f$.

the bicone of F (from the name)

Let $F$ be a function from elements of $J$ to elements of $C$. Then the bicone of $F$ is a bicone of $F$ defined as the bicone of $\operatorname{getBiproductData}$ applied to $F$.

the component of j and k (from the name)

Let $m$ be a homomorphism of the biproduct of $f$ and the biproduct of $g$. Let $j$ be an element of $J$. Let $k$ be an element of $K$. Then the component of $j$ and $k$ is a homomorphism of $f$ applied to $j$ and $g$ applied to $k$ defined as the composition of the inclusion into a summand of $f$ and $j$ and the composition of $m$ and the projection onto a summand of $g$ and $k$.

Let $p$ be a function from elements $b$ of $J$ to homomorphisms of $f$ applied to $b$ and $P$. Then $\operatorname{desc}$ applied to $b$ and $p$ is a homomorphism of the biproduct of $f$ and $P$ defined as the function that maps $p$ to $\operatorname{desc}$ applied to the colimit cocone of $f$, $\operatorname{mk}$ applied to $P$ and $b$ and $p$.

Let $f$ be a function from elements of $J$ to elements of $C$. Let $p$ be a function from elements of $J$ to propositions. Then $\operatorname{fromSubtype}$ applied to $f$ and $p$ is a homomorphism of the biproduct of $\operatorname{restrict}$ applied to $p$ and $f$ and the biproduct of $f$ defined as $\operatorname{desc}$ applied to the function that maps $j$ to the inclusion into a summand of $f$ and $j$.

the bilimit bicone of F (from the docstring)

Let $F$ be a function from elements of $J$ to elements of $C$. Then the bilimit bicone of $F$ is an element of $\operatorname{IsBilimit}$ applied to the bicone of $F$ defined as $\operatorname{isBilimit}$ applied to $\operatorname{getBiproductData}$ applied to $F$.

the colimit cocone of F (from the docstring)

Let $F$ be a function from elements of $J$ to elements of $C$. Then the colimit cocone of $F$ is an element of $\operatorname{IsColimit}$ applied to the cocone of the bicone of $F$ defined as $\operatorname{isColimit}$ applied to $\operatorname{isBilimit}$ applied to $\operatorname{getBiproductData}$ applied to $F$.

Let $f$ be a function from elements of $J$ to elements of $C$. Let $i$ be an element of $J$. Then $\operatorname{isColimitToSubtype}$ applied to $f$ and $i$ is an element of $\operatorname{IsColimit}$ applied to the projection of the subtype of $f$ and the function that maps $j$ to $\mathrm{Neq} (j , i)$ and $\mathrm{CategoryTheory\_\_Limits\_\_biproduct\_\_isColimitToSubtype\_\_\_proof\_1}$ applied to $f$ and $i$.

the limit cone of F (from the docstring)

Let $F$ be a function from elements of $J$ to elements of $C$. Then the limit cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the cone of the bicone of $F$ defined as $\operatorname{isLimit}$ applied to $\operatorname{isBilimit}$ applied to $\operatorname{getBiproductData}$ applied to $F$.

Let $f$ be a function from elements of $J$ to elements of $C$. Let $i$ be an element of $J$. Then $\operatorname{isLimitFromSubtype}$ applied to $f$ and $i$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $\operatorname{fromSubtype}$ applied to $f$ and the function that maps $j$ to $\mathrm{Neq} (j , i)$ and $\mathrm{CategoryTheory\_\_Limits\_\_biproduct\_\_isLimitFromSubtype\_\_\_proof\_1}$ applied to $f$ and $i$.

the isomorphism coproduct of f (from the name)

Let $f$ be a function from elements of $J$ to elements of $C$. Then the isomorphism coproduct of $f$ is an isomorphism of the biproduct of $f$ and the sigma object of $f$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to the colimit cocone of $f$ and $\operatorname{isColimit}$ applied to the functor of $f$.

the isomorphism product of f (from the name)

Let $f$ be a function from elements of $J$ to elements of $C$. Then the isomorphism product of $f$ is an isomorphism of the biproduct of $f$ and the product object of $f$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to the limit cone of $f$ and $\operatorname{isLimit}$ applied to the functor of $f$.

the lift of p (from the name)

Let $p$ be a function from elements $b$ of $J$ to homomorphisms of $P$ and $f$ applied to $b$. Then the lift of $b$ is a homomorphism of $P$ and the biproduct of $f$ defined as the function that maps $p$ to the lift of the limit cone of $f$ and $\operatorname{mk}$ applied to $P$ and $b$.

the map of p (from the name)

Let $p$ be a function from elements $b$ of $J$ to homomorphisms of $f$ applied to $b$ and $g$ applied to $b$. Then the map of $b$ is a homomorphism of the biproduct of $f$ and the biproduct of $g$ defined as the function that maps $p$ to the map of the limit cone of $g$ and the natural transformation of the function that maps $j$ to $b$ applied to $\operatorname{as}$ applied to $j$.

the map of p (from the name)

Let $p$ be a function from elements $b$ of $J$ to homomorphisms of $f$ applied to $b$ and $g$ applied to $b$. Then the map of $b$ is a homomorphism of the biproduct of $f$ and the biproduct of $g$ defined as the function that maps $p$ to the map of the cocone of the bicone of $g$ and the natural transformation of the function that maps $j$ to $b$ applied to $\operatorname{as}$ applied to $j$.

the map isomorphism of p (from the name)

Let $p$ be a function from elements $b$ of $J$ to isomorphisms of $f$ applied to $b$ and $g$ applied to $b$. Then the map isomorphism of $b$ is an isomorphism of the biproduct of $f$ and the biproduct of $g$.

the matrix of m (from the name)

Let $m$ be a function from elements $j$ of $J$ and elements $k$ of $K$ to homomorphisms of $f$ applied to $j$ and $g$ applied to $k$. Then the matrix of $j$ is a homomorphism of the biproduct of $f$ and the biproduct of $g$ defined as the function that maps $k$ and $m$ to $\operatorname{desc}$ applied to the function that maps $j$ to the lift of the function that maps $k$ to $j$ applied to $j$ and $k$, $k$ and $m$.

the matrix equivalence (from the name)

The matrix equivalence is an equivalence from the set of homomorphisms of the biproduct of $f$ and the biproduct of $g$ to the set of functions from elements $j$ of $J$ and elements $k$ of $K$ to homomorphisms of $f$ applied to $j$ and $g$ applied to $k$.

the subtype of f and p (from the name)

Let $f$ be a function from elements of $J$ to elements of $C$. Let $p$ be a function from elements of $J$ to propositions. Then the subtype of $f$ and $p$ is a homomorphism of the biproduct of $f$ and the biproduct of $\operatorname{restrict}$ applied to $p$ and $f$ defined as the lift of the function that maps $x_{2}$ to the projection onto a summand of $f$ and $x_{2}$.

Let $f$ be a function from elements of $J$ to elements of $C$. Let $\mathrm{hb}$ be an element of $\operatorname{IsBilimit}$ applied to $b$. Then $\operatorname{uniqueUpToIso}$ applied to $f$ and $\mathrm{hb}$ is an isomorphism of $\operatorname{pt}$ applied to $b$ and the biproduct of $f$.

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

Let $e$ be an equivalence from $J$ to $K$. Let $w$ be a function from elements $j$ of $J$ to isomorphisms of $g$ applied to $e$ applied to $j$ and $f$ applied to $j$. Then the whisker equivalence of $e$ and $j$ is an isomorphism of the biproduct of $f$ and the biproduct of $g$.

the inclusion into a summand of f and b (from the docstring)

Let $f$ be a function from elements of $J$ to elements of $C$. Let $b$ be an element of $J$. Then the inclusion into a summand of $f$ and $b$ is a homomorphism of $f$ applied to $b$ and the biproduct of $f$ defined as the inclusion of the bicone of $f$ and $b$.

the projection onto a summand of f and b (from the docstring)

Let $f$ be a function from elements of $J$ to elements of $C$. Let $b$ be an element of $J$. Then the projection onto a summand of $f$ and $b$ is a homomorphism of the biproduct of $f$ and $f$ applied to $b$ defined as the projection of the bicone of $f$ and $b$.

the biproduct biproduct isomorphism of f and g (from the name)

Let $f$ be a function from elements of $x_{2}$ to sets. Let $g$ be a function from elements $i_{1}$ of $x_{2}$ and elements of $f$ applied to $i_{1}$ to elements of $C$. Then the biproduct biproduct isomorphism of $f$ and $i_{1}$ is an isomorphism of the biproduct of the function that maps $i$ to the biproduct of $g$ applied to $i$ and the biproduct of the function that maps $p$ to $g$ applied to $\operatorname{fst}$ applied to $p$ and $\operatorname{snd}$ applied to $p$.

the biproduct isomorphism of F (from the name)

Let $F$ be a function from elements of $J$ to elements of $C$. Then the biproduct isomorphism of $F$ is an isomorphism of the product object of $F$ and the sigma object of $F$ defined as the composition of $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to the functor of $F$ and the limit cone of $F$ and $\operatorname{coconePointUniqueUpToIso}$ applied to the colimit cocone of $F$ and $\operatorname{isColimit}$ applied to the functor of $F$.

the biproduct unique isomorphism of f (from the name)

Let $f$ be a function from elements of $J$ to elements of $C$. Then the biproduct unique isomorphism of $f$ is an isomorphism of the biproduct of $f$ and $f$ applied to $\operatorname{default}$ defined as the inverse of $\operatorname{uniqueUpToIso}$ applied to $f$ and $\operatorname{isBilimit}$ applied to the limit bicone of $f$.

the cokernel biproduct from subtype isomorphism of f and p (from the name)

Let $f$ be a function from elements of $K$ to elements of $C$. Let $p$ be a function from elements of $K$ to propositions. Then the cokernel biproduct from subtype isomorphism of $f$ and $p$ is an isomorphism of the cokernel of $\operatorname{fromSubtype}$ applied to $f$ and $p$ and the biproduct of $\operatorname{restrict}$ applied to the complement of $p$ and $f$ defined as the isomorphism colimit cocone of the cokernel cofork biproduct from subtype of $f$ and $p$.

the cokernel biproduct inclusion isomorphism of f and i (from the name)

Let $f$ be a function from elements of $J$ to elements of $C$. Let $i$ be an element of $J$. Then the cokernel biproduct inclusion isomorphism of $f$ and $i$ is an isomorphism of the cokernel of the inclusion into a summand of $f$ and $i$ and the biproduct of $\operatorname{restrict}$ applied to the function that maps $j$ to $\mathrm{Neq} (j , i)$ and $f$.

the cokernel cofork biproduct from subtype of f and p (from the name)

Let $f$ be a function from elements of $K$ to elements of $C$. Let $p$ be a function from elements of $K$ to propositions. Then the cokernel cofork biproduct from subtype of $f$ and $p$ is a colimit cocone of the parallel pair of $\operatorname{fromSubtype}$ applied to $f$ and $p$ and $0$.

Let $F$ be a function from elements of $J$ to elements of $C$. Then $\operatorname{getBiproductData}$ applied to $F$ is a limit bicone of $F$ defined as $\operatorname{choice}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_HasBiproduct\_\_exists\_biproduct}$.

the kernel biproduct to subtype isomorphism of f and p (from the name)

Let $f$ be a function from elements of $K$ to elements of $C$. Let $p$ be a function from elements of $K$ to propositions. Then the kernel biproduct to subtype isomorphism of $f$ and $p$ is an isomorphism of the kernel of the subtype of $f$ and $p$ and the biproduct of $\operatorname{restrict}$ applied to the complement of $p$ and $f$ defined as the isomorphism limit cone of the kernel fork biproduct to subtype of $f$ and $p$.

the kernel biproduct projection isomorphism of f and i (from the name)

Let $f$ be a function from elements of $J$ to elements of $C$. Let $i$ be an element of $J$. Then the kernel biproduct projection isomorphism of $f$ and $i$ is an isomorphism of the kernel of the projection onto a summand of $f$ and $i$ and the biproduct of $\operatorname{restrict}$ applied to the function that maps $j$ to $\mathrm{Neq} (j , i)$ and $f$.

the kernel fork biproduct to subtype of f and p (from the name)

Let $f$ be a function from elements of $K$ to elements of $C$. Let $p$ be a function from elements of $K$ to propositions. Then the kernel fork biproduct to subtype of $f$ and $p$ is a limit cone of the parallel pair of the subtype of $f$ and $p$ and $0$.

the limit bicone of f (from the name)

Let $f$ be a function from elements of $J$ to elements of $C$. Then the limit bicone of $f$ is a limit bicone of $f$.

the comb pair hom of bc and i (from the name)

Let $x_{5}$ be a cofan of $x_{3}$. Let $x_{6}$ be a cofan of $x_{4}$. Let $\mathrm{bc}$ be a binary cofan of $\operatorname{pt}$ applied to $x_{5}$ and $\operatorname{pt}$ applied to $x_{6}$. Let $i$ be an element of $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$. Then the comb pair hom of $\mathrm{bc}$ and $i$ is a homomorphism of $\operatorname{elim}$ applied to $x_{3}$, $x_{4}$ and $i$ and $\operatorname{pt}$ applied to $\mathrm{bc}$.

Let $x_{7}$ be an element of $\operatorname{IsColimit}$ applied to $x_{5}$. Let $x_{8}$ be an element of $\operatorname{IsColimit}$ applied to $x_{6}$. Let $h$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{bc}$. Then $\operatorname{combPairIsColimit}$ applied to $x_{7}$, $x_{8}$ and $h$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $\mathrm{bc}$ and $\operatorname{combPairHoms}$ applied to $\mathrm{bc}$.

the comb pair hom of bc and i (from the name)

Let $x_{5}$ be an element of $\operatorname{Fan}$ applied to $x_{3}$. Let $x_{6}$ be an element of $\operatorname{Fan}$ applied to $x_{4}$. Let $\mathrm{bc}$ be an element of $\operatorname{BinaryFan}$ applied to $\operatorname{pt}$ applied to $x_{5}$ and $\operatorname{pt}$ applied to $x_{6}$. Let $i$ be an element of $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$. Then the comb pair hom of $\mathrm{bc}$ and $i$ is a homomorphism of $\operatorname{pt}$ applied to $\mathrm{bc}$ and $\operatorname{elim}$ applied to $x_{3}$, $x_{4}$ and $i$.

Let $x_{7}$ be an element of $\operatorname{IsLimit}$ applied to $x_{5}$. Let $x_{8}$ be an element of $\operatorname{IsLimit}$ applied to $x_{6}$. Let $h$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{bc}$. Then $\operatorname{combPairIsLimit}$ applied to $x_{7}$, $x_{8}$ and $h$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $\mathrm{bc}$ and $\operatorname{combPairHoms}$ applied to $\mathrm{bc}$.

the multiequalizer equivalence of I (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Then the multiequalizer equivalence of $I$ is an element of $\EquivMACRoAE {\operatorname{ToType} (\operatorname{multiequalizer} (I))}{(\SubtypeSet {x_{3}}{\mathrm{forall} (\operatorname{R} (J), \lambda i . \EqtMACRoH {\operatorname{hom} (\operatorname{fst} (I , i), x_{3} (\operatorname{fst} (J , i)))}{\operatorname{hom} (\operatorname{snd} (I , i), x_{3} (\operatorname{snd} (J , i)))})})}$ defined as the composition of the equivalence between a limiting cone of $\operatorname{isLimitOfPreserves}$ applied to the forgetful functor of $C$ and $\operatorname{isLimit}$ applied to the multicospan of $I$ and $\operatorname{multiequalizerEquivAux}$ applied to $I$.

the equivalence of x3 and x4 (from the docstring)

Let $x_{3}$ and $x_{4}$ be elements of $C$. Then the equivalence of $x_{3}$ and $x_{4}$ is an equivalence from the set of types of the product of $x_{3}$ and $x_{4}$ to $\mathrm{Prod}$ applied to the set of types of $x_{3}$ and the set of types of $x_{4}$ defined as the equivalence of the composition of the isomorphism of $x_{3}$ and $x_{4}$ and the binary product isomorphism of the action of the forgetful functor of $C$ and $x_{3}$ and the action of the forgetful functor of $C$ and $x_{4}$.

the equivalence of F (from the docstring)

Let $F$ be a function from elements of $J$ to elements of $C$. Then the equivalence of $F$ is an equivalence from the set of types of the product object of $F$ to the set of functions from elements $j$ of $J$ to types of $F$ applied to $j$ defined as the equivalence of the composition of the isomorphism of the forgetful functor of $C$ and $F$ and the categorical product in the function that maps $j$ to the set of types of $F$ applied to $j$.

the pullback equivalence of x5 and x6 (from the name)

Let $x_{5}$ be a homomorphism of $x_{3}$ and $S$. Let $x_{6}$ be a homomorphism of $x_{4}$ and $S$. Then the pullback equivalence of $x_{5}$ and $x_{6}$ is an equivalence from the set of types of the pullback of $x_{5}$ and $x_{6}$ to $\SubtypeSet {p}{(\EqtMACRoH {\operatorname{hom} (x_{5} , \ProdfstMACRoZ {p})}{\operatorname{hom} (x_{6} , \ProdsndMACRoAA {p})})}$ defined as the equivalence of the composition of the isomorphism of $x_{5}$ and $x_{6}$ and the pullback isomorphism pullback of the type category of $\operatorname{coe}$ applied to the homomorphism of $x_{5}$ and the type category of $\operatorname{coe}$ applied to the homomorphism of $x_{6}$.

the pullback of x7 and x8 (from the name)

Let $x_{5}$ be a homomorphism of $x_{3}$ and $S$. Let $x_{6}$ be a homomorphism of $x_{4}$ and $S$. Let $x_{7}$ be a type of $x_{3}$. Let $x_{8}$ be a type of $x_{4}$ such that $\EqtMACRoH {\operatorname{hom} (x_{5} , x_{7})}{\operatorname{hom} (x_{6} , x_{8})}$. Then the pullback of $x_{7}$ and $x_{8}$ is a type of the pullback of $x_{5}$ and $x_{6}$ defined as $\operatorname{symm}$ applied to the pullback equivalence of $x_{5}$ and $x_{6}$ and $\ProdmkMACRoU {x_{7}}{x_{8}}$.

C has countable colimits (from the name)

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

C has countable coproducts (from the name)

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

C has countable limits (from the name)

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

C has countable products (from the name)

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

the initial functor of J (from the docstring)

Let $J$ be a set. Then the initial functor of $J$ is a functor of the set of opposites of $\Natural$ and $J$.

the object part of the initial functor of J and x1 (from the docstring)

Let $J$ be a set. Let $x_{1}$ be a natural number. Then the object part of the initial functor of $J$ and $x_{1}$ is an element of $J$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsCofiltered\_\_sequentialFunctor\_obj\_\_\_f}$ applied to $J$.

the initial functor of J (from the docstring)

Let $J$ be a set. Then the initial functor of $J$ is a functor of $\Natural$ and $J$.

the object part of the initial functor of J and x1 (from the docstring)

Let $J$ be a set. Let $x_{1}$ be a natural number. Then the object part of the initial functor of $J$ and $x_{1}$ is an element of $J$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_IsFiltered\_\_sequentialFunctor\_obj\_\_\_f}$ applied to $J$.