Definitions: Mathlib.CategoryTheory, part 13 of 25

I has multicoequalizers (from the name)

Let $I$ be a multispan index of $J$ and $C$. Then $I$ has multicoequalizers, if the multispan of $I$ has colimits.

I has multiequalizers (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Then $I$ has multiequalizers, if the multicospan of $I$ has limits.

Let $I$ be a multispan index of $J$ and $C$. Let $W$ be an element of $C$. Let $k$ be a function from elements $b$ of $\operatorname{R}$ applied to $J$ to homomorphisms of the right of $I$ and $b$ and $W$ such that for all elements $a$ of $\operatorname{L}$ applied to $J$, the composition of the first component of $I$ and $a$ and $k$ applied to the first map of $J$ and $a$ is equal to the composition of the second component of $I$ and $a$ and $k$ applied to the second map of $J$ and $a$. Then $\operatorname{desc}$ applied to $I$, $W$, $b$, $k$ and $h_{1}$ is a homomorphism of the multicoequalizer of $I$ and $W$ defined as the function that maps $h_{1}$ to $\operatorname{desc}$ applied to the multispan of $I$, the projection of $W$ and $b$ and $h_{1}$.

the isomorphism coequalizer of I (from the name)

Let $I$ be a multispan index of $J$ and $C$. Then the isomorphism coequalizer of $I$ is an isomorphism of the multicoequalizer of $I$ and the coequalizer of the induced map of $I$ and the induced map of $I$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the action of the inverse of the multicofork equivalence sigma cofork of $I$ and the cocone of the parallel pair of the induced map of $I$ and the induced map of $I$ and $\operatorname{ofPreservesCoconeInitial}$ applied to the inverse of the multicofork equivalence sigma cofork of $I$ and $\operatorname{isColimit}$ applied to the parallel pair of the induced map of $I$ and the induced map of $I$.

the multicofork of I (from the name)

Let $I$ be a multispan index of $J$ and $C$. Then the multicofork of $I$ is a multicofork of $I$ defined as the cocone of the multispan of $I$.

the canonical projection of I (from the docstring)

Let $I$ be a multispan index of $J$ and $C$. Then the canonical projection of $I$ is a homomorphism of the sigma object of $\operatorname{right}$ applied to $I$ and the multicoequalizer of $I$ defined as the composition of the projection of the induced map of $I$ and the induced map of $I$ and the inverse of the isomorphism coequalizer of $I$.

the projection of I and b (from the name)

Let $I$ be a multispan index of $J$ and $C$. Let $b$ be an element of $\operatorname{R}$ applied to $J$. Then the projection of $I$ and $b$ is a homomorphism of the right of $I$ and $b$ and the multicoequalizer of $I$ defined as the inclusion of the multispan of $I$ and the right of $b$.

multicofork of I (from the name)

Let $I$ be a multispan index of $J$ and $C$. Then a multicofork of $I$ is an element of the function that maps $I$ to the set of cocones of the multispan of $I$.

Let $\mathrm{hK}$ be an element of $\operatorname{IsColimit}$ applied to $K$. Let $k$ be a function from elements $a$ of $\operatorname{R}$ applied to $J$ to homomorphisms of the right of $I$ and $a$ and $T$ such that for all elements $b$ of $\operatorname{L}$ applied to $J$, the composition of the first component of $I$ and $b$ and $k$ applied to the first map of $J$ and $b$ is equal to the composition of the second component of $I$ and $b$ and $k$ applied to the second map of $J$ and $b$. Then $\operatorname{desc}$ applied to $\mathrm{hK}$, $a$, $k$ and $\mathrm{hk}$ is a homomorphism of $\operatorname{pt}$ applied to $K$ and $T$ defined as the function that maps $\mathrm{hk}$ to $\operatorname{desc}$ applied to $\mathrm{hK}$, the projection of $T$ and $a$ and $\mathrm{hk}$.

Let $K$ be a multicofork of $I$. Let $\mathrm{desc}$ be a function from multicoforks $E_{2}$ of $I$ to homomorphisms of $\operatorname{pt}$ applied to $K$ and $\operatorname{pt}$ applied to $E_{2}$ such that for all multicoforks $E_{1}$ of $I$, for all elements $i_{1}$ of $\operatorname{R}$ applied to $J$, the composition of the projection of $K$ and $i_{1}$ and $\mathrm{desc}$ applied to $E_{1}$ is equal to the projection of $E_{1}$ and $i_{1}$ and for all multicoforks $E$ of $I$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $K$ and $\operatorname{pt}$ applied to $E$, if for all elements $i$ of $\operatorname{R}$ applied to $J$, the composition of the projection of $K$ and $i$ and $m$ is equal to the projection of $E$ and $i$, then $\EqtMACRoH {m}{\mathrm{desc} (E)}$. Then $\operatorname{mk}$ applied to $K$, $E_{2}$, $\mathrm{desc}$, $\mathrm{fac}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsColimit}$ applied to $K$.

