Definitions: Mathlib.CategoryTheory, part 8 of 25

Let $F$ be a functor of $C$ and the set of categories. Then the elements of $\operatorname{Grothendieck}$ applied to $F$ are a basic type.

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be elements of $\operatorname{Grothendieck}$ applied to $F$. Then the homomorphisms of $X$ and $Y$ are a basic type.

the base of self (from the name)

Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the base of $\mathrm{self}$ is a homomorphism of the base of $X$ and the base of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the fiber of self (from the name)

Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the fiber of $\mathrm{self}$ is a homomorphism of the action of the functor of the map of $F$ and the base of $\mathrm{self}$ and the object in the fiber of the base object of $X$ and the object in the fiber of the base object of $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the base of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{Grothendieck}$ applied to $F$. Then the base of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the composition of f and g (from the name)

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

the composition as small functor equivalence of F (from the name)

Let $F$ be a functor of $C$ and the set of categories. Then the composition as small functor equivalence of $F$ is an equivalence of $\operatorname{Grothendieck}$ applied to the composition of $F$ and $\operatorname{asSmallFunctor}$ and $\operatorname{Grothendieck}$ applied to $F$.

the composition as small functor equivalence functor of F (from the name)

Let $F$ be a functor of $C$ and the set of categories. Then the composition as small functor equivalence functor of $F$ is a functor of $\operatorname{Grothendieck}$ applied to the composition of $F$ and $\operatorname{asSmallFunctor}$ and $\operatorname{Grothendieck}$ applied to $F$.

the composition as small functor equivalence inverse of F (from the name)

Let $F$ be a functor of $C$ and the set of categories. Then the composition as small functor equivalence inverse of $F$ is a functor of $\operatorname{Grothendieck}$ applied to $F$ and $\operatorname{Grothendieck}$ applied to the composition of $F$ and $\operatorname{asSmallFunctor}$.

the object in the fiber of the base object of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{Grothendieck}$ applied to $F$. Then the object in the fiber of the base object of $\mathrm{self}$ is an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of $F$ and the base of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

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

the Grothendieck construction as a functor from the functor category (from the docstring)

The Grothendieck construction as a functor from the functor category is a functor of the set of functors of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $E$ and the set of categories and $\operatorname{Over}$ applied to $E$.

Let $\mathrm{fib}$ be a function from elements $c_{2}$ of $C$ to functors of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of $F$ and $c_{2}$ and $E$. Let $\mathrm{hom}$ be a function from elements $c_{1}$ of $C$ and elements $\mathrm{c'}$ of $C$ and homomorphisms $f_{1}$ of $c_{1}$ and $\mathrm{c'}$ to homomorphisms of $\mathrm{fib}$ applied to $c_{1}$ and the composition of the functor of the map of $F$ and $f_{1}$ and $\mathrm{fib}$ applied to $\mathrm{c'}$ such that for all elements $c$ of $C$, $\mathrm{hom}$ applied to $c$, $c$ and the identity morphism of $c$ is equal to $\operatorname{eqToHom}$ applied to $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Grothendieck\_\_0\_\_\_proof\_145}$ applied to $\mathrm{fib}$ and $c$ and for all elements $x_{2}$ of $C$, for all elements $x_{3}$ of $C$, for all elements $x_{4}$ of $C$, for all homomorphisms $f$ of $x_{2}$ and $x_{3}$, for all homomorphisms $g$ of $x_{3}$ and $x_{4}$, $\mathrm{hom}$ applied to $x_{2}$, $x_{4}$ and the composition of $f$ and $g$ is equal to the composition of $\mathrm{hom}$ applied to $x_{2}$, $x_{3}$ and $f$ and the composition of the left whisker of the functor of the map of $F$ and $f$ and $\mathrm{hom}$ applied to $x_{3}$, $x_{4}$ and $g$ and $\operatorname{eqToHom}$ applied to $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Grothendieck\_\_0\_\_\_proof\_146}$ applied to $\mathrm{fib}$, $x_{2}$, $x_{3}$, $x_{4}$, $f$ and $g$. Then $\operatorname{functorFrom}$ applied to $c_{2}$, $\mathrm{fib}$, $c_{1}$, $\mathrm{c'}$, $f_{1}$, $\mathrm{hom}$, $\mathrm{hom\_id}$ and $\mathrm{hom\_comp}$ is a functor of $\operatorname{Grothendieck}$ applied to $F$ and $E$.

the Grothendieck type to category of G (from the name)

Let $G$ be a functor of $C$ and the set of sets. Then the Grothendieck type to category of $G$ is an equivalence of $\operatorname{Grothendieck}$ applied to the composition of $G$ and the type to category and the set of elements of $G$.

the identity morphism in the Grothendieck category of X (from the docstring)

Let $X$ be an element of $\operatorname{Grothendieck}$ applied to $F$. Then the identity morphism in the Grothendieck category of $X$ is a homomorphism of $X$ and $X$.

the isomorphism of x1 and x2 (from the name)

Let $x_{1}$ be an isomorphism of the base of $X$ and the base of $Y$. Let $x_{2}$ be an isomorphism of the action of the functor of the map of $F$ and the homomorphism of $x_{1}$ and the object in the fiber of the base object of $X$ and the object in the fiber of the base object of $Y$. Then the isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of $X$ and $Y$.