the extension of e and h (from the name)

Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $K$ and $\operatorname{pt}$ applied to $\mathrm{K'}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ of $\operatorname{R}$ applied to $J$, the composition of the projection of $K$ and $i$ and the homomorphism of $e$ is equal to the projection of $\mathrm{K'}$ and $i$ and $\mathrm{CategoryTheory\_\_Limits\_\_Multicofork\_\_ext\_\_\_auto\_1}$. Then the extension of $e$ and $h$ is an isomorphism of $K$ and $\mathrm{K'}$.

Let $c$ be a multicofork of $I$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $h$ be an element of $\operatorname{SymmStruct}$ applied to $I$. Then $\operatorname{isColimitToLinearOrder}$ applied to $c$, $\mathrm{hc}$ and $h$ is an element of $\operatorname{IsColimit}$ applied to the linear order of $c$.

the isomorphism of t (from the name)

Let $t$ be a multicofork of $I$. Then the isomorphism of $t$ is an isomorphism of $t$ and the projection of $\operatorname{pt}$ applied to $t$ and $\mathrm{CategoryTheory\_\_Limits\_\_Multicofork\_\_\_u3c0\_}$ applied to $t$.

the multicofork of c and h (from the name)

Let $c$ be a multicofork of the linear order of $I$. Let $h$ be an element of $\operatorname{SymmStruct}$ applied to $I$. Then the multicofork of $c$ and $h$ is a multicofork of $I$.

the multicofork of a (from the name)

Let $a$ be a cofork of the first component sigma map of $d$ and $\mathrm{hc}$ and the second component sigma map of $d$ and $\mathrm{hc}$. Then the multicofork of $a$ is a multicofork of $I$.

the projection of P and x1 (from the name)

Let $I$ be a multispan index of $J$ and $C$. Let $P$ be an element of $C$. Let $x_{1}$ be a function from elements $b$ of $\operatorname{R}$ applied to $J$ to homomorphisms of the right of $I$ and $b$ and $P$ such that for all elements $a$ of $\operatorname{L}$ applied to $J$, the composition of the first component of $I$ and $a$ and $x_{1}$ applied to the first map of $J$ and $a$ is equal to the composition of the second component of $I$ and $a$ and $x_{1}$ applied to the second map of $J$ and $a$. Then the projection of $P$ and $b$ is a multicofork of $I$.

the linear order of c (from the name)

Let $c$ be a multicofork of $I$. Then the linear order of $c$ is a multicofork of the linear order of $I$.

the sigma cofork of hd and K (from the name)

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{hd}$ be an element of $\operatorname{IsColimit}$ applied to $d$. Let $K$ be a multicofork of $I$. Then the sigma cofork of $\mathrm{hd}$ and $K$ is a cofork of the first component sigma map of $d$ and $\mathrm{hc}$ and the second component sigma map of $d$ and $\mathrm{hc}$.

the projection of K and b (from the name)

Let $K$ be a multicofork of $I$. Let $b$ be an element of $\operatorname{R}$ applied to $J$. Then the projection of $K$ and $b$ is a homomorphism of the right of $I$ and $b$ and $\operatorname{pt}$ applied to $K$ defined as the component of the inclusion of $K$ and the right of $b$.

multicospan index of J and C (from the name)

Let $J$ be a shape. Let $C$ be a set. Then the multicospan indexes of $J$ and $C$ are a basic type.

the first component of self and b (from the name)

Let $\mathrm{self}$ be a multicospan index of $J$ and $C$. Let $b$ be an element of $\operatorname{R}$ applied to $J$. Then the first component of $\mathrm{self}$ and $b$ is a homomorphism of the left of $\mathrm{self}$ and the first map of $J$ and $b$ and the right of $\mathrm{self}$ and $b$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $b$.

the induced map of I (from the docstring)

Let $I$ be a multicospan index of $J$ and $C$. Then the induced map of $I$ is a homomorphism of the product object of $\operatorname{left}$ applied to $I$ and the product object of $\operatorname{right}$ applied to $I$ defined as the first component product map of the cone of the functor of $\operatorname{left}$ applied to $I$ and $\operatorname{isLimit}$ applied to the functor of $\operatorname{right}$ applied to $I$.

the first component product map of c and hd (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Let $c$ be an element of $\operatorname{Fan}$ applied to $\operatorname{left}$ applied to $I$. Let $\mathrm{hd}$ be an element of $\operatorname{IsLimit}$ applied to $d$. Then the first component product map of $c$ and $\mathrm{hd}$ is a homomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $d$ defined as the lift of $\mathrm{hd}$ and the function that maps $i$ to the composition of the projection of $c$ and the first map of $J$ and $i$ and the first component of $I$ and $i$.

the left of self and x1 (from the name)

Let $\mathrm{self}$ be a multicospan index of $J$ and $C$. Let $x_{1}$ be an element of $\operatorname{L}$ applied to $J$. Then the left of $\mathrm{self}$ and $x_{1}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

the multicospan of I (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Then the multicospan of $I$ is a functor of the set of walking multicospans of $J$ and $C$.

the multifork equivalence product fork of I (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Then the multifork equivalence product fork of $I$ is an equivalence of the set of multiforks of $I$ and the set of forks of the induced map of $I$ and the induced map of $I$ defined as the multifork equivalence product fork of $\operatorname{isLimit}$ applied to the functor of $\operatorname{left}$ applied to $I$ and $\operatorname{isLimit}$ applied to the functor of $\operatorname{right}$ applied to $I$.

the multifork equivalence product fork of hc and hd (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{hd}$ be an element of $\operatorname{IsLimit}$ applied to $d$. Then the multifork equivalence product fork of $\mathrm{hc}$ and $\mathrm{hd}$ is an equivalence of the set of multiforks of $I$ and the set of forks of the first component product map of $c$ and $\mathrm{hd}$ and the second component product map of $c$ and $\mathrm{hd}$.

the multifork of f and g (from the name)

Let $J$ be a shape. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the multifork of $f$ and $g$ is an equivalence of the set of multiforks of the multicospan index of $f$ and $g$ and the set of forks of $f$ and $g$.

the multicospan index of f and g (from the name)

Let $J$ be a shape. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the multicospan index of $f$ and $g$ is a multicospan index of $J$ and $C$ defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ to $X$, the function that maps $x_{2}$ to $Y$, the function that maps $x_{3}$ to $f$ and the function that maps $x_{4}$ to $g$.

the multicospan index of I and hd (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Let $\mathrm{hd}$ be an element of $\operatorname{IsLimit}$ applied to $d$. Then the multicospan index of $I$ and $\mathrm{hd}$ is a functor of the set of forks of the first component product map of $c$ and $\mathrm{hd}$ and the second component product map of $c$ and $\mathrm{hd}$ and the set of multiforks of $I$.

the parallel pair diagram of I (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Then the parallel pair diagram of $I$ is a functor of the set of walking parallel pairs and $C$ defined as the parallel pair of the induced map of $I$ and the induced map of $I$.

the parallel pair diagram of c and hd (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Let $c$ be an element of $\operatorname{Fan}$ applied to $\operatorname{left}$ applied to $I$. Let $\mathrm{hd}$ be an element of $\operatorname{IsLimit}$ applied to $d$. Then the parallel pair diagram of $c$ and $\mathrm{hd}$ is a functor of the set of walking parallel pairs and $C$ defined as the parallel pair of the first component product map of $c$ and $\mathrm{hd}$ and the second component product map of $c$ and $\mathrm{hd}$.

the right of self and x1 (from the name)

Let $\mathrm{self}$ be a multicospan index of $J$ and $C$. Let $x_{1}$ be an element of $\operatorname{R}$ applied to $J$. Then the right of $\mathrm{self}$ and $x_{1}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.

the second component of self and b (from the name)

Let $\mathrm{self}$ be a multicospan index of $J$ and $C$. Let $b$ be an element of $\operatorname{R}$ applied to $J$. Then the second component of $\mathrm{self}$ and $b$ is a homomorphism of the left of $\mathrm{self}$ and the second map of $J$ and $b$ and the right of $\mathrm{self}$ and $b$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $b$.

the induced map of I (from the docstring)

Let $I$ be a multicospan index of $J$ and $C$. Then the induced map of $I$ is a homomorphism of the product object of $\operatorname{left}$ applied to $I$ and the product object of $\operatorname{right}$ applied to $I$ defined as the second component product map of the cone of the functor of $\operatorname{left}$ applied to $I$ and $\operatorname{isLimit}$ applied to the functor of $\operatorname{right}$ applied to $I$.

the second component product map of c and hd (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Let $c$ be an element of $\operatorname{Fan}$ applied to $\operatorname{left}$ applied to $I$. Let $\mathrm{hd}$ be an element of $\operatorname{IsLimit}$ applied to $d$. Then the second component product map of $c$ and $\mathrm{hd}$ is a homomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $d$ defined as the lift of $\mathrm{hd}$ and the function that maps $i$ to the composition of the projection of $c$ and the second map of $J$ and $i$ and the second component of $I$ and $i$.

the product fork functor of hc and hd (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{hd}$ be an element of $\operatorname{IsLimit}$ applied to $d$. Then the product fork functor of $\mathrm{hc}$ and $\mathrm{hd}$ is a functor of the set of multiforks of $I$ and the set of forks of the first component product map of $c$ and $\mathrm{hd}$ and the second component product map of $c$ and $\mathrm{hd}$.

shape (from the docstring)

The shapes are a basic type.

Let $\mathrm{self}$ be a shape. Then an element of $\operatorname{L}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a shape. Then an element of $\operatorname{R}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj1}$ applied to $\mathrm{self}$.

the first map of self and x (from the docstring)

Let $\mathrm{self}$ be a shape. Let $x$ be an element of $\operatorname{R}$ applied to $\mathrm{self}$. Then the first map of $\mathrm{self}$ and $x$ is an element of $\operatorname{L}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x$.

the product of x (from the name)

Let $x$ be a set. Then the product of $x$ is a shape defined as $\operatorname{mk}$ applied to $x$, $\mathrm{Prod}$ applied to $x$ and $x$, $\ProdfstMACRoZ$ and $\ProdsndMACRoAA$.

the second map of self and x (from the docstring)

Let $\mathrm{self}$ be a shape. Let $x$ be an element of $\operatorname{R}$ applied to $\mathrm{self}$. Then the second map of $\mathrm{self}$ and $x$ is an element of $\operatorname{L}$ applied to $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $x$.

the isomorphism equalizer of I (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Then the isomorphism equalizer of $I$ is an isomorphism of the multiequalizer of $I$ and the equalizer of the induced map of $I$ and the induced map of $I$ defined as the isomorphism limit cone of $\operatorname{mk}$ applied to the action of the inverse of the multifork equivalence product fork of $I$ and the cone of the parallel pair of the induced map of $I$ and the induced map of $I$ and $\operatorname{ofPreservesConeTerminal}$ applied to the inverse of the multifork equivalence product fork of $I$ and $\operatorname{isLimit}$ applied to the parallel pair of the induced map of $I$ and the induced map of $I$.

the lift of W and k (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Let $W$ be an element of $C$. Let $k$ be a function from elements $a$ of $\operatorname{L}$ applied to $J$ to homomorphisms of $W$ and the left of $I$ and $a$ such that for all elements $b$ of $\operatorname{R}$ applied to $J$, the composition of $k$ applied to the first map of $J$ and $b$ and the first component of $I$ and $b$ is equal to the composition of $k$ applied to the second map of $J$ and $b$ and the second component of $I$ and $b$. Then the lift of $W$ and $a$ is a homomorphism of $W$ and the multiequalizer of $I$ defined as the function that maps $h_{1}$ to the lift of the multicospan of $I$ and the inclusion of $W$ and $a$.

the multifork of I (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Then the multifork of $I$ is a multifork of $I$ defined as the cone of the multicospan of $I$.

the inclusion of I and a (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Let $a$ be an element of $\operatorname{L}$ applied to $J$. Then the inclusion of $I$ and $a$ is a homomorphism of the multiequalizer of $I$ and the left of $I$ and $a$ defined as the projection from the limit object to a value of the functor of the multicospan of $I$ and the left of $a$.

the inclusion product of I (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Then the inclusion product of $I$ is a homomorphism of the multiequalizer of $I$ and the product object of $\operatorname{left}$ applied to $I$ defined as the composition of the homomorphism of the isomorphism equalizer of $I$ and the inclusion of the induced map of $I$ and the induced map of $I$.

multifork of I (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Then a multifork of $I$ is an element of the function that maps $I$ to the set of cones of the multicospan of $I$.

the lift of hK and k (from the name)

Let $\mathrm{hK}$ be an element of $\operatorname{IsLimit}$ applied to $K$. Let $k$ be a function from elements $a$ of $\operatorname{L}$ applied to $J$ to homomorphisms of $T$ and the left of $I$ and $a$ such that for all elements $b$ of $\operatorname{R}$ applied to $J$, the composition of $k$ applied to the first map of $J$ and $b$ and the first component of $I$ and $b$ is equal to the composition of $k$ applied to the second map of $J$ and $b$ and the second component of $I$ and $b$. Then the lift of $\mathrm{hK}$ and $a$ is a homomorphism of $T$ and $\operatorname{pt}$ applied to $K$ defined as the function that maps $\mathrm{hk}$ to the lift of $\mathrm{hK}$ and the inclusion of $T$ and $a$.

Let $K$ be a multifork of $I$. Let $\mathrm{lift}$ be a function from multiforks $E_{2}$ of $I$ to homomorphisms of $\operatorname{pt}$ applied to $E_{2}$ and $\operatorname{pt}$ applied to $K$ such that for all multiforks $E_{1}$ of $I$, for all elements $i_{1}$ of $\operatorname{L}$ applied to $J$, the composition of $\mathrm{lift}$ applied to $E_{1}$ and the inclusion of $K$ and $i_{1}$ is equal to the inclusion of $E_{1}$ and $i_{1}$ and for all multiforks $E$ of $I$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $E$ and $\operatorname{pt}$ applied to $K$, if for all elements $i$ of $\operatorname{L}$ applied to $J$, the composition of $m$ and the inclusion of $K$ and $i$ is equal to the inclusion of $E$ and $i$, then $\EqtMACRoH {m}{\mathrm{lift} (E)}$. Then $\operatorname{mk}$ applied to $K$, $E_{2}$, $\mathrm{lift}$, $\mathrm{fac}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsLimit}$ applied to $K$.

the extension of e and h (from the name)

Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ of $\operatorname{L}$ applied to $J$, the composition of the homomorphism of $e$ and the inclusion of $s$ and $i$ is equal to the inclusion of $t$ and $i$ and $\mathrm{CategoryTheory\_\_Limits\_\_Multifork\_\_ext\_\_\_auto\_1}$. Then the extension of $e$ and $h$ is an isomorphism of $t$ and $s$.

Let $c$ be a multifork of $I$. Let $\mathrm{c'}$ be a multifork of $\mathrm{I'}$. Let $e$ be an isomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $\mathrm{c'}$. Let $\mathrm{el}$ be a function from elements $i_{4}$ of $\operatorname{L}$ applied to $J$ to isomorphisms of the left of $I$ and $i_{4}$ and the left of $\mathrm{I'}$ and $i_{4}$. Let $\mathrm{er}$ be a function from elements $i_{3}$ of $\operatorname{R}$ applied to $J$ to isomorphisms of the right of $I$ and $i_{3}$ and the right of $\mathrm{I'}$ and $i_{3}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $i_{2}$ of $\operatorname{R}$ applied to $J$, the composition of the first component of $I$ and $i_{2}$ and the homomorphism of $\mathrm{er}$ applied to $i_{2}$ is equal to the composition of the homomorphism of $\mathrm{el}$ applied to the first map of $J$ and $i_{2}$ and the first component of $\mathrm{I'}$ and $i_{2}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Multifork\_\_isLimitEquivOfIsos\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $i_{1}$ of $\operatorname{R}$ applied to $J$, the composition of the second component of $I$ and $i_{1}$ and the homomorphism of $\mathrm{er}$ applied to $i_{1}$ is equal to the composition of the homomorphism of $\mathrm{el}$ applied to the second map of $J$ and $i_{1}$ and the second component of $\mathrm{I'}$ and $i_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Multifork\_\_isLimitEquivOfIsos\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ of $\operatorname{L}$ applied to $J$, the composition of the homomorphism of $e$ and the inclusion of $\mathrm{c'}$ and $i$ is equal to the composition of the inclusion of $c$ and $i$ and the homomorphism of $\mathrm{el}$ applied to $i$ and $\mathrm{CategoryTheory\_\_Limits\_\_Multifork\_\_isLimitEquivOfIsos\_\_\_auto\_5}$. Then $\operatorname{isLimitEquivOfIsos}$ applied to $c$, $\mathrm{c'}$, $e$, $i_{4}$, $\mathrm{el}$, $i_{3}$, $\mathrm{er}$, $\mathrm{hl}$, $\mathrm{hr}$ and $\mathrm{he}$ is an element of $\EquivMACRoAE {\operatorname{IsLimit} (c)}{\operatorname{IsLimit} (\mathrm{c'})}$ defined as the function that maps $\mathrm{hr}$ and $\mathrm{he}$ to the equivalence of $\mathrm{c'}$ and the extension of $e$ and $\mathrm{hl}$.

the isomorphism of t (from the name)

Let $t$ be a multifork of $I$. Then the isomorphism of $t$ is an isomorphism of $t$ and the inclusion of $\operatorname{pt}$ applied to $t$ and $\mathrm{CategoryTheory\_\_Limits\_\_Multifork\_\_\_u3b9\_}$ applied to $t$.

the multifork of a (from the name)

Let $a$ be a fork of the first component product map of $c$ and $\mathrm{hd}$ and the second component product map of $c$ and $\mathrm{hd}$. Then the multifork of $a$ is a multifork of $I$.

the inclusion of P and x1 (from the name)

Let $I$ be a multicospan index of $J$ and $C$. Let $P$ be an element of $C$. Let $x_{1}$ be a function from elements $a$ of $\operatorname{L}$ applied to $J$ to homomorphisms of $P$ and the left of $I$ and $a$ such that for all elements $b$ of $\operatorname{R}$ applied to $J$, the composition of $x_{1}$ applied to the first map of $J$ and $b$ and the first component of $I$ and $b$ is equal to the composition of $x_{1}$ applied to the second map of $J$ and $b$ and the second component of $I$ and $b$. Then the inclusion of $P$ and $a$ is a multifork of $I$.

the product fork of hd and K (from the name)

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{hd}$ be an element of $\operatorname{IsLimit}$ applied to $d$. Let $K$ be a multifork of $I$. Then the product fork of $\mathrm{hd}$ and $K$ is a fork of the first component product map of $c$ and $\mathrm{hd}$ and the second component product map of $c$ and $\mathrm{hd}$.

the inclusion of K and a (from the name)

Let $K$ be a multifork of $I$. Let $a$ be an element of $\operatorname{L}$ applied to $J$. Then the inclusion of $K$ and $a$ is a homomorphism of $\operatorname{pt}$ applied to $K$ and the left of $I$ and $a$ defined as the component of the projection of $K$ and the left of $a$.

multispan index of J and C (from the name)

Let $J$ be a shape. Let $C$ be a set. Then the multispan indexes of $J$ and $C$ are a basic type.

Let $I$ be a multispan index of the product of $x_{1}$ and $C$. Then the elements of $\operatorname{SymmStruct}$ applied to $I$ are a basic type.

the isomorphism of i and j (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{SymmStruct}$ applied to $I$. Let $i$ and $j$ be elements of $x_{1}$. Then the isomorphism of $i$ and $j$ is an isomorphism of the left of $I$ and $\ProdmkMACRoU {i}{j}$ and the left of $I$ and $\ProdmkMACRoU {j}{i}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $i$ and $j$.

the first component of self and a (from the name)

Let $\mathrm{self}$ be a multispan index of $J$ and $C$. Let $a$ be an element of $\operatorname{L}$ applied to $J$. Then the first component of $\mathrm{self}$ and $a$ is a homomorphism of the left of $\mathrm{self}$ and $a$ and the right of $\mathrm{self}$ and the first map of $J$ and $a$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $a$.

the induced map of I (from the docstring)

Let $I$ be a multispan index of $J$ and $C$. Then the induced map of $I$ is a homomorphism of the sigma object of $\operatorname{left}$ applied to $I$ and the sigma object of $\operatorname{right}$ applied to $I$ defined as the first component sigma map of the cocone of the functor of $\operatorname{right}$ applied to $I$ and $\operatorname{isColimit}$ applied to the functor of $\operatorname{left}$ applied to $I$.

the first component sigma map of d and hc (from the name)

Let $I$ be a multispan index of $J$ and $C$. Let $d$ be a cofan of $\operatorname{right}$ applied to $I$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the first component sigma map of $d$ and $\mathrm{hc}$ is a homomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $d$ defined as $\operatorname{desc}$ applied to $\mathrm{hc}$ and the function that maps $i$ to the composition of the first component of $I$ and $i$ and the injection of $d$ and the first map of $J$ and $i$.

the left of self and x1 (from the name)

Let $\mathrm{self}$ be a multispan index of $J$ and $C$. Let $x_{1}$ be an element of $\operatorname{L}$ applied to $J$. Then the left of $\mathrm{self}$ and $x_{1}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

the multicofork equivalence sigma cofork of I (from the name)

Let $I$ be a multispan index of $J$ and $C$. Then the multicofork equivalence sigma cofork of $I$ is an equivalence of the set of multicoforks of $I$ and the set of coforks of the induced map of $I$ and the induced map of $I$ defined as the multicofork equivalence sigma cofork of $\operatorname{isColimit}$ applied to the functor of $\operatorname{left}$ applied to $I$ and $\operatorname{isColimit}$ applied to the functor of $\operatorname{right}$ applied to $I$.

the multicofork equivalence sigma cofork of hc and hd (from the name)

Let $I$ be a multispan index of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{hd}$ be an element of $\operatorname{IsColimit}$ applied to $d$. Then the multicofork equivalence sigma cofork of $\mathrm{hc}$ and $\mathrm{hd}$ is an equivalence of the set of multicoforks of $I$ and the set of coforks of the first component sigma map of $d$ and $\mathrm{hc}$ and the second component sigma map of $d$ and $\mathrm{hc}$.

the multispan of I (from the name)

Let $I$ be a multispan index of $J$ and $C$. Then the multispan of $I$ is a functor of the set of walking multispans of $J$ and $C$.

the multispan index of I and hc (from the name)

Let $I$ be a multispan index of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the multispan index of $I$ and $\mathrm{hc}$ is a functor of the set of coforks of the first component sigma map of $d$ and $\mathrm{hc}$ and the second component sigma map of $d$ and $\mathrm{hc}$ and the set of multicoforks of $I$.

the parallel pair diagram of I (from the name)

Let $I$ be a multispan index of $J$ and $C$. Then the parallel pair diagram of $I$ is a functor of the set of walking parallel pairs and $C$ defined as the parallel pair of the induced map of $I$ and the induced map of $I$.

the parallel pair diagram of d and hc (from the name)

Let $I$ be a multispan index of $J$ and $C$. Let $d$ be a cofan of $\operatorname{right}$ applied to $I$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the parallel pair diagram of $d$ and $\mathrm{hc}$ is a functor of the set of walking parallel pairs and $C$ defined as the parallel pair of the first component sigma map of $d$ and $\mathrm{hc}$ and the second component sigma map of $d$ and $\mathrm{hc}$.

the right of self and x1 (from the name)

Let $\mathrm{self}$ be a multispan index of $J$ and $C$. Let $x_{1}$ be an element of $\operatorname{R}$ applied to $J$. Then the right of $\mathrm{self}$ and $x_{1}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.

the second component of self and a (from the name)

Let $\mathrm{self}$ be a multispan index of $J$ and $C$. Let $a$ be an element of $\operatorname{L}$ applied to $J$. Then the second component of $\mathrm{self}$ and $a$ is a homomorphism of the left of $\mathrm{self}$ and $a$ and the right of $\mathrm{self}$ and the second map of $J$ and $a$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $a$.

the induced map of I (from the docstring)

Let $I$ be a multispan index of $J$ and $C$. Then the induced map of $I$ is a homomorphism of the sigma object of $\operatorname{left}$ applied to $I$ and the sigma object of $\operatorname{right}$ applied to $I$ defined as the second component sigma map of the cocone of the functor of $\operatorname{right}$ applied to $I$ and $\operatorname{isColimit}$ applied to the functor of $\operatorname{left}$ applied to $I$.

the second component sigma map of d and hc (from the name)

Let $I$ be a multispan index of $J$ and $C$. Let $d$ be a cofan of $\operatorname{right}$ applied to $I$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the second component sigma map of $d$ and $\mathrm{hc}$ is a homomorphism of $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $d$ defined as $\operatorname{desc}$ applied to $\mathrm{hc}$ and the function that maps $i$ to the composition of the second component of $I$ and $i$ and the injection of $d$ and the second map of $J$ and $i$.

the linear order of I (from the name)

Let $I$ be a multispan index of the product of $x_{1}$ and $C$. Then the linear order of $I$ is a multispan index of the multispan shape of $x_{1}$ and $C$ defined as $\operatorname{mk}$ applied to the function that maps $j$ to the left of $I$ and $j$, the function that maps $i$ to the right of $I$ and $i$, the function that maps $j_{1}$ to the first component of $I$ and $j_{1}$ and the function that maps $j_{2}$ to the second component of $I$ and $j_{2}$.

the linear order multispan isomorphism of I (from the name)

Let $I$ be a multispan index of the product of $x_{1}$ and $C$. Then the linear order multispan isomorphism of $I$ is an isomorphism of the composition of the inclusion functor of $x_{1}$ and the multispan of $I$ and the multispan of the linear order of $I$.

the sigma cofork functor of hc and hd (from the name)

Let $I$ be a multispan index of $J$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{hd}$ be an element of $\operatorname{IsColimit}$ applied to $d$. Then the sigma cofork functor of $\mathrm{hc}$ and $\mathrm{hd}$ is a functor of the set of multicoforks of $I$ and the set of coforks of the first component sigma map of $d$ and $\mathrm{hc}$ and the second component sigma map of $d$ and $\mathrm{hc}$.

shape (from the docstring)

The shapes are a basic type.

Let $\mathrm{self}$ be a shape. Then an element of $\operatorname{L}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a shape. Then an element of $\operatorname{R}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj1}$ applied to $\mathrm{self}$.

the first map of self and x (from the docstring)

Let $\mathrm{self}$ be a shape. Let $x$ be an element of $\operatorname{L}$ applied to $\mathrm{self}$. Then the first map of $\mathrm{self}$ and $x$ is an element of $\operatorname{R}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x$.

the multispan shape of x (from the name)

Let $x$ be a set. Then the multispan shape of $x$ is a shape defined as $\operatorname{mk}$ applied to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\mathrm{Lt} (\ProdfstMACRoZ {x_{2}}, \ProdsndMACRoAA {x_{2}})$, $x$, the function that maps $x_{3}$ to $\ProdfstMACRoZ {x_{3}}$ and the function that maps $x_{4}$ to $\ProdsndMACRoAA {x_{4}}$.

the product of x (from the name)

Let $x$ be a set. Then the product of $x$ is a shape defined as $\operatorname{mk}$ applied to $\mathrm{Prod}$ applied to $x$ and $x$, $x$, $\ProdfstMACRoZ$ and $\ProdsndMACRoAA$.

the second map of self and x (from the docstring)

Let $\mathrm{self}$ be a shape. Let $x$ be an element of $\operatorname{L}$ applied to $\mathrm{self}$. Then the second map of $\mathrm{self}$ and $x$ is an element of $\operatorname{R}$ applied to $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $x$.

walking multicospan of J (from the name)

Let $J$ be a shape. Then the walking multicospans of $J$ are a basic type.

homomorphism of x and x1 (from the name)

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

the composition of x and x1 (from the name)

Let $x$ be a homomorphism of $A$ and $B$. Let $x_{1}$ be a homomorphism of $B$ and $C$. Then the composition of $x$ and $x_{1}$ is a homomorphism of $A$ and $C$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from walking multicospans $A$ of $J$ to elements of $\mathrm{motive}$ applied to $A$, $A$ and the identity of $A$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to the set of functions from elements $b$ of $\operatorname{R}$ applied to $J$ to elements of $\mathrm{motive}$ applied to the left of the first map of $J$ and $b$, the right of $b$ and the first component of $b$ and $\mathrm{PULift}$ applied to the set of functions from elements $b_{1}$ of $\operatorname{R}$ applied to $J$ to elements of $\mathrm{motive}$ applied to the left of the second map of $J$ and $b_{1}$, the right of $b_{1}$ and the second component of $b_{1}$.

the first component of b (from the name)

Let $b$ be an element of $\operatorname{R}$ applied to $J$. Then the first component of $b$ is a homomorphism of the left of the first map of $J$ and $b$ and the right of $b$.

the identity of A (from the name)

Let $A$ be a walking multicospan of $J$. Then the identity of $A$ is a homomorphism of $A$ and $A$.

the second component of b (from the name)

Let $b$ be an element of $\operatorname{R}$ applied to $J$. Then the second component of $b$ is a homomorphism of the left of the second map of $J$ and $b$ and the right of $b$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x$ of $\operatorname{L}$ applied to $J$ to elements of $\mathrm{motive}$ applied to the left of $x$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $\operatorname{R}$ applied to $J$ to elements of $\mathrm{motive}$ applied to the right of $x_{1}$.

the functor extension of left and i3 (from the name)

Let $\mathrm{left}$ be a function from elements $i_{3}$ of $\operatorname{L}$ applied to $J$ to isomorphisms of the action of $F$ and the left of $i_{3}$ and the action of $G$ and the left of $i_{3}$. Let $\mathrm{right}$ be a function from elements $i_{2}$ of $\operatorname{R}$ applied to $J$ to isomorphisms of the action of $F$ and the right of $i_{2}$ and the action of $G$ and the right of $i_{2}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $i_{1}$ of $\operatorname{R}$ applied to $J$, the composition of the map of $F$ and the first component of $i_{1}$ and the homomorphism of $\mathrm{right}$ applied to $i_{1}$ is equal to the composition of the homomorphism of $\mathrm{left}$ applied to the first map of $J$ and $i_{1}$ and the map of $G$ and the first component of $i_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_WalkingMulticospan\_\_functorExt\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ of $\operatorname{R}$ applied to $J$, the composition of the map of $F$ and the second component of $i$ and the homomorphism of $\mathrm{right}$ applied to $i$ is equal to the composition of the homomorphism of $\mathrm{left}$ applied to the second map of $J$ and $i$ and the map of $G$ and the second component of $i$ and $\mathrm{CategoryTheory\_\_Limits\_\_WalkingMulticospan\_\_functorExt\_\_\_auto\_3}$. Then the functor extension of $i_{3}$ and $\mathrm{left}$ is an isomorphism of $F$ and $G$.

the left of x (from the name)

Let $x$ be an element of $\operatorname{L}$ applied to $J$. Then the left of $x$ is a walking multicospan of $J$.

the right of x (from the name)

Let $x$ be an element of $\operatorname{R}$ applied to $J$. Then the right of $x$ is a walking multicospan of $J$.

walking multispan of J (from the name)

Let $J$ be a shape. Then the walking multispans of $J$ are a basic type.

homomorphism of x and x1 (from the name)

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

the composition of x and x1 (from the name)

Let $x$ be a homomorphism of $A$ and $B$. Let $x_{1}$ be a homomorphism of $B$ and $C$. Then the composition of $x$ and $x_{1}$ is a homomorphism of $A$ and $C$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from walking multispans $A$ of $J$ to elements of $\mathrm{motive}$ applied to $A$, $A$ and the identity of $A$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to the set of functions from elements $a$ of $\operatorname{L}$ applied to $J$ to elements of $\mathrm{motive}$ applied to the left of $a$, the right of the first map of $J$ and $a$ and the first component of $a$ and $\mathrm{PULift}$ applied to the set of functions from elements $a_{1}$ of $\operatorname{L}$ applied to $J$ to elements of $\mathrm{motive}$ applied to the left of $a_{1}$, the right of the second map of $J$ and $a_{1}$ and the second component of $a_{1}$.

the first component of a (from the name)

Let $a$ be an element of $\operatorname{L}$ applied to $J$. Then the first component of $a$ is a homomorphism of the left of $a$ and the right of the first map of $J$ and $a$.

the identity of A (from the name)

Let $A$ be a walking multispan of $J$. Then the identity of $A$ is a homomorphism of $A$ and $A$.

the second component of a (from the name)

Let $a$ be an element of $\operatorname{L}$ applied to $J$. Then the second component of $a$ is a homomorphism of the left of $a$ and the right of the second map of $J$ and $a$.

the arrow equivalence of J (from the name)

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

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x$ of $\operatorname{L}$ applied to $J$ to elements of $\mathrm{motive}$ applied to the left of $x$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $\operatorname{R}$ applied to $J$ to elements of $\mathrm{motive}$ applied to the right of $x_{1}$.

the equivalence of J (from the name)

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

the functor extension of left and i3 (from the name)

Let $\mathrm{left}$ be a function from elements $i_{3}$ of $\operatorname{L}$ applied to $J$ to isomorphisms of the action of $F$ and the left of $i_{3}$ and the action of $G$ and the left of $i_{3}$. Let $\mathrm{right}$ be a function from elements $i_{2}$ of $\operatorname{R}$ applied to $J$ to isomorphisms of the action of $F$ and the right of $i_{2}$ and the action of $G$ and the right of $i_{2}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $i_{1}$ of $\operatorname{L}$ applied to $J$, the composition of the map of $F$ and the first component of $i_{1}$ and the homomorphism of $\mathrm{right}$ applied to the first map of $J$ and $i_{1}$ is equal to the composition of the homomorphism of $\mathrm{left}$ applied to $i_{1}$ and the map of $G$ and the first component of $i_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_WalkingMultispan\_\_functorExt\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ of $\operatorname{L}$ applied to $J$, the composition of the map of $F$ and the second component of $i$ and the homomorphism of $\mathrm{right}$ applied to the second map of $J$ and $i$ is equal to the composition of the homomorphism of $\mathrm{left}$ applied to $i$ and the map of $G$ and the second component of $i$ and $\mathrm{CategoryTheory\_\_Limits\_\_WalkingMultispan\_\_functorExt\_\_\_auto\_3}$. Then the functor extension of $i_{3}$ and $\mathrm{left}$ is an isomorphism of $F$ and $G$.

the inclusion functor of x (from the docstring)

Let $x$ be a set. Then the inclusion functor of $x$ is a functor of the set of walking multispans of the multispan shape of $x$ and the set of walking multispans of the product of $x$ defined as the multispan of $\operatorname{mk}$ applied to the function that maps $j$ to the left of $j$, the function that maps $i$ to the right of $i$, the function that maps $j_{1}$ to the first component of $j_{1}$ and the function that maps $j_{2}$ to the second component of $j_{2}$.

the left of x (from the name)

Let $x$ be an element of $\operatorname{L}$ applied to $J$. Then the left of $x$ is a walking multispan of $J$.

the right of x (from the name)

Let $x$ be an element of $\operatorname{R}$ applied to $J$. Then the right of $x$ is a walking multispan of $J$.

the multicoequalizer of I (from the docstring)

Let $I$ be a multispan index of $J$ and $C$. Then the multicoequalizer of $I$ is an element of $C$ defined as the colimit of the multispan of $I$.

the multiequalizer of I (from the docstring)

Let $I$ be a multicospan index of $J$ and $C$. Then the multiequalizer of $I$ is an element of $C$ defined as the limit of the multicospan of $I$.

the multicofork of #3 (from the name)

Assume that $\operatorname{insert}$ applied to the first map of $J$ and $\operatorname{default}$ and $\operatorname{singleton}$ applied to the second map of $J$ and $\operatorname{default}$ is equal to the universal set. Assume that the first map of $J$ and $\operatorname{default}$ is distinct from the second map of $J$ and $\operatorname{default}$. Let $s$ be a pushout cocone of the first component of $I$ and $\operatorname{default}$ and the second component of $I$ and $\operatorname{default}$. Then the multicofork of $s$ is a multicofork of $I$.

C is a normal epimorphism category (from the name)

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

C is a normal monomorphism category (from the name)

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

f is a normal epimorphism (from the name)

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

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

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

$\operatorname{g}$ is a homomorphism of $\operatorname{W}$ applied to $f$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

$\operatorname{isColimit}$ is an element of $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{w}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the regular epimorphism of f (from the name)

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

f is a normal monomorphism (from the name)

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

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

$\operatorname{g}$ is a homomorphism of $Y$ and $\operatorname{Z}$ applied to $f$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

$\operatorname{isLimit}$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of $f$ and $\operatorname{w}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the lift of f and k (from the name)

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

the regular monomorphism of f (from the name)

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

$\operatorname{isColimitCoforkPushoutEquivIsColimitForkOpPullback}$ is an equivalence from $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{condition}$ to $\operatorname{IsLimit}$ applied to the inclusion of the opposite in $f$ and $\operatorname{condition}$.

$\operatorname{isColimitCoforkPushoutEquivIsColimitForkUnopPullback}$ is an equivalence from $\operatorname{IsColimit}$ applied to the projection of $f$ and $\operatorname{condition}$ to $\operatorname{IsLimit}$ applied to the inclusion of the opposite of $f$ and $\operatorname{condition}$.

Let $c$ be a cofork of $f$ and $g$. Then $\operatorname{isColimitEquivIsLimitOp}$ applied to $c$ is an equivalence from $\operatorname{IsColimit}$ applied to $c$ to $\operatorname{IsLimit}$ applied to the opposite of $c$ defined as the equivalence of the function that maps $h$ to the inverse function of the postcomposition homomorphism equivalence of the inverse of the parallel pair opposite isomorphism of $f$ and $g$ and the whisker of the functor of the equivalence and the opposite of $c$ and the forward map of the whisker equivalence equivalence of the equivalence and the opposite of $h$ and the function that maps $h_{1}$ to the forward map of the equivalence isomorphism colimit of the opposite opposite isomorphism of $c$ and the opposite of the inverse function of the postcomposition homomorphism equivalence of the inverse of the opposite parallel pair isomorphism of the opposite of the opposite in $f$ and the opposite of the opposite in $g$ and the whisker of the functor of the inverse of the equivalence and the opposite of $c$ and the forward map of the whisker equivalence equivalence of the inverse of the equivalence and $h_{1}$.

Let $c$ be a cofork of $f$ and $g$. Then $\operatorname{isColimitEquivIsLimitUnop}$ applied to $c$ is an equivalence from $\operatorname{IsColimit}$ applied to $c$ to $\operatorname{IsLimit}$ applied to the opposite of $c$ defined as the equivalence of the function that maps $h$ to the opposite of the inverse function of the precomposition homomorphism equivalence of the opposite parallel pair isomorphism of the opposite of $f$ and the opposite of $g$ and the whisker of the functor of the inverse of the equivalence and $c$ and the forward map of the whisker equivalence equivalence of the inverse of the equivalence and $h$ and the function that maps $h_{1}$ to the forward map of the equivalence isomorphism colimit of the opposite opposite isomorphism of $c$ and the inverse function of the precomposition homomorphism equivalence of the parallel pair opposite isomorphism of the opposite of $f$ and the opposite of $g$ and the whisker of the functor of the equivalence and the opposite of the opposite of $c$ and the forward map of the whisker equivalence equivalence of the equivalence and the opposite of $h_{1}$.

Let $x_{1}$ and $x_{2}$ be homomorphisms of $Y$ and $P$ such that the composition of $f$ and $x_{1}$ is equal to the composition of $g$ and $x_{1}$, the composition of the opposite in $x_{2}$ and the opposite in $f$ is equal to the composition of the opposite in $x_{2}$ and the opposite in $g$ and $\EqtMACRoH {x_{1}}{x_{2}}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_Cofork\_\_isColimitOf\_u3c0\_EquivIsLimitOp}$ applied to $x_{1}$, $x_{2}$, $w$, $\mathrm{w'}$ and $h$ is an equivalence from $\operatorname{IsColimit}$ applied to the projection of $x_{1}$ and $w$ to $\operatorname{IsLimit}$ applied to the inclusion of the opposite in $x_{2}$ and $\mathrm{w'}$ defined as the composition of $\operatorname{isColimitEquivIsLimitOp}$ applied to the projection of $x_{1}$ and $w$ and the equivalence isomorphism limit of the projection opposite isomorphism of $x_{1}$ and $x_{2}$.

the colimit cocone in x1 (from the docstring)

Let $x_{1}$ and $x_{2}$ be homomorphisms of $Y$ and $P$ such that the composition of $f$ and $x_{1}$ is equal to the composition of $g$ and $x_{1}$, the composition of the opposite of $x_{2}$ and the opposite of $f$ is equal to the composition of the opposite of $x_{2}$ and the opposite of $g$ and $\EqtMACRoH {x_{1}}{x_{2}}$. Then the colimit cocone in $x_{1}$ is an equivalence from $\operatorname{IsColimit}$ applied to the projection of $x_{1}$ and $w$ to $\operatorname{IsLimit}$ applied to the inclusion of the opposite of $x_{2}$ and $\mathrm{w'}$ defined as the composition of $\operatorname{isColimitEquivIsLimitUnop}$ applied to the projection of $x_{1}$ and $w$ and the equivalence isomorphism limit of the projection opposite isomorphism of $x_{1}$ and $x_{2}$.

the projection opposite isomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be homomorphisms of $Y$ and $P$ such that the composition of $f$ and $x_{1}$ is equal to the composition of $g$ and $x_{1}$, the composition of the opposite in $x_{2}$ and the opposite in $f$ is equal to the composition of the opposite in $x_{2}$ and the opposite in $g$ and $\EqtMACRoH {x_{1}}{x_{2}}$. Then the projection opposite isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of the opposite of the projection of $x_{1}$ and $w$ and the inclusion of the opposite in $x_{2}$ and $\mathrm{w'}$.

the projection opposite isomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be homomorphisms of $Y$ and $P$ such that the composition of $f$ and $x_{1}$ is equal to the composition of $g$ and $x_{1}$, the composition of the opposite of $x_{2}$ and the opposite of $f$ is equal to the composition of the opposite of $x_{2}$ and the opposite of $g$ and $\EqtMACRoH {x_{1}}{x_{2}}$. Then the projection opposite isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of the opposite of the projection of $x_{1}$ and $w$ and the inclusion of the opposite of $x_{2}$ and $\mathrm{w'}$.

the opposite of c (from the name)

Let $c$ be a cofork of $f$ and $g$. Then the opposite of $c$ is a fork of the opposite in $f$ and the opposite in $g$ defined as the action of the postcomposition of the homomorphism of the inverse of the parallel pair opposite isomorphism of $f$ and $g$ and the whisker of the functor of the equivalence and the opposite of $c$.

the opposite opposite isomorphism of c (from the name)

Let $c$ be a cofork of $f$ and $g$. Then the opposite opposite isomorphism of $c$ is an isomorphism of the opposite of the opposite of $c$ and $c$.

the opposite of c (from the name)

Let $c$ be a cofork of $f$ and $g$. Then the opposite of $c$ is a fork of the opposite of $f$ and the opposite of $g$ defined as the opposite of the action of the precomposition of the homomorphism of the opposite parallel pair isomorphism of the opposite of $f$ and the opposite of $g$ and the whisker of the inverse of the equivalence and $c$.

the opposite opposite isomorphism of c (from the name)

Let $c$ be a cofork of $f$ and $g$. Then the opposite opposite isomorphism of $c$ is an isomorphism of the opposite of the opposite of $c$ and $c$.

Let $c$ be a fork of $f$ and $g$. Then $\operatorname{isLimitEquivIsColimitOp}$ applied to $c$ is an equivalence from $\operatorname{IsLimit}$ applied to $c$ to $\operatorname{IsColimit}$ applied to the opposite of $c$ defined as the composition of the inverse of the equivalence isomorphism limit of the opposite opposite isomorphism of $c$ and the inverse of $\operatorname{isColimitEquivIsLimitUnop}$ applied to the opposite of $c$.

Let $c$ be a fork of $f$ and $g$. Then $\operatorname{isLimitEquivIsColimitUnop}$ applied to $c$ is an equivalence from $\operatorname{IsLimit}$ applied to $c$ to $\operatorname{IsColimit}$ applied to the opposite of $c$ defined as the composition of the inverse of the equivalence isomorphism limit of the opposite opposite isomorphism of $c$ and the inverse of $\operatorname{isColimitEquivIsLimitOp}$ applied to the opposite of $c$.

$\operatorname{isLimitForkPushoutEquivIsColimitForkOpPullback}$ is an equivalence from $\operatorname{IsLimit}$ applied to the inclusion of $f$ and $\operatorname{condition}$ to $\operatorname{IsColimit}$ applied to the projection of the opposite in $f$ and $\operatorname{condition}$.

$\operatorname{isLimitForkPushoutEquivIsColimitForkUnopPullback}$ is an equivalence from $\operatorname{IsLimit}$ applied to the inclusion of $f$ and $\operatorname{condition}$ to $\operatorname{IsColimit}$ applied to the projection of the opposite of $f$ and $\operatorname{condition}$.

Let $x_{1}$ and $x_{2}$ be homomorphisms of $P$ and $X$ such that the composition of $x_{1}$ and $f$ is equal to the composition of $x_{1}$ and $g$, the composition of the opposite in $f$ and the opposite in $x_{2}$ is equal to the composition of the opposite in $g$ and the opposite in $x_{2}$ and $\EqtMACRoH {x_{1}}{x_{2}}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_Fork\_\_isLimitOf\_u3b9\_EquivIsColimitOp}$ applied to $x_{1}$, $x_{2}$, $w$, $\mathrm{w'}$ and $h$ is an equivalence from $\operatorname{IsLimit}$ applied to the inclusion of $x_{1}$ and $w$ to $\operatorname{IsColimit}$ applied to the projection of the opposite in $x_{2}$ and $\mathrm{w'}$ defined as the composition of $\operatorname{isLimitEquivIsColimitOp}$ applied to the inclusion of $x_{1}$ and $w$ and the equivalence isomorphism colimit of the inclusion opposite isomorphism of $x_{1}$ and $x_{2}$.

the limit cone in x1 (from the docstring)

Let $x_{1}$ and $x_{2}$ be homomorphisms of $P$ and $X$ such that the composition of $x_{1}$ and $f$ is equal to the composition of $x_{1}$ and $g$, the composition of the opposite of $f$ and the opposite of $x_{2}$ is equal to the composition of the opposite of $g$ and the opposite of $x_{2}$ and $\EqtMACRoH {x_{1}}{x_{2}}$. Then the limit cone in $x_{1}$ is an equivalence from $\operatorname{IsLimit}$ applied to the inclusion of $x_{1}$ and $w$ to $\operatorname{IsColimit}$ applied to the projection of the opposite of $x_{2}$ and $\mathrm{w'}$ defined as the composition of $\operatorname{isLimitEquivIsColimitUnop}$ applied to the inclusion of $x_{1}$ and $w$ and the equivalence isomorphism colimit of the inclusion opposite isomorphism of $x_{1}$ and $x_{2}$.

the inclusion opposite isomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be homomorphisms of $P$ and $X$ such that the composition of $x_{1}$ and $f$ is equal to the composition of $x_{1}$ and $g$, the composition of the opposite in $f$ and the opposite in $x_{2}$ is equal to the composition of the opposite in $g$ and the opposite in $x_{2}$ and $\EqtMACRoH {x_{1}}{x_{2}}$. Then the inclusion opposite isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of the opposite of the inclusion of $x_{1}$ and $w$ and the projection of the opposite in $x_{2}$ and $\mathrm{w'}$.

the inclusion opposite isomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be homomorphisms of $P$ and $X$ such that the composition of $x_{1}$ and $f$ is equal to the composition of $x_{1}$ and $g$, the composition of the opposite of $f$ and the opposite of $x_{2}$ is equal to the composition of the opposite of $g$ and the opposite of $x_{2}$ and $\EqtMACRoH {x_{1}}{x_{2}}$. Then the inclusion opposite isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of the opposite of the inclusion of $x_{1}$ and $w$ and the projection of the opposite of $x_{2}$ and $\mathrm{w'}$.

the opposite of c (from the name)

Let $c$ be a fork of $f$ and $g$. Then the opposite of $c$ is a cofork of the opposite in $f$ and the opposite in $g$ defined as the action of the precomposition of the homomorphism of the parallel pair opposite isomorphism of $f$ and $g$ and the whisker of the functor of the equivalence and the opposite of $c$.

the opposite opposite isomorphism of c (from the name)

Let $c$ be a fork of $f$ and $g$. Then the opposite opposite isomorphism of $c$ is an isomorphism of the opposite of the opposite of $c$ and $c$.

the opposite of c (from the name)

Let $c$ be a fork of $f$ and $g$. Then the opposite of $c$ is a cofork of the opposite of $f$ and the opposite of $g$ defined as the opposite of the action of the postcomposition of the homomorphism of the inverse of the opposite parallel pair isomorphism of the opposite of $f$ and the opposite of $g$ and the whisker of the inverse of the equivalence and $c$.

the opposite opposite isomorphism of c (from the name)

Let $c$ be a fork of $f$ and $g$. Then the opposite opposite isomorphism of $c$ is an isomorphism of the opposite of the opposite of $c$ and $c$.

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

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the opposite parallel pair isomorphism of $f$ and $g$ is an isomorphism of the opposite of the parallel pair of $f$ and $g$ and the composition of the inverse of the equivalence and the parallel pair of the opposite in $f$ and the opposite in $g$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the identity of the opposite of the parallel pair of $f$ and $g$ and the right isomorphism whisker of the unit isomorphism of the inverse of the equivalence and the opposite of the parallel pair of $f$ and $g$ and the associator of the functor of the equivalence and the opposite of the parallel pair of $f$ and $g$ and the left isomorphism whisker of the inverse of the equivalence and the inverse of the parallel pair opposite isomorphism of $f$ and $g$.

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

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the parallel pair opposite isomorphism of $f$ and $g$ is an isomorphism of the parallel pair of the opposite in $f$ and the opposite in $g$ and the composition of the functor of the equivalence and the opposite of the parallel pair of $f$ and $g$.

the projection opposite of p and h (from the name)

Let $p$ be a homomorphism of $Y$ and $Q$ such that the composition of $f$ and $p$ is equal to $0$. Let $h$ be an element of $\operatorname{IsColimit}$ applied to the projection of $p$ and $w$. Then the projection opposite of $p$ and $h$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the opposite in $p$ and $\mathrm{CategoryTheory\_\_Limits\_\_CokernelCofork\_\_IsColimit\_\_of\_u3c0\_Op\_\_\_proof\_1}$ applied to $p$ and $w$.

the projection opposite of p and h (from the name)

Let $p$ be a homomorphism of $Y$ and $Q$ such that the composition of $f$ and $p$ is equal to $0$. Let $h$ be an element of $\operatorname{IsColimit}$ applied to the projection of $p$ and $w$. Then the projection opposite of $p$ and $h$ is an element of $\operatorname{IsLimit}$ applied to the inclusion of the opposite of $p$ and $\mathrm{CategoryTheory\_\_Limits\_\_CokernelCofork\_\_IsColimit\_\_of\_u3c0\_Unop\_\_\_proof\_1}$ applied to $p$ and $w$.

the inclusion opposite of i and h (from the name)

Let $i$ be a homomorphism of $K$ and $X$ such that the composition of $i$ and $f$ is equal to $0$. Let $h$ be an element of $\operatorname{IsLimit}$ applied to the inclusion of $i$ and $w$. Then the inclusion opposite of $i$ and $h$ is an element of $\operatorname{IsColimit}$ applied to the projection of the opposite in $i$ and $\mathrm{CategoryTheory\_\_Limits\_\_KernelFork\_\_IsLimit\_\_of\_u3b9\_Op\_\_\_proof\_1}$ applied to $i$ and $w$.

the inclusion opposite of i and h (from the name)

Let $i$ be a homomorphism of $K$ and $X$ such that the composition of $i$ and $f$ is equal to $0$. Let $h$ be an element of $\operatorname{IsLimit}$ applied to the inclusion of $i$ and $w$. Then the inclusion opposite of $i$ and $h$ is an element of $\operatorname{IsColimit}$ applied to the projection of the opposite of $i$ and $\mathrm{CategoryTheory\_\_Limits\_\_KernelFork\_\_IsLimit\_\_of\_u3b9\_Unop\_\_\_proof\_1}$ applied to $i$ and $w$.

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 c (from the name)

Let $c$ be a cofan of $Z$. Then the opposite of $c$ is an element of $\operatorname{Fan}$ applied to the function that maps $x_{2}$ to $\operatorname{op}$ applied to $Z$ applied to $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ and the function that maps $a$ to the opposite in the injection of $c$ and $a$.

the opposite of hf (from the name)

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

the opposite of f (from the name)

Let $f$ be an element of $\operatorname{Fan}$ applied to $Z$. Then the opposite of $f$ is a cofan of the function that maps $x_{2}$ to $\operatorname{op}$ applied to $Z$ applied to $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $f$ and the function that maps $a$ to the opposite in the projection of $f$ and $a$.

the opposite coproduct isomorphism product of Z (from the name)

Let $Z$ be a function from elements of $x_{1}$ to elements of $C$. Then the opposite coproduct isomorphism product of $Z$ is an isomorphism of $\operatorname{op}$ applied to the sigma object of $Z$ and the product object of the function that maps $x_{2}$ to $\operatorname{op}$ applied to $Z$ applied to $x_{2}$ defined as the canonical isomorphism from the opposite of $\operatorname{coproductIsCoproduct}$ applied to $Z$ and $\operatorname{productIsProduct}$ applied to the function that maps $x_{2}$ to $\operatorname{op}$ applied to $Z$ applied to $x_{2}$.

the canonical isomorphism from the opposite of hc and hf (from the docstring)

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{hf}$ be an element of $\operatorname{IsLimit}$ applied to $f$. Then the canonical isomorphism from the opposite of $\mathrm{hc}$ and $\mathrm{hf}$ is an isomorphism of $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{pt}$ applied to $f$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to the opposite of $\mathrm{hc}$ and $\mathrm{hf}$.

the opposite product isomorphism coproduct of A and B (from the name)

Let $A$ and $B$ be elements of $C$. Then the opposite product isomorphism coproduct of $A$ and $B$ is an isomorphism of $\operatorname{op}$ applied to the product of $A$ and $B$ and the coproduct of $\operatorname{op}$ applied to $A$ and $\operatorname{op}$ applied to $B$.

the opposite product isomorphism coproduct of Z (from the name)

Let $Z$ be a function from elements of $x_{1}$ to elements of $C$. Then the opposite product isomorphism coproduct of $Z$ is an isomorphism of $\operatorname{op}$ applied to the product object of $Z$ and the sigma object of the function that maps $x_{2}$ to $\operatorname{op}$ applied to $Z$ applied to $x_{2}$ defined as the canonical isomorphism from the opposite of $\operatorname{productIsProduct}$ applied to $Z$ and $\operatorname{coproductIsCoproduct}$ applied to the function that maps $x_{2}$ to $\operatorname{op}$ applied to $Z$ applied to $x_{2}$.

the canonical isomorphism from the opposite of hf and hc (from the docstring)

Let $\mathrm{hf}$ be an element of $\operatorname{IsLimit}$ applied to $f$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the canonical isomorphism from the opposite of $\mathrm{hf}$ and $\mathrm{hc}$ is an isomorphism of $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $f$ and $\operatorname{pt}$ applied to $c$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to the opposite of $\mathrm{hf}$ and $\mathrm{hc}$.

the cocone opposite of p (from the name)

Assume that $\operatorname{CommSq}$ holds for $f$, $g$, $h$ and $i$. Then the cocone opposite of $p$ is an isomorphism of the opposite of the cocone of $p$ and the cone of $\operatorname{op}$ applied to $\operatorname{flip}$ applied to $p$.

the cocone opposite of p (from the name)

Assume that $\operatorname{CommSq}$ holds for $f$, $g$, $h$ and $i$. Then the cocone opposite of $p$ is an isomorphism of the opposite of the cocone of $p$ and the cone of $\operatorname{unop}$ applied to $\operatorname{flip}$ applied to $p$.

the cone opposite of p (from the name)

Assume that $\operatorname{CommSq}$ holds for $f$, $g$, $h$ and $i$. Then the cone opposite of $p$ is an isomorphism of the opposite of the cone of $p$ and the cocone of $\operatorname{op}$ applied to $\operatorname{flip}$ applied to $p$.

the cone opposite of p (from the name)

Assume that $\operatorname{CommSq}$ holds for $f$, $g$, $h$ and $i$. Then the cone opposite of $p$ is an isomorphism of the opposite of the cone of $p$ and the cocone of $\operatorname{unop}$ applied to $\operatorname{flip}$ applied to $p$.

Let $c$ be a pullback cone of $f$ and $g$. Then $\operatorname{isLimitEquivIsColimitOp}$ applied to $c$ is an equivalence from $\operatorname{IsLimit}$ applied to $c$ to $\operatorname{IsColimit}$ applied to the opposite of $c$ defined as the composition of the inverse of the equivalence isomorphism limit of the opposite opposite isomorphism of $c$ and the inverse of $\operatorname{isColimitEquivIsLimitUnop}$ applied to the opposite of $c$.

Let $c$ be a pullback cone of $f$ and $g$. Then $\operatorname{isLimitEquivIsColimitUnop}$ applied to $c$ is an equivalence from $\operatorname{IsLimit}$ applied to $c$ to $\operatorname{IsColimit}$ applied to the opposite of $c$ defined as the composition of the inverse of the equivalence isomorphism limit of the opposite opposite isomorphism of $c$ and the inverse of $\operatorname{isColimitEquivIsLimitOp}$ applied to the opposite of $c$.

the opposite of c (from the name)

Let $c$ be a pullback cone of $f$ and $g$. Then the opposite of $c$ is a pushout cocone of the opposite in $f$ and the opposite in $g$ defined as the action of the precomposition of the homomorphism of the span opposite of $f$ and $g$ and the whisker of the inverse of the duality equivalence and the opposite of $c$.

the opposite opposite isomorphism of c (from the name)

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

the opposite of c (from the name)

Let $c$ be a pullback cone of $f$ and $g$. Then the opposite of $c$ is a pushout cocone of the opposite of $f$ and the opposite of $g$ defined as the opposite of the action of the postcomposition of the homomorphism of the inverse of the opposite span of the opposite of $f$ and the opposite of $g$ and the whisker of the functor of the duality equivalence and $c$.

the opposite opposite isomorphism of c (from the name)

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

Let $c$ be a pushout cocone of $f$ and $g$. Then $\operatorname{isColimitEquivIsLimitOp}$ applied to $c$ is an equivalence from $\operatorname{IsColimit}$ applied to $c$ to $\operatorname{IsLimit}$ applied to the opposite of $c$ defined as the equivalence of the function that maps $h$ to the inverse function of the postcomposition homomorphism equivalence of the inverse of the cospan opposite of $f$ and $g$ and the whisker of the inverse of the duality equivalence and the opposite of $c$ and the forward map of the whisker equivalence equivalence of the inverse of the duality equivalence and the opposite of $h$ and the function that maps $h_{1}$ to the forward map of the equivalence isomorphism colimit of the opposite opposite isomorphism of $c$ and the opposite of the inverse function of the postcomposition homomorphism equivalence of the inverse of the opposite span of the opposite of the opposite in $f$ and the opposite of the opposite in $g$ and the whisker of the functor of the duality equivalence and the opposite of $c$ and the forward map of the whisker equivalence equivalence of the duality equivalence and $h_{1}$.

Let $c$ be a pushout cocone of $f$ and $g$. Then $\operatorname{isColimitEquivIsLimitUnop}$ applied to $c$ is an equivalence from $\operatorname{IsColimit}$ applied to $c$ to $\operatorname{IsLimit}$ applied to the opposite of $c$ defined as the equivalence of the function that maps $h$ to the opposite of the inverse function of the precomposition homomorphism equivalence of the opposite cospan of the opposite of $f$ and the opposite of $g$ and the whisker of the functor of the duality equivalence and $c$ and the forward map of the whisker equivalence equivalence of the duality equivalence and $h$ and the function that maps $h_{1}$ to the forward map of the equivalence isomorphism colimit of the opposite opposite isomorphism of $c$ and the inverse function of the precomposition homomorphism equivalence of the span opposite of the opposite of $f$ and the opposite of $g$ and the whisker of the inverse of the duality equivalence and the opposite of the opposite of $c$ and the forward map of the whisker equivalence equivalence of the inverse of the duality equivalence and the opposite of $h_{1}$.

the opposite of c (from the name)

Let $c$ be a pushout cocone of $f$ and $g$. Then the opposite of $c$ is a pullback cone of the opposite in $f$ and the opposite in $g$ defined as the action of the postcomposition of the homomorphism of the inverse of the cospan opposite of $f$ and $g$ and the whisker of the inverse of the duality equivalence and the opposite of $c$.

the opposite opposite isomorphism of c (from the name)

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

the opposite of c (from the name)

Let $c$ be a pushout cocone of $f$ and $g$. Then the opposite of $c$ is a pullback cone of the opposite of $f$ and the opposite of $g$ defined as the opposite of the action of the precomposition of the homomorphism of the opposite cospan of the opposite of $f$ and the opposite of $g$ and the whisker of the functor of the duality equivalence and $c$.

the opposite opposite isomorphism of c (from the name)

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

the cospan opposite of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the cospan opposite of $f$ and $g$ is an isomorphism of the cospan of the opposite in $f$ and the opposite in $g$ and the composition of the inverse of the duality equivalence and the opposite of the span of $f$ and $g$.

the cospan opposite of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the cospan opposite of $f$ and $g$ is an isomorphism of the cospan of the opposite of $f$ and the opposite of $g$ and the composition of the inverse of the duality equivalence and the left opposite of the span of $f$ and $g$.

the opposite cospan of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the opposite cospan of $f$ and $g$ is an isomorphism of the opposite of the cospan of $f$ and $g$ and the composition of the functor of the duality equivalence and the span of the opposite in $f$ and the opposite in $g$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the identity of the opposite of the cospan of $f$ and $g$ and the right isomorphism whisker of the unit isomorphism of the duality equivalence and the opposite of the cospan of $f$ and $g$ and the associator of the inverse of the duality equivalence and the opposite of the cospan of $f$ and $g$ and the left isomorphism whisker of the functor of the duality equivalence and the inverse of the span opposite of $f$ and $g$.

the opposite span of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the opposite span of $f$ and $g$ is an isomorphism of the opposite of the span of $f$ and $g$ and the composition of the functor of the duality equivalence and the cospan of the opposite in $f$ and the opposite in $g$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the identity of the opposite of the span of $f$ and $g$ and the right isomorphism whisker of the unit isomorphism of the duality equivalence and the opposite of the span of $f$ and $g$ and the associator of the inverse of the duality equivalence and the opposite of the span of $f$ and $g$ and the left isomorphism whisker of the functor of the duality equivalence and the inverse of the cospan opposite of $f$ and $g$.

the pullback isomorphism opposite pushout of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback isomorphism opposite pushout of $f$ and $g$ is an isomorphism of the pullback of $f$ and $g$ and $\operatorname{op}$ applied to the pushout of the opposite of $f$ and the opposite of $g$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to the cospan of $f$ and $g$ and $\operatorname{isColimitEquivIsLimitOp}$ applied to the cocone of the span of the opposite of $f$ and the opposite of $g$ and $\operatorname{isColimit}$ applied to the span of the opposite of $f$ and the opposite of $g$.

the pullback isomorphism opposite pushout of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback isomorphism opposite pushout of $f$ and $g$ is an isomorphism of the pullback of $f$ and $g$ and the opposite of the pushout of the opposite in $f$ and the opposite in $g$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to the cospan of $f$ and $g$ and $\operatorname{isColimitEquivIsLimitUnop}$ applied to the cocone of the span of the opposite in $f$ and the opposite in $g$ and $\operatorname{isColimit}$ applied to the span of the opposite in $f$ and the opposite in $g$.

the pushout isomorphism opposite pullback of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $X$ and $Y$. Then the pushout isomorphism opposite pullback of $f$ and $g$ is an isomorphism of the pushout of $f$ and $g$ and $\operatorname{op}$ applied to the pullback of the opposite of $f$ and the opposite of $g$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the span of $f$ and $g$ and $\operatorname{isLimitEquivIsColimitOp}$ applied to the cone of the cospan of the opposite of $f$ and the opposite of $g$ and $\operatorname{isLimit}$ applied to the cospan of the opposite of $f$ and the opposite of $g$.

the pushout isomorphism opposite pullback of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $X$ and $Y$. Then the pushout isomorphism opposite pullback of $f$ and $g$ is an isomorphism of the pushout of $f$ and $g$ and the opposite of the pullback of the opposite in $f$ and the opposite in $g$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the span of $f$ and $g$ and $\operatorname{isLimitEquivIsColimitUnop}$ applied to the cone of the cospan of the opposite in $f$ and the opposite in $g$ and $\operatorname{isLimit}$ applied to the cospan of the opposite in $f$ and the opposite in $g$.

the span opposite of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the span opposite of $f$ and $g$ is an isomorphism of the span of the opposite in $f$ and the opposite in $g$ and the composition of the inverse of the duality equivalence and the opposite of the cospan of $f$ and $g$.

the span opposite of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the span opposite of $f$ and $g$ is an isomorphism of the span of the opposite of $f$ and the opposite of $g$ and the composition of the inverse of the duality equivalence and the left opposite of the cospan of $f$ and $g$.

Let $X$ be a function from elements of $I$ to elements of $C$. Let $P$ be a function from elements of $I$ to propositions. Then $\operatorname{binaryFanOfProp}$ applied to $X$ and $P$ is an element of $\operatorname{BinaryFan}$ applied to the product object of the function that maps $i$ to $X$ applied to $i$ and the product object of the function that maps $i_{1}$ to $X$ applied to $i_{1}$ defined as $\operatorname{mk}$ applied to the map of the function that maps $x_{1}$ to $P$ applied to $x_{1}$ and the function that maps $x_{2}$ to the identity morphism of $X$ applied to $x_{2}$ and the map of the function that maps $x_{3}$ to the proposition that it is not the case that $P$ holds for $x_{3}$ and the function that maps $x_{4}$ to the identity morphism of $X$ applied to $x_{4}$.

Let $X$ be a function from elements of $I$ to elements of $C$. Let $P$ be a function from elements of $I$ to propositions. Then $\operatorname{binaryFanOfPropIsLimit}$ applied to $X$ and $P$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{binaryFanOfProp}$ applied to $X$ and $P$.

the initial object in n (from the docstring)

Let $n$ be a natural number. Then the initial object in $n$ is an element of $\operatorname{IsInitial}$ applied to $0$ defined as $\operatorname{isInitialBot}$.

the terminal object in n (from the docstring)

Let $n$ be a natural number. Then the terminal object in $n$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{last}$ applied to $n$ defined as $\operatorname{isTerminalTop}$.

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

the cocone of f and F (from the name)

Let $f$ be an element of $\mathrm{PrincipalSeg}$ applied to the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{Lt} (x_{5} , x_{6})$ and the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{Lt} (x_{7} , x_{8})$. Let $F$ be a functor of $x_{1}$ and $C$. Then the cocone of $f$ and $F$ is a cocone of the composition of the functor of $\operatorname{monotone}$ applied to $f$ and $F$.

transfinite composition of shape of J and f (from the name)

Let $J$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the transfinite compositions of shape of $J$ and $f$ are a basic type.

Let $\mathrm{self}$ be a transfinite composition of shape of $J$ and $f$. Then $\operatorname{F}$ applied to $\mathrm{self}$ is a functor of $J$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $c$ be a transfinite composition of shape of $J$ and $f$. Let $j$ be an element of $J$. Then $\operatorname{ici}$ applied to $c$ and $j$ is a transfinite composition of shape of the set of elements of $\operatorname{Ici}$ applied to $j$ and the component of the inclusion of $c$ and $j$.

Let $c$ be a transfinite composition of shape of $J$ and $f$. Let $j$ be an element of $J$. Then $\operatorname{iic}$ applied to $c$ and $j$ is a transfinite composition of shape of the set of elements of $\operatorname{Iic}$ applied to $j$ and the map of $\operatorname{F}$ applied to $c$ and the homomorphism of $\mathrm{bot\_le}$.

the inclusion of self (from the name)

Let $\mathrm{self}$ be a transfinite composition of shape of $J$ and $f$. Then the inclusion of $\mathrm{self}$ is a homomorphism of $\operatorname{F}$ applied to $\mathrm{self}$ and the action of the constant of $J$ and $Y$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the colimit of self (from the docstring)

Let $\mathrm{self}$ be a transfinite composition of shape of $J$ and $f$. Then the colimit of $\mathrm{self}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $Y$ and the inclusion of $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

the isomorphism of self (from the docstring)

Let $\mathrm{self}$ be a transfinite composition of shape of $J$ and $f$. Then the isomorphism of $\mathrm{self}$ is an isomorphism of the action of $\operatorname{F}$ applied to $\mathrm{self}$ and the bottom and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the map of c and F (from the name)

Let $c$ be a transfinite composition of shape of $J$ and $f$. Let $F$ be a functor of $C$ and $D$. Then the map of $c$ and $F$ is a transfinite composition of shape of $J$ and the map of $F$ and $f$.

the transfinite composition of shape of c and e (from the name)

Let $c$ be a transfinite composition of shape of $J$ and $f$. Let $e$ be an isomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $\mathrm{f'}$. Then the transfinite composition of shape of $c$ and $e$ is a transfinite composition of shape of $J$ and $\mathrm{f'}$.

the transfinite composition of shape of G (from the name)

Let $G$ be a composable arrow of $C$ and $n$. Then the transfinite composition of shape of $G$ is a transfinite composition of shape of $\mathrm{Fin}$ applied to $n + 1$ and the homomorphism of $G$.

the transfinite composition of shape of c and e (from the name)

Let $c$ be a transfinite composition of shape of $J$ and $f$. Let $e$ be an order isomorphism of $\mathrm{J'}$ and $J$. Then the transfinite composition of shape of $c$ and $e$ is a transfinite composition of shape of $\mathrm{J'}$ and $f$.

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

Let $F$ be a functor of $J$ and $C$. Let $m$ be an element of $J$ such that $m$ is a successor limit. Then $\operatorname{isColimitOfIsWellOrderContinuous}$ applied to $F$, $m$ and $\mathrm{hm}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of the principal segment of $m$ and $F$ defined as $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_Functor\_\_IsWellOrderContinuous\_\_nonempty\_isColimit}$ applied to $m$ and $\mathrm{hm}$.

Let $F$ be a functor of $J$ and $C$. Let $f$ be an element of $\mathrm{PrincipalSeg}$ applied to the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Lt} (x_{6} , x_{7})$ such that the top of $f$ is a successor limit. Then $\operatorname{isColimitOfIsWellOrderContinuous'}$ applied to $F$, $f$ and $h_{1}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $f$ and $F$ defined as the whisker equivalence of $\operatorname{isColimitOfIsWellOrderContinuous}$ applied to $F$, the top of $f$ and $h_{1}$ and the equivalence of $\operatorname{orderIsoIio}$ applied to $f$.

cofan of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $C$. Then a cofan of $f$ is an element of the function that maps $f$ to the set of cocones of the functor of $f$.

Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $f$ be a function from elements $i$ of $x$ to homomorphisms of $F$ applied to $i$ and $A$. Then $\operatorname{desc}$ applied to $\mathrm{hc}$, $i$ and $f$ is a homomorphism of $\operatorname{pt}$ applied to $c$ and $A$ defined as the function that maps $f$ to $\operatorname{desc}$ applied to $\mathrm{hc}$, $\operatorname{mk}$ applied to $A$ and $i$ and $f$.

Let $t$ be a cofan of $f$. Let $\mathrm{lift}$ be a function from cofans $s_{2}$ of $f$ to homomorphisms of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s_{2}$ such that $\mathrm{autoParam}$ holds for the proposition that for all cofans $s_{1}$ of $f$, for all elements $j_{1}$ of $x$, the composition of the injection of $t$ and $j_{1}$ and $\mathrm{lift}$ applied to $s_{1}$ is equal to the injection of $s_{1}$ and $j_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Cofan\_\_IsColimit\_\_mk\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that for all cofans $s$ of $f$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $t$ and $\operatorname{pt}$ applied to $s$, if for all elements $j$ of $x$, the composition of the injection of $t$ and $j$ and $m$ is equal to the injection of $s$ and $j$, then $\EqtMACRoH {m}{\mathrm{lift} (s)}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Cofan\_\_IsColimit\_\_mk\_\_\_auto\_3}$. Then $\operatorname{mk}$ applied to $t$, $s_{2}$, $\mathrm{lift}$, $\mathrm{fac}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsColimit}$ applied to $t$.

the product of hc and i1 (from the name)

Let $c$ be a function from elements $i_{2}$ of $x_{1}$ to cofans of the function that maps $j$ to $X$ applied to $i_{2}$ and $j$. Let $\mathrm{hc}$ be a function from elements $i_{1}$ of $x_{1}$ to elements of $\operatorname{IsColimit}$ applied to $c$ applied to $i_{1}$. Let $\mathrm{c'}$ be a cofan of the function that maps $i$ to $\operatorname{pt}$ applied to $c$ applied to $i$. Let $\mathrm{hc'}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{c'}$. Then the product of $i_{1}$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $\mathrm{c'}$ and the function that maps $p$ to the composition of the injection of $c$ applied to $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$ and the injection of $\mathrm{c'}$ and $\ProdfstMACRoZ {p}$.

the extension of e and w (from the name)

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

the injection of p and j (from the name)

Let $p$ be a cofan of $f$. Let $j$ be an element of $x$. Then the injection of $p$ and $j$ is a homomorphism of $f$ applied to $j$ and $\operatorname{pt}$ applied to $p$ defined as the component of the inclusion of $p$ and $\operatorname{mk}$ applied to $j$.

Let $x_{3}$ be an equivalence from $x$ to $x_{2}$. Let $c$ be a cofan of $f$. Then $\operatorname{isColimitEquivOfEquiv}$ applied to $x_{3}$ and $c$ is an equivalence from $\operatorname{IsColimit}$ applied to $c$ to $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and the function that maps $i$ to the injection of $c$ and $x_{3}$ applied to $i$ defined as the whisker equivalence equivalence of the equivalence of $x_{3}$.

Let $F$ be a functor of $C$ and $D$. Let $X$ be a function from elements of $x_{2}$ to elements of $C$. Let $c$ be a cofan of $X$. Then $\operatorname{isColimitMapCoconeEquiv}$ applied to $F$, $X$ and $c$ is an equivalence from $\operatorname{IsColimit}$ applied to the map cocone of $F$ and $c$ to $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the action of $F$ and $\operatorname{pt}$ applied to $c$ and the function that maps $i$ to the map of $F$ and the injection of $c$ and $i$.

Let $e$ be an isomorphism of $X$ and $Y$. Let $J$ be a set. Then $\operatorname{isColimitMkOfUnique}$ applied to $e$ and $J$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $X$ and the function that maps $x_{2}$ to the inverse of $e$.

Let $c$ be a cofan of $f$. Then $\operatorname{isColimitOfIsIsoSigmaDesc}$ applied to $c$ is an element of $\operatorname{IsColimit}$ applied to $c$.

Let $c$ be a cofan of $X$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $x_{3}$ be a function from elements $a_{3}$ of $x$ and elements $b_{2}$ of $x_{2}$ applied to $a_{3}$ to homomorphisms of $Y$ applied to $a_{3}$ and $b_{2}$ and $X$ applied to $a_{3}$. Let $\mathrm{hs}$ be a function from elements $a_{2}$ of $x$ to elements of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $X$ applied to $a_{2}$ and $x_{3}$ applied to $a_{2}$. Then $\operatorname{isColimitTrans}$ applied to $c$, $\mathrm{hc}$, $a_{3}$, $b_{2}$, $x_{3}$, $a_{2}$ and $\mathrm{hs}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and the function that maps $x_{4}$ to $\mathrm{CategoryTheory\_\_Limits\_\_Cofan\_\_isColimitTrans\_\_match\_1}$ applied to the function that maps $x_{5}$ to the set of homomorphisms of $\mathrm{CategoryTheory\_\_Limits\_\_Cofan\_\_isColimitTrans\_\_match\_1}$ applied to the function that maps $x_{6}$ to $C$, $x_{5}$ and the function that maps $a$ and $b$ to $Y$ applied to $a$ and $b$ and $\operatorname{pt}$ applied to $c$, $x_{4}$ and the function that maps $a_{1}$ and $b_{1}$ to the composition of $x_{3}$ applied to $a_{1}$ and $b_{1}$ and the injection of $c$ and $a_{1}$.

Let $P$ be an element of $C$. Let $p$ be a function from elements $b$ of $x$ to homomorphisms of $f$ applied to $b$ and $P$. Then $\operatorname{mk}$ applied to $P$, $b$ and $p$ is a cofan of $f$ defined as the function that maps $p$ to $\operatorname{mk}$ applied to $P$, the natural transformation of the function that maps $X$ to $b$ applied to $\operatorname{as}$ applied to $X$ and $p$.

Let $f$ be a function from elements of $x$ to elements of $C$. Then an element of $\operatorname{Fan}$ applied to $f$ is an element of the function that maps $f$ to the set of cones of the functor of $f$.

the lift of hc and f (from the name)

Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $f$ be a function from elements $i$ of $x$ to homomorphisms of $A$ and $F$ applied to $i$. Then the lift of $\mathrm{hc}$ and $i$ is a homomorphism of $A$ and $\operatorname{pt}$ applied to $c$ defined as the function that maps $f$ to the lift of $\mathrm{hc}$ and $\operatorname{mk}$ applied to $A$ and $i$.

Let $t$ be an element of $\operatorname{Fan}$ applied to $f$. Let $\mathrm{lift}$ be a function from elements $s_{2}$ of $\operatorname{Fan}$ applied to $f$ to homomorphisms of $\operatorname{pt}$ applied to $s_{2}$ and $\operatorname{pt}$ applied to $t$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $s_{1}$ of $\operatorname{Fan}$ applied to $f$, for all elements $j_{1}$ of $x$, the composition of $\mathrm{lift}$ applied to $s_{1}$ and the projection of $t$ and $j_{1}$ is equal to the projection of $s_{1}$ and $j_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Fan\_\_IsLimit\_\_mk\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $s$ of $\operatorname{Fan}$ applied to $f$, for all homomorphisms $m$ of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$, if for all elements $j$ of $x$, the composition of $m$ and the projection of $t$ and $j$ is equal to the projection of $s$ and $j$, then $\EqtMACRoH {m}{\mathrm{lift} (s)}$ and $\mathrm{CategoryTheory\_\_Limits\_\_Fan\_\_IsLimit\_\_mk\_\_\_auto\_3}$. Then $\operatorname{mk}$ applied to $t$, $s_{2}$, $\mathrm{lift}$, $\mathrm{fac}$ and $\mathrm{uniq}$ is an element of $\operatorname{IsLimit}$ applied to $t$.

the product of hc and i1 (from the name)

Let $c$ be a function from elements $i_{2}$ of $x_{1}$ to elements of $\operatorname{Fan}$ applied to the function that maps $j$ to $X$ applied to $i_{2}$ and $j$. Let $\mathrm{hc}$ be a function from elements $i_{1}$ of $x_{1}$ to elements of $\operatorname{IsLimit}$ applied to $c$ applied to $i_{1}$. Let $\mathrm{c'}$ be an element of $\operatorname{Fan}$ applied to the function that maps $i$ to $\operatorname{pt}$ applied to $c$ applied to $i$. Let $\mathrm{hc'}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{c'}$. Then the product of $i_{1}$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $\mathrm{c'}$ and the function that maps $p$ to the composition of the projection of $\mathrm{c'}$ and $\ProdfstMACRoZ {p}$ and the projection of $c$ applied to $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$.

the extension of e and w (from the name)

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

Let $x_{3}$ be an equivalence from $x$ to $x_{2}$. Let $c$ be an element of $\operatorname{Fan}$ applied to $f$. Then $\operatorname{isLimitEquivOfEquiv}$ applied to $x_{3}$ and $c$ is an equivalence from $\operatorname{IsLimit}$ applied to $c$ to $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and the function that maps $i$ to the projection of $c$ and $x_{3}$ applied to $i$ defined as the whisker equivalence equivalence of the equivalence of $x_{3}$.

Let $F$ be a functor of $C$ and $D$. Let $X$ be a function from elements of $x_{2}$ to elements of $C$. Let $c$ be an element of $\operatorname{Fan}$ applied to $X$. Then $\operatorname{isLimitMapConeEquiv}$ applied to $F$, $X$ and $c$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $F$ and $c$ to $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the action of $F$ and $\operatorname{pt}$ applied to $c$ and the function that maps $i$ to the map of $F$ and the projection of $c$ and $i$.

Let $e$ be an isomorphism of $X$ and $Y$. Let $J$ be a set. Then $\operatorname{isLimitMkOfUnique}$ applied to $e$ and $J$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $X$ and the function that maps $x_{2}$ to the homomorphism of $e$.

Let $c$ be an element of $\operatorname{Fan}$ applied to $f$. Then $\operatorname{isLimitOfIsIsoPiLift}$ applied to $c$ is an element of $\operatorname{IsLimit}$ applied to $c$.

Let $P$ be an element of $C$. Let $p$ be a function from elements $b$ of $x$ to homomorphisms of $P$ and $f$ applied to $b$. Then $\operatorname{mk}$ applied to $P$, $b$ and $p$ is an element of $\operatorname{Fan}$ applied to $f$ defined as the function that maps $p$ to $\operatorname{mk}$ applied to $P$, the natural transformation of the function that maps $X$ to $b$ applied to $\operatorname{as}$ applied to $X$ and $p$.

the projection of p and j (from the name)

Let $p$ be an element of $\operatorname{Fan}$ applied to $f$. Let $j$ be an element of $x$. Then the projection of $p$ and $j$ is a homomorphism of $\operatorname{pt}$ applied to $p$ and $f$ applied to $j$ defined as the component of the projection of $p$ and $\operatorname{mk}$ applied to $j$.

f has coproducts (from the name)

Let $f$ be a function from elements of $x$ to elements of $C$. Then $f$ has coproducts, if the functor of $f$ has colimits.

C has coproducts (from the name)

Let $C$ be a set. Then $C$ has coproducts, if for all sets $J$, $\operatorname{HasColimitsOfShape}$ holds for $\operatorname{Discrete}$ applied to $J$ and $C$.

Let $x$ and $C$ be sets. Then $\operatorname{HasCoproductsOfShape}$ holds for $x$ and $C$, if $\operatorname{HasColimitsOfShape}$ holds for $\operatorname{Discrete}$ applied to $x$ and $C$.

f has products (from the name)

Let $f$ be a function from elements of $x$ to elements of $C$. Then $f$ has products, if the functor of $f$ has limits.

C has products (from the name)

Let $C$ be a set. Then $C$ has products, if for all sets $J$, $\operatorname{HasLimitsOfShape}$ holds for $\operatorname{Discrete}$ applied to $J$ and $C$.

Let $x$ and $C$ be sets. Then $\operatorname{HasProductsOfShape}$ holds for $x$ and $C$, if $\operatorname{HasLimitsOfShape}$ holds for $\operatorname{Discrete}$ applied to $x$ and $C$.

the cone of X (from the name)

Let $X$ be a functor of $\operatorname{Discrete}$ applied to $x$ and $C$. Then the cone of $X$ is a cone of $X$ defined as $\operatorname{mk}$ applied to the product object of the function that maps $j$ to the action of $X$ and $\operatorname{mk}$ applied to $j$ and the natural transformation of the function that maps $x_{2}$ to the projection of the function that maps $j_{1}$ to the action of $X$ and $\operatorname{mk}$ applied to $j_{1}$ and $\operatorname{as}$ applied to $x_{2}$.

the constant composition product isomorphism constant of X (from the name)

Let $X$ be a function from elements of $x$ to elements of $C$. Then the constant composition product isomorphism constant of $X$ is an isomorphism of the composition of the product of the function that maps $i$ to the action of the constant of $I$ applied to $i$ and $X$ applied to $i$ and the functor of $x$ and the action of the constant of the set of functions from elements $i_{1}$ of $x$ to elements of $I$ applied to $i_{1}$ and the product object of $X$.

the functor of x (from the docstring)

Let $x$ be a set. Then the functor of $x$ is a functor of the set of functions from elements of $x$ to elements of $C$ and $C$.

the functor projection of a (from the name)

Let $a$ be an element of $x$. Then the functor projection of $a$ is a homomorphism of the functor of $x$ and the evaluation of the function that maps $x_{2}$ to $C$ and $a$.

the isomorphism of X (from the docstring)

Let $X$ be a functor of $\operatorname{Discrete}$ applied to $x$ and $C$. Then the isomorphism of $X$ is an isomorphism of the product object of the function that maps $j$ to the action of $X$ and $\operatorname{mk}$ applied to $j$ and the limit of $X$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{productIsProduct'}$ applied to $X$ and $\operatorname{isLimit}$ applied to $X$.

the lift of p (from the name)

Let $p$ be a function from elements $b$ of $x$ to homomorphisms of $P$ and $f$ applied to $b$. Then the lift of $b$ is a homomorphism of $P$ and the product object of $f$ defined as the function that maps $p$ to the lift of the functor 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 $x$ to homomorphisms of $f$ applied to $b$ and $g$ applied to $b$. Then the map of $b$ is a homomorphism of the product object of $f$ and the product object of $g$ defined as the function that maps $p$ to the limit map of the natural transformation of the function that maps $X$ to $b$ applied to $\operatorname{as}$ applied to $X$.

the map of p and q (from the name)

Let $p$ be a function from elements of $x$ to elements of $x_{1}$. Let $q$ be a function from elements $b$ of $x$ to homomorphisms of $f$ applied to $p$ applied to $b$ and $g$ applied to $b$. Then the map of $p$ and $b$ is a homomorphism of the product object of $f$ and the product object of $g$ defined as the function that maps $q$ to the lift of the function that maps $a$ to the composition of the projection of $f$ and $p$ applied to $a$ and $b$ applied to $a$.

the map isomorphism of p (from the name)

Let $p$ be a function from elements $b$ of $x$ to isomorphisms of $f$ applied to $b$ and $g$ applied to $b$. Then the map isomorphism of $b$ is an isomorphism of the product object of $f$ and the product object of $g$ defined as the function that maps $p$ to the map isomorphism of the limit and the natural isomorphism of the function that maps $X$ to $b$ applied to $\operatorname{as}$ applied to $X$.

the reindexing of x3 and f (from the name)

Let $x_{3}$ be an equivalence from $x$ to $x_{2}$. Let $f$ be a function from elements of $x_{2}$ to elements of $C$. Then the reindexing of $x_{3}$ and $f$ is an isomorphism of the product object of $\operatorname{comp}$ applied to $f$ and $\operatorname{coe}$ applied to $x_{3}$ and the product object of $f$ defined as the isomorphism of the equivalence of $x_{3}$ and the natural isomorphism of the function that maps $x_{4}$ to the identity of the action of the composition of the functor of the equivalence of $x_{3}$ and the functor of $f$ and $x_{4}$.

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 product object of $f$ and the product object of $g$.

the projection of f and b (from the name)

Let $f$ be a function from elements of $x$ to elements of $C$. Let $b$ be an element of $x$. Then the projection of $f$ and $b$ is a homomorphism of the product object of $f$ and $f$ applied to $b$ defined as the projection from the limit object to a value of the functor of the functor of $f$ and $\operatorname{mk}$ applied to $b$.

the cocone of X (from the name)

Let $X$ be a functor of $\operatorname{Discrete}$ applied to $x$ and $C$. Then the cocone of $X$ is a cocone of $X$ defined as $\operatorname{mk}$ applied to the sigma object of the function that maps $j$ to the action of $X$ and $\operatorname{mk}$ applied to $j$ and the natural transformation of the function that maps $x_{2}$ to the inclusion of the function that maps $j_{1}$ to the action of $X$ and $\operatorname{mk}$ applied to $j_{1}$ and $\operatorname{as}$ applied to $x_{2}$.

the constant composition sigma isomorphism constant of X (from the name)

Let $X$ be a function from elements of $x$ to elements of $C$. Then the constant composition sigma isomorphism constant of $X$ is an isomorphism of the composition of the product of the function that maps $i$ to the action of the constant of $I$ applied to $i$ and $X$ applied to $i$ and the functor of $x$ and the action of the constant of the set of functions from elements $i_{1}$ of $x$ to elements of $I$ applied to $i_{1}$ and the sigma object of $X$.

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

the functor of x (from the docstring)

Let $x$ be a set. Then the functor of $x$ is a functor of the set of functions from elements of $x$ to elements of $C$ and $C$.

the functor inclusion of a (from the name)

Let $a$ be an element of $x$. Then the functor inclusion of $a$ is a homomorphism of the evaluation of the function that maps $x_{2}$ to $C$ and $a$ and the functor of $x$.

the isomorphism of X (from the docstring)

Let $X$ be a functor of $\operatorname{Discrete}$ applied to $x$ and $C$. Then the isomorphism of $X$ is an isomorphism of the sigma object of the function that maps $j$ to the action of $X$ and $\operatorname{mk}$ applied to $j$ and the colimit of $X$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{coproductIsCoproduct'}$ applied to $X$ and $\operatorname{isColimit}$ applied to $X$.

the map of p (from the name)

Let $p$ be a function from elements $b$ of $x$ to homomorphisms of $g$ applied to $b$ and $f$ applied to $b$. Then the map of $b$ is a homomorphism of the sigma object of $g$ and the sigma object of $f$ defined as the function that maps $p$ to the colimit map of the natural transformation of the function that maps $X$ to $b$ applied to $\operatorname{as}$ applied to $X$.

the map of p and q (from the name)

Let $p$ be a function from elements of $x$ to elements of $x_{1}$. Let $q$ be a function from elements $b$ of $x$ to homomorphisms of $g$ applied to $b$ and $f$ applied to $p$ applied to $b$. Then the map of $p$ and $b$ is a homomorphism of the sigma object of $g$ and the sigma object of $f$ defined as the function that maps $q$ to $\operatorname{desc}$ applied to the function that maps $a$ to the composition of $b$ applied to $a$ and the inclusion of $f$ and $p$ applied to $a$ and $q$.

the map isomorphism of p (from the name)

Let $p$ be a function from elements $b$ of $x$ to isomorphisms of $f$ applied to $b$ and $g$ applied to $b$. Then the map isomorphism of $b$ is an isomorphism of the sigma object of $f$ and the sigma object of $g$ defined as the function that maps $p$ to the map isomorphism of the colimit and the natural isomorphism of the function that maps $X$ to $b$ applied to $\operatorname{as}$ applied to $X$.

the reindexing of x3 and f (from the name)

Let $x_{3}$ be an equivalence from $x$ to $x_{2}$. Let $f$ be a function from elements of $x_{2}$ to elements of $C$. Then the reindexing of $x_{3}$ and $f$ is an isomorphism of the sigma object of $\operatorname{comp}$ applied to $f$ and $\operatorname{coe}$ applied to $x_{3}$ and the sigma object of $f$ defined as the isomorphism of the equivalence of $x_{3}$ and the natural isomorphism of the function that maps $x_{4}$ to the identity of the action of the composition of the functor of the equivalence of $x_{3}$ and the functor of $f$ and $x_{4}$.

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 sigma object of $f$ and the sigma object of $g$.

the inclusion of f and b (from the name)

Let $f$ be a function from elements of $x$ to elements of $C$. Let $b$ be an element of $x$. Then the inclusion of $f$ and $b$ is a homomorphism of $f$ applied to $b$ and the sigma object of $f$ defined as the inclusion of the functor of $f$ and $\operatorname{mk}$ applied to $b$.

the colimit cocone of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $C$. Then the colimit cocone of $f$ is a colimit cocone of the functor of $f$.

Let $f$ be a function from elements of $x$ to elements of $C$. Then $\operatorname{coproductIsCoproduct}$ applied to $f$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the sigma object of $f$ and $\mathrm{CategoryTheory\_\_Limits\_\_Sigma\_\_\_u3b9\_}$ applied to $f$.

Let $X$ be a functor of $\operatorname{Discrete}$ applied to $x$ and $C$. Then $\operatorname{coproductIsCoproduct'}$ applied to $X$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $X$.

the coproduct unique isomorphism of f (from the name)

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

Let $c$ be a cocone of $K$. Then $\operatorname{isColimitEquivCofanOfIsThin}$ applied to $c$ is an equivalence from $\operatorname{IsColimit}$ applied to $c$ to $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{NatTrans}$ applied to the inclusion of $c$.

Let $c$ be a cone of $K$. Then $\operatorname{isLimitEquivFanOfIsThin}$ applied to $c$ is an equivalence from $\operatorname{IsLimit}$ applied to $c$ to $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{NatTrans}$ applied to the projection of $c$.

the limit cone for the product of f (from the docstring)

Let $f$ be a function from elements of $x$ to elements of $C$. Then the limit cone for the product of $f$ is a limit cone of the functor of $f$.

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

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $x$ to elements of $C$. Then the product comparison of $G$ and $f$ is a homomorphism of the action of $G$ and the product object of $f$ and the product object of the function that maps $b$ to the action of $G$ and $f$ applied to $b$ defined as the lift of the function that maps $b$ to the map of $G$ and the projection of $f$ and $b$.

the product constant (from the name)

The product constant is a functor of $C$ and the set of functors of the set of opposites of the set of sets and $C$.

the product constant adjoint of X (from the name)

Let $X$ be an element of $C$. Then the product constant adjoint of $X$ is an adjunction of the right opposite of the action of the product constant and $X$ and the action of the Yoneda and $X$.

the product equivalence functor discrete composition colimit of x (from the name)

Let $x$ be a set. Then the product equivalence functor discrete composition colimit of $x$ is an isomorphism of the composition of the functor of $\operatorname{piEquivalenceFunctorDiscrete}$ applied to $x$ and $C$ and the colimit and the functor of $x$.

the product equivalence functor discrete composition limit of x (from the name)

Let $x$ be a set. Then the product equivalence functor discrete composition limit of $x$ is an isomorphism of the composition of the functor of $\operatorname{piEquivalenceFunctorDiscrete}$ applied to $x$ and $C$ and the limit and the functor of $x$.

the product object of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $C$. Then the product object of $f$ is an element of $C$ defined as the limit of the functor of $f$.

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

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

Let $f$ be a function from elements of $x$ to elements of $C$. Then $\operatorname{productIsProduct}$ applied to $f$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the product object of $f$ and $\mathrm{CategoryTheory\_\_Limits\_\_Pi\_\_\_u3c0\_}$ applied to $f$.

Let $X$ be a functor of $\operatorname{Discrete}$ applied to $x$ and $C$. Then $\operatorname{productIsProduct'}$ applied to $X$ is an element of $\operatorname{IsLimit}$ applied to the cone of $X$.

the product unique isomorphism of f (from the name)

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

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

Let $G$ be a functor of $C$ and $D$. Let $f$ be a function from elements of $x$ to elements of $C$. Then the sigma comparison of $G$ and $f$ is a homomorphism of the sigma object of the function that maps $b$ to the action of $G$ and $f$ applied to $b$ and the action of $G$ and the sigma object of $f$ defined as $\operatorname{desc}$ applied to the function that maps $b$ to the map of $G$ and the inclusion of $f$ and $b$.

the sigma constant (from the name)

The sigma constant is a functor of $C$ and the set of functors of the set of sets and $C$.

the sigma constant adjoint of X (from the name)

Let $X$ be an element of $C$. Then the sigma constant adjoint of $X$ is an adjunction of the action of the sigma constant and $X$ and the action of the Coyoneda and $\operatorname{op}$ applied to $X$.

the sigma object of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $C$. Then the sigma object of $f$ is an element of $C$ defined as the colimit of the functor of $f$.

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

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

the pullback associator of x8 and x9 (from the name)

Let $x_{6}$ be a homomorphism of $x_{1}$ and $x_{4}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{4}$. Let $x_{8}$ be a homomorphism of $x_{2}$ and $x_{5}$. Let $x_{9}$ be a homomorphism of $x_{3}$ and $x_{5}$. Then the pullback associator of $x_{8}$ and $x_{9}$ is an isomorphism of the pullback of the composition of the second projection of the pullback of $x_{6}$ and $x_{7}$ and $x_{8}$ and $x_{9}$ and the pullback of $x_{6}$ and the composition of the first projection of the pullback of $x_{8}$ and $x_{9}$ and $x_{7}$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{pullbackPullbackLeftIsPullback}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ and $\operatorname{pullbackPullbackRightIsPullback}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$.

Let $x_{6}$ be a homomorphism of $x_{1}$ and $x_{4}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{4}$. Let $x_{8}$ be a homomorphism of $x_{2}$ and $x_{5}$. Let $x_{9}$ be a homomorphism of $x_{3}$ and $x_{5}$. Then $\operatorname{pullbackAssocIsPullback}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the composition of the first projection of the pullback of the composition of the second projection of the pullback of $x_{6}$ and $x_{7}$ and $x_{8}$ and $x_{9}$ and the first projection of the pullback of $x_{6}$ and $x_{7}$, the lift of the composition of the first projection of the pullback of the composition of the second projection of the pullback of $x_{6}$ and $x_{7}$ and $x_{8}$ and $x_{9}$ and the second projection of the pullback of $x_{6}$ and $x_{7}$ and the second projection of the pullback of the composition of the second projection of the pullback of $x_{6}$ and $x_{7}$ and $x_{8}$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_Limits\_\_pullbackAssocIsPullback\_\_\_proof\_1}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$.

Let $x_{6}$ be a homomorphism of $x_{1}$ and $x_{4}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{4}$. Let $x_{8}$ be a homomorphism of $x_{2}$ and $x_{5}$. Let $x_{9}$ be a homomorphism of $x_{3}$ and $x_{5}$. Then $\operatorname{pullbackAssocSymmIsPullback}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the lift of the first projection of the pullback of $x_{6}$ and the composition of the first projection of the pullback of $x_{8}$ and $x_{9}$ and $x_{7}$ and the composition of the second projection of the pullback of $x_{6}$ and the composition of the first projection of the pullback of $x_{8}$ and $x_{9}$ and $x_{7}$ and the first projection of the pullback of $x_{8}$ and $x_{9}$, the composition of the second projection of the pullback of $x_{6}$ and the composition of the first projection of the pullback of $x_{8}$ and $x_{9}$ and $x_{7}$ and the second projection of the pullback of $x_{8}$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_Limits\_\_pullbackAssocSymmIsPullback\_\_\_proof\_1}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$.

Let $x_{6}$ be a homomorphism of $x_{1}$ and $x_{4}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{4}$. Let $x_{8}$ be a homomorphism of $x_{2}$ and $x_{5}$. Let $x_{9}$ be a homomorphism of $x_{3}$ and $x_{5}$. Then $\operatorname{pullbackPullbackLeftIsPullback}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the first projection of the pullback of the composition of the second projection of the pullback of $x_{6}$ and $x_{7}$ and $x_{8}$ and $x_{9}$, the lift of the composition of the first projection of the pullback of the composition of the second projection of the pullback of $x_{6}$ and $x_{7}$ and $x_{8}$ and $x_{9}$ and the second projection of the pullback of $x_{6}$ and $x_{7}$ and the second projection of the pullback of the composition of the second projection of the pullback of $x_{6}$ and $x_{7}$ and $x_{8}$ and $x_{9}$ and $\operatorname{symm}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_pullback\_\_lift\_fst}$ applied to the composition of the first projection of the pullback of the composition of the second projection of the pullback of $x_{6}$ and $x_{7}$ and $x_{8}$ and $x_{9}$ and the second projection of the pullback of $x_{6}$ and $x_{7}$, the second projection of the pullback of the composition of the second projection of the pullback of $x_{6}$ and $x_{7}$ and $x_{8}$ and $x_{9}$ and $\operatorname{trans}$ applied to $\operatorname{assoc}$ applied to the first projection of the pullback of the composition of the second projection of the pullback of $x_{6}$ and $x_{7}$ and $x_{8}$ and $x_{9}$, the second projection of the pullback of $x_{6}$ and $x_{7}$ and $x_{8}$ and $\operatorname{condition}$.

Let $x_{6}$ be a homomorphism of $x_{1}$ and $x_{4}$. Let $x_{7}$ be a homomorphism of $x_{2}$ and $x_{4}$. Let $x_{8}$ be a homomorphism of $x_{2}$ and $x_{5}$. Let $x_{9}$ be a homomorphism of $x_{3}$ and $x_{5}$. Then $\operatorname{pullbackPullbackRightIsPullback}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the lift of the first projection of the pullback of $x_{6}$ and the composition of the first projection of the pullback of $x_{8}$ and $x_{9}$ and $x_{7}$ and the composition of the second projection of the pullback of $x_{6}$ and the composition of the first projection of the pullback of $x_{8}$ and $x_{9}$ and $x_{7}$ and the first projection of the pullback of $x_{8}$ and $x_{9}$, the second projection of the pullback of $x_{6}$ and the composition of the first projection of the pullback of $x_{8}$ and $x_{9}$ and $x_{7}$ and $\mathrm{CategoryTheory\_\_Limits\_\_pullback\_\_lift\_snd}$ applied to the first projection of the pullback of $x_{6}$ and the composition of the first projection of the pullback of $x_{8}$ and $x_{9}$ and $x_{7}$, the composition of the second projection of the pullback of $x_{6}$ and the composition of the first projection of the pullback of $x_{8}$ and $x_{9}$ and $x_{7}$ and the first projection of the pullback of $x_{8}$ and $x_{9}$ and $\operatorname{trans}$ applied to $\operatorname{condition}$ and $\operatorname{symm}$ applied to $\operatorname{assoc}$ applied to the second projection of the pullback of $x_{6}$ and the composition of the first projection of the pullback of $x_{8}$ and $x_{9}$ and $x_{7}$, the first projection of the pullback of $x_{8}$ and $x_{9}$ and $x_{7}$.

the pushout associator of x8 and x9 (from the name)

Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{1}$. Let $x_{7}$ be a homomorphism of $x_{4}$ and $x_{2}$. Let $x_{8}$ be a homomorphism of $x_{5}$ and $x_{2}$. Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{3}$. Then the pushout associator of $x_{8}$ and $x_{9}$ is an isomorphism of the pushout of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$ and the pushout of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{pushoutPushoutLeftIsPushout}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ and $\operatorname{pushoutPushoutRightIsPushout}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$.

Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{1}$. Let $x_{7}$ be a homomorphism of $x_{4}$ and $x_{2}$. Let $x_{8}$ be a homomorphism of $x_{5}$ and $x_{2}$. Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{3}$. Then $\operatorname{pushoutAssocIsPushout}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the composition of the left injection of $x_{6}$ and $x_{7}$ and the left injection of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$, $\operatorname{desc}$ applied to the composition of the right injection of $x_{6}$ and $x_{7}$ and the left injection of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$, the right injection of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$ and $\operatorname{trans}$ applied to $\operatorname{symm}$ applied to $\operatorname{assoc}$ applied to $x_{8}$, the right injection of $x_{6}$ and $x_{7}$ and the left injection of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$ and $\operatorname{condition}$ and $\mathrm{CategoryTheory\_\_Limits\_\_pushoutAssocIsPushout\_\_\_proof\_1}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$.

Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{1}$. Let $x_{7}$ be a homomorphism of $x_{4}$ and $x_{2}$. Let $x_{8}$ be a homomorphism of $x_{5}$ and $x_{2}$. Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{3}$. Then $\operatorname{pushoutAssocSymmIsPushout}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{desc}$ applied to the left injection of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$, the composition of the left injection of $x_{8}$ and $x_{9}$ and the right injection of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$ and $\operatorname{trans}$ applied to $\operatorname{condition}$ and $\operatorname{assoc}$ applied to $x_{7}$, the left injection of $x_{8}$ and $x_{9}$ and the right injection of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$, the composition of the right injection of $x_{8}$ and $x_{9}$ and the right injection of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_Limits\_\_pushoutAssocSymmIsPushout\_\_\_proof\_1}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$.

Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{1}$. Let $x_{7}$ be a homomorphism of $x_{4}$ and $x_{2}$. Let $x_{8}$ be a homomorphism of $x_{5}$ and $x_{2}$. Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{3}$. Then $\operatorname{pushoutPushoutLeftIsPushout}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to the left injection of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$, $\operatorname{desc}$ applied to the composition of the right injection of $x_{6}$ and $x_{7}$ and the left injection of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$, the right injection of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$ and $\operatorname{trans}$ applied to $\operatorname{symm}$ applied to $\operatorname{assoc}$ applied to $x_{8}$, the right injection of $x_{6}$ and $x_{7}$ and the left injection of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$ and $\operatorname{condition}$ and $\operatorname{symm}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_pushout\_\_inl\_desc}$ applied to the composition of the right injection of $x_{6}$ and $x_{7}$ and the left injection of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$, the right injection of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$ and $\operatorname{trans}$ applied to $\operatorname{symm}$ applied to $\operatorname{assoc}$ applied to $x_{8}$, the right injection of $x_{6}$ and $x_{7}$ and the left injection of the composition of $x_{8}$ and the right injection of $x_{6}$ and $x_{7}$ and $x_{9}$ and $\operatorname{condition}$.

Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{1}$. Let $x_{7}$ be a homomorphism of $x_{4}$ and $x_{2}$. Let $x_{8}$ be a homomorphism of $x_{5}$ and $x_{2}$. Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{3}$. Then $\operatorname{pushoutPushoutRightIsPushout}$ applied to $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ is an element of $\operatorname{IsColimit}$ applied to $\operatorname{mk}$ applied to $\operatorname{desc}$ applied to the left injection of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$, the composition of the left injection of $x_{8}$ and $x_{9}$ and the right injection of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$ and $\operatorname{trans}$ applied to $\operatorname{condition}$ and $\operatorname{assoc}$ applied to $x_{7}$, the left injection of $x_{8}$ and $x_{9}$ and the right injection of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$, the right injection of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_Limits\_\_pushout\_\_inr\_desc}$ applied to the left injection of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$, the composition of the left injection of $x_{8}$ and $x_{9}$ and the right injection of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$ and $\operatorname{trans}$ applied to $\operatorname{condition}$ and $\operatorname{assoc}$ applied to $x_{7}$, the left injection of $x_{8}$ and $x_{9}$ and the right injection of $x_{6}$ and the composition of $x_{7}$ and the left injection of $x_{8}$ and $x_{9}$.

categorical pullback of F and G (from the name)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Then the categorical pullbacks of $F$ and $G$ are a basic type.

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Let $X$ be a set. Then the elements of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$ are a basic type.

homomorphism of x4 and y (from the name)

Let $X$ be a set. Let $x_{4}$ and $y$ be elements of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$. Then the homomorphisms of $x_{4}$ and $y$ are a basic type.

the first component of self (from the docstring)

Let $\mathrm{self}$ be a homomorphism of $x_{4}$ and $y$. Then the first component of $\mathrm{self}$ is a homomorphism of the first projection functor of $x_{4}$ and the first projection functor of $y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the second component of self (from the docstring)

Let $\mathrm{self}$ be a homomorphism of $x_{4}$ and $y$. Then the second component of $\mathrm{self}$ is a homomorphism of the second projection functor of $x_{4}$ and the second projection functor of $y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Let $X$ be a set. Then $\operatorname{e}$ applied to $F$, $G$ and $X$ is an isomorphism of the composition of the first component functor of $F$ and $G$ and the action of the right whiskering of $A$ and $B$ and $F$ and the composition of the second component functor of $F$ and $G$ and the action of the right whiskering of $C$ and $B$ and $G$.

the first projection functor of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$. Then the first projection functor of $\mathrm{self}$ is a functor of $X$ and $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the first component functor of F and G (from the name)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Let $X$ be a set. Then the first component functor of $F$ and $G$ is a functor of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$ and the set of functors of $X$ and $A$.

the structural natural isomorphism of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$. Then the structural natural isomorphism of $\mathrm{self}$ is an isomorphism of the composition of the first projection functor of $\mathrm{self}$ and $F$ and the composition of the second projection functor of $\mathrm{self}$ and $G$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the isomorphism of x4 and x5 (from the name)

Let $x_{4}$ be an isomorphism of the first projection functor of $S$ and the first projection functor of $\mathrm{S'}$. Let $x_{5}$ be an isomorphism of the second projection functor of $S$ and the second projection functor of $\mathrm{S'}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the right whisker of the homomorphism of $x_{4}$ and $F$ and the homomorphism of the structural natural isomorphism of $\mathrm{S'}$ is equal to the composition of the homomorphism of the structural natural isomorphism of $S$ and the right whisker of the homomorphism of $x_{5}$ and $G$ and $\mathrm{CategoryTheory\_\_Limits\_\_CategoricalPullback\_\_CatCommSqOver\_\_mkIso\_\_\_auto\_1}$. Then the isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $S$ and $\mathrm{S'}$.

the precomposition of F and G (from the name)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Then the precomposition of $F$ and $G$ is a functor of the set of functors of $X$ and $Y$ and the set of functors of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $Y$ and $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$.

the precomposition object composition of U and V (from the name)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Let $U$ be a functor of $X$ and $Y$. Let $V$ be a functor of $Y$ and $Z$. Then the precomposition object composition of $U$ and $V$ is an isomorphism of the action of the precomposition of $F$ and $G$ and the composition of $U$ and $V$ and the composition of the action of the precomposition of $F$ and $G$ and $V$ and the action of the precomposition of $F$ and $G$ and $U$.

the precomposition object identity of F and G (from the name)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Let $X$ be a set. Then the precomposition object identity of $F$ and $G$ is an isomorphism of the action of the precomposition of $F$ and $G$ and the identity of $X$ and the identity of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$.

the second projection functor of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$. Then the second projection functor of $\mathrm{self}$ is a functor of $X$ and $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the second component functor of F and G (from the name)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Let $X$ be a set. Then the second component functor of $F$ and $G$ is a functor of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$ and the set of functors of $X$ and $C$.

the functor to categorical pullback of F and G (from the name)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Let $X$ be a set. Then the functor to categorical pullback of $F$ and $G$ is a functor of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$ and the set of functors of $X$ and the set of categorical pullbacks of $F$ and $G$.

the transform of X (from the name)

Let $X$ be a set. Then the transform of $X$ is a functor of the set of category cospan transforms of $x_{9}$ and $x_{10}$ and the set of functors of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$ and $\operatorname{CatCommSqOver}$ applied to $x_{9}$, $x_{10}$ and $X$.

the transform object composition of x20 and x21 (from the name)

Let $X$ be a set. Let $x_{20}$ be a category cospan transform of $x_{9}$ and $x_{10}$. Let $x_{21}$ be a category cospan transform of $x_{17}$ and $x_{18}$. Then the transform object composition of $x_{20}$ and $x_{21}$ is an isomorphism of the action of the transform of $X$ and the composition of $x_{20}$ and $x_{21}$ and the composition of the action of the transform of $X$ and $x_{20}$ and the action of the transform of $X$ and $x_{21}$.

the transform object identity of F and G (from the name)

Let $X$ be a set. Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Then the transform object identity of $F$ and $G$ is an isomorphism of the action of the transform of $X$ and the identity of $F$ and $G$ and the identity of $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$.

homomorphism of x3 and y (from the name)

Let $x_{3}$ and $y$ be categorical pullbacks of $F$ and $G$. Then the homomorphisms of $x_{3}$ and $y$ are a basic type.

the first component of self (from the docstring)

Let $\mathrm{self}$ be a homomorphism of $x_{3}$ and $y$. Then the first component of $\mathrm{self}$ is a homomorphism of the first component element of $x_{3}$ and the first component element of $y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the second component of self (from the docstring)

Let $\mathrm{self}$ be a homomorphism of $x_{3}$ and $y$. Then the second component of $\mathrm{self}$ is a homomorphism of the second component element of $x_{3}$ and the second component element of $y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the first component element of self (from the docstring)

Let $\mathrm{self}$ be a categorical pullback of $F$ and $G$. Then the first component element of $\mathrm{self}$ is an element of $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

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

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Let $X$ be a set. Then the functor equivalence of $F$ and $G$ is an equivalence of the set of functors of $X$ and the set of categorical pullbacks of $F$ and $G$ and $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$.

the structural isomorphism of self (from the docstring)

Let $\mathrm{self}$ be a categorical pullback of $F$ and $G$. Then the structural isomorphism of $\mathrm{self}$ is an isomorphism of the action of $F$ and the first component element of $\mathrm{self}$ and the action of $G$ and the second component element of $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the isomorphism of x4 and x5 (from the name)

Let $x_{4}$ be an isomorphism of the first component element of $x_{3}$ and the first component element of $y$. Let $x_{5}$ be an isomorphism of the second component element of $x_{3}$ and the second component element of $y$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the homomorphism of $x_{4}$ and the homomorphism of the structural isomorphism of $y$ is equal to the composition of the homomorphism of the structural isomorphism of $x_{3}$ and the map of $G$ and the homomorphism of $x_{5}$ and $\mathrm{CategoryTheory\_\_Limits\_\_CategoricalPullback\_\_mkIso\_\_\_auto\_1}$. Then the isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $x_{3}$ and $y$.

the natural isomorphism of x4 and x5 (from the name)

Let $x_{4}$ be an isomorphism of the composition of $J$ and the first projection of $F$ and $G$ and the composition of $K$ and the first projection of $F$ and $G$. Let $x_{5}$ be an isomorphism of the composition of $J$ and the second projection of $F$ and $G$ and the composition of $K$ and the second projection of $F$ and $G$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the right whisker of the homomorphism of $x_{4}$ and $F$ and the composition of the homomorphism of the associator of the first projection of $F$ and $G$ and $F$ and the composition of the left whisker of $K$ and the homomorphism of the isomorphism of $F$ and $G$ and the inverse of the associator of the second projection of $F$ and $G$ and $G$ is equal to the composition of the homomorphism of the associator of the first projection of $F$ and $G$ and $F$ and the composition of the left whisker of $J$ and the homomorphism of the isomorphism of $F$ and $G$ and the composition of the inverse of the associator of the second projection of $F$ and $G$ and $G$ and the right whisker of the homomorphism of $x_{5}$ and $G$ and $\mathrm{CategoryTheory\_\_Limits\_\_CategoricalPullback\_\_mkNatIso\_\_\_auto\_1}$. Then the natural isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $J$ and $K$.

the second component element of self (from the docstring)

Let $\mathrm{self}$ be a categorical pullback of $F$ and $G$. Then the second component element of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Let $X$ be a set. Then $\operatorname{toCatCommSqOver}$ applied to $F$, $G$ and $X$ is a functor of the set of functors of $X$ and the set of categorical pullbacks of $F$ and $G$ and $\operatorname{CatCommSqOver}$ applied to $F$, $G$ and $X$.

the first projection of F and G (from the docstring)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Then the first projection of $F$ and $G$ is a functor of the set of categorical pullbacks of $F$ and $G$ and $A$.

the second projection of F and G (from the docstring)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Then the second projection of $F$ and $G$ is a functor of the set of categorical pullbacks of $F$ and $G$ and $C$.

category cospan transform of #3 and #4 (from the name)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Let $\mathrm{F'}$ be a functor of $\mathrm{A'}$ and $\mathrm{B'}$. Let $\mathrm{G'}$ be a functor of $\mathrm{C'}$ and $\mathrm{B'}$. Then the category cospan transforms of $\mathrm{F'}$ and $\mathrm{G'}$ are a basic type.

the associator of x13 and x14 (from the name)

Let $x_{12}$ be a category cospan transform of $\mathrm{F'}$ and $\mathrm{G'}$. Let $x_{13}$ be a category cospan transform of $\mathrm{F''}$ and $\mathrm{G''}$. Let $x_{14}$ be a category cospan transform of $\mathrm{F'''}$ and $\mathrm{G'''}$. Then the associator of $x_{13}$ and $x_{14}$ is an isomorphism of the composition of the composition of $x_{12}$ and $x_{13}$ and $x_{14}$ and the composition of $x_{12}$ and the composition of $x_{13}$ and $x_{14}$.

the functor on the base component of self (from the docstring)

Let $\mathrm{self}$ be a category cospan transform of $\mathrm{F'}$ and $\mathrm{G'}$. Then the functor on the base component of $\mathrm{self}$ is a functor of $B$ and $\mathrm{B'}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the base isomorphism of e (from the name)

Let $e$ be an isomorphism of $x_{6}$ and $x_{7}$. Then the base isomorphism of $e$ is an isomorphism of the functor on the base component of $x_{6}$ and the functor on the base component of $x_{7}$.

the composition of x9 and x10 (from the name)

Let $x_{9}$ be a category cospan transform of $\mathrm{F'}$ and $\mathrm{G'}$. Let $x_{10}$ be a category cospan transform of $\mathrm{F''}$ and $\mathrm{G''}$. Then the composition of $x_{9}$ and $x_{10}$ is a category cospan transform of $\mathrm{F''}$ and $\mathrm{G''}$ defined as $\operatorname{mk}$ applied to the composition of the functor on the left component of $x_{9}$ and the functor on the left component of $x_{10}$, the composition of the functor on the base component of $x_{9}$ and the functor on the base component of $x_{10}$, the composition of the functor on the right component of $x_{9}$ and the functor on the right component of $x_{10}$, $\operatorname{vComp'}$ applied to $\operatorname{squareLeft}$ applied to $x_{9}$ and $\operatorname{squareLeft}$ applied to $x_{10}$ and $\operatorname{vComp'}$ applied to $\operatorname{squareRight}$ applied to $x_{9}$ and $\operatorname{squareRight}$ applied to $x_{10}$.

the identity of F and G (from the docstring)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $B$. Then the identity of $F$ and $G$ is a category cospan transform of $F$ and $G$ defined as $\operatorname{mk}$ applied to the identity of $A$, the identity of $B$, the identity of $C$, $\mathrm{inferInstance}$ and $\mathrm{inferInstance}$.

the functor on the left component of self (from the docstring)

Let $\mathrm{self}$ be a category cospan transform of $\mathrm{F'}$ and $\mathrm{G'}$. Then the functor on the left component of $\mathrm{self}$ is a functor of $A$ and $\mathrm{A'}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the left isomorphism of e (from the name)

Let $e$ be an isomorphism of $x_{6}$ and $x_{7}$. Then the left isomorphism of $e$ is an isomorphism of the functor on the left component of $x_{6}$ and the functor on the left component of $x_{7}$.

the left unitor of x6 (from the name)

Let $x_{6}$ be a category cospan transform of $\mathrm{F'}$ and $\mathrm{G'}$. Then the left unitor of $x_{6}$ is an isomorphism of the composition of the identity of $F$ and $G$ and $x_{6}$ and $x_{6}$.

the isomorphism of right and base (from the name)

Let $\mathrm{left}$ be an isomorphism of the functor on the left component of $x_{6}$ and the functor on the left component of $x_{7}$. Let $\mathrm{right}$ be an isomorphism of the functor on the right component of $x_{6}$ and the functor on the right component of $x_{7}$. Let $\mathrm{base}$ be an isomorphism of the functor on the base component of $x_{6}$ and the functor on the base component of $x_{7}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of the isomorphism of the functor on the base component of $x_{6}$ and $\mathrm{F'}$ and the right whisker of the homomorphism of $\mathrm{left}$ and $\mathrm{F'}$ is equal to the composition of the left whisker of $F$ and the homomorphism of $\mathrm{base}$ and the homomorphism of the isomorphism of the functor on the base component of $x_{7}$ and $\mathrm{F'}$ and $\mathrm{CategoryTheory\_\_Limits\_\_CatCospanTransform\_\_mkIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of the isomorphism of the functor on the base component of $x_{6}$ and $\mathrm{G'}$ and the right whisker of the homomorphism of $\mathrm{right}$ and $\mathrm{G'}$ is equal to the composition of the left whisker of $G$ and the homomorphism of $\mathrm{base}$ and the homomorphism of the isomorphism of the functor on the base component of $x_{7}$ and $\mathrm{G'}$ and $\mathrm{CategoryTheory\_\_Limits\_\_CatCospanTransform\_\_mkIso\_\_\_auto\_3}$. Then the isomorphism of $\mathrm{right}$ and $\mathrm{base}$ is an isomorphism of $x_{6}$ and $x_{7}$.

the functor on the right component of self (from the docstring)

Let $\mathrm{self}$ be a category cospan transform of $\mathrm{F'}$ and $\mathrm{G'}$. Then the functor on the right component of $\mathrm{self}$ is a functor of $C$ and $\mathrm{C'}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the right isomorphism of e (from the name)

Let $e$ be an isomorphism of $x_{6}$ and $x_{7}$. Then the right isomorphism of $e$ is an isomorphism of the functor on the right component of $x_{6}$ and the functor on the right component of $x_{7}$.

the right unitor of x6 (from the name)

Let $x_{6}$ be a category cospan transform of $\mathrm{F'}$ and $\mathrm{G'}$. Then the right unitor of $x_{6}$ is an isomorphism of the composition of $x_{6}$ and the identity of $\mathrm{F'}$ and $\mathrm{G'}$ and $x_{6}$.

category cospan transform morphism of x6 and x7 (from the name)

Let $x_{6}$ and $x_{7}$ be category cospan transforms of $\mathrm{F'}$ and $\mathrm{G'}$. Then the category cospan transform morphisms of $x_{6}$ and $x_{7}$ are a basic type.

the base of self (from the name)

Let $\mathrm{self}$ be a category cospan transform morphism of $x_{6}$ and $x_{7}$. Then the base of $\mathrm{self}$ is a homomorphism of the functor on the base component of $x_{6}$ and the functor on the base component of $x_{7}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the left of self (from the name)

Let $\mathrm{self}$ be a category cospan transform morphism of $x_{6}$ and $x_{7}$. Then the left of $\mathrm{self}$ is a homomorphism of the functor on the left component of $x_{6}$ and the functor on the left component of $x_{7}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the right of self (from the name)

Let $\mathrm{self}$ be a category cospan transform morphism of $x_{6}$ and $x_{7}$. Then the right of $\mathrm{self}$ is a homomorphism of the functor on the right component of $x_{6}$ and the functor on the right component of $x_{7}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the left whisker of x9 and x12 (from the name)

Let $x_{9}$ be a category cospan transform of $\mathrm{F'}$ and $\mathrm{G'}$. Let $x_{12}$ be a homomorphism of $x_{10}$ and $x_{11}$. Then the left whisker of $x_{9}$ and $x_{12}$ is a homomorphism of the composition of $x_{9}$ and $x_{10}$ and the composition of $x_{9}$ and $x_{11}$.

the right whisker of x11 and x12 (from the name)

Let $x_{11}$ be a homomorphism of $x_{9}$ and $x_{10}$. Let $x_{12}$ be a category cospan transform of $\mathrm{F''}$ and $\mathrm{G''}$. Then the right whisker of $x_{11}$ and $x_{12}$ is a homomorphism of the composition of $x_{9}$ and $x_{12}$ and the composition of $x_{10}$ and $x_{12}$.

chosen pullback of x3 and x4 (from the name)

Let $x_{3}$ be a homomorphism of $x_{1}$ and $S$. Let $x_{4}$ be a homomorphism of $x_{2}$ and $S$. Then the chosen pullbacks of $x_{3}$ and $x_{4}$ are a basic type.

diagonal of h (from the name)

Let $h$ be a chosen pullback of $f$ and $f$. Then a diagonal of $h$ is an element of the function that maps $h$ to $\operatorname{LiftStruct}$ applied to $h$, the identity morphism of $X$, the identity morphism of $X$ and $f$.

Let $h$ be a chosen pullback of $x_{3}$ and $x_{4}$. Let $x_{5}$ be a homomorphism of $Y$ and $x_{1}$. Let $x_{6}$ be a homomorphism of $Y$ and $x_{2}$. Let $b$ be a homomorphism of $Y$ and $S$. Then the elements of $\operatorname{LiftStruct}$ applied to $h$, $x_{5}$, $x_{6}$ and $b$ are a basic type.

Let $\mathrm{self}$ be an element of $\operatorname{LiftStruct}$ applied to $h$, $x_{5}$, $x_{6}$ and $b$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $Y$ and the pullback of $h$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a chosen pullback of $x_{3}$ and $x_{4}$. Then $\operatorname{isLimit}$ applied to $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2081\_}$ applied to $\mathrm{self}$, $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2082\_}$ applied to $\mathrm{self}$ and $\operatorname{condition}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a chosen pullback of $x_{3}$ and $x_{4}$. Then $\operatorname{p}$ applied to $\mathrm{self}$ is a homomorphism of the pullback of $\mathrm{self}$ and $S$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

the pullback of self (from the docstring)

Let $\mathrm{self}$ be a chosen pullback of $x_{3}$ and $x_{4}$. Then the pullback of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a chosen pullback of $x_{3}$ and $x_{4}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of the pullback of $\mathrm{self}$ and $x_{1}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a chosen pullback of $x_{3}$ and $x_{4}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of the pullback of $\mathrm{self}$ and $x_{2}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

chosen pullback of x8 and x9 (from the name)

Let $x_{7}$ be a chosen pullback of $x_{4}$ and $x_{5}$. Let $x_{8}$ be a chosen pullback of $x_{5}$ and $x_{6}$. Let $x_{9}$ be a chosen pullback of $x_{4}$ and $x_{6}$. Then the chosen pullbacks of $x_{8}$ and $x_{9}$ are a basic type.

the chosen pullback of self (from the name)

Let $\mathrm{self}$ be a chosen pullback of $x_{8}$ and $x_{9}$. Then the chosen pullback of $\mathrm{self}$ is a chosen pullback of $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2082\_}$ applied to $x_{7}$ and $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2081\_}$ applied to $x_{8}$ defined as $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a chosen pullback of $x_{8}$ and $x_{9}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_l}$ applied to $\mathrm{self}$ is an element of $\operatorname{LiftStruct}$ applied to $x_{9}$, $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_p\_u2081\_}$ applied to $\mathrm{self}$, $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_p\_u2083\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_p}$ applied to $\mathrm{self}$ defined as $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_proj4}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a chosen pullback of $x_{8}$ and $x_{9}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_p}$ applied to $\mathrm{self}$ is a homomorphism of the pullback of the chosen pullback of $\mathrm{self}$ and $S$ defined as $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_proj1}$ applied to $\mathrm{self}$.

the chosen wide pullback of h (from the docstring)

Let $h$ be a chosen pullback of $x_{8}$ and $x_{9}$. Then the chosen wide pullback of $h$ is an element of $C$ defined as the pullback of the chosen pullback of $h$.

Let $\mathrm{self}$ be a chosen pullback of $x_{8}$ and $x_{9}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_p\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of the pullback of the chosen pullback of $\mathrm{self}$ and $x_{1}$ defined as $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_proj2}$ applied to $\mathrm{self}$.

Let $h$ be a chosen pullback of $x_{8}$ and $x_{9}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_p\_u2081\_\_u2082\_}$ applied to $h$ is a homomorphism of the chosen wide pullback of $h$ and the pullback of $x_{7}$ defined as $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2081\_}$ applied to the chosen pullback of $h$.

Let $h$ be a chosen pullback of $x_{8}$ and $x_{9}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_p\_u2081\_\_u2083\_}$ applied to $h$ is a homomorphism of the chosen wide pullback of $h$ and the pullback of $x_{9}$ defined as $\operatorname{f}$ applied to $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_l}$ applied to $h$.

Let $h$ be a chosen pullback of $x_{8}$ and $x_{9}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_p\_u2082\_}$ applied to $h$ is a homomorphism of the chosen wide pullback of $h$ and $x_{2}$ defined as $\operatorname{p}$ applied to the chosen pullback of $h$.

Let $h$ be a chosen pullback of $x_{8}$ and $x_{9}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_p\_u2082\_\_u2083\_}$ applied to $h$ is a homomorphism of the chosen wide pullback of $h$ and the pullback of $x_{8}$ defined as $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2082\_}$ applied to the chosen pullback of $h$.

Let $\mathrm{self}$ be a chosen pullback of $x_{8}$ and $x_{9}$. Then $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_p\_u2083\_}$ applied to $\mathrm{self}$ is a homomorphism of the pullback of the chosen pullback of $\mathrm{self}$ and $x_{3}$ defined as $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_u2083\_\_\_proj3}$ applied to $\mathrm{self}$.

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $\mathrm{cF}$ be a cocone of $F$. Let $\mathrm{cG}$ be a cocone of $G$. Let $f$ be a homomorphism of $\mathrm{cF}$ and the action of the precomposition of $x_{2}$ and $\mathrm{cG}$ such that for all elements $i$ of $I$, $\operatorname{IsPushout}$ holds for the component of the inclusion of $\mathrm{cF}$ and $i$, the component of $x_{2}$ and $i$, the homomorphism of $f$ and the component of the inclusion of $\mathrm{cG}$ and $i$. Let $\mathrm{hcF}$ be an element of $\operatorname{IsColimit}$ applied to $\mathrm{cF}$. Then $\operatorname{isColimitOfIsPushoutOfIsConnected}$ applied to $x_{2}$, $\mathrm{cF}$, $\mathrm{cG}$, $f$, $\mathrm{hf}$ and $\mathrm{hcF}$ is an element of $\operatorname{IsColimit}$ applied to $\mathrm{cG}$.

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $\mathrm{cF}$ be a cone of $F$. Let $\mathrm{cG}$ be a cone of $G$. Let $f$ be a homomorphism of the action of the postcomposition of $x_{2}$ and $\mathrm{cF}$ and $\mathrm{cG}$ such that for all elements $i$ of $I$, $\operatorname{IsPullback}$ holds for the component of the projection of $\mathrm{cF}$ and $i$, the homomorphism of $f$, the component of $x_{2}$ and $i$ and the component of the projection of $\mathrm{cG}$ and $i$. Let $\mathrm{hcG}$ be an element of $\operatorname{IsLimit}$ applied to $\mathrm{cG}$. Then $\operatorname{isLimitOfIsPullbackOfIsConnected}$ applied to $x_{2}$, $\mathrm{cF}$, $\mathrm{cG}$, $f$, $\mathrm{hf}$ and $\mathrm{hcG}$ is an element of $\operatorname{IsLimit}$ applied to $\mathrm{cF}$.