the map of x1 (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $G$. Then the map of $x_{1}$ is a functor of $\operatorname{Grothendieck}$ applied to $F$ and $\operatorname{Grothendieck}$ applied to $G$.

the map composition isomorphism of x1 and x2 (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $G$. Let $x_{2}$ be a homomorphism of $G$ and $H$. Then the map composition isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of the map of the composition of $x_{1}$ and $x_{2}$ and the composition of the map of $x_{1}$ and the map of $x_{2}$ defined as $\operatorname{eqToIso}$ applied to $\mathrm{CategoryTheory\_\_Grothendieck\_\_map\_comp\_eq}$ applied to $x_{1}$ and $x_{2}$.

the map identity isomorphism (from the name)

The map identity isomorphism is an isomorphism of the category homomorphism of the map of the identity morphism of $F$ and the identity morphism of $\operatorname{of}$ applied to $\operatorname{Grothendieck}$ applied to $F$.

the map whisker left isomorphism conjugate map of G and x2 (from the name)

Let $G$ be an equivalence of $D$ and $C$. Let $x_{2}$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the map whisker left isomorphism conjugate map of $G$ and $x_{2}$ is an isomorphism of the map of the left whisker of the functor of $G$ and $x_{2}$ and the composition of the functor of the equivalence of $F$ and $G$ and the composition of the map of $x_{2}$ and the inverse of the equivalence of $\mathrm{F'}$ and $G$ defined as the composition of the inverse of the right unitor of the map of the left whisker of the functor of $G$ and $x_{2}$ and the left isomorphism whisker of the map of the left whisker of the functor of $G$ and $x_{2}$ and the unit isomorphism of the equivalence of $\mathrm{F'}$ and $G$.

the map whisker right as small functor of x1 (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $G$. Then the map whisker right as small functor of $x_{1}$ is an isomorphism of the map of the right whisker of $x_{1}$ and $\operatorname{asSmallFunctor}$ and the composition of the functor of the composition as small functor equivalence of $F$ and the composition of the map of $x_{1}$ and the inverse of the composition as small functor equivalence of $G$.

Let $F$ be a functor of $C$ and the set of categories. Let $G$ be a functor of $D$ and $C$. Then $\operatorname{pre}$ applied to $F$ and $G$ is a functor of $\operatorname{Grothendieck}$ applied to the composition of $G$ and $F$ and $\operatorname{Grothendieck}$ applied to $F$.

the equivalence of F and G (from the name)

Let $F$ be a functor of $C$ and the set of categories. Let $G$ be an equivalence of $D$ and $C$. Then the equivalence of $F$ and $G$ is an equivalence of $\operatorname{Grothendieck}$ applied to the composition of the functor of $G$ and $F$ and $\operatorname{Grothendieck}$ applied to $F$.

the inverse of F and G (from the name)

Let $F$ be a functor of $C$ and the set of categories. Let $G$ be an equivalence of $D$ and $C$. Then the inverse of $F$ and $G$ is a functor of $\operatorname{Grothendieck}$ applied to $F$ and $\operatorname{Grothendieck}$ applied to the composition of the functor of $G$ and $F$ defined as the composition of the map of the right whisker of the inverse of the counit of $G$ and $F$ and $\operatorname{pre}$ applied to the composition of the functor of $G$ and $F$ and the inverse of $G$.

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

Let $F$ be a functor of $C$ and the set of categories. Let $x_{2}$ be an isomorphism of $G$ and $H$. Then the natural isomorphism of $F$ and $x_{2}$ is an isomorphism of $\operatorname{pre}$ applied to $F$ and $G$ and the composition of the map of the right whisker of the homomorphism of $x_{2}$ and $F$ and $\operatorname{pre}$ applied to $F$ and $H$.

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

Let $F$ be a functor of $C$ and the set of categories. Let $G$ be an equivalence of $D$ and $C$. Then the unit isomorphism of $F$ and $G$ is an isomorphism of the map of the right whisker of the inverse of the unit of $G$ and the composition of the functor of $G$ and $F$ and $\operatorname{pre}$ applied to the composition of the functor of $G$ and $F$ and the composition of the functor of $G$ and the inverse of $G$ defined as the inverse of the natural isomorphism of the composition of the functor of $G$ and $F$ and the inverse of the unit isomorphism of $G$.

the transport of x1 and t (from the name)

Let $x_{1}$ be an element of $\operatorname{Grothendieck}$ applied to $F$. Let $t$ be a homomorphism of the base of $x_{1}$ and $c$. Then the transport of $x_{1}$ and $t$ is a homomorphism of $x_{1}$ and the transport of $x_{1}$ and $t$ defined as $\operatorname{mk}$ applied to $t$ and the identity morphism of the action of the functor of the map of $F$ and $t$ and the object in the fiber of the base object of $x_{1}$.

the transport of x1 and t (from the name)

Let $x_{1}$ be an element of $\operatorname{Grothendieck}$ applied to $F$. Let $t$ be a homomorphism of the base of $x_{1}$ and $c$. Then the transport of $x_{1}$ and $t$ is an element of $\operatorname{Grothendieck}$ applied to $F$ defined as $\operatorname{mk}$ applied to $c$ and the action of the functor of the map of $F$ and $t$ and the object in the fiber of the base object of $x_{1}$.

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

Let $x_{1}$ be an element of $\operatorname{Grothendieck}$ applied to $F$. Let $x_{2}$ be an isomorphism of the base of $x_{1}$ and $c$. Then the transport isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of the transport of $x_{1}$ and the homomorphism of $x_{2}$ and $x_{1}$ defined as the inverse of the isomorphism of $x_{2}$ and the identity of the action of the functor of the map of $F$ and the homomorphism of $x_{2}$ and the object in the fiber of the base object of $x_{1}$.

the inclusion of F and c (from the docstring)

Let $F$ be a functor of $C$ and the set of categories. Let $c$ be an element of $C$. Then the inclusion of $F$ and $c$ is a functor of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of $F$ and $c$ and $\operatorname{Grothendieck}$ applied to $F$.

Let $\mathrm{fib}$ be a function from elements $c_{3}$ of $C$ to functors of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the action of $F$ and $c_{3}$ and $E$. Let $\mathrm{hom}$ be a function from elements $c_{2}$ of $C$ and elements $\mathrm{c'}$ of $C$ and homomorphisms $f_{1}$ of $c_{2}$ and $\mathrm{c'}$ to homomorphisms of $\mathrm{fib}$ applied to $c_{2}$ and the composition of the functor of the map of $F$ and $f_{1}$ and $\mathrm{fib}$ applied to $\mathrm{c'}$ such that for all elements $c_{1}$ of $C$, $\mathrm{hom}$ applied to $c_{1}$, $c_{1}$ and the identity morphism of $c_{1}$ is equal to $\operatorname{eqToHom}$ applied to $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Grothendieck\_\_0\_\_\_proof\_145}$ applied to $\mathrm{fib}$ and $c_{1}$ and for all elements $x_{4}$ of $C$, for all elements $x_{5}$ of $C$, for all elements $x_{6}$ of $C$, for all homomorphisms $f$ of $x_{4}$ and $x_{5}$, for all homomorphisms $g$ of $x_{5}$ and $x_{6}$, $\mathrm{hom}$ applied to $x_{4}$, $x_{6}$ and the composition of $f$ and $g$ is equal to the composition of $\mathrm{hom}$ applied to $x_{4}$, $x_{5}$ and $f$ and the composition of the left whisker of the functor of the map of $F$ and $f$ and $\mathrm{hom}$ applied to $x_{5}$, $x_{6}$ and $g$ and $\operatorname{eqToHom}$ applied to $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Grothendieck\_\_0\_\_\_proof\_146}$ applied to $\mathrm{fib}$, $x_{4}$, $x_{5}$, $x_{6}$, $f$ and $g$. Let $c$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_Grothendieck\_\_\_u3b9\_CompFunctorFrom}$ applied to $c_{3}$, $\mathrm{fib}$, $c_{2}$, $\mathrm{c'}$, $f_{1}$, $\mathrm{hom}$, $\mathrm{hom\_id}$, $\mathrm{hom\_comp}$ and $c$ is an isomorphism of the composition of the inclusion of $F$ and $c$ and $\operatorname{functorFrom}$ applied to $\mathrm{fib}$, the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{hom}$ applied to $x_{2}$ and $x_{3}$, $\mathrm{hom\_id}$ and $\mathrm{hom\_comp}$ and $\mathrm{fib}$ applied to $c$.

the fiber inclusion of x1 and c (from the docstring)

Let $x_{1}$ be a homomorphism of $F$ and $\mathrm{F'}$. Let $c$ be an element of $C$. Then the fiber inclusion of $x_{1}$ and $c$ is an isomorphism of the composition of the inclusion of $F$ and $c$ and the map of $x_{1}$ and the composition of the functor of the component of $x_{1}$ and $c$ and the inclusion of $\mathrm{F'}$ and $c$.

the inclusion natural transformation of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the inclusion natural transformation of $f$ is a homomorphism of the inclusion of $F$ and $X$ and the composition of the functor of the map of $F$ and $f$ and the inclusion of $F$ and $Y$.

obj is a groupoid (from the name)

Let $\mathrm{obj}$ be a set. Then we can say that $\mathrm{obj}$ is a groupoid.

the inverse morphism of x (from the docstring)

Let $x$ be a homomorphism of $X$ and $Y$. Then the inverse morphism of $x$ is a homomorphism of $Y$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x$.

the inverse equivalence (from the name)

The inverse equivalence is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of $Y$ and $X$.

the inverse equivalence of C (from the name)

Let $C$ be a set. Then the inverse equivalence of $C$ is an equivalence of $C$ and the set of opposites of $C$.

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

Let $X$ and $Y$ be elements of $C$. Then the isomorphism equivalence homomorphism of $X$ and $Y$ is an equivalence from the set of isomorphisms of $X$ and $Y$ to the set of homomorphisms of $X$ and $Y$.

C is a groupoid (from the name)

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

large groupoid of C (from the name)

Let $C$ be a set. Then a large groupoid of $C$ is an element of the function that maps $C$ to the proposition that $C$ is a groupoid.

small groupoid of C (from the name)

Let $C$ be a set. Then a small groupoid of $C$ is an element of the function that maps $C$ to the proposition that $C$ is a groupoid.

C is totally disconnected (from the docstring)

free groupoid of V (from the name)

Let $V$ be a set. Then a free groupoid of $V$ is an element of the function that maps $V$ to the set of quotients of $\operatorname{redStep}$.

the lift of x2 (from the docstring)

Let $x_{2}$ be a prefunctor of $V$ and $\mathrm{V'}$. Then the lift of $x_{2}$ is a functor of the set of free groupoids of $V$ and $\mathrm{V'}$.

Let $V$ be a set. Then $\operatorname{of}$ applied to $V$ is a prefunctor of $V$ and the set of free groupoids of $V$ defined as $\operatorname{mk}$ applied to the function that maps $X$ to $\operatorname{mk}$ applied to $X$ and the function that maps $x_{1}$, $x_{2}$ and $f$ to $\operatorname{mk}$ applied to the composition closure of $\operatorname{redStep}$ and the positive part path of $f$.

the inverse of f (from the docstring)

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

There is a homomorphism relation of the set of paths of $\operatorname{Symmetrify}$ applied to $V$.

the negation path of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the negation path of $f$ is a homomorphism of $Y$ and $X$ defined as the path of the negation of $f$.

the positive part path of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the positive part path of $f$ is a homomorphism of $X$ and $Y$ defined as the path of the positive part of $f$.

the functor of free groupoid induced by a prefunctor of quivers of x2 (from the docstring)

Let $x_{2}$ be a prefunctor of $V$ and $\mathrm{V'}$. Then the functor of free groupoid induced by a prefunctor of quivers of $x_{2}$ is a functor of the set of free groupoids of $V$ and the set of free groupoids of $\mathrm{V'}$ defined as the lift of the composition of $x_{2}$ and $\operatorname{of}$ applied to $\mathrm{V'}$.

free groupoid of C (from the name)

Let $C$ be a set. Then a free groupoid of $C$ is an element of the function that maps $C$ to the set of quotients of the homomorphism relation of $C$.

the functor equivalence (from the name)

The functor equivalence is an equivalence from the set of functors of the set of free groupoids of $C$ and $D$ to the set of functors of $C$ and $D$.

the homomorphism of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a homomorphism of $\operatorname{mk}$ applied to $X$ and $\operatorname{mk}$ applied to $Y$ defined as the map of $\operatorname{of}$ applied to $C$ and $f$.

the homomorphism relation of C (from the name)

Let $C$ be a set. Then the homomorphism relation of $C$ is a homomorphism relation of the set of free groupoids of $C$.

the lift of x2 (from the docstring)

Let $x_{2}$ be a functor of $C$ and $G$. Then the lift of $x_{2}$ is a functor of the set of free groupoids of $C$ and $G$.

the lift natural isomorphism of x3 and x4 (from the name)

Let $x_{2}$ and $x_{3}$ be functors of the set of free groupoids of $C$ and $G$. Let $x_{4}$ be an isomorphism of the composition of $\operatorname{of}$ applied to $C$ and $x_{2}$ and the composition of $\operatorname{of}$ applied to $C$ and $x_{3}$. Then the lift natural isomorphism of $x_{3}$ and $x_{4}$ is an isomorphism of $x_{2}$ and $x_{3}$ defined as the lift natural isomorphism of $x_{3}$ and $x_{4}$.

the map of x2 (from the name)

Let $x_{2}$ be a functor of $C$ and $D$. Then the map of $x_{2}$ is a functor of the set of free groupoids of $C$ and the set of free groupoids of $D$ defined as the lift of the composition of $x_{2}$ and $\operatorname{of}$ applied to $D$.

the functor induced by a composition of x3 and x4 (from the docstring)

Let $x_{3}$ be a functor of $C$ and $D$. Let $x_{4}$ be a functor of $D$ and $E$. Then the functor induced by a composition of $x_{3}$ and $x_{4}$ is an isomorphism of the map of the composition of $x_{3}$ and $x_{4}$ and the composition of the map of $x_{3}$ and the map of $x_{4}$ defined as the lift natural isomorphism of the composition of the map of $x_{3}$ and the map of $x_{4}$ and the identity of the composition of $\operatorname{of}$ applied to $C$ and the map of the composition of $x_{3}$ and $x_{4}$.

the map composition lift of F and G (from the name)

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the map composition lift of $F$ and $G$ is an isomorphism of the composition of the map of $F$ and the lift of $G$ and the lift of the composition of $F$ and $G$ defined as the lift natural isomorphism of the lift of the composition of $F$ and $G$ and the identity of the composition of $\operatorname{of}$ applied to $C$ and the composition of the map of $F$ and the lift of $G$.

the functor induced by the identity of C (from the docstring)

Let $C$ be a set. Then the functor induced by the identity of $C$ is an isomorphism of the map of the identity of $C$ and the identity of the set of free groupoids of $C$ defined as the lift natural isomorphism of the identity of the set of free groupoids of $C$ and the identity of the composition of $\operatorname{of}$ applied to $C$ and the map of the identity of $C$.

Let $X$ be an element of $C$. Then $\operatorname{mk}$ applied to $X$ is a free groupoid of $C$ defined as the action of $\operatorname{of}$ applied to $C$ and $X$.

Let $C$ be a set. Then $\operatorname{of}$ applied to $C$ is a functor of $C$ and the set of free groupoids of $C$.

the free groupoid of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the free groupoid of $F$ is an isomorphism of the composition of $\operatorname{of}$ applied to $C$ and the map of $F$ and the composition of $F$ and $\operatorname{of}$ applied to $D$ defined as the identity of the composition of $\operatorname{of}$ applied to $C$ and the map of $F$.

the universal property of the free groupoid (from the docstring)

The universal property of the free groupoid is a strict universal property fixed target of the top and $G$.

the free groupoid construction (from the docstring)

The free groupoid construction is a functor of the set of categories and $\operatorname{Grpd}$.

$\operatorname{freeForgetAdjunction}$ is an adjunction of the free groupoid construction and $\operatorname{forgetToCat}$.

An element of $\operatorname{Grpd}$ is an element of $\operatorname{Bundled}$ applied to the proposition that $\operatorname{Groupoid}$.

$\operatorname{forgetToCat}$ is a functor of $\operatorname{Grpd}$ and the set of categories.

the object (from the name)

The object is a functor of $\operatorname{Grpd}$ and the set of sets.

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

the product of J and f (from the docstring)

Let $J$ be a set. Let $f$ be a function from elements of $J$ to elements of $\operatorname{Grpd}$. Then the product of $J$ and $f$ is an isomorphism of $\operatorname{of}$ applied to the set of functions from elements $j$ of $J$ to elements of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $f$ applied to $j$ and the product object of $f$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{piLimitFanIsLimit}$ applied to $f$ and $\operatorname{isLimit}$ applied to the functor of $f$.

Let $F$ be a function from elements of $J$ to elements of $\operatorname{Grpd}$. Then $\operatorname{piLimitFan}$ applied to $F$ is an element of $\operatorname{Fan}$ applied to $F$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to the set of functions from elements $j$ of $J$ to elements of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $F$ applied to $j$ and the function that maps $j_{1}$ to the evaluation of the function that maps $j_{2}$ to $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $F$ applied to $j_{2}$ and $j_{1}$.

Let $F$ be a function from elements of $J$ to elements of $\operatorname{Grpd}$. Then $\operatorname{piLimitFanIsLimit}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{piLimitFan}$ applied to $F$.

Let $C$ be a set. Then the elements of $\operatorname{Subgroupoid}$ applied to $C$ are a basic type.

Let $c$ and $d$ be elements of $C$. Let $x_{1}$ be a homomorphism of $c$ and $d$. Then we can say that $\operatorname{Arrows}$ holds for $c$, $d$ and $x_{1}$.

S is normal (from the docstring)

Let $S$ be an element of $\operatorname{Subgroupoid}$ applied to $C$. Then we can say that $S$ is normal.

S is thin (from the name)

Let $S$ be an element of $\operatorname{Subgroupoid}$ applied to $C$. Then $S$ is thin, if the set of elements of $\operatorname{objs}$ applied to $S$ is thin.

S is totally disconnected (from the name)

S is wide (from the docstring)

Let $S$ be an element of $\operatorname{Subgroupoid}$ applied to $C$. Then we can say that $S$ is wide.

Let $x_{2}$ be a functor of $C$ and $D$ such that $\operatorname{obj}$ applied to $x_{2}$ is injective. Let $S$ be an element of $\operatorname{Subgroupoid}$ applied to $C$. Let $c$ and $d$ be elements of $D$. Let $x_{3}$ be a homomorphism of $c$ and $d$. Then we can say that $\operatorname{Arrows}$ holds for $x_{2}$, $h$, $S$, $c$, $d$ and $x_{3}$.

the arrow of c and d (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{Subgroupoid}$ applied to $C$. Let $c$ and $d$ be elements of $C$. Then the arrow of $c$ and $d$ is an element of the power set of the set of homomorphisms of $c$ and $d$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $c$ and $d$.

the preimage of x2 and S (from the name)

Let $x_{2}$ be a functor of $C$ and $D$. Let $S$ be an element of $\operatorname{Subgroupoid}$ applied to $D$. Then the preimage of $x_{2}$ and $S$ is an element of $\operatorname{Subgroupoid}$ applied to $C$.

Let $S$ be an element of $\operatorname{Subgroupoid}$ applied to $C$. Then $\operatorname{disconnect}$ applied to $S$ is an element of $\operatorname{Subgroupoid}$ applied to $C$.

$\operatorname{discrete}$ is an element of $\operatorname{Subgroupoid}$ applied to $C$.

Let $D$ be an element of $\wp C$. Then $\operatorname{full}$ applied to $D$ is an element of $\operatorname{Subgroupoid}$ applied to $C$.

Let $X$ be a function from elements $c$ of $C$ and elements $d$ of $C$ to elements of the power set of the set of homomorphisms of $c$ and $d$. Then $\operatorname{generated}$ applied to $c$, $d$ and $X$ is an element of $\operatorname{Subgroupoid}$ applied to $C$ defined as the function that maps $d$ and $X$ to the infimum of $\operatorname{ofPred}$ applied to the function that maps $S$ to the proposition that for all elements $c$ and $d$ of $C$, $c$ applied to $c$ and $d$ is less than or equal to the arrow of $c$ and $d$.

Let $X$ be a function from elements $c$ of $C$ and elements $d$ of $C$ to elements of the power set of the set of homomorphisms of $c$ and $d$. Then $\operatorname{generatedNormal}$ applied to $c$, $d$ and $X$ is an element of $\operatorname{Subgroupoid}$ applied to $C$ defined as the function that maps $d$ and $X$ to the infimum of $\operatorname{ofPred}$ applied to the function that maps $S$ to the proposition that for all elements $c$ of $C$, for all elements $d$ of $C$, $c$ applied to $c$ and $d$ is less than or equal to the arrow of $c$ and $d$ and $S$ is normal.

the homomorphism of S (from the name)

Let $S$ be an element of $\operatorname{Subgroupoid}$ applied to $C$. Then the homomorphism of $S$ is a functor of the set of elements of $\operatorname{objs}$ applied to $S$ and $C$.

the image of x2 and h (from the docstring)

Let $x_{2}$ be a functor of $C$ and $D$ such that $\operatorname{obj}$ applied to $x_{2}$ is injective. Then the image of $x_{2}$ and $h$ is an element of $\operatorname{Subgroupoid}$ applied to $D$ defined as the map of $x_{2}$ and the top.

the inclusion of h (from the name)

Assume that $S \leq T$. Then the inclusion of $h$ is a functor of the set of elements of $\operatorname{objs}$ applied to $S$ and the set of elements of $\operatorname{objs}$ applied to $T$.

the kernel of x2 (from the docstring)

Let $x_{2}$ be a functor of $C$ and $D$. Then the kernel of $x_{2}$ is an element of $\operatorname{Subgroupoid}$ applied to $C$ defined as the preimage of $x_{2}$ and $\operatorname{discrete}$.

the map of x2 and S (from the name)

Let $x_{2}$ be a functor of $C$ and $D$ such that $\operatorname{obj}$ applied to $x_{2}$ is injective. Let $S$ be an element of $\operatorname{Subgroupoid}$ applied to $C$. Then the map of $x_{2}$ and $S$ is an element of $\operatorname{Subgroupoid}$ applied to $D$.

Let $S$ be an element of $\operatorname{Subgroupoid}$ applied to $C$. Then $\operatorname{objs}$ applied to $S$ is an element of $\wp C$ defined as $\operatorname{ofPred}$ applied to the function that maps $c$ to the proposition that the arrow of $c$ and $c$ is nonempty.

the set of all arrows of S (from the docstring)

Let $S$ be an element of $\operatorname{Subgroupoid}$ applied to $C$. Then the set of all arrows of $S$ is an element of the power set of $\Sigma$ applied to the function that maps $c$ to $\Sigma$ applied to the function that maps $d$ to the set of homomorphisms of $c$ and $d$ defined as $\operatorname{ofPred}$ applied to the function that maps $F$ to the proposition that $\operatorname{snd}$ applied to $\operatorname{snd}$ applied to $F$ is an element of the arrow of $\operatorname{fst}$ applied to $F$ and $\operatorname{fst}$ applied to $\operatorname{snd}$ applied to $F$.

the vertex subgroup of S and hc (from the name)

Let $S$ be an element of $\operatorname{Subgroupoid}$ applied to $C$ such that $\MembershipmemMACRoT {\operatorname{objs} (S)}{c}$. Then the vertex subgroup of $S$ and $\mathrm{hc}$ is a subgroup of the set of homomorphisms of $c$ and $c$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the arrow of $c$ and $c$ and the function that maps $x_{1}$, $x_{2}$, $\mathrm{hf}$ and $\mathrm{hg}$ to $\operatorname{mul}$ applied to $S$, $\mathrm{hf}$ and $\mathrm{hg}$ and $\mathrm{CategoryTheory\_\_Subgroupoid\_\_id\_mem\_of\_nonempty\_isotropy}$ applied to $S$, $c$ and $\mathrm{hc}$ and the function that maps $x_{3}$ and $\mathrm{hf1}$ to $\operatorname{inv}$ applied to $S$ and $\mathrm{hf1}$.

the map vertex group of x2 and c (from the name)

Let $x_{2}$ be a functor of $C$ and $D$. Let $c$ be an element of $C$. Then the map vertex group of $x_{2}$ and $c$ is a monoid homomorphism of the set of homomorphisms of $c$ and $c$ and the set of homomorphisms of the action of $x_{2}$ and $c$ and the action of $x_{2}$ and $c$.

Let $f$ be a homomorphism of $c$ and $d$. Then $\operatorname{vertexGroupIsomOfMap}$ applied to $f$ is a multiplicative equivalence of the set of homomorphisms of $c$ and $c$ and the set of homomorphisms of $d$ and $d$.

Let $p$ be a path of $c$ and $d$. Then $\operatorname{vertexGroupIsomOfPath}$ applied to $p$ is a multiplicative equivalence of the set of homomorphisms of $c$ and $c$ and the set of homomorphisms of $d$ and $d$ defined as $\operatorname{vertexGroupIsomOfMap}$ applied to $\operatorname{composePath}$ applied to $p$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $g$ be a homomorphism of the action of $R$ and $x_{8}$ and the action of $B$ and $x_{9}$. Then an element of $\operatorname{CostructuredArrowDownwards}$ applied to $w$ and $g$ is an element of the function that maps $w$ and $g$ to the set of costructured arrows of $\operatorname{structuredArrowDownwards}$ applied to $w$ and $x_{8}$ and $\operatorname{mk}$ applied to $g$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $g$ be a homomorphism of the action of $R$ and $x_{8}$ and the action of $B$ and $x_{9}$. Let $x_{10}$ be an element of $x$. Let $a$ be a homomorphism of $x_{8}$ and the action of $T$ and $x_{10}$. Let $b$ be a homomorphism of the action of $L$ and $x_{10}$ and $x_{9}$ such that the composition of the map of $R$ and $a$ and the composition of the component of $w$ and $x_{10}$ and the map of $B$ and $b$ is equal to $g$. Then $\operatorname{mk}$ applied to $w$, $g$, $x_{10}$, $a$, $b$ and $\mathrm{comm}$ is an element of $\operatorname{CostructuredArrowDownwards}$ applied to $w$ and $g$.

the functor of w and g (from the name)

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $g$ be a homomorphism of the action of $R$ and $x_{8}$ and the action of $B$ and $x_{9}$. Then the functor of $w$ and $g$ is a functor of $\operatorname{StructuredArrowRightwards}$ applied to $w$ and $g$ and $\operatorname{CostructuredArrowDownwards}$ applied to $w$ and $g$.

the inverse of w and g (from the name)

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $g$ be a homomorphism of the action of $R$ and $x_{8}$ and the action of $B$ and $x_{9}$. Then the inverse of $w$ and $g$ is a functor of $\operatorname{CostructuredArrowDownwards}$ applied to $w$ and $g$ and $\operatorname{StructuredArrowRightwards}$ applied to $w$ and $g$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Then we can say that $\operatorname{GuitartExact}$ holds for $w$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $g$ be a homomorphism of the action of $R$ and $x_{8}$ and the action of $B$ and $x_{9}$. Then an element of $\operatorname{StructuredArrowRightwards}$ applied to $w$ and $g$ is an element of the function that maps $w$ and $g$ to the set of structured arrows of $\operatorname{mk}$ applied to $g$ and $\operatorname{costructuredArrowRightwards}$ applied to $w$ and $x_{9}$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $g$ be a homomorphism of the action of $R$ and $x_{8}$ and the action of $B$ and $x_{9}$. Let $x_{10}$ be an element of $x$. Let $a$ be a homomorphism of $x_{8}$ and the action of $T$ and $x_{10}$. Let $b$ be a homomorphism of the action of $L$ and $x_{10}$ and $x_{9}$ such that the composition of the map of $R$ and $a$ and the composition of the component of $w$ and $x_{10}$ and the map of $B$ and $b$ is equal to $g$. Then $\operatorname{mk}$ applied to $w$, $g$, $x_{10}$, $a$, $b$ and $\mathrm{comm}$ is an element of $\operatorname{StructuredArrowRightwards}$ applied to $w$ and $g$ defined as $\operatorname{mk}$ applied to the homomorphism of $a$ and $\mathrm{comm}$.

the costructured arrow downward precomposition of x11 and h (from the name)

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $g$ be a homomorphism of the action of $R$ and $x_{8}$ and the action of $B$ and $x_{10}$. Let $\mathrm{g'}$ be a homomorphism of the action of $R$ and $x_{9}$ and the action of $B$ and $x_{10}$. Let $x_{11}$ be a homomorphism of $x_{9}$ and $x_{8}$ such that the composition of the map of $R$ and $x_{11}$ and $g$ is equal to $\mathrm{g'}$. Then the costructured arrow downward precomposition of $\mathrm{g'}$ and $x_{11}$ is a functor of $\operatorname{CostructuredArrowDownwards}$ applied to $w$ and $g$ and $\operatorname{CostructuredArrowDownwards}$ applied to $w$ and $\mathrm{g'}$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $x_{8}$ be an element of $x_{2}$. Then $\operatorname{costructuredArrowRightwards}$ applied to $w$ and $x_{8}$ is a functor of the set of costructured arrows of $L$ and $x_{8}$ and the set of costructured arrows of $R$ and the action of $B$ and $x_{8}$ defined as the composition of the post of $B$ and $x_{8}$ and the composition of the left map of $\operatorname{fromPUnit}$ applied to the action of $B$ and $x_{8}$ and $w$ and $\operatorname{pre}$ applied to $T$, $R$ and the action of $B$ and $x_{8}$.

the equivalence of w and g (from the name)

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $g$ be a homomorphism of the action of $R$ and $x_{8}$ and the action of $B$ and $x_{9}$. Then the equivalence of $w$ and $g$ is an equivalence of $\operatorname{StructuredArrowRightwards}$ applied to $w$ and $g$ and $\operatorname{CostructuredArrowDownwards}$ applied to $w$ and $g$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $x_{8}$ be an element of $x_{1}$. Then $\operatorname{structuredArrowDownwards}$ applied to $w$ and $x_{8}$ is a functor of the set of structured arrows of $x_{8}$ and $T$ and the set of structured arrows of the action of $R$ and $x_{8}$ and $B$ defined as the composition of the post of $T$ and $R$ and the composition of the right map of $\operatorname{fromPUnit}$ applied to the action of $R$ and $x_{8}$ and $w$ and $\operatorname{pre}$ applied to the action of $R$ and $x_{8}$, $L$ and $B$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $x_{13}$, $x_{12}$, $x_{15}$ and $x_{14}$. Let $\mathrm{w'}$ be an element of $\operatorname{TwoSquare}$ applied to $x_{16}$, $x_{15}$, $x_{18}$ and $x_{17}$. Let $x_{19}$ be an element of $x_{3}$. Then $\operatorname{costructuredArrowRightwardsComp}$ applied to $w$, $\mathrm{w'}$ and $x_{19}$ is an isomorphism of the composition of $\operatorname{costructuredArrowRightwards}$ applied to $w$ and $x_{19}$ and $\operatorname{costructuredArrowRightwards}$ applied to $\mathrm{w'}$ and the action of $x_{14}$ and $x_{19}$ and $\operatorname{costructuredArrowRightwards}$ applied to the composition of $w$ and $\mathrm{w'}$ and $x_{19}$.

the composition of eB and #4 (from the name)

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $x_{13}$, $x_{12}$, $x_{15}$ and $x_{14}$. Let $\mathrm{w'}$ be an element of $\operatorname{TwoSquare}$ applied to $x_{16}$, $x_{15}$, $x_{18}$ and $x_{17}$. Let $\mathrm{eT}$ be an isomorphism of the composition of $x_{13}$ and $x_{16}$ and $x_{19}$. Let $\mathrm{eB}$ be an isomorphism of the composition of $x_{14}$ and $x_{17}$ and $x_{20}$. Then the composition of $\mathrm{eT}$ and $\mathrm{eB}$ is an element of $\operatorname{TwoSquare}$ applied to $x_{19}$, $x_{12}$, $x_{18}$ and $x_{20}$ defined as $\operatorname{whiskerHorizontal}$ applied to the composition of $w$ and $\mathrm{w'}$, the inverse of $\mathrm{eT}$ and the homomorphism of $\mathrm{eB}$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $x_{8}$ be a homomorphism of $\mathrm{T'}$ and $T$. Let $x_{9}$ be a homomorphism of $B$ and $\mathrm{B'}$. Then $\operatorname{whiskerHorizontal}$ applied to $w$, $x_{8}$ and $x_{9}$ is an element of $\operatorname{TwoSquare}$ applied to $\mathrm{T'}$, $L$, $R$ and $\mathrm{B'}$ defined as the whisker bottom of the whisker top of $w$ and $x_{8}$ and $x_{9}$.

Let $h$ be an element of $\operatorname{IsPointwiseLeftKanExtension}$ applied to $E$. Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $\operatorname{compTwoSquare}$ applied to $E$ and $w$. Proof. Let $h$ be arbitrary. Let $w$ be arbitrary. Let $x_{9}$ be arbitrary. By E. By w. By x9. By CategoryTheory__Functor__LeftExtension__isPointwiseLeftKanExtensionAtCompTwoSquareEquiv. By B. By x9. By CategoryTheory__Functor__obj. By h. By Equiv__symm__app.

Let $E$ be a left extension of $R$ and $F$. Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Then $\operatorname{compTwoSquare}$ applied to $E$ and $w$ is a left extension of $L$ and the composition of $T$ and $F$ defined as $\operatorname{mk}$ applied to the composition of $B$ and the right object of $E$ and the composition of the left whisker of $T$ and the homomorphism of $E$ and the composition of the inverse of the associator of $R$ and the right object of $E$ and the composition of the right whisker of $w$ and the right object of $E$ and the homomorphism of the associator of $B$ and the right object of $E$.

Let $E$ be a left extension of $R$ and $F$. Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $x_{9}$ be an element of $x_{2}$. Then $\operatorname{isPointwiseLeftKanExtensionAtCompTwoSquareEquiv}$ applied to $E$, $w$ and $x_{9}$ is an equivalence from $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $\operatorname{compTwoSquare}$ applied to $E$ and $w$ and $x_{9}$ to $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $E$ and the action of $B$ and $x_{9}$.

Let $E$ be a left extension of $R$ and $F$. Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Then $\operatorname{isPointwiseLeftKanExtensionEquivOfGuitartExact}$ applied to $E$ and $w$ is an element of $\EquivMACRoAE {\operatorname{IsPointwiseLeftKanExtension} (\operatorname{compTwoSquare} (E , w))}{\operatorname{IsPointwiseLeftKanExtension} (E)}$.

Let $E$ be a left extension of $R$ and $F$. Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $h_{2}$ be an element of $\operatorname{IsPointwiseLeftKanExtension}$ applied to $\operatorname{compTwoSquare}$ applied to $E$ and $w$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $E$. Proof. Let $E$ be arbitrary. Let $w$ be arbitrary. Let $h_{2}$ be arbitrary. Let $x_{9}$ be arbitrary. By E. By E. By w. By B. By x9. By CategoryTheory__Functor__objPreimage. By B. By x9. By CategoryTheory__Functor__objPreimage. By h2. By CategoryTheory__Functor__LeftExtension__isPointwiseLeftKanExtensionAtCompTwoSquareEquiv__app. By B. By x9. By CategoryTheory__Functor__objObjPreimageIso. By CategoryTheory__Functor__LeftExtension__isPointwiseLeftKanExtensionAtOfIso'.

Let $h$ be an element of $\operatorname{IsPointwiseRightKanExtension}$ applied to $E$. Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Then $\operatorname{IsPointwiseRightKanExtension}$ holds for $\operatorname{compTwoSquare}$ applied to $E$ and $w$. Proof. Let $h$ be arbitrary. Let $w$ be arbitrary. Let $x_{9}$ be arbitrary. By E. By w. By x9. By CategoryTheory__Functor__RightExtension__isPointwiseRightKanExtensionAtCompTwoSquareEquiv. By R. By x9. By CategoryTheory__Functor__obj. By h. By Equiv__symm__app.

Let $E$ be a right extension of $B$ and $F$. Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Then $\operatorname{compTwoSquare}$ applied to $E$ and $w$ is a right extension of $T$ and the composition of $L$ and $F$ defined as $\operatorname{mk}$ applied to the composition of $R$ and the left object of $E$ and the composition of the inverse of the associator of $R$ and the left object of $E$ and the composition of the right whisker of $w$ and the left object of $E$ and the composition of the homomorphism of the associator of $B$ and the left object of $E$ and the left whisker of $L$ and the homomorphism of $E$.

Let $E$ be a right extension of $B$ and $F$. Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $x_{9}$ be an element of $x_{1}$. Then $\operatorname{isPointwiseRightKanExtensionAtCompTwoSquareEquiv}$ applied to $E$, $w$ and $x_{9}$ is an equivalence from $\operatorname{IsPointwiseRightKanExtensionAt}$ applied to $\operatorname{compTwoSquare}$ applied to $E$ and $w$ and $x_{9}$ to $\operatorname{IsPointwiseRightKanExtensionAt}$ applied to $E$ and the action of $R$ and $x_{9}$.

Let $E$ be a right extension of $B$ and $F$. Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Then $\operatorname{isPointwiseRightKanExtensionEquivOfGuitartExact}$ applied to $E$ and $w$ is an element of $\EquivMACRoAE {\operatorname{IsPointwiseRightKanExtension} (\operatorname{compTwoSquare} (E , w))}{\operatorname{IsPointwiseRightKanExtension} (E)}$.

Let $E$ be a right extension of $B$ and $F$. Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $h_{2}$ be an element of $\operatorname{IsPointwiseRightKanExtension}$ applied to $\operatorname{compTwoSquare}$ applied to $E$ and $w$. Then $\operatorname{IsPointwiseRightKanExtension}$ holds for $E$. Proof. Let $E$ be arbitrary. Let $w$ be arbitrary. Let $h_{2}$ be arbitrary. Let $x_{9}$ be arbitrary. By E. By E. By w. By R. By x9. By CategoryTheory__Functor__objPreimage. By R. By x9. By CategoryTheory__Functor__objPreimage. By h2. By CategoryTheory__Functor__RightExtension__isPointwiseRightKanExtensionAtCompTwoSquareEquiv__app. By R. By x9. By CategoryTheory__Functor__objObjPreimageIso. By CategoryTheory__Functor__RightExtension__isPointwiseRightKanExtensionAtOfIso'.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Then $\operatorname{lanBaseChange}$ applied to $w$ is a homomorphism of the composition of the action of the left whiskering of $x_{1}$ and $D$ and $T$ and $\operatorname{lan}$ applied to $L$ and the composition of $\operatorname{lan}$ applied to $R$ and the action of the left whiskering of $x_{3}$ and $D$ and $B$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Then $\operatorname{ranBaseChange}$ applied to $w$ is a homomorphism of the composition of $\operatorname{ran}$ applied to $B$ and the action of the left whiskering of $x_{3}$ and $D$ and $R$ and the composition of the action of the left whiskering of $x_{2}$ and $D$ and $L$ and $\operatorname{ran}$ applied to $T$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $g$ be a homomorphism of the action of the opposite of $B$ and $x_{8}$ and the action of the opposite of $R$ and $x_{9}$. Then $\operatorname{structuredArrowRightwardsOpEquivalence}$ applied to $w$ and $g$ is an equivalence of the set of opposites of $\operatorname{StructuredArrowRightwards}$ applied to the opposite of $w$ and $g$ and $\operatorname{CostructuredArrowDownwards}$ applied to $w$ and the opposite of $g$.

Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then $\operatorname{overPost}$ applied to $F$ and $X$ is an element of $\operatorname{TwoSquare}$ applied to the post of $F$, $\operatorname{forget}$ applied to $X$, $\operatorname{forget}$ applied to the action of $F$ and $X$ and $F$ defined as $\operatorname{mk}$ applied to the post of $F$, $\operatorname{forget}$ applied to $X$, $\operatorname{forget}$ applied to the action of $F$ and $X$, $F$ and the identity morphism of the composition of the post of $F$ and $\operatorname{forget}$ applied to the action of $F$ and $X$.

the product equivalence of g and #3 (from the name)

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $\mathrm{w'}$ be an element of $\operatorname{TwoSquare}$ applied to $\mathrm{T'}$, $\mathrm{L'}$, $\mathrm{R'}$ and $\mathrm{B'}$. Let $g$ be a homomorphism of the action of the product of $R$ and $\mathrm{R'}$ and $x_{16}$ and the action of the product of $B$ and $\mathrm{B'}$ and $x_{17}$. Then the product equivalence of $\mathrm{w'}$ and $g$ is an equivalence of $\operatorname{StructuredArrowRightwards}$ applied to the external product of two of $w$ and $\mathrm{w'}$ and $g$ and $\mathrm{Prod}$ applied to $\operatorname{StructuredArrowRightwards}$ applied to $w$ and $\ProdfstMACRoZ {g}$ and $\operatorname{StructuredArrowRightwards}$ applied to $\mathrm{w'}$ and $\ProdsndMACRoAA {g}$.

the structured arrow downward composition of x19 and #3 (from the name)

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $x_{12}$, $x_{13}$, $x_{14}$ and $x_{15}$. Let $\mathrm{w'}$ be an element of $\operatorname{TwoSquare}$ applied to $x_{15}$, $x_{16}$, $x_{17}$ and $x_{18}$. Let $x_{19}$ be an element of $x_{3}$. Then the structured arrow downward composition of $\mathrm{w'}$ and $x_{19}$ is an isomorphism of the composition of $\operatorname{structuredArrowDownwards}$ applied to $w$ and $x_{19}$ and $\operatorname{structuredArrowDownwards}$ applied to $\mathrm{w'}$ and the action of $x_{14}$ and $x_{19}$ and $\operatorname{structuredArrowDownwards}$ applied to the composition of $w$ and $\mathrm{w'}$ and $x_{19}$.

the composition of eR and #4 (from the name)

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $x_{12}$, $x_{13}$, $x_{14}$ and $x_{15}$. Let $\mathrm{w'}$ be an element of $\operatorname{TwoSquare}$ applied to $x_{15}$, $x_{16}$, $x_{17}$ and $x_{18}$. Let $\mathrm{eL}$ be an isomorphism of the composition of $x_{13}$ and $x_{16}$ and $x_{19}$. Let $\mathrm{eR}$ be an isomorphism of the composition of $x_{14}$ and $x_{17}$ and $x_{20}$. Then the composition of $\mathrm{eL}$ and $\mathrm{eR}$ is an element of $\operatorname{TwoSquare}$ applied to $x_{12}$, $x_{19}$, $x_{20}$ and $x_{18}$ defined as $\operatorname{whiskerVertical}$ applied to the composition of $w$ and $\mathrm{w'}$, the homomorphism of $\mathrm{eL}$ and the inverse of $\mathrm{eR}$.

Let $w$ be an element of $\operatorname{TwoSquare}$ applied to $T$, $L$, $R$ and $B$. Let $x_{8}$ be a homomorphism of $L$ and $\mathrm{L'}$. Let $x_{9}$ be a homomorphism of $\mathrm{R'}$ and $R$. Then $\operatorname{whiskerVertical}$ applied to $w$, $x_{8}$ and $x_{9}$ is an element of $\operatorname{TwoSquare}$ applied to $T$, $\mathrm{L'}$, $\mathrm{R'}$ and $B$ defined as the right whisker of the left whisker of $w$ and $x_{8}$ and $x_{9}$.

the homomorphism congruence of x3 and x4 (from the name)

Let $x_{3}$ be an isomorphism of $X$ and $x_{1}$. Let $x_{4}$ be an isomorphism of $Y$ and $x_{2}$. Then the homomorphism congruence of $x_{3}$ and $x_{4}$ is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of $x_{1}$ and $x_{2}$.

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

Let $f$ be an isomorphism of $x_{1}$ and $x_{3}$. Let $g$ be an isomorphism of $x_{2}$ and $x_{4}$. Then the isomorphism congruence of $f$ and $g$ is an equivalence from the set of isomorphisms of $x_{1}$ and $x_{2}$ to the set of isomorphisms of $x_{3}$ and $x_{4}$.

the left isomorphism congruence of f (from the name)

Let $f$ be an isomorphism of $x_{1}$ and $x_{2}$. Then the left isomorphism congruence of $f$ is an equivalence from the set of isomorphisms of $x_{1}$ and $Y$ to the set of isomorphisms of $x_{2}$ and $Y$ defined as the isomorphism congruence of $f$ and the identity of $Y$.

the right isomorphism congruence of g (from the name)

Let $g$ be an isomorphism of $x_{1}$ and $x_{2}$. Then the right isomorphism congruence of $g$ is an equivalence from the set of isomorphisms of $X$ and $x_{1}$ to the set of isomorphisms of $X$ and $x_{2}$ defined as the isomorphism congruence of the identity of $X$ and $g$.

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

the bicone of F (from the name)

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

the complement of P (from the name)

Let $P$ be an element of $\operatorname{Karoubi}$ applied to $C$. Then the complement of $P$ is an element of $\operatorname{Karoubi}$ applied to $C$.

the decomposition of P (from the name)

Let $P$ be an element of $\operatorname{Karoubi}$ applied to $C$. Then the decomposition of $P$ is an isomorphism of the biproduct of $P$ and the complement of $P$ and the action of $\operatorname{toKaroubi}$ applied to $C$ and $\operatorname{X}$ applied to $P$.

the map of f (from the name)

Let $f$ be a homomorphism of $P$ and $Q$. Then the map of $f$ is a homomorphism of the object of $P$ and the object of $Q$.

the object of P (from the name)

Let $P$ be an element of $\operatorname{Karoubi}$ applied to the set of functors of $J$ and $C$. Then the object of $P$ is a functor of $J$ and $\operatorname{Karoubi}$ applied to $C$.

the tautological fully faithful functor of J and C (from the docstring)

the map of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the map of $x_{2}$ is a homomorphism of the object of $F$ and the object of $G$.

the object of F (from the name)

Let $F$ be a functor of $C$ and $\operatorname{Karoubi}$ applied to $D$. Then the object of $F$ is a functor of $\operatorname{Karoubi}$ applied to $C$ and $\operatorname{Karoubi}$ applied to $D$.

the counit isomorphism of the equivalence of C and D (from the docstring)

Let $C$ and $D$ be sets. Then the counit isomorphism of the equivalence of $C$ and $D$ is an isomorphism of the composition of the action of the left whiskering of $\operatorname{Karoubi}$ applied to $C$ and $\operatorname{Karoubi}$ applied to $D$ and $\operatorname{toKaroubi}$ applied to $C$ and the canonical functor of $C$ and $D$ and the identity of the set of functors of $\operatorname{Karoubi}$ applied to $C$ and $\operatorname{Karoubi}$ applied to $D$.

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

Let $C$ and $D$ be sets. Then the functor extension of $C$ and $D$ is a functor of the set of functors of $C$ and $D$ and the set of functors of $\operatorname{Karoubi}$ applied to $C$ and $D$ defined as the composition of the canonical functor of $C$ and $D$ and the action of the right whiskering of $\operatorname{Karoubi}$ applied to $D$ and $D$ and the inverse of the equivalence of $D$.

the canonical functor of C and D (from the docstring)

Let $C$ and $D$ be sets. Then the canonical functor of $C$ and $D$ is a functor of the set of functors of $C$ and $\operatorname{Karoubi}$ applied to $D$ and the set of functors of $\operatorname{Karoubi}$ applied to $C$ and $\operatorname{Karoubi}$ applied to $D$.

the functor extension composition of F and G (from the name)

Let $C$, $D$ and $E$ be sets. Let $F$ be a functor of $C$ and $\operatorname{Karoubi}$ applied to $D$. Let $G$ be a functor of $D$ and $\operatorname{Karoubi}$ applied to $E$. Then the functor extension composition of $F$ and $G$ is an isomorphism of the action of the canonical functor of $C$ and $E$ and the composition of $F$ and the action of the canonical functor of $D$ and $E$ and $G$ and the composition of the action of the canonical functor of $C$ and $D$ and $F$ and the action of the canonical functor of $D$ and $E$ and $G$ defined as the identity of the action of the canonical functor of $C$ and $E$ and the composition of $F$ and the action of the canonical functor of $D$ and $E$ and $G$.

Let $C$ and $D$ be sets. Then $\mathrm{CategoryTheory\_\_Idempotents\_\_functorExtension\_u2081\_CompWhiskeringLeftToKaroubiIso}$ applied to $C$ and $D$ is an isomorphism of the composition of the canonical functor of $C$ and $D$ and the action of the left whiskering of $\operatorname{Karoubi}$ applied to $C$ and $\operatorname{Karoubi}$ applied to $D$ and $\operatorname{toKaroubi}$ applied to $C$ and the identity of the set of functors of $C$ and $\operatorname{Karoubi}$ applied to $D$.

the canonical functor of C and D (from the docstring)

Let $C$ and $D$ be sets. Then the canonical functor of $C$ and $D$ is a functor of the set of functors of $C$ and $D$ and the set of functors of $\operatorname{Karoubi}$ applied to $C$ and $\operatorname{Karoubi}$ applied to $D$ defined as the composition of the action of the right whiskering of $D$ and $\operatorname{Karoubi}$ applied to $D$ and $\operatorname{toKaroubi}$ applied to $D$ and the canonical functor of $C$ and $D$.

Let $C$ and $D$ be sets. Then $\mathrm{CategoryTheory\_\_Idempotents\_\_functorExtension\_u2082\_CompWhiskeringLeftToKaroubiIso}$ applied to $C$ and $D$ is an isomorphism of the composition of the canonical functor of $C$ and $D$ and the action of the left whiskering of $\operatorname{Karoubi}$ applied to $C$ and $\operatorname{Karoubi}$ applied to $D$ and $\operatorname{toKaroubi}$ applied to $C$ and the action of the right whiskering of $D$ and $\operatorname{Karoubi}$ applied to $D$ and $\operatorname{toKaroubi}$ applied to $D$.

Let $C$ and $D$ be sets. Then $\operatorname{karoubiUniversal}$ applied to $C$ and $D$ is an equivalence of the set of functors of $C$ and $D$ and the set of functors of $\operatorname{Karoubi}$ applied to $C$ and $D$ defined as the composition of $\mathrm{CategoryTheory\_\_Idempotents\_\_karoubiUniversal\_u2082\_}$ applied to $C$ and $D$ and the right congruence of the inverse of $\operatorname{asEquivalence}$ applied to $\operatorname{toKaroubi}$ applied to $D$.

Let $C$ and $D$ be sets. Then $\mathrm{CategoryTheory\_\_Idempotents\_\_karoubiUniversal\_u2081\_}$ applied to $C$ and $D$ is an equivalence of the set of functors of $C$ and $\operatorname{Karoubi}$ applied to $D$ and the set of functors of $\operatorname{Karoubi}$ applied to $C$ and $\operatorname{Karoubi}$ applied to $D$.

Let $C$ and $D$ be sets. Then $\mathrm{CategoryTheory\_\_Idempotents\_\_karoubiUniversal\_u2082\_}$ applied to $C$ and $D$ is an equivalence of the set of functors of $C$ and $D$ and the set of functors of $\operatorname{Karoubi}$ applied to $C$ and $\operatorname{Karoubi}$ applied to $D$ defined as the composition of the right congruence of $\operatorname{asEquivalence}$ applied to $\operatorname{toKaroubi}$ applied to $D$ and $\mathrm{CategoryTheory\_\_Idempotents\_\_karoubiUniversal\_u2081\_}$ applied to $C$ and $D$.

$\operatorname{whiskeringLeftObjToKaroubiFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the action of the left whiskering of $\operatorname{Karoubi}$ applied to $C$ and $D$ and $\operatorname{toKaroubi}$ applied to $C$.

the map of f (from the name)

Let $f$ be a homomorphism of $P$ and $Q$. Then the map of $f$ is a homomorphism of the object of $P$ and the object of $Q$.

the object of P (from the name)

Let $P$ be an element of $\operatorname{Karoubi}$ applied to the set of homological complexes of $C$ and $c$. Then the object of $P$ is a homological complex of $\operatorname{Karoubi}$ applied to $C$ and $c$.

the map of f (from the name)

Let $f$ be a homomorphism of $K$ and $L$. Then the map of $f$ is a homomorphism of the object of $K$ and the object of $L$.

the object of K (from the name)

Let $K$ be a homological complex of $\operatorname{Karoubi}$ applied to $C$ and $c$. Then the object of $K$ is an element of $\operatorname{Karoubi}$ applied to the set of homological complexes of $C$ and $c$.

the counit isomorphism of the equivalence (from the docstring)

The counit isomorphism of the equivalence is an isomorphism of the composition of the inverse and the functor and the identity of the set of homological complexes of $\operatorname{Karoubi}$ applied to $C$ and $c$.

the functor (from the docstring)

The functor is a functor of $\operatorname{Karoubi}$ applied to the set of homological complexes of $C$ and $c$ and the set of homological complexes of $\operatorname{Karoubi}$ applied to $C$ and $c$.

the inverse (from the name)

The inverse is a functor of the set of homological complexes of $\operatorname{Karoubi}$ applied to $C$ and $c$ and $\operatorname{Karoubi}$ applied to the set of homological complexes of $C$ and $c$.

the unit isomorphism of the equivalence (from the docstring)

The unit isomorphism of the equivalence is an isomorphism of the identity of $\operatorname{Karoubi}$ applied to the set of homological complexes of $C$ and $c$ and the composition of the functor and the inverse.

the equivalence of C and x2 (from the docstring)

Let $C$ and $x_{2}$ be sets. Then the equivalence of $C$ and $x_{2}$ is an equivalence of $\operatorname{Karoubi}$ applied to the set of chain complexes of $C$ and $x_{2}$ and the set of chain complexes of $\operatorname{Karoubi}$ applied to $C$ and $x_{2}$ defined as the equivalence of $C$ and $\operatorname{down}$ applied to $x_{2}$.

the equivalence of C and x2 (from the docstring)

Let $C$ and $x_{2}$ be sets. Then the equivalence of $C$ and $x_{2}$ is an equivalence of $\operatorname{Karoubi}$ applied to the set of cochain complexes of $C$ and $x_{2}$ and the set of cochain complexes of $\operatorname{Karoubi}$ applied to $C$ and $x_{2}$ defined as the equivalence of $C$ and $\operatorname{up}$ applied to $x_{2}$.

the equivalence of C and c (from the docstring)

Let $C$ be a set. Let $c$ be a complex shape of $x_{2}$. Then the equivalence of $C$ and $c$ is an equivalence of $\operatorname{Karoubi}$ applied to the set of homological complexes of $C$ and $c$ and the set of homological complexes of $\operatorname{Karoubi}$ applied to $C$ and $c$.

Let $C$ be a set. Then the elements of $\operatorname{Karoubi}$ applied to $C$ are a basic type.

homomorphism of P and Q (from the name)

Let $P$ and $Q$ be elements of $\operatorname{Karoubi}$ applied to $C$. Then the homomorphisms of $P$ and $Q$ are a basic type.

Let $\mathrm{self}$ be a homomorphism of $P$ and $Q$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{X}$ applied to $P$ and $\operatorname{X}$ applied to $Q$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{Karoubi}$ applied to $C$. Then $\operatorname{X}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the decomposition identity of P (from the name)

Let $P$ be an element of $\operatorname{Karoubi}$ applied to $C$. Then the decomposition identity of $P$ is a homomorphism of $P$ and $\operatorname{mk}$ applied to $\operatorname{X}$ applied to $P$, the identity morphism of $\operatorname{X}$ applied to $P$ and $\mathrm{CategoryTheory\_\_Idempotents\_\_Karoubi\_\_coe\_\_\_proof\_1}$ applied to $\operatorname{X}$ applied to $P$.

the decomposition identity of P (from the name)

Let $P$ be an element of $\operatorname{Karoubi}$ applied to $C$. Then the decomposition identity of $P$ is a homomorphism of $\operatorname{mk}$ applied to $\operatorname{X}$ applied to $P$, the identity morphism of $\operatorname{X}$ applied to $P$ and $\mathrm{CategoryTheory\_\_Idempotents\_\_Karoubi\_\_coe\_\_\_proof\_1}$ applied to $\operatorname{X}$ applied to $P$ and $P$.

the inclusion homomorphism of P and Q (from the name)

Let $P$ and $Q$ be elements of $\operatorname{Karoubi}$ applied to $C$. Then the inclusion homomorphism of $P$ and $Q$ is an additive monoid homomorphism of the set of homomorphisms of $P$ and $Q$ and the set of homomorphisms of $\operatorname{X}$ applied to $P$ and $\operatorname{X}$ applied to $Q$.

Let $\mathrm{self}$ be an element of $\operatorname{Karoubi}$ applied to $C$. Then $\operatorname{p}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{X}$ applied to $\mathrm{self}$ and $\operatorname{X}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the retract of X (from the name)

Let $X$ be an element of $\operatorname{Karoubi}$ applied to $C$. Then the retract of $X$ is a retract of $X$ and the action of $\operatorname{toKaroubi}$ applied to $C$ and $\operatorname{X}$ applied to $X$.

Let $C$ be a set. Then $\operatorname{fullyFaithfulToKaroubi}$ applied to $C$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{toKaroubi}$ applied to $C$.

Let $C$ be a set. Then $\operatorname{toKaroubi}$ applied to $C$ is a functor of $C$ and $\operatorname{Karoubi}$ applied to $C$.

the equivalence of C (from the docstring)

Let $C$ be a set. Then the equivalence of $C$ is an equivalence of $C$ and $\operatorname{Karoubi}$ applied to $C$ defined as $\operatorname{asEquivalence}$ applied to $\operatorname{toKaroubi}$ applied to $C$.

the counit isomorphism of the equivalence of C (from the docstring)

Let $C$ be a set. Then the counit isomorphism of the equivalence of $C$ is an isomorphism of the composition of the inverse of $C$ and $\operatorname{toKaroubi}$ applied to $\operatorname{Karoubi}$ applied to $C$ and the identity of $\operatorname{Karoubi}$ applied to $\operatorname{Karoubi}$ applied to $C$.

the equivalence of C (from the docstring)

Let $C$ be a set. Then the equivalence of $C$ is an equivalence of $\operatorname{Karoubi}$ applied to $C$ and $\operatorname{Karoubi}$ applied to $\operatorname{Karoubi}$ applied to $C$.

the inverse of C (from the name)

Let $C$ be a set. Then the inverse of $C$ is a functor of $\operatorname{Karoubi}$ applied to $\operatorname{Karoubi}$ applied to $C$ and $\operatorname{Karoubi}$ applied to $C$.

the unit isomorphism of the equivalence of C (from the docstring)

Let $C$ be a set. Then the unit isomorphism of the equivalence of $C$ is an isomorphism of the identity of $\operatorname{Karoubi}$ applied to $C$ and the composition of $\operatorname{toKaroubi}$ applied to $\operatorname{Karoubi}$ applied to $C$ and the inverse of $C$.

induced category of D and _F (from the name)

Let $D$ be a set. Let $\mathrm{\_F}$ be a function from elements of $C$ to elements of $D$. Then an induced category of $D$ and $\mathrm{\_F}$ is an element of the function that maps $D$ and $\mathrm{\_F}$ to $C$.

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be induced categories of $D$ and $F$. Then the homomorphisms of $X$ and $Y$ are a basic type.

the homomorphism of self (from the name)

Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of $F$ applied to $X$ and $F$ applied to $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the homomorphism equivalence (from the name)

The homomorphism equivalence is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of $F$ applied to $X$ and $F$ applied to $Y$.

the homomorphism of f (from the name)

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

the isomorphism of f (from the name)

Let $f$ be an isomorphism of $F$ applied to $X$ and $F$ applied to $Y$. Then the isomorphism of $f$ is an isomorphism of $X$ and $Y$.

the induced functor of F (from the docstring)

Let $F$ be a function from elements of $C$ to elements of $D$. Then the induced functor of $F$ is an element of $\operatorname{FullyFaithful}$ applied to the induced functor of $F$.

the induced functor of F (from the name)

Let $F$ be a function from elements of $C$ to elements of $D$. Then the induced functor of $F$ is a functor of the set of induced categories of $D$ and $F$ and $D$.

J is connected (from the name)

Let $J$ be a set. Then we can say that $J$ is connected.

J is preconnected (from the name)

Let $J$ be a set. Then we can say that $J$ is preconnected.

Let $x_{1}$ and $x_{2}$ be elements of $J$. Then $\operatorname{Zag}$ holds for $x_{1}$ and $x_{2}$, if $\mathrm{Nonempty}$ holds for the set of homomorphisms of $x_{1}$ and $x_{2}$ or $\mathrm{Nonempty}$ holds for the set of homomorphisms of $x_{2}$ and $x_{1}$.

Let $x_{1}$ and $x_{2}$ be elements of $J$. Then $\operatorname{Zigzag}$ holds for $x_{1}$ and $x_{2}$, if $\operatorname{ReflTransGen}$ holds for $\operatorname{Zag}$, $x_{1}$ and $x_{2}$.

$\operatorname{discreteIsConnectedEquivPUnit}$ is an equivalence from $x$ to $\mathrm{PUnit}$.

the isomorphism constant of F and j (from the name)

Let $F$ be a functor of $J$ and $\operatorname{Discrete}$ applied to $x_{1}$. Let $j$ be an element of $J$. Then the isomorphism constant of $F$ and $j$ is an isomorphism of $F$ and the action of the constant of $J$ and the action of $F$ and $j$.

the map isomorphism of F and i (from the name)

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

f is a isomorphism (from the name)

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

isomorphism of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the isomorphisms of $X$ and $Y$ are a basic type.

the homomorphism of self (from the name)

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

the homomorphism from equivalence of x1 (from the name)

Let $x_{1}$ be an isomorphism of $X$ and $Y$. Then the homomorphism from equivalence of $x_{1}$ is an equivalence from the set of homomorphisms of $X$ and $Z$ to the set of homomorphisms of $Y$ and $Z$.

the homomorphism to equivalence of x1 (from the name)

Let $x_{1}$ be an isomorphism of $X$ and $Y$. Then the homomorphism to equivalence of $x_{1}$ is an equivalence from the set of homomorphisms of $Z$ and $X$ to the set of homomorphisms of $Z$ and $Y$.

the inverse of self (from the name)

Let $\mathrm{self}$ be an isomorphism of $X$ and $Y$. Then the inverse of $\mathrm{self}$ is a homomorphism of $Y$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the identity of X (from the name)

Let $X$ be an element of $C$. Then the identity of $X$ is an isomorphism of $X$ and $X$.

the inverse of I (from the name)

Let $I$ be an isomorphism of $X$ and $Y$. Then the inverse of $I$ is an isomorphism of $Y$ and $X$.

the composition of x1 and x2 (from the name)

Let $x_{1}$ be an isomorphism of $X$ and $Y$. Let $x_{2}$ be an isomorphism of $Y$ and $Z$. Then the composition of $x_{1}$ and $x_{2}$ is an isomorphism of $X$ and $Z$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{asIso}$ applied to $f$ is an isomorphism of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $f$, the inverse of $f$, $\mathrm{CategoryTheory\_\_IsIso\_\_hom\_inv\_id}$ applied to $f$ and $\mathrm{CategoryTheory\_\_IsIso\_\_inv\_hom\_id}$ applied to $f$.

Let $f$ be a homomorphism of $Y$ and $X$. Then $\operatorname{asIso'}$ applied to $f$ is an isomorphism of $X$ and $Y$ defined as $\operatorname{mk}$ applied to the inverse of $f$, $f$, $\mathrm{CategoryTheory\_\_IsIso\_\_inv\_hom\_id}$ applied to $f$ and $\mathrm{CategoryTheory\_\_IsIso\_\_hom\_inv\_id}$ applied to $f$.

the inverse of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the inverse of $f$ is a homomorphism of $Y$ and $X$ defined as $\operatorname{choose}$ applied to $\operatorname{out}$.

the isomorphism category of e (from the name)

Let $e$ be an equivalence of $C$ and $D$ such that for all elements $X_{1}$ of $C$, the action of the inverse of $e$ and the action of the functor of $e$ and $X_{1}$ is equal to $X_{1}$, for all elements $Y_{1}$ of $D$, the action of the functor of $e$ and the action of the inverse of $e$ and $Y_{1}$ is equal to $Y_{1}$, $\mathrm{autoParam}$ holds for the proposition that for all elements $X$ of $C$, the component of the homomorphism of the unit isomorphism of $e$ and $X$ is equal to $\operatorname{eqToHom}$ applied to $\operatorname{symm}$ applied to $h$ applied to $X$ and $\mathrm{CategoryTheory\_\_Equivalence\_\_toIsoCat\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $Y$ of $D$, the component of the homomorphism of the counit isomorphism of $e$ and $Y$ is equal to $\operatorname{eqToHom}$ applied to $\mathrm{h'}$ applied to $Y$ and $\mathrm{CategoryTheory\_\_Equivalence\_\_toIsoCat\_\_\_auto\_3}$. Then the isomorphism category of $e$ is an isomorphism category of $C$ and $D$.

F is a isomorphism (from the name)

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

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

the object equivalence of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the object equivalence of $F$ is an equivalence from $C$ to $D$ defined as the equivalence of $\operatorname{obj}$ applied to $F$ and $\mathrm{CategoryTheory\_\_Functor\_\_IsIso\_\_bijective\_obj}$ applied to $F$.

the strict inverse of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the strict inverse of $F$ is a functor of $D$ and $C$.

the equivalence of e (from the name)

Let $e$ be an equivalence from $D$ to $C$. Then the equivalence of $e$ is an equivalence of the set of induced categories of $C$ and $\operatorname{coe}$ applied to $e$ and $C$ defined as the equivalence of the isomorphism category of $e$.

the isomorphism category of e (from the name)

Let $e$ be an equivalence from $D$ to $C$. Then the isomorphism category of $e$ is an isomorphism category of the set of induced categories of $C$ and $\operatorname{coe}$ applied to $e$ and $C$.

isomorphism category of C and D (from the name)

Let $C$ and $D$ be sets. Then the isomorphism categories of $C$ and $D$ are a basic type.

the forward functor of self (from the docstring)

Let $\mathrm{self}$ be an isomorphism category of $C$ and $D$. Then the forward functor of $\mathrm{self}$ is a functor of $C$ and $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the inverse functor of self (from the docstring)

Let $\mathrm{self}$ be an isomorphism category of $C$ and $D$. Then the inverse functor of $\mathrm{self}$ is a functor of $D$ and $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the object equivalence of e (from the name)

Let $e$ be an isomorphism category of $C$ and $D$. Then the object equivalence of $e$ is an equivalence from $C$ to $D$.

the identity of C (from the name)

Let $C$ be a set. Then the identity of $C$ is an isomorphism category of $C$ and $C$.

the inverse of e (from the name)

Let $e$ be an isomorphism category of $C$ and $D$. Then the inverse of $e$ is an isomorphism category of $D$ and $C$.

the equivalence of e (from the name)

Let $e$ be an isomorphism category of $C$ and $D$. Then the equivalence of $e$ is an equivalence of $C$ and $D$.

the composition of e and f (from the name)

Let $e$ be an isomorphism category of $C$ and $D$. Let $f$ be an isomorphism category of $D$ and $E$. Then the composition of $e$ and $f$ is an isomorphism category of $C$ and $E$.

x1 is isomorphic to x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $C$. Then $x_{1}$ is isomorphic to $x_{2}$, if $\mathrm{Nonempty}$ holds for the set of isomorphisms of $x_{1}$ and $x_{2}$.

the isomorphism class (from the name)

The isomorphism class is a functor of the set of categories and the set of sets.

join of C and D (from the name)

Let $C$ and $D$ be sets. Then the joins of $C$ and $D$ are a basic type.

homomorphism of x2 and x3 (from the name)

Let $x_{2}$ and $x_{3}$ be joins of $C$ and $D$. Then the homomorphisms of $x_{2}$ and $x_{3}$ are a basic type.

the composition of x3 and x4 (from the name)

Let $x_{3}$ be a homomorphism of $x_{2}$ and $y$. Let $x_{4}$ be a homomorphism of $y$ and $z$. Then the composition of $x_{3}$ and $x_{4}$ is a homomorphism of $x_{2}$ and $z$.

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

the edge of c and d (from the name)

Let $c$ be an element of $C$. Let $d$ be an element of $D$. Then the edge of $c$ and $d$ is a homomorphism of the left of $c$ and the right of $d$ defined as $\operatorname{default}$.

the edge transform of C and D (from the name)

Let $C$ and $D$ be sets. Then the edge transform of $C$ and $D$ is a homomorphism of the composition of the first component of $C$ and $D$ and the left inclusion of $C$ and $D$ and the composition of the second component of $C$ and $D$ and the right inclusion of $C$ and $D$.

the homomorphism induction of y2 and f2 (from the name)

Let $\mathrm{left}$ be a function from elements $x_{4}$ of $C$ and elements $y_{2}$ of $C$ and homomorphisms $f_{2}$ of $x_{4}$ and $y_{2}$ to elements of $P$ applied to the action of the left inclusion of $C$ and $D$ and $x_{4}$, the action of the left inclusion of $C$ and $D$ and $y_{2}$ and the map of the left inclusion of $C$ and $D$ and $f_{2}$. Let $\mathrm{right}$ be a function from elements $x_{3}$ of $D$ and elements $y_{1}$ of $D$ and homomorphisms $f_{1}$ of $x_{3}$ and $y_{1}$ to elements of $P$ applied to the action of the right inclusion of $C$ and $D$ and $x_{3}$, the action of the right inclusion of $C$ and $D$ and $y_{1}$ and the map of the right inclusion of $C$ and $D$ and $f_{1}$. Let $\mathrm{edge}$ be a function from elements $c$ of $C$ and elements $d$ of $D$ to elements of $P$ applied to the left of $c$, the right of $d$ and the edge of $c$ and $d$. Let $f$ be a homomorphism of $x_{2}$ and $y$. Then the homomorphism induction of $f_{2}$ and $\mathrm{left}$ is an element of $P$ applied to $x_{2}$, $y$ and $f$.

the identity of X (from the name)

Let $X$ be a join of $C$ and $D$. Then the identity of $X$ is a homomorphism of $X$ and $X$.

the left inclusion of C and D (from the name)

Let $C$ and $D$ be sets. Then the left inclusion of $C$ and $D$ is a functor of $C$ and the set of joins of $C$ and $D$.

the left inclusion of C and D (from the docstring)

Let $C$ and $D$ be sets. Then the left inclusion of $C$ and $D$ is an element of $\operatorname{FullyFaithful}$ applied to the left inclusion of $C$ and $D$.

the right inclusion of C and D (from the name)

Let $C$ and $D$ be sets. Then the right inclusion of $C$ and $D$ is a functor of $D$ and the set of joins of $C$ and $D$.

the right inclusion of C and D (from the docstring)

Let $C$ and $D$ be sets. Then the right inclusion of $C$ and $D$ is an element of $\operatorname{FullyFaithful}$ applied to the right inclusion of $C$ and $D$.

the isomorphism functor of F (from the name)

Let $F$ be a functor of the set of joins of $C$ and $D$ and $E$. Then the isomorphism functor of $F$ is an isomorphism of $F$ and the functor of the composition of the right inclusion of $C$ and $D$ and $F$ and the right whisker of the edge transform of $C$ and $D$ and $F$.

the left of x2 (from the name)

Let $x_{2}$ be an element of $C$. Then the left of $x_{2}$ is a join of $C$ and $D$.

the left map isomorphism whisker of H and x6 (from the name)

Let $H$ be a functor of $C$ and $E$. Let $x_{6}$ be an isomorphism of $x_{4}$ and $x_{5}$. Then the left map isomorphism whisker of $H$ and $x_{6}$ is an isomorphism of the map pair of $H$ and $x_{4}$ and the map pair of $H$ and $x_{5}$.

the right map isomorphism whisker of x6 and H (from the name)

Let $x_{6}$ be an isomorphism of $x_{4}$ and $x_{5}$. Let $H$ be a functor of $D$ and $\mathrm{E'}$. Then the right map isomorphism whisker of $x_{6}$ and $H$ is an isomorphism of the map pair of $x_{4}$ and $H$ and the map pair of $x_{5}$ and $H$.

the map pair of x4 and x5 (from the name)

Let $x_{4}$ be a functor of $C$ and $E$. Let $x_{5}$ be a functor of $D$ and $\mathrm{E'}$. Then the map pair of $x_{4}$ and $x_{5}$ is a functor of the set of joins of $C$ and $D$ and the set of joins of $E$ and $\mathrm{E'}$.

the map pair composition of x8 and x9 (from the name)

Let $x_{6}$ be a functor of $C$ and $E$. Let $x_{7}$ be a functor of $D$ and $\mathrm{E'}$. Let $x_{8}$ be a functor of $E$ and $J$. Let $x_{9}$ be a functor of $\mathrm{E'}$ and $K$. Then the map pair composition of $x_{8}$ and $x_{9}$ is an isomorphism of the map pair of the composition of $x_{6}$ and $x_{8}$ and the composition of $x_{7}$ and $x_{9}$ and the composition of the map pair of $x_{6}$ and $x_{7}$ and the map pair of $x_{8}$ and $x_{9}$.

the map pair equivalence of e and #2 (from the name)

Let $e$ be an equivalence of $C$ and $\mathrm{C'}$. Let $\mathrm{e'}$ be an equivalence of $D$ and $\mathrm{D'}$. Then the map pair equivalence of $e$ and $\mathrm{e'}$ is an equivalence of the set of joins of $C$ and $D$ and the set of joins of $\mathrm{C'}$ and $\mathrm{D'}$.

the map pair identity (from the name)

The map pair identity is an isomorphism of the map pair of the identity of $C$ and the identity of $D$ and the identity of the set of joins of $C$ and $D$.

the left map pair of x4 and x5 (from the name)

Let $x_{4}$ be a functor of $C$ and $E$. Let $x_{5}$ be a functor of $D$ and $\mathrm{E'}$. Then the left map pair of $x_{4}$ and $x_{5}$ is an isomorphism of the composition of the left inclusion of $C$ and $D$ and the map pair of $x_{4}$ and $x_{5}$ and the composition of $x_{4}$ and the left inclusion of $E$ and $\mathrm{E'}$.

the right map pair of x4 and x5 (from the name)

Let $x_{4}$ be a functor of $C$ and $E$. Let $x_{5}$ be a functor of $D$ and $\mathrm{E'}$. Then the right map pair of $x_{4}$ and $x_{5}$ is an isomorphism of the composition of the right inclusion of $C$ and $D$ and the map pair of $x_{4}$ and $x_{5}$ and the composition of $x_{5}$ and the right inclusion of $E$ and $\mathrm{E'}$.

the left map whisker of H and x6 (from the name)

Let $H$ be a functor of $C$ and $E$. Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{5}$. Then the left map whisker of $H$ and $x_{6}$ is a homomorphism of the map pair of $H$ and $x_{4}$ and the map pair of $H$ and $x_{5}$.

the right map whisker of x6 and H (from the name)

Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $H$ be a functor of $D$ and $\mathrm{E'}$. Then the right map whisker of $x_{6}$ and $H$ is a homomorphism of the map pair of $x_{4}$ and $H$ and the map pair of $x_{5}$ and $H$.

the functor of G and x3 (from the name)

Let $F$ be a functor of $C$ and $E$. Let $G$ be a functor of $D$ and $E$. Let $x_{3}$ be a homomorphism of the composition of the first component of $C$ and $D$ and $F$ and the composition of the second component of $C$ and $D$ and $G$. Then the functor of $G$ and $x_{3}$ is a functor of the set of joins of $C$ and $D$ and $E$.

the left functor of G and x3 (from the name)

Let $F$ be a functor of $C$ and $E$. Let $G$ be a functor of $D$ and $E$. Let $x_{3}$ be a homomorphism of the composition of the first component of $C$ and $D$ and $F$ and the composition of the second component of $C$ and $D$ and $G$. Then the left functor of $G$ and $x_{3}$ is an isomorphism of the composition of the left inclusion of $C$ and $D$ and the functor of $G$ and $x_{3}$ and $F$ defined as the identity of the composition of the left inclusion of $C$ and $D$ and the functor of $G$ and $x_{3}$.

the right functor of G and x3 (from the name)

Let $F$ be a functor of $C$ and $E$. Let $G$ be a functor of $D$ and $E$. Let $x_{3}$ be a homomorphism of the composition of the first component of $C$ and $D$ and $F$ and the composition of the second component of $C$ and $D$ and $G$. Then the right functor of $G$ and $x_{3}$ is an isomorphism of the composition of the right inclusion of $C$ and $D$ and the functor of $G$ and $x_{3}$ and $G$ defined as the identity of the composition of the right inclusion of $C$ and $D$ and the functor of $G$ and $x_{3}$.

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

Let $x_{3}$ be an isomorphism of the composition of the left inclusion of $C$ and $D$ and $F$ and the composition of the left inclusion of $C$ and $D$ and $G$. Let $x_{4}$ be an isomorphism of the composition of the right inclusion of $C$ and $D$ and $F$ and the composition of the right inclusion of $C$ and $D$ and $G$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the right whisker of the edge transform of $C$ and $D$ and $F$ and the homomorphism of the left isomorphism whisker of the second component of $C$ and $D$ and $x_{4}$ is equal to the composition of the homomorphism of the left isomorphism whisker of the first component of $C$ and $D$ and $x_{3}$ and the right whisker of the edge transform of $C$ and $D$ and $G$ and $\mathrm{CategoryTheory\_\_Join\_\_mkNatIso\_\_\_auto\_1}$. Then the natural isomorphism of $x_{3}$ and $x_{4}$ is an isomorphism of $F$ and $G$.

the natural transformation of x3 and x4 (from the name)

Let $x_{3}$ be a homomorphism of the composition of the left inclusion of $C$ and $D$ and $F$ and the composition of the left inclusion of $C$ and $D$ and $\mathrm{F'}$. Let $x_{4}$ be a homomorphism of the composition of the right inclusion of $C$ and $D$ and $F$ and the composition of the right inclusion of $C$ and $D$ and $\mathrm{F'}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the right whisker of the edge transform of $C$ and $D$ and $F$ and the left whisker of the second component of $C$ and $D$ and $x_{4}$ is equal to the composition of the left whisker of the first component of $C$ and $D$ and $x_{3}$ and the right whisker of the edge transform of $C$ and $D$ and $\mathrm{F'}$ and $\mathrm{CategoryTheory\_\_Join\_\_mkNatTrans\_\_\_auto\_1}$. Then the natural transformation of $x_{3}$ and $x_{4}$ is a homomorphism of $F$ and $\mathrm{F'}$.

the right of x2 (from the name)

Let $x_{2}$ be an element of $D$. Then the right of $x_{2}$ is a join of $C$ and $D$.

the costructured arrow equivalence of d (from the name)

Let $C$ and $D$ be sets. Let $d$ be an element of $D$. Then the costructured arrow equivalence of $d$ is an equivalence of the set of costructured arrows of the left inclusion of $C$ and $D$ and the right of $d$ and $C$.

the structured arrow equivalence of c (from the name)

Let $C$ and $D$ be sets. Let $c$ be an element of $C$. Then the structured arrow equivalence of $c$ is an equivalence of the set of structured arrows of the left of $c$ and the right inclusion of $C$ and $D$ and $D$.

the inclusion left composition right opposite opposite equivalence functor of C and D (from the name)

Let $C$ and $D$ be sets. Then the inclusion left composition right opposite opposite equivalence functor of $C$ and $D$ is an isomorphism of the composition of the left inclusion of $C$ and $D$ and the right opposite of the functor of the equivalence of $C$ and $D$ and the right opposite of the right inclusion of the set of opposites of $D$ and the set of opposites of $C$.

the inclusion right composition right opposite opposite equivalence functor of C and D (from the name)

Let $C$ and $D$ be sets. Then the inclusion right composition right opposite opposite equivalence functor of $C$ and $D$ is an isomorphism of the composition of the right inclusion of $C$ and $D$ and the right opposite of the functor of the equivalence of $C$ and $D$ and the right opposite of the left inclusion of the set of opposites of $D$ and the set of opposites of $C$.

the inclusion left composition opposite equivalence inverse of C and D (from the name)

Let $C$ and $D$ be sets. Then the inclusion left composition opposite equivalence inverse of $C$ and $D$ is an isomorphism of the composition of the left inclusion of the set of opposites of $D$ and the set of opposites of $C$ and the inverse of the equivalence of $C$ and $D$ and the opposite of the right inclusion of $C$ and $D$.

the inclusion right composition opposite equivalence inverse of C and D (from the name)

Let $C$ and $D$ be sets. Then the inclusion right composition opposite equivalence inverse of $C$ and $D$ is an isomorphism of the composition of the right inclusion of the set of opposites of $D$ and the set of opposites of $C$ and the inverse of the equivalence of $C$ and $D$ and the opposite of the left inclusion of $C$ and $D$.

the equivalence of C and D (from the docstring)

Let $C$ and $D$ be sets. Then the equivalence of $C$ and $D$ is an equivalence of the set of opposites of the set of joins of $C$ and $D$ and the set of joins of the set of opposites of $D$ and the set of opposites of $C$.

the structural isomorphism for composition of D (from the docstring)

Let $D$ be a set. Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $B$ and $C$. Then the structural isomorphism for composition of $D$ is an isomorphism of the map pair of the composition of $F$ and $G$ and the identity of $D$ and the composition of the map pair of $F$ and the identity of $D$ and the map pair of $G$ and the identity of $D$ defined as the composition of the left map isomorphism whisker of the composition of $F$ and $G$ and the inverse of the left unitor of the identity of $D$ and the map pair composition of $G$ and the identity of $D$.

the structural isomorphism for composition of A (from the docstring)

Let $A$ be a set. Let $F$ be a functor of $B$ and $C$. Let $G$ be a functor of $C$ and $D$. Then the structural isomorphism for composition of $A$ is an isomorphism of the map pair of the identity of $A$ and the composition of $F$ and $G$ and the composition of the map pair of the identity of $A$ and $F$ and the map pair of the identity of $A$ and $G$ defined as the composition of the right map isomorphism whisker of the inverse of the left unitor of the identity of $A$ and the composition of $F$ and $G$ and the map pair composition of the identity of $A$ and $G$.

the left pseudofunctor of D (from the name)

Let $D$ be a set. Then the left pseudofunctor of $D$ is a pseudofunctor of the set of categories and the set of categories.

the right pseudofunctor of C (from the name)

Let $C$ be a set. Then the right pseudofunctor of $C$ is a pseudofunctor of the set of categories and the set of categories.

the canonical functor from the sum to the join of C and D (from the docstring)

Let $C$ and $D$ be sets. Then the canonical functor from the sum to the join of $C$ and $D$ is a functor of $\mathrm{Sum}$ applied to $C$ and $D$ and the set of joins of $C$ and $D$ defined as the sum of the left inclusion of $C$ and $D$ and the right inclusion of $C$ and $D$.

the left injection composition from sum of C and D (from the name)

Let $C$ and $D$ be sets. Then the left injection composition from sum of $C$ and $D$ is an isomorphism of the composition of the left injection of $C$ and $D$ and the canonical functor from the sum to the join of $C$ and $D$ and the left inclusion of $C$ and $D$ defined as the sum of the left inclusion of $C$ and $D$ and the right inclusion of $C$ and $D$.

the right injection composition from sum of C and D (from the name)

Let $C$ and $D$ be sets. Then the right injection composition from sum of $C$ and $D$ is an isomorphism of the composition of the right injection of $C$ and $D$ and the canonical functor from the sum to the join of $C$ and $D$ and the right inclusion of $C$ and $D$ defined as the sum of the left inclusion of $C$ and $D$ and the right inclusion of $C$ and $D$.

Assume that $\operatorname{CommSq}$ holds for $v$, $p$, the map of $G$ and $i$ and $u$. Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then $\operatorname{leftAdjointLiftStructEquiv}$ applied to $\mathrm{sq}$ and $\mathrm{adj}$ is an element of $\EquivMACRoAE {\operatorname{LiftStruct} (\mathrm{sq})}{\operatorname{LiftStruct} (\mathrm{CategoryTheory\_\_CommSq\_\_left\_adjoint} (\mathrm{sq} , \mathrm{adj}))}$.

Assume that $\operatorname{CommSq}$ holds for $u$, the map of $G$ and $i$, $p$ and $v$. Let $\mathrm{adj}$ be an adjunction of $G$ and $F$. Then $\operatorname{rightAdjointLiftStructEquiv}$ applied to $\mathrm{sq}$ and $\mathrm{adj}$ is an element of $\EquivMACRoAE {\operatorname{LiftStruct} (\mathrm{sq})}{\operatorname{LiftStruct} (\mathrm{CategoryTheory\_\_CommSq\_\_right\_adjoint} (\mathrm{sq} , \mathrm{adj}))}$.

Let $x_{1}$ be a homomorphism of $f$ and $g$. Then the elements of $\operatorname{LiftStruct}$ applied to $x_{1}$ are a basic type.

Let $i$ be a homomorphism of $A$ and $B$. Let $p$ be a homomorphism of $X$ and $Y$. Then we can say that $\operatorname{HasLiftingProperty}$ holds for $i$ and $p$.

Let $i$ be a homomorphism of $A$ and $B$. Let $p$ be a homomorphism of $X$ and $Y$. Let $b$ be a homomorphism of $B$ and $Y$. Then $\operatorname{HasLiftingPropertyFixedBot}$ holds for $i$, $p$ and $b$, if for all homomorphisms $b_{1}$ of $A$ and $X$, for all elements $\mathrm{sq}$ of $\mathrm{Proof}$ applied to $\operatorname{CommSq}$ applied to $b_{1}$, $i$, $p$ and $b$, $\mathrm{sq}$ has lifts.

Let $i$ be a homomorphism of $A$ and $B$. Let $p$ be a homomorphism of $X$ and $Y$. Let $t$ be a homomorphism of $A$ and $X$. Then $\operatorname{HasLiftingPropertyFixedTop}$ holds for $i$, $p$ and $t$, if for all homomorphisms $b$ of $B$ and $Y$, for all elements $\mathrm{sq}$ of $\mathrm{Proof}$ applied to $\operatorname{CommSq}$ applied to $t$, $i$, $p$ and $b$, $\mathrm{sq}$ has lifts.

the arrow homomorphism equivalence of x16 and x17 (from the name)

Let $x_{6}$ be a parametrized adjunction of $F$ and $G$. Let $x_{16}$ be a pushout object object of $x_{9}$ and $x_{12}$. Let $x_{17}$ be a pullback object object of $x_{9}$ and $x_{15}$. Then the arrow homomorphism equivalence of $x_{16}$ and $x_{17}$ is an equivalence from the set of homomorphisms of $\operatorname{mk}$ applied to the inclusion of $x_{16}$ and $\operatorname{mk}$ applied to $x_{15}$ to the set of homomorphisms of $\operatorname{mk}$ applied to $x_{12}$ and $\operatorname{mk}$ applied to the projection of $x_{17}$.

Let $x_{6}$ be a parametrized adjunction of $F$ and $G$. Let $x_{16}$ be a pushout object object of $x_{9}$ and $x_{12}$. Let $x_{17}$ be a pullback object object of $x_{9}$ and $x_{15}$. Let $x_{18}$ be a homomorphism of $\operatorname{mk}$ applied to the inclusion of $x_{16}$ and $\operatorname{mk}$ applied to $x_{15}$. Then $\operatorname{liftStructEquiv}$ applied to $x_{6}$, $x_{16}$, $x_{17}$ and $x_{18}$ is an element of $\EquivMACRoAE {\operatorname{LiftStruct} (x_{18})}{\operatorname{LiftStruct} (\operatorname{arrowHomEquiv} (x_{6} , x_{16} , x_{17} , x_{18}))}$.

bicone of J (from the name)

Let $J$ be a set. Then the bicones of $J$ are a basic type.

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

the diagram of val (from the name)

Let $\mathrm{val}$ be an element of $J$. Then the diagram of $\mathrm{val}$ is a bicone of $J$.

the left (from the name)

The left is a bicone of $J$.

the right (from the name)

The right is a bicone of $J$.

bicone homomorphism of x1 and x2 (from the name)

Let $J$ be a set. Let $x_{1}$ and $x_{2}$ be bicones of $J$. Then the bicone homomorphisms of $x_{1}$ and $x_{2}$ are a basic type.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the left, the left and the left identity and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the right, the right and the right identity and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to the set of functions from elements $j$ of $J$ to elements of $\mathrm{motive}$ applied to the left, the diagram of $j$ and the left of $j$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $3$, $\mathrm{PULift}$ applied to the set of functions from elements $j_{1}$ of $J$ to elements of $\mathrm{motive}$ applied to the right, the diagram of $j_{1}$ and the right of $j_{1}$ and $\mathrm{PULift}$ applied to the set of functions from elements $j_{2}$ of $J$ and elements $k$ of $J$ and homomorphisms $f$ of $j_{2}$ and $k$ to elements of $\mathrm{motive}$ applied to the diagram of $j_{2}$, the diagram of $k$ and the diagram of $f$.

the diagram of f (from the name)

Let $f$ be a homomorphism of $j$ and $k$. Then the diagram of $f$ is a bicone homomorphism of the diagram of $j$ and the diagram of $k$.

the left of j (from the name)

Let $j$ be an element of $J$. Then the left of $j$ is a bicone homomorphism of the left and the diagram of $j$.

the left identity (from the name)

The left identity is a bicone homomorphism of the left and the left.

the right of j (from the name)

Let $j$ be an element of $J$. Then the right of $j$ is a bicone homomorphism of the right and the diagram of $j$.

the right identity (from the name)

The right identity is a bicone homomorphism of the right and the right.

the bicone of x2 and x3 (from the name)

Let $J$ be a set. Let $x_{2}$ and $x_{3}$ be cones of $F$. Then the bicone of $x_{2}$ and $x_{3}$ is a functor of the set of bicones of $J$ and $C$.

chosen coend of C (from the name)

Let $C$ be a set. Then a chosen coend of $C$ is an element of the function that maps $C$ to the set of functions from sets $J$ and elements $x_{1}$ of $\mathrm{Proof}$ applied to the proposition that $J$ is a category to elements of $\operatorname{ChosenCoendsOfShape}$ applied to $J$ and $C$.

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

the chosen cowedge of F (from the docstring)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then the chosen cowedge of $F$ is a cowedge of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $F$.

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then $\operatorname{isCoend}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the chosen cowedge of $F$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $F$.

chosen end of C (from the name)

Let $C$ be a set. Then a chosen end of $C$ is an element of the function that maps $C$ to the set of functions from sets $J$ and elements $x_{1}$ of $\mathrm{Proof}$ applied to the proposition that $J$ is a category to elements of $\operatorname{ChosenEndsOfShape}$ applied to $J$ and $C$.

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

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then $\operatorname{isEnd}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the chosen wedge of $F$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $F$.

the chosen wedge of F (from the docstring)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then the chosen wedge of $F$ is a wedge of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $F$.

the chosen coend of F (from the docstring)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then the chosen coend of $F$ is an element of $C$ defined as $\operatorname{pt}$ applied to the chosen cowedge of $F$.

Let $f$ be a function from elements $j_{1}$ of $J$ to homomorphisms of the action of the action of $F$ and $\operatorname{op}$ applied to $j_{1}$ and $j_{1}$ and $X$ such that for all elements $i$ and $j$ of $J$, for all homomorphisms $g$ of $i$ and $j$, the composition of the component of the map of $F$ and the opposite in $g$ and $i$ and $f$ applied to $i$ is equal to the composition of the map of the action of $F$ and $\operatorname{op}$ applied to $j$ and $g$ and $f$ applied to $j$. Then $\operatorname{desc}$ applied to $j_{1}$, $f$ and $\mathrm{hf}$ is a homomorphism of the chosen coend of $F$ and $X$ defined as the function that maps $\mathrm{hf}$ to $\operatorname{desc}$ applied to $\operatorname{isCoend}$ applied to $F$, $j_{1}$, $f$ and $\mathrm{hf}$.

the map of f (from the name)

Let $f$ be a homomorphism of $F$ and $G$. Then the map of $f$ is a homomorphism of the chosen coend of $F$ and the chosen coend of $G$.

the inclusion of F and j (from the name)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Let $j$ be an element of $J$. Then the inclusion of $F$ and $j$ is a homomorphism of the action of the action of $F$ and $\operatorname{op}$ applied to $j$ and $j$ and the chosen coend of $F$ defined as the projection of the chosen cowedge of $F$ and $j$.

the chosen coend construction (from the docstring)

The chosen coend construction is a functor of the set of functors of the set of opposites of $J$ and the set of functors of $J$ and $C$ and $C$.

the chosen end of F (from the docstring)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Then the chosen end of $F$ is an element of $C$ defined as $\operatorname{pt}$ applied to the chosen wedge of $F$.

the lift of f and j1 (from the name)

Let $f$ be a function from elements $j_{1}$ of $J$ to homomorphisms of $X$ and the action of the action of $F$ and $\operatorname{op}$ applied to $j_{1}$ and $j_{1}$ such that for all elements $i$ and $j$ of $J$, for all homomorphisms $g$ of $i$ and $j$, the composition of $f$ applied to $i$ and the map of the action of $F$ and $\operatorname{op}$ applied to $i$ and $g$ is equal to the composition of $f$ applied to $j$ and the component of the map of $F$ and the opposite in $g$ and $j$. Then the lift of $j_{1}$ and $f$ is a homomorphism of $X$ and the chosen end of $F$ defined as the function that maps $\mathrm{hf}$ to the lift of $\operatorname{isEnd}$ applied to $F$ and $j_{1}$.

the map of f (from the name)

Let $f$ be a homomorphism of $F$ and $G$. Then the map of $f$ is a homomorphism of the chosen end of $F$ and the chosen end of $G$.

the projection of F and j (from the name)

Let $F$ be a functor of the set of opposites of $J$ and the set of functors of $J$ and $C$. Let $j$ be an element of $J$. Then the projection of $F$ and $j$ is a homomorphism of the chosen end of $F$ and the action of the action of $F$ and $\operatorname{op}$ applied to $j$ and $j$ defined as the inclusion of the chosen wedge of $F$ and $j$.

the chosen end construction (from the docstring)

The chosen end construction is a functor of the set of functors of the set of opposites of $J$ and the set of functors of $J$ and $C$ and $C$.

the cocone flip of F (from the name)

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

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then $\operatorname{isColimitCoconeFlip}$ applied to $F$ is an element of $\operatorname{IsColimit}$ applied to the cocone flip of $F$ defined as $\operatorname{evaluationJointlyReflectsColimits}$ applied to the cocone flip of $F$ and the function that maps $x_{3}$ to $\operatorname{isColimit}$ applied to the composition of the flip of $F$ and the action of the evaluation of $J$ and $C$ and $x_{3}$.

the colimit limit to limit colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the colimit limit to limit colimit of $F$ is a homomorphism of the colimit of the composition of the flip of $F$ and the limit and the limit of the composition of $F$ and the colimit defined as $\operatorname{desc}$ applied to the composition of the flip of $F$ and the limit and the map cocone of the limit and the cocone flip of $F$.

the colimit limit to limit colimit of F (from the name)

Let $F$ be a functor of $\mathrm{Prod}$ applied to $J$ and $K$ and $C$. Then the colimit limit to limit colimit of $F$ is a homomorphism of the colimit of the composition of the action of the curry and the composition of the swap of $K$ and $J$ and $F$ and the limit and the limit of the composition of the action of the curry and $F$ and the colimit.

the colimit limit to limit colimit cone of G (from the name)

Let $G$ be a functor of $J$ and the set of functors of $K$ and $C$. Then the colimit limit to limit colimit cone of $G$ is a homomorphism of the map cone of the colimit and the cone of $G$ and the cone of the composition of $G$ and the colimit.

the cone of F (from the name)

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

Let $F$ be a functor of $J$ and the set of functors of $K$ and $C$. Then $\operatorname{isLimitCone}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the cone of $F$ defined as $\operatorname{evaluationJointlyReflectsLimits}$ applied to the cone of $F$ and the function that maps $x_{3}$ to $\operatorname{isLimit}$ applied to the composition of $F$ and the action of the evaluation of $K$ and $C$ and $x_{3}$.

the cocone of x5 and x6 (from the name)

Let $F$ be a functor of $J$ and the set of commas of $L$ and $R$. Let $x_{5}$ be an element of $\operatorname{IsColimit}$ applied to $x_{4}$. Let $x_{6}$ be a cocone of the composition of $F$ and the second component of $L$ and $R$. Then the cocone of $x_{5}$ and $x_{6}$ is a cocone of $F$.

the cocone of x5 and x7 (from the name)

Let $F$ be a functor of $J$ and the set of commas of $L$ and $R$. Let $x_{5}$ be an element of $\operatorname{IsColimit}$ applied to $x_{4}$. Let $x_{7}$ be an element of $\operatorname{IsColimit}$ applied to $x_{6}$. Then the cocone of $x_{5}$ and $x_{7}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $x_{5}$ and $x_{6}$ defined as $\operatorname{fstSndJointlyReflectColimit}$ applied to $x_{5}$ and $x_{7}$.

the colimit auxiliary cocone of F and x4 (from the name)

Let $F$ be a functor of $J$ and the set of commas of $L$ and $R$. Let $x_{4}$ be a cocone of the composition of $F$ and the second component of $L$ and $R$. Then the colimit auxiliary cocone of $F$ and $x_{4}$ is a cocone of the composition of the composition of $F$ and the first component of $L$ and $R$ and $L$ defined as the action of the precomposition of the left whisker of $F$ and the natural transformation of $L$ and $R$ and the map cocone of $R$ and $x_{4}$.

the cone of x4 and x6 (from the name)

Let $F$ be a functor of $J$ and the set of commas of $L$ and $R$. Let $x_{4}$ be a cone of the composition of $F$ and the first component of $L$ and $R$. Let $x_{6}$ be an element of $\operatorname{IsLimit}$ applied to $x_{5}$. Then the cone of $x_{4}$ and $x_{6}$ is a cone of $F$.

the cone of x5 and x7 (from the name)

Let $F$ be a functor of $J$ and the set of commas of $L$ and $R$. Let $x_{5}$ be an element of $\operatorname{IsLimit}$ applied to $x_{4}$. Let $x_{7}$ be an element of $\operatorname{IsLimit}$ applied to $x_{6}$. Then the cone of $x_{5}$ and $x_{7}$ is an element of $\operatorname{IsLimit}$ applied to the cone of $x_{4}$ and $x_{7}$ defined as $\operatorname{fstSndJointlyReflectLimit}$ applied to $x_{5}$ and $x_{7}$.

Let $x_{4}$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of the first component of $L$ and $R$ and $c$. Let $x_{5}$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of the second component of $L$ and $R$ and $c$. Then $\operatorname{fstSndJointlyReflectColimit}$ applied to $x_{4}$ and $x_{5}$ is an element of $\operatorname{IsColimit}$ applied to $c$.

Let $x_{4}$ be an element of $\operatorname{IsLimit}$ applied to the map cone of the first component of $L$ and $R$ and $c$. Let $x_{5}$ be an element of $\operatorname{IsLimit}$ applied to the map cone of the second component of $L$ and $R$ and $c$. Then $\operatorname{fstSndJointlyReflectLimit}$ applied to $x_{4}$ and $x_{5}$ is an element of $\operatorname{IsLimit}$ applied to $c$.

the limit auxiliary cone of F and x4 (from the name)

Let $F$ be a functor of $J$ and the set of commas of $L$ and $R$. Let $x_{4}$ be a cone of the composition of $F$ and the first component of $L$ and $R$. Then the limit auxiliary cone of $F$ and $x_{4}$ is a cone of the composition of the composition of $F$ and the second component of $L$ and $R$ and $R$ defined as the action of the postcomposition of the left whisker of $F$ and the natural transformation of $L$ and $R$ and the map cone of $L$ and $x_{4}$.

the costructured arrow isomorphism to costructured arrow of X and f (from the name)

Let $G$ be a functor of $J$ and $K$. Let $F$ be a functor of $K$ and $C$. Let $X$ be an element of $C$. Let $f$ be a function from elements $Y_{1}$ of $J$ to homomorphisms of the action of $F$ and the action of $G$ and $Y_{1}$ and $X$ such that for all elements $Y$ and $Z$ of $J$, for all homomorphisms $g$ of $Y$ and $Z$, the composition of the map of $F$ and the map of $G$ and $g$ and $f$ applied to $Z$ is equal to $f$ applied to $Y$. Then the costructured arrow isomorphism to costructured arrow of $X$ and $Y_{1}$ is an isomorphism of the costructured arrow of $X$ and $f$ and the composition of the costructured arrow of $\operatorname{mk}$ applied to $X$ and $\operatorname{mk}$ applied to $f$ and $\mathrm{CategoryTheory\_\_Functor\_\_toCostructuredArrowIsoToCostructuredArrow\_\_\_proof\_1}$ applied to $G$, $F$, $X$, $f$ and $h$ and $\operatorname{pre}$ applied to $G$, $F$ and $\operatorname{pt}$ applied to $\operatorname{mk}$ applied to $X$ and $\operatorname{mk}$ applied to $f$ and $\mathrm{CategoryTheory\_\_Functor\_\_toCostructuredArrowIsoToCostructuredArrow\_\_\_proof\_1}$ applied to $G$, $F$, $X$, $f$ and $h$ defined as the function that maps $h$ to the identity of the costructured arrow of $X$ and $Y_{1}$.

the structured arrow isomorphism to structured arrow of F and f (from the name)

Let $G$ be a functor of $J$ and $K$. Let $X$ be an element of $C$. Let $F$ be a functor of $K$ and $C$. Let $f$ be a function from elements $Y_{1}$ of $J$ to homomorphisms of $X$ and the action of $F$ and the action of $G$ and $Y_{1}$ such that for all elements $Y$ and $Z$ of $J$, for all homomorphisms $g$ of $Y$ and $Z$, the composition of $f$ applied to $Y$ and the map of $F$ and the map of $G$ and $g$ is equal to $f$ applied to $Z$. Then the structured arrow isomorphism to structured arrow of $F$ and $Y_{1}$ is an isomorphism of the structured arrow of $F$ and $f$ and the composition of the structured arrow of $\operatorname{mk}$ applied to $X$ and $\operatorname{mk}$ applied to $f$ and $\mathrm{CategoryTheory\_\_Functor\_\_toStructuredArrowIsoToStructuredArrow\_\_\_proof\_1}$ applied to $G$, $X$, $F$, $f$ and $h$ and $\operatorname{pre}$ applied to $\operatorname{pt}$ applied to $\operatorname{mk}$ applied to $X$ and $\operatorname{mk}$ applied to $f$ and $\mathrm{CategoryTheory\_\_Functor\_\_toStructuredArrowIsoToStructuredArrow\_\_\_proof\_1}$ applied to $G$, $X$, $F$, $f$ and $h$, $G$ and $F$ defined as the function that maps $h$ to the identity of the structured arrow of $F$ and $Y_{1}$.

the equivalence structured arrow of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the equivalence structured arrow of $F$ is an equivalence of the set of cocones of $F$ and the set of structured arrows of $F$ and the constant of $J$.

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $J$ and the set of costructured arrows of $F$ and $X$. Then $\operatorname{fromCostructuredArrow}$ applied to $F$ and $G$ is a cocone of the composition of $G$ and the composition of the projection of $F$ and $X$ and $F$.

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

Let $c$ be a cocone of $F$. Then $\operatorname{isColimitEquivIsInitial}$ applied to $c$ is an element of $\EquivMACRoAE {\operatorname{IsColimit} (c)}{\operatorname{IsInitial} (c)}$.

Let $c$ be a cocone of $F$. Then $\operatorname{mapCoconeToOver}$ applied to $c$ is an isomorphism of the map cocone of $\operatorname{forget}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{toOver}$ applied to $c$ and $c$ defined as the identity of the map cocone of $\operatorname{forget}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{toOver}$ applied to $c$.

the costructured arrow of c (from the name)

Let $c$ be a cocone of $F$. Then the costructured arrow of $c$ is a functor of $J$ and the set of costructured arrows of $F$ and $\operatorname{pt}$ applied to $c$.

the costructured arrow cocone of F and f (from the name)

Let $c$ be a cocone of $K$. Let $F$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of the action of $F$ and $\operatorname{pt}$ applied to $c$ and $X$. Then the costructured arrow cocone of $F$ and $f$ is a cocone of the composition of the costructured arrow of the map cocone of $F$ and $c$ and the composition of the map of $f$ and $\operatorname{pre}$ applied to $K$, $F$ and $X$.

the costructured arrow composition projection of c (from the name)

Let $c$ be a cocone of $F$. Then the costructured arrow composition projection of $c$ is an isomorphism of the composition of the costructured arrow of $c$ and the projection of $F$ and $\operatorname{pt}$ applied to $c$ and the identity of $J$ defined as the identity of the composition of the costructured arrow of $c$ and the projection of $F$ and $\operatorname{pt}$ applied to $c$.

Let $c$ be a cocone of $F$. Then $\operatorname{toCostructuredArrowCompToOverCompForget}$ applied to $c$ is an isomorphism of the composition of the costructured arrow of $c$ and the composition of $\operatorname{toOver}$ applied to $F$ and $\operatorname{pt}$ applied to $c$ and $\operatorname{forget}$ applied to $\operatorname{pt}$ applied to $c$ and $F$ defined as the identity of the composition of the costructured arrow of $c$ and the composition of $\operatorname{toOver}$ applied to $F$ and $\operatorname{pt}$ applied to $c$ and $\operatorname{forget}$ applied to $\operatorname{pt}$ applied to $c$.

the costructured arrow isomorphism to costructured arrow of c (from the name)

Let $c$ be a cocone of $F$. Then the costructured arrow isomorphism to costructured arrow of $c$ is an isomorphism of the costructured arrow of $c$ and the costructured arrow of $\operatorname{pt}$ applied to $c$ and $\operatorname{NatTrans}$ applied to the inclusion of $c$ defined as the identity of the costructured arrow of $c$.

Let $c$ be a cocone of $F$. Then $\operatorname{toOver}$ applied to $c$ is a cocone of the composition of the costructured arrow of $c$ and $\operatorname{toOver}$ applied to $F$ and $\operatorname{pt}$ applied to $c$.

the structured arrow of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the structured arrow of $F$ is a functor of the set of cocones of $F$ and the set of structured arrows of $F$ and the constant of $J$.

the equivalence costructured arrow of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the equivalence costructured arrow of $F$ is an equivalence of the set of cones of $F$ and the set of costructured arrows of the constant of $J$ and $F$.

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

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $J$ and the set of structured arrows of $X$ and $F$. Then $\operatorname{fromStructuredArrow}$ applied to $F$ and $G$ is a cone of the composition of $G$ and the composition of the projection of $X$ and $F$ and $F$.

Let $c$ be a cone of $F$. Then $\operatorname{isLimitEquivIsTerminal}$ applied to $c$ is an element of $\EquivMACRoAE {\operatorname{IsLimit} (c)}{\operatorname{IsTerminal} (c)}$.

Let $c$ be a cone of $F$. Then $\operatorname{mapConeToUnder}$ applied to $c$ is an isomorphism of the map cone of $\operatorname{forget}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{toUnder}$ applied to $c$ and $c$ defined as the identity of the map cone of $\operatorname{forget}$ applied to $\operatorname{pt}$ applied to $c$ and $\operatorname{toUnder}$ applied to $c$.

the costructured arrow of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the costructured arrow of $F$ is a functor of the set of cones of $F$ and the set of costructured arrows of the constant of $J$ and $F$.

the structured arrow of c (from the name)

Let $c$ be a cone of $F$. Then the structured arrow of $c$ is a functor of $J$ and the set of structured arrows of $\operatorname{pt}$ applied to $c$ and $F$.

the structured arrow composition projection of c (from the name)

Let $c$ be a cone of $F$. Then the structured arrow composition projection of $c$ is an isomorphism of the composition of the structured arrow of $c$ and the projection of $\operatorname{pt}$ applied to $c$ and $F$ and the identity of $J$ defined as the identity of the composition of the structured arrow of $c$ and the projection of $\operatorname{pt}$ applied to $c$ and $F$.

Let $c$ be a cone of $F$. Then $\operatorname{toStructuredArrowCompToUnderCompForget}$ applied to $c$ is an isomorphism of the composition of the structured arrow of $c$ and the composition of $\operatorname{toUnder}$ applied to $\operatorname{pt}$ applied to $c$ and $F$ and $\operatorname{forget}$ applied to $\operatorname{pt}$ applied to $c$ and $F$ defined as the identity of the composition of the structured arrow of $c$ and the composition of $\operatorname{toUnder}$ applied to $\operatorname{pt}$ applied to $c$ and $F$ and $\operatorname{forget}$ applied to $\operatorname{pt}$ applied to $c$.

the structured arrow cone of F and f (from the name)

Let $c$ be a cone of $K$. Let $F$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of $X$ and the action of $F$ and $\operatorname{pt}$ applied to $c$. Then the structured arrow cone of $F$ and $f$ is a cone of the composition of the structured arrow of the map cone of $F$ and $c$ and the composition of the map of $f$ and $\operatorname{pre}$ applied to $X$, $K$ and $F$.

the structured arrow isomorphism to structured arrow of c (from the name)

Let $c$ be a cone of $F$. Then the structured arrow isomorphism to structured arrow of $c$ is an isomorphism of the structured arrow of $c$ and the structured arrow of $F$ and $\operatorname{NatTrans}$ applied to the projection of $c$ defined as the identity of the structured arrow of $c$.

Let $c$ be a cone of $F$. Then $\operatorname{toUnder}$ applied to $c$ is a cone of the composition of the structured arrow of $c$ and $\operatorname{toUnder}$ applied to $\operatorname{pt}$ applied to $c$ and $F$.

Let $G$ be a functor of the set of cocones of $F$ and the set of cocones of $\mathrm{F'}$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{ofPreservesCoconeInitial}$ applied to $G$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the action of $G$ and $c$ defined as $\operatorname{symm}$ applied to $\operatorname{isColimitEquivIsInitial}$ applied to the action of $G$ and $c$ and $\operatorname{isInitialObj}$ applied to $G$, $c$ and $\operatorname{isColimitEquivIsInitial}$ applied to $c$ and $\mathrm{hc}$.

Let $G$ be a functor of the set of cocones of $F$ and the set of cocones of $\mathrm{F'}$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to the action of $G$ and $c$. Then $\operatorname{ofReflectsCoconeInitial}$ applied to $G$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to $c$ defined as $\operatorname{symm}$ applied to $\operatorname{isColimitEquivIsInitial}$ applied to $c$ and $\operatorname{isInitialOfObj}$ applied to $G$, $c$ and $\operatorname{isColimitEquivIsInitial}$ applied to the action of $G$ and $c$ and $\mathrm{hc}$.

Let $G$ be a functor of the set of cones of $F$ and the set of cones of $\mathrm{F'}$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{ofPreservesConeTerminal}$ applied to $G$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the action of $G$ and $c$ defined as $\operatorname{symm}$ applied to $\operatorname{isLimitEquivIsTerminal}$ applied to the action of $G$ and $c$ and $\operatorname{isTerminalObj}$ applied to $G$, $c$ and $\operatorname{isLimitEquivIsTerminal}$ applied to $c$ and $\mathrm{hc}$.

Let $G$ be a functor of the set of cones of $F$ and the set of cones of $\mathrm{F'}$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to the action of $G$ and $c$. Then $\operatorname{ofReflectsConeTerminal}$ applied to $G$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to $c$ defined as $\operatorname{symm}$ applied to $\operatorname{isLimitEquivIsTerminal}$ applied to $c$ and $\operatorname{isTerminalOfObj}$ applied to $G$, $c$ and $\operatorname{isLimitEquivIsTerminal}$ applied to the action of $G$ and $c$ and $\mathrm{hc}$.

the costructured arrow of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the costructured arrow of $F$ is a functor of $J$ and the set of costructured arrows of $F$ and the colimit of $F$.

Let $F$ be a functor of $J$ and $C$. Then $\operatorname{toOver}$ applied to $F$ is a cocone of the composition of the costructured arrow of $F$ and $\operatorname{toOver}$ applied to $F$ and the colimit of $F$.

the structured arrow of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the structured arrow of $F$ is a functor of $J$ and the set of structured arrows of the limit of $F$ and $F$.

Let $F$ be a functor of $J$ and $C$. Then $\operatorname{toUnder}$ applied to $F$ is a cone of the composition of the structured arrow of $F$ and $\operatorname{toUnder}$ applied to the limit of $F$ and $F$.