walking cospan (from the name)

A walking cospan is a wide pullback shape of the set of walking pairs.

homomorphism of x and x1 (from the name)

Let $x$ and $x_{1}$ be walking cospans. Then a homomorphism of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of homomorphisms of $x$ and $x_{1}$.

the identity of X (from the name)

Let $X$ be a walking cospan. Then the identity of $X$ is a homomorphism of $X$ and $X$ defined as the identity of $X$.

the left arrow of the walking cospan (from the docstring)

The left arrow of the walking cospan is a homomorphism of the left point of the walking cospan and the one defined as $\operatorname{term}$ applied to the left.

the right arrow of the walking cospan (from the docstring)

The right arrow of the walking cospan is a homomorphism of the right point of the walking cospan and the one defined as $\operatorname{term}$ applied to the right.

the extension of i (from the name)

Let $i$ be an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ such that the component of the projection of $s$ and the left point of the walking cospan is equal to the composition of the homomorphism of $i$ and the component of the projection of $t$ and the left point of the walking cospan and the component of the projection of $s$ and the right point of the walking cospan is equal to the composition of the homomorphism of $i$ and the component of the projection of $t$ and the right point of the walking cospan. Then the extension of $i$ is an isomorphism of $s$ and $t$.

the left point of the walking cospan (from the docstring)

The left point of the walking cospan is a walking cospan defined as $\operatorname{some}$ applied to the left.

the one (from the name)

The one is a walking cospan defined as $\operatorname{none}$.

the right point of the walking cospan (from the docstring)

The right point of the walking cospan is a walking cospan defined as $\operatorname{some}$ applied to the right.

walking span (from the name)

A walking span is a wide pushout shape of the set of walking pairs.

homomorphism of x and x1 (from the name)

Let $x$ and $x_{1}$ be walking spans. Then a homomorphism of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of homomorphisms of $x$ and $x_{1}$.

the first component (from the name)

The first component is a homomorphism of the zero and the left point of the walking span defined as $\operatorname{init}$ applied to the left.

the identity of X (from the name)

Let $X$ be a walking span. Then the identity of $X$ is a homomorphism of $X$ and $X$ defined as the identity of $X$.

the second component (from the name)

The second component is a homomorphism of the zero and the right point of the walking span defined as $\operatorname{init}$ applied to the right.

the extension of i (from the name)

Let $i$ be an isomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to $t$ such that the composition of the component of the inclusion of $s$ and the left point of the walking cospan and the homomorphism of $i$ is equal to the component of the inclusion of $t$ and the left point of the walking cospan and the composition of the component of the inclusion of $s$ and the right point of the walking cospan and the homomorphism of $i$ is equal to the component of the inclusion of $t$ and the right point of the walking cospan. Then the extension of $i$ is an isomorphism of $s$ and $t$.

the left point of the walking span (from the docstring)

The left point of the walking span is a walking span defined as $\operatorname{some}$ applied to the left.

the right point of the walking span (from the docstring)

The right point of the walking span is a walking span defined as $\operatorname{some}$ applied to the right.

the zero (from the name)

The zero is a walking span defined as $\operatorname{none}$.

the cospan of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the cospan of $f$ and $g$ is a functor of the set of walking cospans and $C$.

the cospan composition isomorphism of f and g (from the name)

Let $F$ 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 cospan composition isomorphism of $f$ and $g$ is an isomorphism of the composition of the cospan of $f$ and $g$ and $F$ and the cospan of the map of $F$ and $f$ and the map of $F$ and $g$.

the cospan extension of iY and iZ (from the name)

Let $\mathrm{iX}$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $\mathrm{iY}$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Let $\mathrm{iZ}$ be an isomorphism of $Z$ and $\mathrm{Z'}$ such that the composition of the homomorphism of $\mathrm{iX}$ and $\mathrm{f'}$ is equal to the composition of $f$ and the homomorphism of $\mathrm{iZ}$ and the composition of the homomorphism of $\mathrm{iY}$ and $\mathrm{g'}$ is equal to the composition of $g$ and the homomorphism of $\mathrm{iZ}$. Then the cospan extension of $\mathrm{iY}$ and $\mathrm{iZ}$ is an isomorphism of the cospan of $f$ and $g$ and the cospan of $\mathrm{f'}$ and $\mathrm{g'}$.

the cospan homomorphism of l and r (from the name)

Let $z$ be a homomorphism of the action of $F$ and the one and the action of $G$ and the one. Let $l$ be a homomorphism of the action of $F$ and the left point of the walking cospan and the action of $G$ and the left point of the walking cospan. Let $r$ be a homomorphism of the action of $F$ and the right point of the walking cospan and the action of $G$ and the right point of the walking cospan. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the left arrow of the walking cospan and $z$ is equal to the composition of $l$ and the map of $G$ and the left arrow of the walking cospan and $\mathrm{CategoryTheory\_\_Limits\_\_cospanHomMk\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the right arrow of the walking cospan and $z$ is equal to the composition of $r$ and the map of $G$ and the right arrow of the walking cospan and $\mathrm{CategoryTheory\_\_Limits\_\_cospanHomMk\_\_\_auto\_3}$. Then the cospan homomorphism of $l$ and $r$ is a homomorphism of $F$ and $G$.

the cospan isomorphism of l and r (from the name)

Let $z$ be an isomorphism of the action of $F$ and the one and the action of $G$ and the one. Let $l$ be an isomorphism of the action of $F$ and the left point of the walking cospan and the action of $G$ and the left point of the walking cospan. Let $r$ be an isomorphism of the action of $F$ and the right point of the walking cospan and the action of $G$ and the right point of the walking cospan. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the left arrow of the walking cospan and the homomorphism of $z$ is equal to the composition of the homomorphism of $l$ and the map of $G$ and the left arrow of the walking cospan and $\mathrm{CategoryTheory\_\_Limits\_\_cospanIsoMk\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the right arrow of the walking cospan and the homomorphism of $z$ is equal to the composition of the homomorphism of $r$ and the map of $G$ and the right arrow of the walking cospan and $\mathrm{CategoryTheory\_\_Limits\_\_cospanIsoMk\_\_\_auto\_3}$. Then the cospan isomorphism of $l$ and $r$ is an isomorphism of $F$ and $G$.

the diagram isomorphism cospan of F (from the name)

Let $F$ be a functor of the set of walking cospans and $C$. Then the diagram isomorphism cospan of $F$ is an isomorphism of $F$ and the cospan of the map of $F$ and the left arrow of the walking cospan and the map of $F$ and the right arrow of the walking cospan.

the diagram isomorphism span of F (from the name)

Let $F$ be a functor of the set of walking spans and $C$. Then the diagram isomorphism span of $F$ is an isomorphism of $F$ and the span of the map of $F$ and the first component and the map of $F$ and the second component.

the span of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the span of $f$ and $g$ is a functor of the set of walking spans and $C$.

the span composition isomorphism of f and g (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $X$ and $Z$. Then the span composition isomorphism of $f$ and $g$ is an isomorphism of the composition of the span of $f$ and $g$ and $F$ and the span of the map of $F$ and $f$ and the map of $F$ and $g$.

the span extension of iY and iZ (from the name)

Let $\mathrm{iX}$ be an isomorphism of $X$ and $\mathrm{X'}$. Let $\mathrm{iY}$ be an isomorphism of $Y$ and $\mathrm{Y'}$. Let $\mathrm{iZ}$ be an isomorphism of $Z$ and $\mathrm{Z'}$. Assume that the composition of the homomorphism of $\mathrm{iX}$ and $\mathrm{f'}$ is equal to the composition of $f$ and the homomorphism of $\mathrm{iY}$. Assume that the composition of the homomorphism of $\mathrm{iX}$ and $\mathrm{g'}$ is equal to the composition of $g$ and the homomorphism of $\mathrm{iZ}$. Then the span extension of $\mathrm{iY}$ and $\mathrm{iZ}$ is an isomorphism of the span of $f$ and $g$ and the span of $\mathrm{f'}$ and $\mathrm{g'}$.

the span homomorphism of l and r (from the name)

Let $z$ be a homomorphism of the action of $F$ and the zero and the action of $G$ and the zero. Let $l$ be a homomorphism of the action of $F$ and the left point of the walking span and the action of $G$ and the left point of the walking span. Let $r$ be a homomorphism of the action of $F$ and the right point of the walking span and the action of $G$ and the right point of the walking span. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the first component and $l$ is equal to the composition of $z$ and the map of $G$ and the first component and $\mathrm{CategoryTheory\_\_Limits\_\_spanHomMk\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the second component and $r$ is equal to the composition of $z$ and the map of $G$ and the second component and $\mathrm{CategoryTheory\_\_Limits\_\_spanHomMk\_\_\_auto\_3}$. Then the span homomorphism of $l$ and $r$ is a homomorphism of $F$ and $G$.

the span isomorphism of l and r (from the name)

Let $z$ be an isomorphism of the action of $F$ and the zero and the action of $G$ and the zero. Let $l$ be an isomorphism of the action of $F$ and the left point of the walking span and the action of $G$ and the left point of the walking span. Let $r$ be an isomorphism of the action of $F$ and the right point of the walking span and the action of $G$ and the right point of the walking span. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the first component and the homomorphism of $l$ is equal to the composition of the homomorphism of $z$ and the map of $G$ and the first component and $\mathrm{CategoryTheory\_\_Limits\_\_spanIsoMk\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $F$ and the second component and the homomorphism of $r$ is equal to the composition of the homomorphism of $z$ and the map of $G$ and the second component and $\mathrm{CategoryTheory\_\_Limits\_\_spanIsoMk\_\_\_auto\_3}$. Then the span isomorphism of $l$ and $r$ is an isomorphism of $F$ and $G$.

the equalizer pullback map isomorphism of v (from the name)

Assume that the composition of $f$ and $t$ is equal to $s$. Assume that the composition of $g$ and $t$ is equal to $s$. Let $v$ be a homomorphism of $T$ and $S$. Then the equalizer pullback map isomorphism of $v$ is an isomorphism of the equalizer of the map of the identity morphism of $T$ and the identity morphism of $S$ and the map of the identity morphism of $T$ and the identity morphism of $S$ and the pullback of the inclusion of $f$ and $g$ and the first projection of the pullback of $s$ and $v$.