Definitions: Mathlib.CategoryTheory, part 4 of 25

free identity of V (from the name)

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

the homomorphism of f (from the name)

Let $f$ be a homomorphism of $v$ and $w$. Then the homomorphism of $f$ is a homomorphism of $\operatorname{mk}$ applied to $v$ and $\operatorname{mk}$ applied to $w$ defined as the map of the quotient functor of $V$ and the path of $f$.

the induction of mk and v (from the name)

Let $\mathrm{mk}$ be a function from elements $v$ of $V$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $v$. Let $x_{1}$ be a free identity of $V$. Then the induction of $v$ and $\mathrm{mk}$ is an element of $\mathrm{motive}$ applied to $x_{1}$ defined as the function that maps $x_{1}$ to $v$ applied to $\operatorname{as}$ applied to $\mathrm{mk}$ and $x_{1}$.

the lift of F (from the name)

Let $F$ be an identity prefunctor of $V$ and $D$. Then the lift of $F$ is a functor of the set of free identities of $V$ and $D$.

the lift of obj and map (from the name)

Let $\mathrm{obj}$ be a function from elements of $V$ to elements of $D$. Let $\mathrm{map}$ be a function from elements $v_{1}$ of $V$ and elements $w$ of $V$ and homomorphisms of $v_{1}$ and $w$ to homomorphisms of $\mathrm{obj}$ applied to $v_{1}$ and $\mathrm{obj}$ applied to $w$ such that for all elements $v$ of $V$, $\mathrm{map}$ applied to $v$, $v$ and the identity morphism of $v$ is equal to the identity morphism of $\mathrm{obj}$ applied to $v$. Then the lift of $\mathrm{obj}$ and $v_{1}$ is a functor of the set of free identities of $V$ and $D$ defined as the function that maps $\mathrm{map}$ and $\mathrm{map\_id}$ to the lift of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\mathrm{obj}$ and the function that maps $x_{2}$ and $x_{3}$ to $v_{1}$ applied to $x_{2}$ and $x_{3}$ and $w$.

Let $v$ be an element of $V$. Then $\operatorname{mk}$ applied to $v$ is a free identity of $V$ defined as the action of the functor of $\operatorname{FreeReflRel}$ applied to $V$ and $v$.

the morphism property homomorphism of V (from the name)

Let $V$ be a set. Then the morphism property homomorphism of $V$ is a morphism property of the set of free identities of $V$ defined as the morphism property of the function that maps $e$ to the homomorphism of $\operatorname{snd}$ applied to $\operatorname{snd}$ applied to $e$.

the quotient functor of V (from the name)

Let $V$ be a set. Then the quotient functor of $V$ is a functor of the set of paths of $V$ and the set of free identities of $V$ defined as the functor of $\operatorname{FreeReflRel}$ applied to $V$.

Let $V$ be a set. Let $X$ and $Y$ be paths of $V$. Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then we can say that $\operatorname{FreeReflRel}$ holds for $V$, $X$, $Y$, $f$ and $g$.

the free identity (from the name)

The free identity is a functor of $\operatorname{ReflQuiv}$ and the set of categories.

the free identity map of F (from the name)

Let $F$ be an identity prefunctor of $V$ and $W$. Then the free identity map of $F$ is a functor of the set of free identities of $V$ and the set of free identities of $W$.

the free identity natural transformation (from the name)

The free identity natural transformation is a homomorphism of the composition of $\operatorname{forgetToQuiv}$ and the free and the free identity.

the free identity of V (from the name)

Let $V$ be a set. Then the free identity of $V$ is an identity prefunctor of $V$ and the set of free identities of $V$.

the functor of F and hyp (from the name)

Let $F$ be a homomorphism of $\operatorname{of}$ applied to $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $C$ and $\operatorname{of}$ applied to $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $D$ such that for all elements $X$, $Y$ and $Z$ of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $C$, for all homomorphisms $f$ of $X$ and $Y$, for all homomorphisms $g$ of $Y$ and $Z$, the map of $\operatorname{toPrefunctor}$ applied to $F$ and the composition of $f$ and $g$ is equal to the composition of the map of $\operatorname{toPrefunctor}$ applied to $F$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $F$ and $g$. Then the functor of $F$ and $\mathrm{hyp}$ is a functor of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $C$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $D$.

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

the adjoint (from the name)

The adjoint is an adjunction of the free identity and $\operatorname{forget}$.

the homomorphism equivalence (from the name)

The homomorphism equivalence is an equivalence from the set of functors of the set of free identities of $V$ and $C$ to the set of identity prefunctors of $V$ and $C$.

$\operatorname{forget}$ is a functor of the set of categories and $\operatorname{ReflQuiv}$.

$\operatorname{forgetToQuiv}$ is a functor of $\operatorname{ReflQuiv}$ and $\operatorname{Quiv}$.

the isomorphism of e and he (from the name)

Let $e$ be an equivalence from $V$ to $W$. Let $\mathrm{he}$ be a function from elements $X_{1}$ of $V$ and elements $Y$ of $V$ to equivalences from the set of homomorphisms of $X_{1}$ and $Y$ to the set of homomorphisms of $e$ applied to $X_{1}$ and $e$ applied to $Y$ such that for all elements $X$ of $V$, $\mathrm{he}$ applied to $X$, $X$ and the identity morphism of $X$ is equal to the identity morphism of $e$ applied to $X$. Then the isomorphism of $e$ and $X_{1}$ is an isomorphism of $\operatorname{of}$ applied to $V$ and $\operatorname{of}$ applied to $W$ defined as the function that maps $\mathrm{he}$ and $\mathrm{h\_id}$ to the isomorphism of the isomorphism of $e$ and $X_{1}$ and $Y$.

the isomorphism of e and h_id (from the name)

Let $e$ be an isomorphism of $\operatorname{of}$ applied to $V$ and $\operatorname{of}$ applied to $W$ such that for all elements $X$ of $V$, the map of the homomorphism of $e$ and the identity morphism of $X$ is equal to the identity morphism of the object of the homomorphism of $e$ and $X$. Then the isomorphism of $e$ and $\mathrm{h\_id}$ is an isomorphism of $\operatorname{of}$ applied to $V$ and $\operatorname{of}$ applied to $W$.

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

the underlying quiver of C (from the docstring)

Let $C$ be an element of $\operatorname{ReflQuiv}$. Then the underlying quiver of $C$ is an element of $\operatorname{Quiv}$ defined as $\operatorname{of}$ applied to $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $C$.

relative category (from the name)

A relative category is a set.

homomorphism of X and Y (from the name)

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

the relation of self (from the name)

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

the graph functor (from the name)

The graph functor is a functor of the set of sets and the set of relative categories.

the opposite equivalence (from the name)

The opposite equivalence is an equivalence of the set of relative categories and the set of opposites of the set of relative categories.

the opposite functor (from the name)

The opposite functor is a functor of the set of relative categories and the set of opposites of the set of relative categories.

the opposite functor (from the name)

The opposite functor is a functor of the set of opposites of the set of relative categories and the set of relative categories.

The elements of $\mathrm{TwoP}$ are a basic type.

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

Let $\mathrm{toTwoPointing}$ be an element of $\mathrm{TwoPointing}$ applied to $X$. Then $\operatorname{of}$ applied to $\mathrm{toTwoPointing}$ is an element of $\mathrm{TwoP}$ defined as $\operatorname{mk}$ applied to $X$ and $\mathrm{toTwoPointing}$.

the swap (from the name)

The swap is a functor of $\mathrm{TwoP}$ and $\mathrm{TwoP}$.

the swap equivalence (from the name)

The swap equivalence is an equivalence of $\mathrm{TwoP}$ and $\mathrm{TwoP}$.

Let $X$ be an element of $\mathrm{TwoP}$. Then $\operatorname{toBipointed}$ applied to $X$ is an element of $\mathrm{Bipointed}$ defined as $\operatorname{Bipointed}$ applied to $\operatorname{toProd}$ applied to $\operatorname{toTwoPointing}$ applied to $X$.

Let $\mathrm{self}$ be an element of $\mathrm{TwoP}$. Then $\operatorname{toTwoPointing}$ applied to $\mathrm{self}$ is an element of $\mathrm{TwoPointing}$ applied to $\operatorname{X}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{toTwoPointing}$ be an element of $\mathrm{TwoPointing}$ applied to $X$. Then $\operatorname{TwoP}$ applied to $\mathrm{toTwoPointing}$ is an element of $\mathrm{TwoP}$ defined as $\operatorname{of}$ applied to $\mathrm{toTwoPointing}$.

the pointed to two first component (from the name)

The pointed to two first component is a functor of the set of pointeds and $\mathrm{TwoP}$.

$\mathrm{pointedToTwoPFstForgetCompBipointedToPointedFstAdjunction}$ is an adjunction of the pointed to two first component and the composition of the forgetful functor of $\mathrm{TwoP}$ and $\mathrm{Bipointed}$ and $\mathrm{bipointedToPointedFst}$.

the pointed to two second component (from the name)

The pointed to two second component is a functor of the set of pointeds and $\mathrm{TwoP}$.

$\mathrm{pointedToTwoPSndForgetCompBipointedToPointedSndAdjunction}$ is an adjunction of the pointed to two second component and the composition of the forgetful functor of $\mathrm{TwoP}$ and $\mathrm{Bipointed}$ and $\mathrm{bipointedToPointedSnd}$.

small category equivalent to D (from the docstring)

Let $D$ be a set. Then a small category equivalent to $D$ is an element of the function that maps $D$ to $\mathrm{ULift}$ applied to $D$.

$\operatorname{down}$ is a functor of the set of small category equivalents to $C$ and $C$.

the equivalence (from the name)

The equivalence is an equivalence of $C$ and the set of small category equivalents to $C$.

$\operatorname{up}$ is a functor of $C$ and the set of small category equivalents to $C$.

$\operatorname{downFunctor}$ is a functor of $\mathrm{ULift}$ applied to $C$ and $C$.

the equivalence (from the name)

The equivalence is an equivalence of $C$ and $\mathrm{ULift}$ applied to $C$.

$\operatorname{upFunctor}$ is a functor of $C$ and $\mathrm{ULift}$ applied to $C$.

lift homomorphism of C (from the name)

Let $C$ be a set. Then a lift homomorphism of $C$ is an element of the function that maps $C$ to $C$.

$\operatorname{down}$ is a functor of the set of lift homomorphisms of $C$ and $C$.

the equivalence (from the name)

The equivalence is an equivalence of $C$ and the set of lift homomorphisms of $C$.

Let $A$ be a lift homomorphism of $C$. Then $\operatorname{objDown}$ applied to $A$ is an element of $C$ defined as $A$.

the object equivalence (from the name)

The object equivalence is an equivalence from $C$ to the set of lift homomorphisms of $C$.

Let $A$ be an element of $C$. Then $\operatorname{objUp}$ applied to $A$ is a lift homomorphism of $C$ defined as $A$.

$\operatorname{up}$ is a functor of $C$ and the set of lift homomorphisms of $C$.

the equivalence of C (from the name)

Let $C$ be a set. Then the equivalence of $C$ is an equivalence of $C$ and the set of lift homomorphisms of $\mathrm{ULift}$ applied to $C$ defined as the composition of the equivalence and the equivalence.

the left equivalence congruence (from the name)

The left equivalence congruence is an equivalence from the set of functors of $C$ and $D$ to the set of functors of $C$ and the set of lift homomorphisms of $\mathrm{ULift}$ applied to $D$.

the object equivalence (from the name)

The object equivalence is an equivalence from $C$ to the set of lift homomorphisms of $\mathrm{ULift}$ applied to $C$ defined as the composition of the inverse of the lift and the object equivalence.

category center of C (from the name)

Let $C$ be a set. Then a category center of $C$ is an element of the function that maps $C$ to the set of ends of the identity of $C$.

the action of the center of x1 and X (from the docstring)

Let $x_{1}$ be a category center of $C$. Let $X$ be an element of $C$. Then the action of the center of $x_{1}$ and $X$ is a homomorphism of $X$ and $X$ defined as the component of $\operatorname{asHom}$ applied to $x_{1}$ and $X$.

the category center of R and C (from the name)

Let $R$ and $C$ be sets. Then the category center of $R$ and $C$ is a ring homomorphism of $R$ and the set of category centers of $C$.

the localization of L and W (from the name)

Let $r$ be a category center of $C$. Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Then the localization of $L$ and $W$ is a category center of $D$ defined as $\operatorname{of}$ applied to the lift natural transformation of the identity of $D$ and the right whisker of $\operatorname{asHom}$ applied to $r$ and $L$.

the morphism of rings of L and W (from the docstring)

Let $L$ be a functor of $C$ and $D$. Let $W$ be a morphism property of $C$. Then the morphism of rings of $L$ and $W$ is a ring homomorphism of the set of category centers of $C$ and the set of category centers of $D$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $r$ to the localization of $L$ and $W$ and $\mathrm{CategoryTheory\_\_CatCenter\_\_localization\_one}$ applied to $L$ and $W$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{CategoryTheory\_\_CatCenter\_\_localization\_mul}$ applied to $x_{4}$, $x_{5}$, $L$ and $W$, $\mathrm{CategoryTheory\_\_CatCenter\_\_localization\_zero}$ applied to $L$ and $W$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{CategoryTheory\_\_CatCenter\_\_localization\_add}$ applied to $x_{6}$, $x_{7}$, $L$ and $W$.

codiscrete of x (from the name)

Let $x$ be a set. Then the codiscretes of $x$ are a basic type.

the adjoint (from the name)

The adjoint is an adjunction of the object and the functor to category.

Let $\mathrm{self}$ be a codiscrete of $x$. Then $\operatorname{as}$ applied to $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the counit application of A and x (from the name)

Let $A$ be a set. Let $x$ be a codiscrete of $A$. Then the counit application of $A$ and $x$ is an element of $A$ defined as $\operatorname{as}$ applied to $x$.

the equivalence functor to codiscrete (from the name)

The equivalence functor to codiscrete is an equivalence from the set of functions from elements of $C$ to elements of $A$ to the set of functors of $C$ and the set of codiscretes of $A$.

the functor of F (from the name)

Let $F$ be a function from elements of $C$ to elements of $A$. Then the functor of $F$ is a functor of $C$ and the set of codiscretes of $A$.

the functor of f (from the name)

Let $f$ be a function from elements of $A$ to elements of $B$. Then the functor of $f$ is a functor of the set of codiscretes of $A$ and the set of codiscretes of $B$ defined as the functor of $\operatorname{comp}$ applied to $f$ and $\operatorname{as}$.

the functor to category (from the name)

The functor to category is a functor of the set of sets and the set of categories.

the underlying function of F and x1 (from the docstring)

Let $F$ be a functor of $C$ and the set of codiscretes of $A$. Let $x_{1}$ be an element of $C$. Then the underlying function of $F$ and $x_{1}$ is an element of $A$ defined as $\operatorname{comp}$ applied to $\operatorname{as}$, $\operatorname{obj}$ applied to $F$ and $x_{1}$.

the isomorphism of x and y (from the name)

Let $x$ and $y$ be codiscretes of $A$. Then the isomorphism of $x$ and $y$ is an isomorphism of $x$ and $y$.

the natural isomorphism (from the name)

The natural isomorphism is an isomorphism of $F$ and $G$.

the natural isomorphism functor (from the name)

The natural isomorphism functor is an isomorphism of $F$ and the functor of $\operatorname{comp}$ applied to $\operatorname{as}$ and $\operatorname{obj}$ applied to $F$ defined as the identity of $F$.

the natural transformation (from the name)

The natural transformation is a homomorphism of $F$ and $G$.

the opposite equivalence of A (from the name)

Let $A$ be a set. Then the opposite equivalence of $A$ is an equivalence of the set of opposites of the set of codiscretes of $A$ and the set of codiscretes of $A$.

the unit application of C (from the name)

Let $C$ be a set. Then the unit application of $C$ is a functor of $C$ and the set of codiscretes of $C$ defined as the functor of $\mathrm{id}$.

the codiscrete equivalence (from the name)

The codiscrete equivalence is an equivalence from the set of codiscretes of $x$ to $x$.

Let $F$ be a functor of $J$ and the set of sets. Then $\operatorname{IsMittagLeffler}$ holds for $F$, if for all elements $j$ of $J$, there exists an element $i$ of $J$, such that there exists a homomorphism $f$ of $i$ and $j$, such that for all elements $k$ of $J$, for all homomorphisms $g$ of $k$ and $j$, the range of $\operatorname{coe}$ applied to the homomorphism of the map of $F$ and $f$ is less than or equal to the range of $\operatorname{coe}$ applied to the homomorphism of the map of $F$ and $g$.

the eventual range of the functor of F and j (from the docstring)

Let $F$ be a functor of $J$ and the set of sets. Let $j$ be an element of $J$. Then the eventual range of the functor of $F$ and $j$ is an element of the power set of the function that maps $X$ to $X$ applied to the action of $F$ and $j$ defined as the intersection of the function that maps $i$ to the intersection of the function that maps $f$ to the range of $\operatorname{coe}$ applied to the homomorphism of the map of $F$ and $f$.

the eventual range of F (from the name)

Let $F$ be a functor of $J$ and the set of sets. Then the eventual range of $F$ is a functor of $J$ and the set of sets.

the eventual range section equivalence of F (from the name)

Let $F$ be a functor of $J$ and the set of sets. Then the eventual range section equivalence of $F$ is an equivalence from the set of elements of the section of the eventual range of $F$ to the set of elements of the section of $F$.

the preimage of F and s (from the name)

Let $F$ be a functor of $J$ and the set of sets. Let $s$ be an element of the power set of the action of $F$ and $i$. Then the preimage of $F$ and $s$ is a functor of $J$ and the set of sets.

Let $f$ be a homomorphism of $W$ and $X$. Let $g$ be a homomorphism of $W$ and $Y$. Let $h$ be a homomorphism of $X$ and $Z$. Let $i$ be a homomorphism of $Y$ and $Z$. Then we can say that $\operatorname{CommSq}$ holds for $f$, $g$, $h$ and $i$.

sq has lifts (from the name)

Assume that $\operatorname{CommSq}$ holds for $f$, $i$, $p$ and $g$. Then we can say that $\mathrm{sq}$ has lifts.

Assume that $\operatorname{CommSq}$ holds for $f$, $i$, $p$ and $g$. Then the elements of $\operatorname{LiftStruct}$ applied to $\mathrm{sq}$ are a basic type.

Let $\mathrm{self}$ be an element of $\operatorname{LiftStruct}$ applied to $\mathrm{sq}$. Then $\operatorname{l}$ applied to $\mathrm{self}$ is a homomorphism of $B$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the opposite of l (from the name)

Let $l$ be an element of $\operatorname{LiftStruct}$ applied to $\mathrm{sq}$. Then the opposite of $l$ is an element of $\operatorname{LiftStruct}$ applied to $\operatorname{op}$ applied to $\mathrm{sq}$.

the opposite equivalence of sq (from the name)

Assume that $\operatorname{CommSq}$ holds for $f$, $i$, $p$ and $g$. Then the opposite equivalence of $\mathrm{sq}$ is an element of $\EquivMACRoAE {\operatorname{LiftStruct} (\mathrm{sq})}{\operatorname{LiftStruct} (\operatorname{op} (\mathrm{sq}))}$.

the opposite of l (from the name)

Let $l$ be an element of $\operatorname{LiftStruct}$ applied to $\mathrm{sq}$. Then the opposite of $l$ is an element of $\operatorname{LiftStruct}$ applied to $\operatorname{unop}$ applied to $\mathrm{sq}$.

the opposite equivalence of sq (from the name)

Assume that $\operatorname{CommSq}$ holds for $f$, $i$, $p$ and $g$. Then the opposite equivalence of $\mathrm{sq}$ is an element of $\EquivMACRoAE {\operatorname{LiftStruct} (\mathrm{sq})}{\operatorname{LiftStruct} (\operatorname{unop} (\mathrm{sq}))}$.

the lift of sq (from the name)

Assume that $\operatorname{CommSq}$ holds for $f$, $i$, $p$ and $g$. Then the lift of $\mathrm{sq}$ is a homomorphism of $B$ and $X$ defined as $\operatorname{l}$ applied to $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_CommSq\_\_HasLift\_\_exists\_lift}$.

arrow of T (from the name)

Let $T$ be a set. Then an arrow of $T$ is an element of the function that maps $T$ to the set of commas of the identity of $T$ and the identity of $T$.

homomorphism of f and g (from the name)

Let $f$ and $g$ be arrows of $T$. Then a homomorphism of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of comma morphisms of $f$ and $g$.

the left part of f (from the docstring)

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

the right part of f (from the docstring)

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

the equivalence of S (from the docstring)

Let $S$ be a set. Then the equivalence of $S$ is an equivalence from the set of arrows of $\operatorname{Discrete}$ applied to $S$ to $S$.

the equivalence sigma of T (from the name)

Let $T$ be a set. Then the equivalence sigma of $T$ is an equivalence from the set of arrows of $T$ to $\Sigma$ applied to the function that maps $X$ to $\Sigma$ applied to the function that maps $Y$ to the set of homomorphisms of $X$ and $Y$.

the homomorphism of X (from the name)

Let $X$ be an arrow of $T$. Then the homomorphism of $X$ is a homomorphism of the left object of $X$ and the right object of $X$ defined as the homomorphism of $X$.

the homomorphism of u and v (from the name)

Let $u$ be a homomorphism of the left object of $f$ and the left object of $g$. Let $v$ be a homomorphism of the right object of $f$ and the right object of $g$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $u$ and the homomorphism of $g$ is equal to the composition of the homomorphism of $f$ and $v$ and $\mathrm{CategoryTheory\_\_Arrow\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $u$ and $v$ is a homomorphism of $f$ and $g$ defined as $\operatorname{mk}$ applied to $u$, $v$ and $w$.

the homomorphism of u and v (from the name)

Let $u$ be a homomorphism of $X$ and $P$. Let $v$ be a homomorphism of $Y$ and $Q$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $u$ and $g$ is equal to the composition of $f$ and $v$ and $\mathrm{CategoryTheory\_\_Arrow\_\_homMk'\_\_\_auto\_1}$. Then the homomorphism of $u$ and $v$ is a homomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $g$ defined as $\operatorname{mk}$ applied to $u$, $v$ and $w$.

the isomorphism of l and r (from the name)

Let $l$ be an isomorphism of the left object of $f$ and the left object of $g$. Let $r$ be an isomorphism of the right object of $f$ and the right object of $g$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $l$ and the homomorphism of $g$ is equal to the composition of the homomorphism of $f$ and the homomorphism of $r$ and $\mathrm{CategoryTheory\_\_Arrow\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $l$ and $r$ is an isomorphism of $f$ and $g$ defined as the isomorphism of $l$ and $r$.

the isomorphism of x1 and x2 (from the name)

Let $f$ be a homomorphism of $W$ and $X$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $x_{1}$ be an isomorphism of $W$ and $Y$. Let $x_{2}$ be an isomorphism of $X$ and $Z$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $x_{1}$ and $g$ is equal to the composition of $f$ and the homomorphism of $x_{2}$ and $\mathrm{CategoryTheory\_\_Arrow\_\_isoMk'\_\_\_auto\_1}$. Then the isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $g$ defined as the isomorphism of $x_{1}$ and $x_{2}$.

the isomorphism of e and f (from the name)

Let $e$ be an isomorphism of $F$ and $G$. Let $f$ be an arrow of $C$. Then the isomorphism of $e$ and $f$ is an isomorphism of the action of the map arrow of $F$ and $f$ and the action of the map arrow of $G$ and $f$.

the left object of X (from the docstring)

Let $X$ be an arrow of $T$. Then the left object of $X$ is an element of $T$ defined as the left subobject of $X$.

the left function (from the name)

The left function is a functor of the set of arrows of $C$ and $C$.

$\operatorname{leftToRight}$ is a homomorphism of the left function and the right function.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{mk}$ applied to $f$ is an arrow of $T$ defined as $\operatorname{mk}$ applied to $X$, $Y$ and $f$.

the right object of X (from the docstring)

Let $X$ be an arrow of $T$. Then the right object of $X$ is an element of $T$ defined as the right subobject of $X$.

the right function (from the name)

The right function is a functor of the set of arrows of $C$ and $C$.

the square to second component of sq (from the name)

Let $\mathrm{sq}$ be a homomorphism of $i$ and $\operatorname{mk}$ applied to the composition of $f$ and $g$. Then the square to second component of $\mathrm{sq}$ is a homomorphism of $i$ and $\operatorname{mk}$ applied to $g$.

the map arrow of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the map arrow of $F$ is a functor of the set of arrows of $C$ and the set of arrows of $D$.

the map arrow equivalence of e (from the name)

Let $e$ be an equivalence of $C$ and $D$. Then the map arrow equivalence of $e$ is an equivalence of the set of arrows of $C$ and the set of arrows of $D$.

the functor of C and D (from the docstring)

Let $C$ and $D$ be sets. Then the functor of $C$ and $D$ is a functor of the set of functors of $C$ and $D$ and the set of functors of the set of arrows of $C$ and the set of arrows of $D$.

comma of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the commas of $L$ and $R$ are a basic type.

the equivalence product of L and R (from the name)

Let $L$ be a functor of $A$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$. Let $R$ be a functor of $B$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$. Then the equivalence product of $L$ and $R$ is an equivalence of the set of commas of $L$ and $R$ and $\mathrm{Prod}$ applied to $A$ and $B$.

Let $L$ be a functor of $A$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$. Let $R$ be a functor of $B$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$. Then $\operatorname{fromProd}$ applied to $L$ and $R$ is a functor of $\mathrm{Prod}$ applied to $A$ and $B$ and the set of commas of $L$ and $R$.

the first component of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the first component of $L$ and $R$ is a functor of the set of commas of $L$ and $R$ and $A$.

the homomorphism of self (from the name)

Let $\mathrm{self}$ be a comma of $L$ and $R$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of the action of $L$ and the left subobject of $\mathrm{self}$ and the action of $R$ and the right subobject of $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the isomorphism of l and r (from the name)

Let $l$ be an isomorphism of the left subobject of $X$ and the left subobject of $Y$. Let $r$ be an isomorphism of the right subobject of $X$ and the right subobject of $Y$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $x_{3}$ and the homomorphism of $l$ and the homomorphism of $Y$ is equal to the composition of the homomorphism of $X$ and the map of $x_{4}$ and the homomorphism of $r$ and $\mathrm{CategoryTheory\_\_Comma\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $l$ and $r$ is an isomorphism of $X$ and $Y$.

the left subobject of self (from the docstring)

Let $\mathrm{self}$ be a comma of $L$ and $R$. Then the left subobject of $\mathrm{self}$ is an element of $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the left isomorphism of x5 (from the name)

Let $x_{5}$ be an isomorphism of $X$ and $Y$. Then the left isomorphism of $x_{5}$ is an isomorphism of the left subobject of $X$ and the left subobject of $Y$ defined as the map isomorphism of the first component of $x_{3}$ and $x_{4}$ and $x_{5}$.

the map of x8 and x9 (from the name)

Let $x_{8}$ be a homomorphism of the composition of $x_{6}$ and $\mathrm{L'}$ and the composition of $L$ and $F$. Let $x_{9}$ be a homomorphism of the composition of $R$ and $F$ and the composition of $x_{7}$ and $\mathrm{R'}$. Then the map of $x_{8}$ and $x_{9}$ is a functor of the set of commas of $L$ and $R$ and the set of commas of $\mathrm{L'}$ and $\mathrm{R'}$.

the map first component of x8 and x9 (from the name)

Let $x_{8}$ be a homomorphism of the composition of $x_{6}$ and $\mathrm{L'}$ and the composition of $L$ and $F$. Let $x_{9}$ be a homomorphism of the composition of $R$ and $F$ and the composition of $x_{7}$ and $\mathrm{R'}$. Then the map first component of $x_{8}$ and $x_{9}$ is an isomorphism of the composition of the map of $x_{8}$ and $x_{9}$ and the first component of $\mathrm{L'}$ and $\mathrm{R'}$ and the composition of the first component of $L$ and $R$ and $x_{6}$.

the left map of R and l (from the name)

Let $R$ be a functor of $B$ and $T$. Let $l$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the left map of $R$ and $l$ is a functor of the set of commas of $x_{4}$ and $R$ and the set of commas of $x_{3}$ and $R$.

the map left composition of l and #3 (from the name)

Let $R$ be a functor of $B$ and $T$. Let $l$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $\mathrm{l'}$ be a homomorphism of $x_{4}$ and $x_{5}$. Then the map left composition of $l$ and $\mathrm{l'}$ is an isomorphism of the left map of $R$ and the composition of $l$ and $\mathrm{l'}$ and the composition of the left map of $R$ and $\mathrm{l'}$ and the left map of $R$ and $l$.

Let $R$ be a functor of $B$ and $T$. Let $l$ and $\mathrm{l'}$ be homomorphisms of $x_{3}$ and $x_{4}$ such that $\EqtMACRoH {l}{\mathrm{l'}}$. Then $\operatorname{mapLeftEq}$ applied to $R$, $l$, $\mathrm{l'}$ and $h$ is an isomorphism of the left map of $R$ and $l$ and the left map of $R$ and $\mathrm{l'}$.

the map left identity of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the map left identity of $L$ and $R$ is an isomorphism of the left map of $R$ and the identity morphism of $L$ and the identity of the set of commas of $L$ and $R$.

the map left isomorphism of R and i (from the name)

Let $R$ be a functor of $B$ and $T$. Let $i$ be an isomorphism of $x_{3}$ and $x_{4}$. Then the map left isomorphism of $R$ and $i$ is an equivalence of the set of commas of $x_{3}$ and $R$ and the set of commas of $x_{4}$ and $R$.

the right map of L and r (from the name)

Let $L$ be a functor of $A$ and $T$. Let $r$ be a homomorphism of $x_{4}$ and $x_{3}$. Then the right map of $L$ and $r$ is a functor of the set of commas of $L$ and $x_{4}$ and the set of commas of $L$ and $x_{3}$.

the map right composition of r and #3 (from the name)

Let $L$ be a functor of $A$ and $T$. Let $r$ be a homomorphism of $x_{4}$ and $x_{3}$. Let $\mathrm{r'}$ be a homomorphism of $x_{5}$ and $x_{4}$. Then the map right composition of $r$ and $\mathrm{r'}$ is an isomorphism of the right map of $L$ and the composition of $\mathrm{r'}$ and $r$ and the composition of the right map of $L$ and $\mathrm{r'}$ and the right map of $L$ and $r$.

Let $L$ be a functor of $A$ and $T$. Let $r$ and $\mathrm{r'}$ be homomorphisms of $x_{4}$ and $x_{3}$ such that $\EqtMACRoH {r}{\mathrm{r'}}$. Then $\operatorname{mapRightEq}$ applied to $L$, $r$, $\mathrm{r'}$ and $h$ is an isomorphism of the right map of $L$ and $r$ and the right map of $L$ and $\mathrm{r'}$.

the map right identity of R and L (from the name)

Let $R$ be a functor of $B$ and $T$. Let $L$ be a functor of $A$ and $T$. Then the map right identity of $R$ and $L$ is an isomorphism of the right map of $L$ and the identity morphism of $R$ and the identity of the set of commas of $L$ and $R$.

the map right isomorphism of L and i (from the name)

Let $L$ be a functor of $A$ and $T$. Let $i$ be an isomorphism of $x_{3}$ and $x_{4}$. Then the map right isomorphism of $L$ and $i$ is an equivalence of the set of commas of $L$ and $x_{3}$ and the set of commas of $L$ and $x_{4}$.

the map second component of x8 and x9 (from the name)

Let $x_{8}$ be a homomorphism of the composition of $x_{7}$ and $\mathrm{L'}$ and the composition of $L$ and $F$. Let $x_{9}$ be a homomorphism of the composition of $R$ and $F$ and the composition of $x_{6}$ and $\mathrm{R'}$. Then the map second component of $x_{8}$ and $x_{9}$ is an isomorphism of the composition of the map of $x_{8}$ and $x_{9}$ and the second component of $\mathrm{L'}$ and $\mathrm{R'}$ and the composition of the second component of $L$ and $R$ and $x_{6}$.

the natural transformation of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the natural transformation of $L$ and $R$ is a homomorphism of the composition of the first component of $L$ and $R$ and $L$ and the composition of the second component of $L$ and $R$ and $R$.

the opposite equivalence of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the opposite equivalence of $L$ and $R$ is an equivalence of the set of commas of $L$ and $R$ and the set of opposites of the set of commas of the opposite of $R$ and the opposite of $L$.

the opposite functor of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the opposite functor of $L$ and $R$ is a functor of the set of commas of $L$ and $R$ and the set of opposites of the set of commas of the opposite of $R$ and the opposite of $L$.

the opposite functor composition first component of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the opposite functor composition first component of $L$ and $R$ is an isomorphism of the composition of the left opposite of the opposite functor of $L$ and $R$ and the first component of the opposite of $R$ and the opposite of $L$ and the opposite of the second component of $L$ and $R$ defined as the identity of the composition of the left opposite of the opposite functor of $L$ and $R$ and the first component of the opposite of $R$ and the opposite of $L$.

the opposite functor composition second component of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the opposite functor composition second component of $L$ and $R$ is an isomorphism of the composition of the left opposite of the opposite functor of $L$ and $R$ and the second component of the opposite of $R$ and the opposite of $L$ and the opposite of the first component of $L$ and $R$ defined as the identity of the composition of the left opposite of the opposite functor of $L$ and $R$ and the second component of the opposite of $R$ and the opposite of $L$.

the post of R and F (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Let $F$ be a functor of $T$ and $C$. Then the post of $R$ and $F$ is a functor of the set of commas of $L$ and $R$ and the set of commas of the composition of $L$ and $F$ and the composition of $R$ and $F$.

the post isomorphism of R and F (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Let $F$ be a functor of $T$ and $C$. Then the post isomorphism of $R$ and $F$ is an isomorphism of the post of $R$ and $F$ and the map of the homomorphism of the left unitor of the composition of $L$ and $F$ and the inverse of the left unitor of the composition of $R$ and $F$.

the left of L and R (from the name)

Let $F$ be a functor of $C$ and $A$. Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the left of $L$ and $R$ is a functor of the set of commas of the composition of $F$ and $L$ and $R$ and the set of commas of $L$ and $R$.

the left isomorphism of L and R (from the name)

Let $F$ be a functor of $C$ and $A$. Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the left isomorphism of $L$ and $R$ is an isomorphism of the left of $L$ and $R$ and the map of the inverse of the right unitor of the composition of $F$ and $L$ and the composition of the homomorphism of the right unitor of $R$ and the inverse of the left unitor of $R$.

the right of F and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $F$ be a functor of $C$ and $B$. Let $R$ be a functor of $B$ and $T$. Then the right of $F$ and $R$ is a functor of the set of commas of $L$ and the composition of $F$ and $R$ and the set of commas of $L$ and $R$.

the right isomorphism of F and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $F$ be a functor of $C$ and $B$. Let $R$ be a functor of $B$ and $T$. Then the right isomorphism of $F$ and $R$ is an isomorphism of the right of $F$ and $R$ and the map of the composition of the homomorphism of the left unitor of $L$ and the inverse of the right unitor of $L$ and the homomorphism of the right unitor of the composition of $F$ and $R$.

the right subobject of self (from the docstring)

Let $\mathrm{self}$ be a comma of $L$ and $R$. Then the right subobject of $\mathrm{self}$ is an element of $B$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the right isomorphism of x5 (from the name)

Let $x_{5}$ be an isomorphism of $X$ and $Y$. Then the right isomorphism of $x_{5}$ is an isomorphism of the right subobject of $X$ and the right subobject of $Y$ defined as the map isomorphism of the second component of $x_{4}$ and $x_{3}$ and $x_{5}$.

the second component of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the second component of $L$ and $R$ is a functor of the set of commas of $L$ and $R$ and $B$.

the identity unit equivalence of L and R (from the name)

Let $L$ be a functor of $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$. Let $R$ be a functor of $B$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$. Then the identity unit equivalence of $L$ and $R$ is an equivalence of the set of commas of $L$ and $R$ and $B$ defined as the composition of the equivalence product of $L$ and $R$ and the left unitor equivalence of $B$.

the unit identity equivalence of L and R (from the name)

Let $L$ be a functor of $A$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$. Let $R$ be a functor of $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$. Then the unit identity equivalence of $L$ and $R$ is an equivalence of the set of commas of $L$ and $R$ and $A$ defined as the composition of the equivalence product of $L$ and $R$ and the right unitor equivalence of $A$.

the opposite functor of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the opposite functor of $L$ and $R$ is a functor of the set of commas of the opposite of $L$ and the opposite of $R$ and the set of opposites of the set of commas of $R$ and $L$.

the opposite functor composition first component of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the opposite functor composition first component of $L$ and $R$ is an isomorphism of the composition of the opposite functor of $L$ and $R$ and the opposite of the first component of $R$ and $L$ and the second component of the opposite of $L$ and the opposite of $R$ defined as the identity of the composition of the opposite functor of $L$ and $R$ and the opposite of the first component of $R$ and $L$.

the opposite functor composition second component of L and R (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Then the opposite functor composition second component of $L$ and $R$ is an isomorphism of the composition of the opposite functor of $L$ and $R$ and the opposite of the second component of $R$ and $L$ and the first component of the opposite of $L$ and the opposite of $R$ defined as the identity of the composition of the opposite functor of $L$ and $R$ and the opposite of the second component of $R$ and $L$.

comma morphism of X and Y (from the name)

Let $X$ and $Y$ be commas of $L$ and $R$. Then the comma morphisms of $X$ and $Y$ are a basic type.

the left of self (from the name)

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

the right of self (from the name)

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

the opposite equivalence of C (from the name)

Let $C$ be a set. Then the opposite equivalence of $C$ is an equivalence from the set of arrows of the set of opposites of $C$ to the set of arrows of $C$.

the shrink equivalence of C (from the name)

Let $C$ be a set. Then the shrink equivalence of $C$ is an equivalence from the set of arrows of the set of shrinks of $C$ to the set of arrows of $C$.

the shrink hom equivalence of C (from the name)

Let $C$ be a set. Then the shrink hom equivalence of $C$ is an equivalence from the set of arrows of the set of shrink homs of $C$ to the set of arrows of $C$.

Let $F$ be a functor of $D$ and $T$. Let $Y$ be an element of $\operatorname{Over}$ applied to $X$. Then $\operatorname{costructuredArrowToOverEquivalence}$ applied to $F$ and $Y$ is an equivalence of the set of costructured arrows of $\operatorname{toOver}$ applied to $F$ and $X$ and $Y$ and the set of costructured arrows of $F$ and the left of $Y$.

the costructured arrow of G and c (from the name)

Let $F$ be a functor of $C$ and $T$. Let $G$ be a functor of $D$ and $T$. Let $c$ be an element of $C$. Then the costructured arrow of $G$ and $c$ is an equivalence of the set of costructured arrows of the first component of $F$ and $G$ and $c$ and the set of commas of the composition of $\operatorname{forget}$ applied to $c$ and $F$ and $G$.

the costructured arrow of G and c (from the name)

Let $F$ be a functor of $C$ and $T$. Let $G$ be a functor of $D$ and $T$. Let $c$ be an element of $C$. Then the costructured arrow of $G$ and $c$ is a functor of the set of costructured arrows of the first component of $F$ and $G$ and $c$ and the set of commas of the composition of $\operatorname{forget}$ applied to $c$ and $F$ and $G$.

the costructured arrow of G and c (from the name)

Let $F$ be a functor of $C$ and $T$. Let $G$ be a functor of $D$ and $T$. Let $c$ be an element of $C$. Then the costructured arrow of $G$ and $c$ is a functor of the set of commas of the composition of $\operatorname{forget}$ applied to $c$ and $F$ and $G$ and the set of costructured arrows of the first component of $F$ and $G$ and $c$.

the costructured arrow of Y and X (from the name)

Let $F$ be a functor of $T$ and $D$. Let $Y$ be an element of $D$. Let $X$ be an element of $T$. Then the costructured arrow of $Y$ and $X$ is an equivalence of the set of costructured arrows of the projection of $F$ and $Y$ and $X$ and the set of costructured arrows of the composition of $\operatorname{forget}$ applied to $X$ and $F$ and $Y$.

the functor of Y and X (from the name)

Let $F$ be a functor of $T$ and $D$. Let $Y$ be an element of $D$. Let $X$ be an element of $T$. Then the functor of $Y$ and $X$ is a functor of the set of costructured arrows of the projection of $F$ and $Y$ and $X$ and the set of costructured arrows of the composition of $\operatorname{forget}$ applied to $X$ and $F$ and $Y$.

the inverse functor of F (from the docstring)

Let $F$ be a functor of $T$ and $D$. Let $Y$ be an element of $D$. Let $X$ be an element of $T$. Then the inverse functor of $F$ is a functor of the set of costructured arrows of the composition of $\operatorname{forget}$ applied to $X$ and $F$ and $Y$ and the set of costructured arrows of the projection of $F$ and $Y$ and $X$.

the costructured arrow of X (from the name)

Let $X$ be an element of $\mathrm{Prod}$ applied to $T$ and $T$. Then the costructured arrow of $X$ is an equivalence of the set of costructured arrows of the diagonal functor of $T$ and $X$ and the set of costructured arrows of $\operatorname{forget}$ applied to $\ProdfstMACRoZ {X}$ and $\ProdsndMACRoAA {X}$.

the costructured arrow of X (from the name)

Let $X$ be an element of $\mathrm{Prod}$ applied to $T$ and $T$. Then the costructured arrow of $X$ is an equivalence of the set of costructured arrows of the diagonal functor of $T$ and $X$ and the set of costructured arrows of $\operatorname{forget}$ applied to $\ProdsndMACRoAA {X}$ and $\ProdfstMACRoZ {X}$ defined as the composition of the costructured arrow of $X$ and the composition of the costructured arrow of $\ProdfstMACRoZ {X}$ and $\ProdsndMACRoAA {X}$ and the map natural isomorphism of the right unitor of $\operatorname{forget}$ applied to $\ProdsndMACRoAA {X}$.

the functor of X (from the name)

Let $X$ be an element of $\mathrm{Prod}$ applied to $T$ and $T$. Then the functor of $X$ is a functor of the set of costructured arrows of the diagonal functor of $T$ and $X$ and the set of costructured arrows of $\operatorname{forget}$ applied to $\ProdfstMACRoZ {X}$ and $\ProdsndMACRoAA {X}$.

the inverse functor of X (from the docstring)

Let $X$ be an element of $\mathrm{Prod}$ applied to $T$ and $T$. Then the inverse functor of $X$ is a functor of the set of costructured arrows of $\operatorname{forget}$ applied to $\ProdfstMACRoZ {X}$ and $\ProdsndMACRoAA {X}$ and the set of costructured arrows of the diagonal functor of $T$ and $X$.

Let $F$ be a functor of $D$ and $T$. Let $X$ be an element of $T$. Then $\operatorname{toOver}$ applied to $F$ and $X$ is a functor of the set of costructured arrows of $F$ and $X$ and $\operatorname{Over}$ applied to $X$ defined as $\operatorname{pre}$ applied to $F$, the identity of $T$ and $X$.

Let $X$ be an element of $T$. Let $F$ be a functor of $T$ and $D$. Let $h$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then $\operatorname{over}$ applied to $X$, $F$ and $h$ is an element of $\operatorname{FullyFaithful}$ applied to the post of $F$.

Let $X$ be an element of $T$. Let $F$ be a functor of $T$ and $D$. Let $h$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then $\operatorname{under}$ applied to $X$, $F$ and $h$ is an element of $\operatorname{FullyFaithful}$ applied to the post of $F$.

Let $F$ be a functor of $S$ and $T$. Let $X$ be an element of $T$. Let $f$ be a function from elements $Y_{1}$ of $S$ to homomorphisms of the action of $F$ and $Y_{1}$ and $X$ such that for all elements $Y$ and $Z$ of $S$, for all homomorphisms $g$ of $Y$ and $Z$, the composition of the map of $F$ and $g$ and $f$ applied to $Z$ is equal to $f$ applied to $Y$. Then $\operatorname{toOver}$ applied to $F$, $X$, $Y_{1}$, $f$ and $h$ is a functor of $S$ and $\operatorname{Over}$ applied to $X$ defined as the function that maps $h$ to the costructured arrow of $X$ and $Y_{1}$.

Let $F$ be a functor of $S$ and $T$. Let $X$ be an element of $T$. Let $f$ be a function from elements $Y_{1}$ of $S$ to homomorphisms of the action of $F$ and $Y_{1}$ and $X$ such that for all elements $Y$ and $Z$ of $S$, for all homomorphisms $g$ of $Y$ and $Z$, the composition of the map of $F$ and $g$ and $f$ applied to $Z$ is equal to $f$ applied to $Y$. Then $\operatorname{toOverCompForget}$ applied to $F$, $X$, $Y_{1}$, $f$ and $h$ is an isomorphism of the composition of $\operatorname{toOver}$ applied to $F$, $X$, $f$ and the function that maps $x_{2}$ and $x_{3}$ to $h$ applied to $x_{2}$ and $x_{3}$ and $\operatorname{forget}$ applied to $X$ and $F$ defined as the function that maps $h$ to the identity of the composition of $\operatorname{toOver}$ applied to $F$, $X$, $Y_{1}$ and the function that maps $x_{2}$ and $x_{3}$ to $f$ applied to $x_{2}$ and $x_{3}$ and $\operatorname{forget}$ applied to $X$.

Let $F$ be a functor of $S$ and $T$. Let $X$ be an element of $T$. Let $f$ be a function from elements $Y_{1}$ of $S$ to homomorphisms of $X$ and the action of $F$ and $Y_{1}$ such that for all elements $Y$ and $Z$ of $S$, for all homomorphisms $g$ of $Y$ and $Z$, the composition of $f$ applied to $Y$ and the map of $F$ and $g$ is equal to $f$ applied to $Z$. Then $\operatorname{toUnder}$ applied to $F$, $X$, $Y_{1}$, $f$ and $h$ is a functor of $S$ and $\operatorname{Under}$ applied to $X$ defined as the function that maps $h$ to the structured arrow of the identity of $T$ and $Y_{1}$.

Let $F$ be a functor of $S$ and $T$. Let $X$ be an element of $T$. Let $f$ be a function from elements $Y_{1}$ of $S$ to homomorphisms of $X$ and the action of $F$ and $Y_{1}$ such that for all elements $Y$ and $Z$ of $S$, for all homomorphisms $g$ of $Y$ and $Z$, the composition of $f$ applied to $Y$ and the map of $F$ and $g$ is equal to $f$ applied to $Z$. Then $\operatorname{toUnderCompForget}$ applied to $F$, $X$, $Y_{1}$, $f$ and $h$ is an isomorphism of the composition of $\operatorname{toUnder}$ applied to $F$, $X$, $f$ and the function that maps $x_{2}$ and $x_{3}$ to $h$ applied to $x_{2}$ and $x_{3}$ and $\operatorname{forget}$ applied to $X$ and $F$ defined as the function that maps $h$ to the identity of the composition of $\operatorname{toUnder}$ applied to $F$, $X$, $Y_{1}$ and the function that maps $x_{2}$ and $x_{3}$ to $f$ applied to $x_{2}$ and $x_{3}$ and $\operatorname{forget}$ applied to $X$.

Let $c$ be a cocone of $D$. Let $j$ be an element of $J$. Then $\operatorname{underPost}$ applied to $c$ and $j$ is a cocone of the post of $D$.

Let $c$ be a cone of $D$. Let $j$ be an element of $J$. Then $\operatorname{overPost}$ applied to $c$ and $j$ is a cone of the post of $D$.

Let $X$ be an element of $T$. Then an element of $\operatorname{Over}$ applied to $X$ is an element of the function that maps $X$ to the set of costructured arrows of the identity of $T$ and $X$.

homomorphism of f and g (from the name)

Let $f$ and $g$ be elements of $\operatorname{Over}$ applied to $X$. Then a homomorphism of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of comma morphisms of $f$ and $g$.

the left of x1 (from the name)

Let $x_{1}$ be a homomorphism of $f$ and $g$. Then the left of $x_{1}$ is a homomorphism of the left of $f$ and the left of $g$ defined as the left of $x_{1}$.

the equivalence of hX (from the name)

Let $\mathrm{hX}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then the equivalence of $\mathrm{hX}$ is an equivalence of $\operatorname{Over}$ applied to $X$ and $T$.

Let $X$ be an element of $T$. Then $\operatorname{forget}$ applied to $X$ is a functor of $\operatorname{Over}$ applied to $X$ and $T$ defined as the first component of the identity of $T$ and $\operatorname{fromPUnit}$ applied to $X$.

the natural cocone over the forgetful functor of X (from the docstring)

Let $X$ be an element of $T$. Then the natural cocone over the forgetful functor of $X$ is a cocone of $\operatorname{forget}$ applied to $X$.

the homomorphism of f (from the name)

Let $f$ be an element of $\operatorname{Over}$ applied to $X$. Then the homomorphism of $f$ is a homomorphism of the left of $f$ and $X$ defined as the homomorphism of $f$.

the homomorphism of f and w (from the name)

Let $f$ be a homomorphism of the left of $U$ and the left of $V$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $f$ and the homomorphism of $V$ is equal to the homomorphism of $U$ and $\mathrm{CategoryTheory\_\_Over\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $f$ and $w$ is a homomorphism of $U$ and $V$ defined as the homomorphism of $f$ and $w$.

Let $D$ be a functor of $J$ and $T$. Let $s$ be a homomorphism of $D$ and the action of the constant of $J$ and $X$. Let $c$ be a cone of $D$. Let $p$ be a homomorphism of $\operatorname{pt}$ applied to $c$ and $X$ such that for all elements $j$ of $J$, the composition of the component of the projection of $c$ and $j$ and the component of $s$ and $j$ is equal to $p$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitLiftCone}$ applied to $D$, $s$, $c$, $p$, $\mathrm{hp}$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the lift cone of $c$ and $p$.

the isomorphism of hl and hw (from the name)

Let $\mathrm{hl}$ be an isomorphism of the left of $f$ and the left of $g$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $\mathrm{hl}$ and the homomorphism of $g$ is equal to the homomorphism of $f$ and $\mathrm{CategoryTheory\_\_Over\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $\mathrm{hl}$ and $\mathrm{hw}$ is an isomorphism of $f$ and $g$ defined as the isomorphism of $\mathrm{hl}$ and $\mathrm{hw}$.

Let $f$ be an element of $\operatorname{Over}$ applied to $X$. Then $\operatorname{iteratedSliceBackward}$ applied to $f$ is a functor of $\operatorname{Over}$ applied to the left of $f$ and $\operatorname{Over}$ applied to $f$.

the iterated slice equivalence of f (from the name)

Let $f$ be an element of $\operatorname{Over}$ applied to $X$. Then the iterated slice equivalence of $f$ is an equivalence of $\operatorname{Over}$ applied to $f$ and $\operatorname{Over}$ applied to the left of $f$.

the iterated slice equivalence over map isomorphism of p (from the name)

Let $p$ be a homomorphism of $f$ and $g$. Then the iterated slice equivalence over map isomorphism of $p$ is an isomorphism of the composition of $\operatorname{iteratedSliceForward}$ applied to $f$ and the composition of the map of the left of $p$ and $\operatorname{iteratedSliceBackward}$ applied to $g$ and the map of $p$.

Let $f$ be an element of $\operatorname{Over}$ applied to $X$. Then $\operatorname{iteratedSliceForward}$ applied to $f$ is a functor of $\operatorname{Over}$ applied to $f$ and $\operatorname{Over}$ applied to the left of $f$.

the iterated slice forward isomorphism post of X and f (from the name)

Let $X$ be an element of $T$. Let $f$ be an element of $\operatorname{Over}$ applied to $X$. Then the iterated slice forward isomorphism post of $X$ and $f$ is an isomorphism of the post of $\operatorname{forget}$ applied to $X$ and $\operatorname{iteratedSliceForward}$ applied to $f$ defined as the identity of the post of $\operatorname{forget}$ applied to $X$.

the iterated slice forward naturality isomorphism of p (from the name)

Let $p$ be a homomorphism of $f$ and $g$. Then the iterated slice forward naturality isomorphism of $p$ is an isomorphism of the composition of $\operatorname{iteratedSliceForward}$ applied to $f$ and the map of the left of $p$ and the composition of the map of $p$ and $\operatorname{iteratedSliceForward}$ applied to $g$ defined as the identity of the composition of $\operatorname{iteratedSliceForward}$ applied to $f$ and the map of the left of $p$.

the left of f (from the name)

Let $f$ be an element of $\operatorname{Over}$ applied to $X$. Then the left of $f$ is an element of $T$ defined as the left subobject of $f$.

the lift of D and s (from the name)

Let $D$ be a functor of $J$ and $T$. Let $s$ be a homomorphism of $D$ and the action of the constant of $J$ and $X$. Then the lift of $D$ and $s$ is a functor of $J$ and $\operatorname{Over}$ applied to $X$.

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

Let $D$ be a functor of $J$ and $T$. Let $s$ be a homomorphism of $D$ and the action of the constant of $J$ and $X$. Let $c$ be a cone of $D$. Let $p$ be a homomorphism of $\operatorname{pt}$ applied to $c$ and $X$ such that for all elements $j$ of $J$, the composition of the component of the projection of $c$ and $j$ and the component of $s$ and $j$ is equal to $p$. Then the lift cone of $c$ and $p$ is a cone of the lift of $D$ and $s$.

the map of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $f$ is a functor of $\operatorname{Over}$ applied to $X$ and $\operatorname{Over}$ applied to $Y$ defined as the right map of the identity of $T$ and the natural transformation of the function that maps $x_{1}$ to $f$.

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

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

Let $f$ and $g$ be homomorphisms of $X$ and $Y$ such that $\EqtMACRoH {f}{g}$. Then the map congruence of $f$ and $g$ is an isomorphism of the map of $f$ and the map of $g$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{mapForget}$ applied to $f$ is an isomorphism of the composition of the map of $f$ and $\operatorname{forget}$ applied to $Y$ and $\operatorname{forget}$ applied to $X$ defined as $\operatorname{eqToIso}$ applied to $\mathrm{CategoryTheory\_\_Over\_\_mapForget\_eq}$ applied to $f$.

the map functor of T (from the name)

Let $T$ be a set. Then the map functor of $T$ is a functor of $T$ and the set of categories.

the map identity of Y (from the name)

Let $Y$ be an element of $T$. Then the map identity of $Y$ is an isomorphism of the map of the identity morphism of $Y$ and the identity of $\operatorname{Over}$ applied to $Y$.

the map isomorphism of f (from the name)

Let $f$ be an isomorphism of $X$ and $Y$. Then the map isomorphism of $f$ is an equivalence of $\operatorname{Over}$ applied to $X$ and $\operatorname{Over}$ applied to $Y$ defined as the map right isomorphism of the identity of $T$ and the natural isomorphism of the function that maps $x_{1}$ to $f$.

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

the identity terminal (from the name)

The identity terminal is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{mk}$ applied to the identity morphism of $X$ defined as the identity costructured arrow.

Let $X$ be an element of $T$. Then $\operatorname{opEquivOpUnder}$ applied to $X$ is an equivalence of $\operatorname{Over}$ applied to $\operatorname{op}$ applied to $X$ and the set of opposites of $\operatorname{Under}$ applied to $X$.

the post of F (from the name)

Let $F$ be a functor of $T$ and $D$. Then the post of $F$ is a functor of $\operatorname{Over}$ applied to $X$ and $\operatorname{Over}$ applied to the action of $F$ and $X$.

the right post adjunction of a (from the name)

Let $a$ be an adjunction of $F$ and $G$. Then the right post adjunction of $a$ is an adjunction of the composition of the post of $F$ and the map of the component of the counit of $a$ and $Y$ and the post of $G$.

the post composition of F and G (from the name)

Let $F$ be a functor of $T$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the post composition of $F$ and $G$ is an isomorphism of the post of the composition of $F$ and $G$ and the composition of the post of $F$ and the post of $G$.

the post congruence of e (from the name)

Let $e$ be an isomorphism of $F$ and $G$. Then the post congruence of $e$ is an isomorphism of the composition of the post of $F$ and the map of the component of the homomorphism of $e$ and $X$ and the post of $G$.

the post equivalence of X and F (from the name)

Let $X$ be an element of $T$. Let $F$ be an equivalence of $T$ and $D$. Then the post equivalence of $X$ and $F$ is an equivalence of $\operatorname{Over}$ applied to $X$ and $\operatorname{Over}$ applied to the action of the functor of $F$ and $X$.

the post map of e (from the name)

Let $e$ be a homomorphism of $F$ and $G$. Then the post map of $e$ is a homomorphism of the composition of the post of $F$ and the map of the component of $e$ and $X$ and the post of $G$.

the structured arrow of G and c (from the name)

Let $F$ be a functor of $C$ and $T$. Let $G$ be a functor of $D$ and $T$. Let $c$ be an element of $C$. Then the structured arrow of $G$ and $c$ is an equivalence of the set of structured arrows of $c$ and the first component of $F$ and $G$ and the set of commas of the composition of $\operatorname{forget}$ applied to $c$ and $F$ and $G$.

the structured arrow of G and c (from the name)

Let $F$ be a functor of $C$ and $T$. Let $G$ be a functor of $D$ and $T$. Let $c$ be an element of $C$. Then the structured arrow of $G$ and $c$ is a functor of the set of structured arrows of $c$ and the first component of $F$ and $G$ and the set of commas of the composition of $\operatorname{forget}$ applied to $c$ and $F$ and $G$.

the structured arrow of G and c (from the name)

Let $F$ be a functor of $C$ and $T$. Let $G$ be a functor of $D$ and $T$. Let $c$ be an element of $C$. Then the structured arrow of $G$ and $c$ is a functor of the set of commas of the composition of $\operatorname{forget}$ applied to $c$ and $F$ and $G$ and the set of structured arrows of $c$ and the first component of $F$ and $G$.

the structured arrow of X (from the name)

Let $X$ be an element of $\mathrm{Prod}$ applied to $T$ and $T$. Then the structured arrow of $X$ is an equivalence of the set of structured arrows of $X$ and the diagonal functor of $T$ and the set of structured arrows of $\ProdsndMACRoAA {X}$ and $\operatorname{forget}$ applied to $\ProdfstMACRoZ {X}$.

the structured arrow of X (from the name)

Let $X$ be an element of $\mathrm{Prod}$ applied to $T$ and $T$. Then the structured arrow of $X$ is an equivalence of the set of structured arrows of $X$ and the diagonal functor of $T$ and the set of structured arrows of $\ProdfstMACRoZ {X}$ and $\operatorname{forget}$ applied to $\ProdsndMACRoAA {X}$ defined as the composition of the structured arrow of $X$ and the composition of the structured arrow of $\ProdfstMACRoZ {X}$ and $\ProdsndMACRoAA {X}$ and the map natural isomorphism of the right unitor of $\operatorname{forget}$ applied to $\ProdsndMACRoAA {X}$.

the functor of X (from the name)

Let $X$ be an element of $\mathrm{Prod}$ applied to $T$ and $T$. Then the functor of $X$ is a functor of the set of structured arrows of $X$ and the diagonal functor of $T$ and the set of structured arrows of $\ProdsndMACRoAA {X}$ and $\operatorname{forget}$ applied to $\ProdfstMACRoZ {X}$.

the inverse functor of X (from the docstring)

Let $X$ be an element of $\mathrm{Prod}$ applied to $T$ and $T$. Then the inverse functor of $X$ is a functor of the set of structured arrows of $\ProdsndMACRoAA {X}$ and $\operatorname{forget}$ applied to $\ProdfstMACRoZ {X}$ and the set of structured arrows of $X$ and the diagonal functor of $T$.

the structured arrow of Y and X (from the name)

Let $F$ be a functor of $D$ and $T$. Let $Y$ be an element of $T$. Let $X$ be an element of $D$. Then the structured arrow of $Y$ and $X$ is an equivalence of the set of structured arrows of $X$ and the projection of $Y$ and $F$ and the set of structured arrows of $Y$ and the composition of $\operatorname{forget}$ applied to $X$ and $F$.

the functor of Y and X (from the name)

Let $F$ be a functor of $D$ and $T$. Let $Y$ be an element of $T$. Let $X$ be an element of $D$. Then the functor of $Y$ and $X$ is a functor of the set of structured arrows of $X$ and the projection of $Y$ and $F$ and the set of structured arrows of $Y$ and the composition of $\operatorname{forget}$ applied to $X$ and $F$.

the inverse functor of F (from the docstring)

Let $F$ be a functor of $D$ and $T$. Let $Y$ be an element of $T$. Let $X$ be an element of $D$. Then the inverse functor of $F$ is a functor of the set of structured arrows of $Y$ and the composition of $\operatorname{forget}$ applied to $X$ and $F$ and the set of structured arrows of $X$ and the projection of $Y$ and $F$.

Let $X$ be an element of $T$. Let $F$ be a functor of $D$ and $T$. Then $\operatorname{toUnder}$ applied to $X$ and $F$ is a functor of the set of structured arrows of $X$ and $F$ and $\operatorname{Under}$ applied to $X$ defined as $\operatorname{pre}$ applied to $X$, $F$ and the identity of $T$.

Let $X$ be an element of $T$. Then an element of $\operatorname{Under}$ applied to $X$ is an element of the function that maps $X$ to the set of structured arrows of $X$ and the identity of $T$.

homomorphism of f and g (from the name)

Let $f$ and $g$ be elements of $\operatorname{Under}$ applied to $X$. Then a homomorphism of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of comma morphisms of $f$ and $g$.

the right of x1 (from the name)

Let $x_{1}$ be a homomorphism of $f$ and $g$. Then the right of $x_{1}$ is a homomorphism of the right of $f$ and the right of $g$ defined as the right of $x_{1}$.

the equivalence of hX (from the name)

Let $\mathrm{hX}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Then the equivalence of $\mathrm{hX}$ is an equivalence of $\operatorname{Under}$ applied to $X$ and $T$.

Let $X$ be an element of $T$. Then $\operatorname{forget}$ applied to $X$ is a functor of $\operatorname{Under}$ applied to $X$ and $T$ defined as the second component of $\operatorname{fromPUnit}$ applied to $X$ and the identity of $T$.

the natural cone over the forgetful functor of X (from the docstring)

Let $X$ be an element of $T$. Then the natural cone over the forgetful functor of $X$ is a cone of $\operatorname{forget}$ applied to $X$.

the homomorphism of f (from the name)

Let $f$ be an element of $\operatorname{Under}$ applied to $X$. Then the homomorphism of $f$ is a homomorphism of $X$ and the right of $f$ defined as the homomorphism of $f$.

the homomorphism of f and w (from the name)

Let $f$ be a homomorphism of the right of $U$ and the right of $V$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $U$ and $f$ is equal to the homomorphism of $V$ and $\mathrm{CategoryTheory\_\_Under\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $f$ and $w$ is a homomorphism of $U$ and $V$ defined as the homomorphism of $f$ and $w$.

Let $D$ be a functor of $J$ and $T$. Let $s$ be a homomorphism of the action of the constant of $J$ and $X$ and $D$. Let $c$ be a cocone of $D$. Let $p$ be a homomorphism of $X$ and $\operatorname{pt}$ applied to $c$ such that for all elements $j$ of $J$, the composition of the component of $s$ and $j$ and the component of the inclusion of $c$ and $j$ is equal to $p$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitLiftCocone}$ applied to $D$, $s$, $c$, $p$, $\mathrm{hp}$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the lift cocone of $c$ and $p$.

the isomorphism of hr and hw (from the name)

Let $\mathrm{hr}$ be an isomorphism of the right of $f$ and the right of $g$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $f$ and the homomorphism of $\mathrm{hr}$ is equal to the homomorphism of $g$ and $\mathrm{CategoryTheory\_\_Under\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $\mathrm{hr}$ and $\mathrm{hw}$ is an isomorphism of $f$ and $g$ defined as the isomorphism of $\mathrm{hr}$ and $\mathrm{hw}$.

the lift of D and s (from the name)

Let $D$ be a functor of $J$ and $T$. Let $s$ be a homomorphism of the action of the constant of $J$ and $X$ and $D$. Then the lift of $D$ and $s$ is a functor of $J$ and $\operatorname{Under}$ applied to $X$.

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

Let $D$ be a functor of $J$ and $T$. Let $s$ be a homomorphism of the action of the constant of $J$ and $X$ and $D$. Let $c$ be a cocone of $D$. Let $p$ be a homomorphism of $X$ and $\operatorname{pt}$ applied to $c$ such that for all elements $j$ of $J$, the composition of the component of $s$ and $j$ and the component of the inclusion of $c$ and $j$ is equal to $p$. Then the lift cocone of $c$ and $p$ is a cocone of the lift of $D$ and $s$.

the map of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $f$ is a functor of $\operatorname{Under}$ applied to $Y$ and $\operatorname{Under}$ applied to $X$ defined as the left map of the identity of $T$ and the natural transformation of the function that maps $x_{1}$ to $f$.

the map 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 map composition of $f$ and $g$ is an isomorphism of the map of the composition of $f$ and $g$ and the composition of the map of $g$ and the map of $f$ defined as $\operatorname{eqToIso}$ applied to $\mathrm{CategoryTheory\_\_Under\_\_mapComp\_eq}$ applied to $f$ and $g$.

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

Let $f$ and $g$ be homomorphisms of $X$ and $Y$ such that $\EqtMACRoH {f}{g}$. Then the map congruence of $f$ and $g$ is an isomorphism of the map of $f$ and the map of $g$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{mapForget}$ applied to $f$ is an isomorphism of the composition of the map of $f$ and $\operatorname{forget}$ applied to $X$ and $\operatorname{forget}$ applied to $Y$ defined as $\operatorname{eqToIso}$ applied to $\mathrm{CategoryTheory\_\_Under\_\_mapForget\_eq}$ applied to $f$.

the map functor of T (from the name)

Let $T$ be a set. Then the map functor of $T$ is a functor of the set of opposites of $T$ and the set of categories.

the map identity of Y (from the name)

Let $Y$ be an element of $T$. Then the map identity of $Y$ is an isomorphism of the map of the identity morphism of $Y$ and the identity of $\operatorname{Under}$ applied to $Y$.

the map isomorphism of f (from the name)

Let $f$ be an isomorphism of $X$ and $Y$. Then the map isomorphism of $f$ is an equivalence of $\operatorname{Under}$ applied to $Y$ and $\operatorname{Under}$ applied to $X$ defined as the map left isomorphism of the identity of $T$ and the natural isomorphism of the function that maps $x_{1}$ to the inverse of $f$.

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

$\operatorname{mkIdInitial}$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{mk}$ applied to the identity morphism of $X$ defined as the identity structured arrow.

Let $X$ be an element of $T$. Then $\operatorname{opEquivOpOver}$ applied to $X$ is an equivalence of $\operatorname{Under}$ applied to $\operatorname{op}$ applied to $X$ and the set of opposites of $\operatorname{Over}$ applied to $X$.

the post of F (from the name)

Let $F$ be a functor of $T$ and $D$. Then the post of $F$ is a functor of $\operatorname{Under}$ applied to $X$ and $\operatorname{Under}$ applied to the action of $F$ and $X$.

the left post adjunction of a (from the name)

Let $a$ be an adjunction of $F$ and $G$. Then the left post adjunction of $a$ is an adjunction of the post of $F$ and the composition of the post of $G$ and the map of the component of the unit of $a$ and $X$.

the post composition of F and G (from the name)

Let $F$ be a functor of $T$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the post composition of $F$ and $G$ is an isomorphism of the post of the composition of $F$ and $G$ and the composition of the post of $F$ and the post of $G$.

the post congruence of e (from the name)

Let $e$ be an isomorphism of $F$ and $G$. Then the post congruence of $e$ is an isomorphism of the post of $F$ and the composition of the post of $G$ and the map of the component of the homomorphism of $e$ and $X$.

the post equivalence of X and F (from the name)

Let $X$ be an element of $T$. Let $F$ be an equivalence of $T$ and $D$. Then the post equivalence of $X$ and $F$ is an equivalence of $\operatorname{Under}$ applied to $X$ and $\operatorname{Under}$ applied to the action of the functor of $F$ and $X$.

the post map of e (from the name)

Let $e$ be a homomorphism of $F$ and $G$. Then the post map of $e$ is a homomorphism of the post of $F$ and the composition of the post of $G$ and the map of the component of $e$ and $X$.

the right of f (from the name)

Let $f$ be an element of $\operatorname{Under}$ applied to $X$. Then the right of $f$ is an element of $T$ defined as the right subobject of $f$.

Let $X$ be an element of $C$. Let $S$ be an element of $\mathrm{semiOutParam}$ applied to $C$. Then we can say that $\operatorname{CanonicallyOverClass}$ holds for $X$ and $S$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $S$ be an element of $C$. Then we can say that $\operatorname{HomIsOver}$ holds for $f$ and $S$.

Let $X$, $Y$ and $S$ be elements of $C$. Then $\operatorname{IsOverTower}$ holds for $X$, $Y$ and $S$, if $\operatorname{HomIsOver}$ holds for $\operatorname{over}$ applied to $X$, $Y$ and $\mathrm{inferInstance}$ and $S$.

Let $S$ be an element of $C$. Let $e$ be an isomorphism of $X$ and $Y$. Then $\operatorname{asOver}$ applied to $S$ and $e$ is an isomorphism of $\operatorname{asOver}$ applied to $X$ and $S$ and $\operatorname{asOver}$ applied to $Y$ and $S$.

Let $X$ and $S$ be elements of $C$. Then we can say that $\operatorname{OverClass}$ holds for $X$ and $S$.

Let $X$ and $S$ be elements of $C$. Then $\operatorname{asOver}$ applied to $X$ and $S$ is an element of $\operatorname{Over}$ applied to $S$ defined as $\operatorname{mk}$ applied to $\operatorname{over}$ applied to $X$, $S$ and $\mathrm{inferInstance}$.

Let $S$ be an element of $C$. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{asOverHom}$ applied to $S$ and $f$ is a homomorphism of $\operatorname{asOver}$ applied to $X$ and $S$ and $\operatorname{asOver}$ applied to $Y$ and $S$ defined as the homomorphism of $f$ and $\mathrm{CategoryTheory\_\_comp\_over}$ applied to $f$ and $S$.

the homomorphism (from the name)

The homomorphism is a homomorphism of $X$ and $S$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $X$ and $S$ be elements of $C$ such that $\mathrm{autoParam}$ holds for $\operatorname{OverClass}$ applied to $X$ and $S$ and $\mathrm{CategoryTheory\_\_over\_\_\_auto\_1}$. Then $\operatorname{over}$ applied to $X$, $S$ and $x_{1}$ is a homomorphism of $X$ and $S$ defined as the homomorphism.

Let $X$ be an element of $C$. Then $\operatorname{forgetAdjStar}$ applied to $X$ is an adjunction of $\operatorname{forget}$ applied to $X$ and the star of $X$ defined as the composition of the adjunction of the inverse of $\operatorname{coalgebraEquivOver}$ applied to $X$ and the adjoint of the product comonad of $X$.

Let $X$ be an element of $C$. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then $\operatorname{forgetMapTerminal}$ applied to $X$ and $\mathrm{hT}$ is an isomorphism of $\operatorname{forget}$ applied to $X$ and the composition of the map of $\operatorname{from}$ applied to $\mathrm{hT}$ and $X$ and the functor of the equivalence of $\mathrm{hT}$.

the map pullback adjoint of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map pullback adjoint of $f$ is an adjunction of the map of $f$ and the pullback of $f$.

the left post adjunction of a (from the name)

Let $a$ be an adjunction of $F$ and $G$. Then the left post adjunction of $a$ is an adjunction of the post of $F$ and the composition of the post of $G$ and the pullback of the component of the unit of $a$ and $X$.

the pullback of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback of $f$ is a functor of $\operatorname{Over}$ applied to $Y$ and $\operatorname{Over}$ applied to $X$.

the pullback 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 pullback composition of $f$ and $g$ is an isomorphism of the pullback of the composition of $f$ and $g$ and the composition of the pullback of $g$ and the pullback of $f$ defined as $\operatorname{conjugateIsoEquiv}$ applied to the map pullback adjoint of the composition of $f$ and $g$, the composition of the map pullback adjoint of $f$ and the map pullback adjoint of $g$ and the inverse of the map composition of $f$ and $g$.

the pullback identity (from the name)

The pullback identity is an isomorphism of the pullback of the identity morphism of $X$ and the identity of $\operatorname{Over}$ applied to $X$ defined as $\operatorname{conjugateIsoEquiv}$ applied to the map pullback adjoint of the identity morphism of $X$, the adjunction between the identity functor and the inverse of the map identity of $X$.

the star of X (from the name)

Let $X$ be an element of $C$. Then the star of $X$ is a functor of $C$ and $\operatorname{Over}$ applied to $X$ defined as the composition of the cofree of the product comonad of $X$ and $\operatorname{coalgebraToOver}$ applied to $X$.

the star pullback isomorphism star of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the star pullback isomorphism star of $f$ is an isomorphism of the composition of the star of $Y$ and the pullback of $f$ and the star of $X$.

Let $X$ be an element of $C$. Then $\operatorname{costar}$ applied to $X$ is a functor of $C$ and $\operatorname{Under}$ applied to $X$ defined as the composition of the free of the coproduct monad of $X$ and $\operatorname{algebraToUnder}$ applied to $X$.

Let $X$ be an element of $C$. Then $\operatorname{costarAdjForget}$ applied to $X$ is an adjunction of $\operatorname{costar}$ applied to $X$ and $\operatorname{forget}$ applied to $X$ defined as the composition of the adjoint of the coproduct monad of $X$ and the adjunction of $\operatorname{algebraEquivUnder}$ applied to $X$.

Let $X$ be an element of $C$. Let $\mathrm{hI}$ be an element of $\operatorname{IsInitial}$ applied to $I$. Then $\operatorname{forgetMapInitial}$ applied to $X$ and $\mathrm{hI}$ is an isomorphism of $\operatorname{forget}$ applied to $X$ and the composition of the map of $\operatorname{to}$ applied to $\mathrm{hI}$ and $X$ and the functor of the equivalence of $\mathrm{hI}$.

the map pushout adjoint of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map pushout adjoint of $f$ is an adjunction of the pushout of $f$ and the map of $f$.

the right post adjunction of a (from the name)

Let $a$ be an adjunction of $F$ and $G$. Then the right post adjunction of $a$ is an adjunction of the composition of the post of $F$ and the pushout of the component of the counit of $a$ and $Y$ and the post of $G$.

the pushout of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the pushout of $f$ is a functor of $\operatorname{Under}$ applied to $X$ and $\operatorname{Under}$ applied to $Y$.

the pushout 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 pushout composition of $f$ and $g$ is an isomorphism of the pushout of the composition of $f$ and $g$ and the composition of the pushout of $f$ and the pushout of $g$ defined as $\operatorname{symm}$ applied to the conjugate isomorphism equivalence of the composition of the map pushout adjoint of $f$ and the map pushout adjoint of $g$ and the map pushout adjoint of the composition of $f$ and $g$ and the inverse of the map composition of $f$ and $g$.

the pushout identity (from the name)

The pushout identity is an isomorphism of the pushout of the identity morphism of $X$ and the identity of $\operatorname{Under}$ applied to $X$ defined as $\operatorname{symm}$ applied to the conjugate isomorphism equivalence of the adjunction between the identity functor and the map pushout adjoint of the identity morphism of $X$ and the inverse of the map identity of $X$.

Let $P$ and $Q$ be morphism properties of $C$. Let $X$ be an element of $C$. Let $h_{4}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Then $\operatorname{overEquivOfIsInitial}$ applied to $P$, $Q$, $X$ and $h_{4}$ is an equivalence of $\operatorname{Over}$ applied to $P$, $Q$ and $X$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$.

Let $P$ and $Q$ be morphism properties of $C$. Let $X$ be an element of $C$. Let $h_{4}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then $\operatorname{underEquivOfIsTerminal}$ applied to $P$, $Q$, $X$ and $h_{4}$ is an equivalence of $\operatorname{Under}$ applied to $P$, $Q$ and $X$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$.

Let $X$ be an element of $C$. Let $h_{1}$ be an element of $\operatorname{IsInitial}$ applied to $X$. Then $\operatorname{overEquivOfIsInitial}$ applied to $X$ and $h_{1}$ is an equivalence of $\operatorname{Over}$ applied to $X$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$.

Let $X$ be an element of $C$. Let $h_{1}$ be an element of $\operatorname{IsTerminal}$ applied to $X$. Then $\operatorname{underEquivOfIsTerminal}$ applied to $X$ and $h_{1}$ is an equivalence of $\operatorname{Under}$ applied to $X$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$.

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{toOverCompCoyoneda}$ applied to $A$ is an isomorphism of the composition of the opposite of $\operatorname{toOver}$ applied to the Yoneda and $A$ and the Coyoneda and the composition of the opposite of the Yoneda and the composition of the Coyoneda and the action of the left whiskering of the set of functors of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets and the set of sets and the functor of $\operatorname{overEquivPresheafCostructuredArrow}$ applied to $A$.

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{toOverCompOverEquivPresheafCostructuredArrow}$ applied to $A$ is an isomorphism of the composition of $\operatorname{toOver}$ applied to the Yoneda and $A$ and the functor of $\operatorname{overEquivPresheafCostructuredArrow}$ applied to $A$ and the Yoneda defined as $\operatorname{toOverYonedaCompRestrictedYoneda}$ applied to $A$.

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Let $T$ be an element of $\operatorname{Over}$ applied to $A$. Then $\operatorname{toOverCompYoneda}$ applied to $A$ and $T$ is an isomorphism of the composition of the opposite of $\operatorname{toOver}$ applied to the Yoneda and $A$ and the action of the Yoneda and $T$ and the composition of the opposite of the Yoneda and the action of the Yoneda and the action of the functor of $\operatorname{overEquivPresheafCostructuredArrow}$ applied to $A$ and $T$.

Let $x_{1}$ be a homomorphism of $F$ and $A$. Let $s$ be a homomorphism of the action of the Yoneda and $X$ and $A$. Let $u$ be an element of the action of $F$ and $\operatorname{op}$ applied to $X$. Then we can say that $\operatorname{MakesOverArrow}$ holds for $x_{1}$, $s$ and $u$.

Let $x_{1}$ be a homomorphism of $F$ and $A$. Let $s$ be a homomorphism of the action of the Yoneda and $X$ and $A$. Then an element of $\operatorname{OverArrows}$ applied to $x_{1}$ and $s$ is an element of the function that maps $x_{1}$ and $s$ to $\SubtypeSet {u}{\operatorname{MakesOverArrow} (x_{1} , s , u)}$.

the costructured arrow isomorphism of s and t (from the name)

Let $s$ and $t$ be costructured arrows of the Yoneda and $A$. Then the costructured arrow isomorphism of $s$ and $t$ is an isomorphism of $\operatorname{OverArrows}$ applied to the homomorphism of $s$ and the homomorphism of $t$ and the set of homomorphisms of $t$ and $s$.

the map of u and x3 (from the name)

Let $u$ be an element of $\operatorname{OverArrows}$ applied to $x_{1}$ and $s$. Let $x_{3}$ be a homomorphism of $F$ and $G$ such that the composition of $x_{3}$ and $x_{2}$ is equal to $x_{1}$. Then the map of $u$ and $x_{3}$ is an element of $\operatorname{OverArrows}$ applied to $x_{2}$ and $s$ defined as $\operatorname{hom}$ applied to the component of $x_{3}$ and $\operatorname{op}$ applied to $X$ and the value of $u$.

the map of u and f (from the name)

Let $u$ be an element of $\operatorname{OverArrows}$ applied to $x_{1}$ and $t$. Let $f$ be a homomorphism of $X$ and $Y$ such that the composition of the map of the Yoneda and $f$ and $t$ is equal to $s$. Then the map of $u$ and $f$ is an element of $\operatorname{OverArrows}$ applied to $x_{1}$ and $s$ defined as $\operatorname{hom}$ applied to the map of $F$ and the opposite in $f$ and the value of $u$.

the value of x2 (from the name)

Let $x_{2}$ be an element of $\operatorname{OverArrows}$ applied to $x_{1}$ and $s$. Then the value of $x_{2}$ is an element of the action of $F$ and $\operatorname{op}$ applied to $X$ defined as $\operatorname{MakesOverArrow}$ applied to $x_{1}$, $s$ and $x_{2}$.

the Yoneda arrow of f and hf (from the name)

Let $f$ be a homomorphism of $X$ and $Y$ such that the composition of the map of the Yoneda and $f$ and $x_{1}$ is equal to $s$. Then the Yoneda arrow of $f$ and $\mathrm{hf}$ is an element of $\operatorname{OverArrows}$ applied to $x_{1}$ and $s$ defined as $f$.

Yoneda collection of F and X (from the name)

Let $F$ be a functor of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets. Let $X$ be an element of $C$. Then a Yoneda collection of $F$ and $X$ is an element of the function that maps $F$ and $X$ to $\Sigma$ applied to the function that maps $s$ to the action of $F$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{symm}$ applied to the Yoneda equivalence and $s$.

the first component of p (from the name)

Let $p$ be a Yoneda collection of $F$ and $X$. Then the first component of $p$ is a homomorphism of the action of the Yoneda and $X$ and $A$ defined as $\operatorname{symm}$ applied to the Yoneda equivalence and $\operatorname{fst}$ applied to $p$.

the map of x1 and x2 (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $G$. Let $x_{2}$ be a Yoneda collection of $F$ and $X$. Then the map of $x_{1}$ and $x_{2}$ is a Yoneda collection of $G$ and $X$ defined as $\operatorname{mk}$ applied to the first component of $x_{2}$ and $\operatorname{hom}$ applied to the component of $x_{1}$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to the first component of $x_{2}$ and the second component of $x_{2}$.

the map of f and p (from the name)

Let $F$ be a functor of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets. Let $f$ be a homomorphism of $X$ and $Y$. Let $p$ be a Yoneda collection of $F$ and $Y$. Then the map of $f$ and $p$ is a Yoneda collection of $F$ and $X$ defined as $\operatorname{mk}$ applied to the composition of the map of the Yoneda and $f$ and the first component of $p$ and $\operatorname{hom}$ applied to the map of $F$ and the opposite in the precomposition of the first component of $p$ and $f$ and the second component of $p$.

Let $s$ be a homomorphism of the action of the Yoneda and $X$ and $A$. Let $x_{1}$ be an element of the action of $F$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $s$. Then $\operatorname{mk}$ applied to $s$ and $x_{1}$ is a Yoneda collection of $F$ and $X$.

the second component of p (from the name)

Let $p$ be a Yoneda collection of $F$ and $X$. Then the second component of $p$ is an element of the action of $F$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to the first component of $p$ defined as $\operatorname{snd}$ applied to $p$.

the Yoneda equivalence first component of p (from the name)

Let $p$ be a Yoneda collection of $F$ and $X$. Then the Yoneda equivalence first component of $p$ is an element of the action of $A$ and $\operatorname{op}$ applied to $X$ defined as $\operatorname{yonedaEquiv}$ applied to the first component of $p$.

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{costructuredArrowPresheafToOver}$ applied to $A$ is a functor of the set of functors of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets and $\operatorname{Over}$ applied to $A$.

the counit of A (from the name)

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Then the counit of $A$ is an isomorphism of the composition of $\operatorname{costructuredArrowPresheafToOver}$ applied to $A$ and the restricted Yoneda of $A$ and the identity of the set of functors of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets.

Let $F$ be a functor of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets. Let $s$ be a costructured arrow of the Yoneda and $A$. Let $x_{1}$ be an element of $\operatorname{OverArrows}$ applied to $\operatorname{yonedaCollectionPresheafToA}$ applied to $F$ and the homomorphism of $s$. Then $\operatorname{counitBackward}$ applied to $F$, $s$ and $x_{1}$ is an element of the action of $F$ and $\operatorname{op}$ applied to $s$.

Let $F$ be a functor of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets. Let $s$ be a costructured arrow of the Yoneda and $A$. Let $x_{1}$ be an element of the action of $F$ and $\operatorname{op}$ applied to $s$. Then $\operatorname{counitForward}$ applied to $F$, $s$ and $x_{1}$ is an element of $\operatorname{OverArrows}$ applied to $\operatorname{yonedaCollectionPresheafToA}$ applied to $F$ and the homomorphism of $s$ defined as $\operatorname{mk}$ applied to the homomorphism of $s$ and $x_{1}$.

the restricted Yoneda of A (from the name)

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Then the restricted Yoneda of $A$ is a functor of $\operatorname{Over}$ applied to $A$ and the set of functors of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets.

the restricted Yoneda object of x1 (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $A$. Then the restricted Yoneda object of $x_{1}$ is a functor of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets.

the restricted Yoneda object map of x3 and h (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$ such that the composition of $x_{3}$ and $x_{2}$ is equal to $x_{1}$. Then the restricted Yoneda object map of $x_{3}$ and $h$ is a homomorphism of the restricted Yoneda object of $x_{1}$ and the restricted Yoneda object of $x_{2}$.

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{toOverYonedaCompRestrictedYoneda}$ applied to $A$ is an isomorphism of the composition of $\operatorname{toOver}$ applied to the Yoneda and $A$ and the restricted Yoneda of $A$ and the Yoneda.

the unit of A (from the name)

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Then the unit of $A$ is an isomorphism of the identity of $\operatorname{Over}$ applied to $A$ and the composition of the restricted Yoneda of $A$ and $\operatorname{costructuredArrowPresheafToOver}$ applied to $A$.

Let $x_{1}$ be a homomorphism of $F$ and $A$. Let $X$ be an element of $C$. Let $x_{2}$ be an element of the action of $F$ and $\operatorname{op}$ applied to $X$. Then $\operatorname{unitBackward}$ applied to $x_{1}$, $X$ and $x_{2}$ is a Yoneda collection of the restricted Yoneda object of $x_{1}$ and $X$ defined as $\operatorname{mk}$ applied to $\operatorname{symm}$ applied to the Yoneda equivalence and $\operatorname{hom}$ applied to the component of $x_{1}$ and $\operatorname{op}$ applied to $X$ and $x_{2}$ and $x_{2}$.

Let $x_{1}$ be a homomorphism of $F$ and $A$. Let $X$ be an element of $C$. Let $x_{2}$ be a Yoneda collection of the restricted Yoneda object of $x_{1}$ and $X$. Then $\operatorname{unitForward}$ applied to $x_{1}$, $X$ and $x_{2}$ is an element of the action of $F$ and $\operatorname{op}$ applied to $X$ defined as the value of the second component of $x_{2}$.

the Yoneda collection functor of A (from the name)

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Then the Yoneda collection functor of $A$ is a functor of the set of functors of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets and the set of functors of the set of opposites of $C$ and the set of sets.

the Yoneda collection presheaf of A and F (from the name)

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Let $F$ be a functor of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets. Then the Yoneda collection presheaf of $A$ and $F$ is a functor of the set of opposites of $C$ and the set of sets.

the Yoneda collection presheaf map of x1 (from the name)

Let $x_{1}$ be a homomorphism of $F$ and $G$. Then the Yoneda collection presheaf map of $x_{1}$ is a homomorphism of the Yoneda collection presheaf of $A$ and $F$ and the Yoneda collection presheaf of $A$ and $G$.

Let $F$ be a functor of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets. Then $\operatorname{yonedaCollectionPresheafToA}$ applied to $F$ is a homomorphism of the Yoneda collection presheaf of $A$ and $F$ and $A$.

Let $A$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{overEquivPresheafCostructuredArrow}$ applied to $A$ is an equivalence of $\operatorname{Over}$ applied to $A$ and the set of functors of the set of opposites of the set of costructured arrows of the Yoneda and $A$ and the set of sets defined as $\operatorname{mk}$ applied to the restricted Yoneda of $A$, $\operatorname{costructuredArrowPresheafToOver}$ applied to $A$, the unit of $A$ and the counit of $A$.

Let $F$ be a functor of $J$ and $\operatorname{Over}$ applied to $A$. Then $\operatorname{toOverCompYonedaColimit}$ applied to $F$ is an isomorphism of the composition of the opposite of $\operatorname{toOver}$ applied to the Yoneda and $A$ and the action of the Yoneda and the colimit of $F$ and the composition of the opposite of $\operatorname{toOver}$ applied to the Yoneda and $A$ and the colimit of the composition of $F$ and the Yoneda defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{toOverCompYoneda}$ applied to $A$ and the colimit of $F$ and the left isomorphism whisker of the opposite of the Yoneda and the map isomorphism of the Yoneda and $\operatorname{preservesColimitIso}$ applied to the functor of $\operatorname{overEquivPresheafCostructuredArrow}$ applied to $A$ and $F$ and the Yoneda Yoneda colimit of the composition of $F$ and the functor of $\operatorname{overEquivPresheafCostructuredArrow}$ applied to $A$ and the left isomorphism whisker of the opposite of the Yoneda and the colimit of the composition of the composition of $F$ and the functor of $\operatorname{overEquivPresheafCostructuredArrow}$ applied to $A$ and the Yoneda and the identity of the composition of the opposite of the Yoneda and the composition of the flip of the composition of the composition of $F$ and the functor of $\operatorname{overEquivPresheafCostructuredArrow}$ applied to $A$ and the Yoneda and the colimit and the right isomorphism whisker of the inverse of $\operatorname{toOverCompCoyoneda}$ applied to $A$ and the composition of the action of the left whiskering of $\operatorname{Over}$ applied to $A$ and the set of sets and $F$ and the colimit and the identity of the composition of the opposite of $\operatorname{toOver}$ applied to the Yoneda and $A$ and the composition of the Coyoneda and the composition of the action of the left whiskering of $\operatorname{Over}$ applied to $A$ and the set of sets and $F$ and the colimit and the left isomorphism whisker of the opposite of $\operatorname{toOver}$ applied to the Yoneda and $A$ and the inverse of the colimit of the composition of $F$ and the Yoneda.

the costructured arrow second component adjunction of R and b (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Let $b$ be an element of $B$. Then the costructured arrow second component adjunction of $R$ and $b$ is an adjunction of the costructured arrow second component projection of $R$ and $b$ and the costructured arrow second component inclusion of $R$ and $b$.

the costructured arrow second component inclusion of R and b (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Let $b$ be an element of $B$. Then the costructured arrow second component inclusion of $R$ and $b$ is a functor of the set of costructured arrows of $L$ and the action of $R$ and $b$ and the set of costructured arrows of the second component of $L$ and $R$ and $b$.

the costructured arrow second component projection of R and b (from the name)

Let $L$ be a functor of $A$ and $T$. Let $R$ be a functor of $B$ and $T$. Let $b$ be an element of $B$. Then the costructured arrow second component projection of $R$ and $b$ is a functor of the set of costructured arrows of the second component of $L$ and $R$ and $b$ and the set of costructured arrows of $L$ and the action of $R$ and $b$.

costructured arrow of S and T (from the name)

Let $S$ be a functor of $C$ and $D$. Let $T$ be an element of $D$. Then a costructured arrow of $S$ and $T$ is an element of the function that maps $S$ and $T$ to the set of commas of $S$ and $\operatorname{fromPUnit}$ applied to $T$.

homomorphism of f and g (from the name)

Let $f$ and $g$ be costructured arrows of $S$ and $T$. Then a homomorphism of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of comma morphisms of $f$ and $g$.

the left of f (from the name)

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

Let $f$ be a costructured arrow of $S$ and $T$. Then an element of $\operatorname{IsUniversal}$ applied to $f$ is an element of the function that maps $f$ to $\operatorname{IsTerminal}$ applied to $f$.

the lift of h and g (from the name)

Let $h$ be an element of $\operatorname{IsUniversal}$ applied to $f$. Let $g$ be a costructured arrow of $S$ and $T$. Then the lift of $h$ and $g$ is a homomorphism of the left object of $g$ and the left object of $f$ defined as the left of $\operatorname{from}$ applied to $h$ and $g$.

Let $f$ be a costructured arrow of $S$ and $T$. Then $\operatorname{eta}$ applied to $f$ is an isomorphism of $f$ and $\operatorname{mk}$ applied to the homomorphism of $f$.

the homomorphism of X (from the name)

Let $X$ be a costructured arrow of $S$ and $T$. Then the homomorphism of $X$ is a homomorphism of the action of $S$ and the left object of $X$ and $T$ defined as the homomorphism of $X$.

the homomorphism of g and w (from the name)

Let $g$ be a homomorphism of the left object of $f$ and the left object of $\mathrm{f'}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $S$ and $g$ and the homomorphism of $\mathrm{f'}$ is equal to the homomorphism of $f$ and $\mathrm{CategoryTheory\_\_CostructuredArrow\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $g$ and $w$ is a homomorphism of $f$ and $\mathrm{f'}$.

the homomorphism of f and g (from the name)

Let $f$ be a costructured arrow of $S$ and $T$. Let $g$ be a homomorphism of $\mathrm{Y'}$ and the left object of $f$. Then the homomorphism of $f$ and $g$ is a homomorphism of $\operatorname{mk}$ applied to the composition of the map of $S$ and $g$ and the homomorphism of $f$ and $f$.

the isomorphism of g and w (from the name)

Let $g$ be an isomorphism of the left object of $f$ and the left object of $\mathrm{f'}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the map of $S$ and the homomorphism of $g$ and the homomorphism of $\mathrm{f'}$ is equal to the homomorphism of $f$ and $\mathrm{CategoryTheory\_\_CostructuredArrow\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $g$ and $w$ is an isomorphism of $f$ and $\mathrm{f'}$.

the left object of X (from the docstring)

Let $X$ be a costructured arrow of $S$ and $T$. Then the left object of $X$ is an element of $C$ defined as the left subobject of $X$.

the map of f (from the name)

Let $f$ be a homomorphism of $T$ and $\mathrm{T'}$. Then the map of $f$ is a functor of the set of costructured arrows of $S$ and $T$ and the set of costructured arrows of $S$ and $\mathrm{T'}$ defined as the right map of $S$ and the map of the constant of $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $f$.

the map isomorphism of i (from the name)

Let $i$ be an isomorphism of $T$ and $\mathrm{T'}$. Then the map isomorphism of $i$ is an equivalence of the set of costructured arrows of $S$ and $T$ and the set of costructured arrows of $S$ and $\mathrm{T'}$ defined as the map right isomorphism of $S$ and the map isomorphism of the constant of $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $i$.

the map natural isomorphism of i (from the name)

Let $i$ be an isomorphism of $S$ and $\mathrm{S'}$. Then the map natural isomorphism of $i$ is an equivalence of the set of costructured arrows of $S$ and $T$ and the set of costructured arrows of $\mathrm{S'}$ and $T$ defined as the map left isomorphism of $\operatorname{fromPUnit}$ applied to $T$ and $i$.

the map of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of the composition of $F$ and $U$ and the composition of $S$ and $G$. Let $x_{5}$ be a homomorphism of the action of $G$ and $T$ and $V$. Then the map of $x_{4}$ and $x_{5}$ is a functor of the set of costructured arrows of $S$ and $T$ and the set of costructured arrows of $U$ and $V$ defined as the map of $x_{4}$ and the natural transformation of the function that maps $x_{6}$ to $x_{5}$.

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

Let $x_{4}$ be a homomorphism of the composition of $F$ and $U$ and the composition of $S$ and $G$. Let $x_{5}$ be a homomorphism of the action of $G$ and $T$ and $V$. Let $x_{8}$ be a homomorphism of the composition of $\mathrm{F'}$ and $S$ and the composition of $R$ and $\mathrm{G'}$. Let $x_{9}$ be a homomorphism of the action of $\mathrm{G'}$ and $X$ and $T$. Then the map composition map isomorphism of $x_{8}$ and $x_{9}$ is an isomorphism of the composition of the map of $x_{8}$ and $x_{9}$ and the map of $x_{4}$ and $x_{5}$ and the map of the composition of the homomorphism of the associator of $F$ and $U$ and the composition of the left whisker of $\mathrm{F'}$ and $x_{4}$ and the composition of the inverse of the associator of $S$ and $G$ and the composition of the right whisker of $x_{8}$ and $G$ and the homomorphism of the associator of $\mathrm{G'}$ and $G$ and the composition of the map of $G$ and $x_{9}$ and $x_{5}$.

the map congruence of x8 and x9 (from the name)

Let $x_{4}$ be a homomorphism of the composition of $F$ and $U$ and the composition of $S$ and $G$. Let $x_{5}$ be a homomorphism of the action of $G$ and $T$ and $V$. Let $x_{6}$ be an isomorphism of $F$ and $\mathrm{F'}$. Let $x_{7}$ be an isomorphism of $G$ and $\mathrm{G'}$. Let $x_{8}$ be a homomorphism of the composition of $\mathrm{F'}$ and $U$ and the composition of $S$ and $\mathrm{G'}$. Let $x_{9}$ be a homomorphism of the action of $\mathrm{G'}$ and $T$ and $V$. Assume that the composition of $x_{4}$ and the left whisker of $S$ and the homomorphism of $x_{7}$ is equal to the composition of the right whisker of the homomorphism of $x_{6}$ and $U$ and $x_{8}$. Assume that $x_{5}$ is equal to the composition of the component of the homomorphism of $x_{7}$ and $T$ and $x_{9}$. Then the map congruence of $x_{8}$ and $x_{9}$ is an isomorphism of the map of $x_{4}$ and $x_{5}$ and the map of $x_{8}$ and $x_{9}$.

the map identity isomorphism of T and x3 (from the name)

Let $x_{2}$ be a homomorphism of the composition of the identity of $C$ and $S$ and the composition of $S$ and the identity of $D$. Let $T$ be an element of $D$. Let $x_{3}$ be a homomorphism of the action of the identity of $D$ and $T$ and $T$. Assume that $\mathrm{autoParam}$ holds for the proposition that $x_{2}$ is equal to the composition of the homomorphism of the left unitor of $S$ and the inverse of the right unitor of $S$ and $\mathrm{CategoryTheory\_\_CostructuredArrow\_\_map\_u2082\_IdIso\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that $x_{3}$ is equal to the identity morphism of the action of the identity of $D$ and $T$ and $\mathrm{CategoryTheory\_\_CostructuredArrow\_\_map\_u2082\_IdIso\_\_\_auto\_3}$. Then the map identity isomorphism of $T$ and $x_{3}$ is an isomorphism of the map of $x_{2}$ and $x_{3}$ and the identity of the set of costructured arrows of $S$ and $T$.

the map isomorphism of x6 and x7 (from the name)

Let $x_{4}$ be a homomorphism of the composition of the functor of $F$ and $U$ and the composition of $S$ and the functor of $G$. Let $x_{5}$ be a homomorphism of the composition of the inverse of $F$ and $S$ and the composition of $U$ and the inverse of $G$ such that the composition of the homomorphism of the left unitor of $S$ and the composition of the inverse of the right unitor of $S$ and the composition of the left whisker of $S$ and the homomorphism of the unit isomorphism of $G$ and the inverse of the associator of the functor of $G$ and the inverse of $G$ is equal to the composition of the right whisker of the homomorphism of the unit isomorphism of $F$ and $S$ and the composition of the homomorphism of the associator of the inverse of $F$ and $S$ and the composition of the left whisker of the functor of $F$ and $x_{5}$ and the composition of the inverse of the associator of $U$ and the inverse of $G$ and the right whisker of $x_{4}$ and the inverse of $G$ and the composition of the left whisker of the inverse of $F$ and $x_{4}$ and the composition of the inverse of the associator of $S$ and the functor of $G$ and the composition of the right whisker of $x_{5}$ and the functor of $G$ and the composition of the homomorphism of the associator of the inverse of $G$ and the functor of $G$ and the left whisker of $U$ and the homomorphism of the counit isomorphism of $G$ is equal to the composition of the inverse of the associator of the functor of $F$ and $U$ and the composition of the right whisker of the homomorphism of the counit isomorphism of $F$ and $U$ and the composition of the homomorphism of the left unitor of $U$ and the inverse of the right unitor of $U$. Let $x_{6}$ be a homomorphism of the action of the functor of $G$ and $T$ and $V$. Let $x_{7}$ be a homomorphism of the action of the inverse of $G$ and $V$ and $T$ such that the composition of the map of the inverse of $G$ and $x_{6}$ and $x_{7}$ is equal to the component of the inverse of the unit isomorphism of $G$ and $T$ and the composition of the map of the functor of $G$ and $x_{7}$ and $x_{6}$ is equal to the component of the homomorphism of the counit isomorphism of $G$ and $V$. Then the map isomorphism of $x_{6}$ and $x_{7}$ is an equivalence of the set of costructured arrows of $S$ and $T$ and the set of costructured arrows of $U$ and $V$.

the map isomorphism equivalence inverse composition projection of e and u (from the name)

Let $T$ be a functor of $C$ and $D$. Let $S$ be a functor of $D$ and $E$. Let $d$ be an element of $D$. Let $e$ be an element of $E$. Let $u$ be a homomorphism of the action of $S$ and $d$ and $e$. Then the map isomorphism equivalence inverse composition projection of $e$ and $u$ is an isomorphism of the map of the identity morphism of the composition of $T$ and $S$ and $u$ and the composition of the inverse of the equivalence of $T$ and $\operatorname{mk}$ applied to $u$ and the projection of $\operatorname{pre}$ applied to $T$, $S$ and $e$ and $\operatorname{mk}$ applied to $u$.

Let $f$ be a homomorphism of the action of $S$ and $Y$ and $T$. Then $\operatorname{mk}$ applied to $f$ is a costructured arrow of $S$ and $T$ defined as $\operatorname{mk}$ applied to $Y$, $\operatorname{mk}$ applied to $\operatorname{unit}$ and $f$.

the identity costructured arrow (from the docstring)

The identity costructured arrow is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{mk}$ applied to the identity morphism of the action of $S$ and $Y$.

the precomposition of f and g (from the name)

Let $f$ be a homomorphism of the action of $S$ and $Y$ and $T$. Let $g$ be a homomorphism of $\mathrm{Y'}$ and $Y$. Then the precomposition of $f$ and $g$ is a homomorphism of $\operatorname{mk}$ applied to the composition of the map of $S$ and $g$ and $f$ and $\operatorname{mk}$ applied to $f$.

the post of G and S (from the name)

Let $F$ be a functor of $B$ and $C$. Let $G$ be a functor of $C$ and $D$. Let $S$ be an element of $C$. Then the post of $G$ and $S$ is a functor of the set of costructured arrows of $F$ and $S$ and the set of costructured arrows of the composition of $F$ and $G$ and the action of $G$ and $S$.

the post isomorphism map of F and G (from the name)

Let $S$ be an element of $C$. Let $F$ be a functor of $B$ and $C$. Let $G$ be a functor of $C$ and $D$. Then the post isomorphism map of $F$ and $G$ is an isomorphism of the post of $G$ and $S$ and the map of the identity morphism of the composition of $F$ and $G$ and the identity morphism of the action of $G$ and $S$.

Let $F$ be a functor of $B$ and $C$. Let $G$ be a functor of $C$ and $D$. Let $S$ be an element of $D$. Then $\operatorname{pre}$ applied to $F$, $G$ and $S$ is a functor of the set of costructured arrows of the composition of $F$ and $G$ and $S$ and the set of costructured arrows of $G$ and $S$ defined as the left of $G$ and $\operatorname{fromPUnit}$ applied to $S$.

the equivalence of F and f (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a costructured arrow of $G$ and $e$. Then the equivalence of $F$ and $f$ is an equivalence of the set of costructured arrows of $\operatorname{pre}$ applied to $F$, $G$ and $e$ and $f$ and the set of costructured arrows of $F$ and the left object of $f$.

the functor of F and f (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a costructured arrow of $G$ and $e$. Then the functor of $F$ and $f$ is a functor of the set of costructured arrows of $\operatorname{pre}$ applied to $F$, $G$ and $e$ and $f$ and the set of costructured arrows of $F$ and the left object of $f$.

the inverse of F and f (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a costructured arrow of $G$ and $e$. Then the inverse of $F$ and $f$ is a functor of the set of costructured arrows of $F$ and the left object of $f$ and the set of costructured arrows of $\operatorname{pre}$ applied to $F$, $G$ and $e$ and $f$.

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

Let $S$ be a functor of $C$ and $D$. Let $\mathrm{S'}$ be a functor of $\mathrm{C'}$ and $\mathrm{D'}$. Let $T$ be an element of $D$. Let $\mathrm{T'}$ be an element of $\mathrm{D'}$. Then the product equivalence of $T$ and $\mathrm{T'}$ is an equivalence of the set of costructured arrows of the product of $S$ and $\mathrm{S'}$ and $\ProdmkMACRoU {T}{\mathrm{T'}}$ and $\mathrm{Prod}$ applied to the set of costructured arrows of $S$ and $T$ and the set of costructured arrows of $\mathrm{S'}$ and $\mathrm{T'}$.

the projection of S and T (from the name)

Let $S$ be a functor of $C$ and $D$. Let $T$ be an element of $D$. Then the projection of $S$ and $T$ is a functor of the set of costructured arrows of $S$ and $T$ and $C$ defined as the first component of $S$ and $\operatorname{fromPUnit}$ applied to $T$.

the structured arrow of F and d (from the name)

Let $F$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Then the structured arrow of $F$ and $d$ is a functor of the set of opposites of the set of costructured arrows of $F$ and $d$ and the set of structured arrows of $\operatorname{op}$ applied to $d$ and the opposite of $F$.

the structured arrow of F and d (from the name)

Let $F$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Then the structured arrow of $F$ and $d$ is a functor of the set of opposites of the set of costructured arrows of the opposite of $F$ and $\operatorname{op}$ applied to $d$ and the set of structured arrows of $d$ and $F$.

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

Let $G$ be a functor of $E$ and $C$. Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $D$. Let $f$ be a function from elements $Y_{1}$ of $E$ 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 $E$, 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 of $X$ and $Y_{1}$ is a functor of $E$ and the set of costructured arrows of $F$ and $X$.

the costructured arrow composition projection of X and f (from the name)

Let $G$ be a functor of $E$ and $C$. Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $D$. Let $f$ be a function from elements $Y_{1}$ of $E$ 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 $E$, 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 composition projection of $X$ and $Y_{1}$ is an isomorphism of the composition of the costructured arrow of $X$ and $f$ and the projection of $F$ and $X$ and $G$ defined as the function that maps $h$ to the identity of the composition of the costructured arrow of $X$ and $Y_{1}$ and the projection of $F$ and $X$.

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

Let $G$ be a functor of $E$ and $C$. Let $X$ be an element of $D$. Let $F$ be a functor of $C$ and $D$. Let $f$ be a function from elements $Y_{1}$ of $E$ 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 $E$, 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 of $F$ and $Y_{1}$ is a functor of $E$ and the set of structured arrows of $X$ and $F$.

the structured arrow composition projection of F and f (from the name)

Let $G$ be a functor of $E$ and $C$. Let $X$ be an element of $D$. Let $F$ be a functor of $C$ and $D$. Let $f$ be a function from elements $Y_{1}$ of $E$ 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 $E$, 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 composition projection of $F$ and $Y_{1}$ is an isomorphism of the composition of the structured arrow of $F$ and $f$ and the projection of $X$ and $F$ and $G$ defined as the function that maps $h$ to the identity of the composition of the structured arrow of $F$ and $Y_{1}$ and the projection of $X$ and $F$.

structured arrow of S and T (from the name)

Let $S$ be an element of $D$. Let $T$ be a functor of $C$ and $D$. Then a structured arrow of $S$ and $T$ is an element of the function that maps $S$ and $T$ to the set of commas of $\operatorname{fromPUnit}$ applied to $S$ and $T$.

homomorphism of f and g (from the name)

Let $f$ and $g$ be structured arrows of $S$ and $T$. Then a homomorphism of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of comma morphisms of $f$ and $g$.

the right of f (from the name)

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

Let $f$ be a structured arrow of $S$ and $T$. Then an element of $\operatorname{IsUniversal}$ applied to $f$ is an element of the function that maps $f$ to $\operatorname{IsInitial}$ applied to $f$.

Let $h$ be an element of $\operatorname{IsUniversal}$ applied to $f$. Let $g$ be a structured arrow of $S$ and $T$. Then $\operatorname{desc}$ applied to $h$ and $g$ is a homomorphism of the right object of $f$ and the right object of $g$ defined as the right of $\operatorname{to}$ applied to $h$ and $g$.

Let $f$ be a structured arrow of $S$ and $T$. Then $\operatorname{eta}$ applied to $f$ is an isomorphism of $f$ and $\operatorname{mk}$ applied to the homomorphism of $f$.

the homomorphism of X (from the name)

Let $X$ be a structured arrow of $S$ and $T$. Then the homomorphism of $X$ is a homomorphism of $S$ and the action of $T$ and the right object of $X$ defined as the homomorphism of $X$.

the homomorphism of g and w (from the name)

Let $g$ be a homomorphism of the right object of $f$ and the right object of $\mathrm{f'}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $f$ and the map of $T$ and $g$ is equal to the homomorphism of $\mathrm{f'}$ and $\mathrm{CategoryTheory\_\_StructuredArrow\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $g$ and $w$ is a homomorphism of $f$ and $\mathrm{f'}$.

the homomorphism of f and g (from the name)

Let $f$ be a structured arrow of $S$ and $T$. Let $g$ be a homomorphism of the right object of $f$ and $\mathrm{Y'}$. Then the homomorphism of $f$ and $g$ is a homomorphism of $f$ and $\operatorname{mk}$ applied to the composition of the homomorphism of $f$ and the map of $T$ and $g$.

the isomorphism of g and w (from the name)

Let $g$ be an isomorphism of the right object of $f$ and the right object of $\mathrm{f'}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $f$ and the map of $T$ and the homomorphism of $g$ is equal to the homomorphism of $\mathrm{f'}$ and $\mathrm{CategoryTheory\_\_StructuredArrow\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $g$ and $w$ is an isomorphism of $f$ and $\mathrm{f'}$.

the map of f (from the name)

Let $f$ be a homomorphism of $S$ and $\mathrm{S'}$. Then the map of $f$ is a functor of the set of structured arrows of $\mathrm{S'}$ and $T$ and the set of structured arrows of $S$ and $T$ defined as the left map of $T$ and the map of the constant of $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $f$.

the map isomorphism of i (from the name)

Let $i$ be an isomorphism of $S$ and $\mathrm{S'}$. Then the map isomorphism of $i$ is an equivalence of the set of structured arrows of $S$ and $T$ and the set of structured arrows of $\mathrm{S'}$ and $T$ defined as the map left isomorphism of $T$ and the map isomorphism of the constant of $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $i$.

the map isomorphism map of f (from the name)

Let $f$ be a homomorphism of $S$ and $\mathrm{S'}$. Then the map isomorphism map of $f$ is an isomorphism of the map of $f$ and the map of $f$ and the identity morphism of $T$.

the map natural isomorphism of i (from the name)

Let $i$ be an isomorphism of $T$ and $\mathrm{T'}$. Then the map natural isomorphism of $i$ is an equivalence of the set of structured arrows of $S$ and $T$ and the set of structured arrows of $S$ and $\mathrm{T'}$ defined as the map right isomorphism of $\operatorname{fromPUnit}$ applied to $S$ and $i$.

the map of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $\mathrm{L'}$ and the action of $G$ and $L$. Let $x_{5}$ be a homomorphism of the composition of $R$ and $G$ and the composition of $F$ and $\mathrm{R'}$. Then the map of $x_{4}$ and $x_{5}$ is a functor of the set of structured arrows of $L$ and $R$ and the set of structured arrows of $\mathrm{L'}$ and $\mathrm{R'}$ defined as the map of the natural transformation of the function that maps $x_{6}$ to $x_{4}$ and $x_{5}$.

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

Let $x_{4}$ be a homomorphism of $\mathrm{L'}$ and the action of $G$ and $L$. Let $x_{5}$ be a homomorphism of the composition of $R$ and $G$ and the composition of $F$ and $\mathrm{R'}$. Let $x_{8}$ be a homomorphism of $L$ and the action of $\mathrm{G'}$ and $\mathrm{L''}$. Let $x_{9}$ be a homomorphism of the composition of $\mathrm{R''}$ and $\mathrm{G'}$ and the composition of $\mathrm{F'}$ and $R$. Then the map composition map isomorphism of $x_{8}$ and $x_{9}$ is an isomorphism of the composition of the map of $x_{8}$ and $x_{9}$ and the map of $x_{4}$ and $x_{5}$ and the map of the composition of $x_{4}$ and the map of $G$ and $x_{8}$ and the composition of the inverse of the associator of $\mathrm{G'}$ and $G$ and the composition of the right whisker of $x_{9}$ and $G$ and the composition of the homomorphism of the associator of $R$ and $G$ and the composition of the left whisker of $\mathrm{F'}$ and $x_{5}$ and the inverse of the associator of $F$ and $\mathrm{R'}$.

the map congruence of x8 and x9 (from the name)

Let $x_{4}$ be a homomorphism of $\mathrm{L'}$ and the action of $G$ and $L$. Let $x_{5}$ be a homomorphism of the composition of $R$ and $G$ and the composition of $F$ and $\mathrm{R'}$. Let $x_{6}$ be an isomorphism of $F$ and $\mathrm{F'}$. Let $x_{7}$ be an isomorphism of $G$ and $\mathrm{G'}$. Let $x_{8}$ be a homomorphism of $\mathrm{L'}$ and the action of $\mathrm{G'}$ and $L$. Let $x_{9}$ be a homomorphism of the composition of $R$ and $\mathrm{G'}$ and the composition of $\mathrm{F'}$ and $\mathrm{R'}$. Assume that $\mathrm{autoParam}$ holds for the proposition that $x_{4}$ is equal to the composition of $x_{8}$ and the component of the inverse of $x_{7}$ and $L$ and $\mathrm{CategoryTheory\_\_StructuredArrow\_\_map\_u2082\_Congr\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{5}$ and the right whisker of the homomorphism of $x_{6}$ and $\mathrm{R'}$ is equal to the composition of the left whisker of $R$ and the homomorphism of $x_{7}$ and $x_{9}$ and $\mathrm{CategoryTheory\_\_StructuredArrow\_\_map\_u2082\_Congr\_\_\_auto\_3}$. Then the map congruence of $x_{8}$ and $x_{9}$ is an isomorphism of the map of $x_{4}$ and $x_{5}$ and the map of $x_{8}$ and $x_{9}$.

the map identity isomorphism of x2 and x3 (from the name)

Let $T$ be an element of $D$. Let $x_{2}$ be a homomorphism of $T$ and the action of the identity of $D$ and $T$. Let $x_{3}$ be a homomorphism of the composition of $R$ and the identity of $D$ and the composition of the identity of $C$ and $R$. Assume that $\mathrm{autoParam}$ holds for the proposition that $x_{2}$ is equal to the identity morphism of $T$ and $\mathrm{CategoryTheory\_\_StructuredArrow\_\_map\_u2082\_IdIso\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that $x_{3}$ is equal to the composition of the homomorphism of the right unitor of $R$ and the inverse of the left unitor of $R$ and $\mathrm{CategoryTheory\_\_StructuredArrow\_\_map\_u2082\_IdIso\_\_\_auto\_3}$. Then the map identity isomorphism of $x_{2}$ and $x_{3}$ is an isomorphism of the map of $x_{2}$ and $x_{3}$ and the identity of the set of structured arrows of $T$ and $R$.

the map isomorphism of x6 and x7 (from the name)

Let $x_{4}$ be a homomorphism of $\mathrm{L'}$ and the action of the functor of $G$ and $L$. Let $x_{5}$ be a homomorphism of $L$ and the action of the inverse of $G$ and $\mathrm{L'}$. Let $x_{6}$ be a homomorphism of the composition of $R$ and the functor of $G$ and the composition of the functor of $F$ and $\mathrm{R'}$. Let $x_{7}$ be a homomorphism of the composition of $\mathrm{R'}$ and the inverse of $G$ and the composition of the inverse of $F$ and $R$. Assume that the composition of $x_{4}$ and the map of the functor of $G$ and $x_{5}$ is equal to the component of the inverse of the counit isomorphism of $G$ and $\mathrm{L'}$. Assume that the composition of $x_{5}$ and the map of the inverse of $G$ and $x_{4}$ is equal to the component of the homomorphism of the unit isomorphism of $G$ and $L$. Assume that the composition of the homomorphism of the right unitor of $R$ and the composition of the inverse of the left unitor of $R$ and the composition of the right whisker of the homomorphism of the unit isomorphism of $F$ and $R$ and the homomorphism of the associator of the inverse of $F$ and $R$ is equal to the composition of the left whisker of $R$ and the homomorphism of the unit isomorphism of $G$ and the composition of the inverse of the associator of the functor of $G$ and the inverse of $G$ and the composition of the right whisker of $x_{6}$ and the inverse of $G$ and the composition of the homomorphism of the associator of $\mathrm{R'}$ and the inverse of $G$ and the left whisker of the functor of $F$ and $x_{7}$. Assume that the composition of the right whisker of $x_{7}$ and the functor of $G$ and the composition of the homomorphism of the associator of $R$ and the functor of $G$ and the composition of the left whisker of the inverse of $F$ and $x_{6}$ and the composition of the inverse of the associator of the functor of $F$ and $\mathrm{R'}$ and the right whisker of the homomorphism of the counit isomorphism of $F$ and $\mathrm{R'}$ is equal to the composition of the homomorphism of the associator of the inverse of $G$ and the functor of $G$ and the composition of the left whisker of $\mathrm{R'}$ and the homomorphism of the counit isomorphism of $G$ and the composition of the homomorphism of the right unitor of $\mathrm{R'}$ and the inverse of the left unitor of $\mathrm{R'}$. Then the map isomorphism of $x_{6}$ and $x_{7}$ is an equivalence of the set of structured arrows of $L$ and $R$ and the set of structured arrows of $\mathrm{L'}$ and $\mathrm{R'}$.

the map isomorphism equivalence inverse composition projection of u and x3 (from the name)

Let $d$ be an element of $D$. Let $e$ be an element of $E$. Let $u$ be a homomorphism of $e$ and the action of $S$ and $d$. Let $x_{3}$ be a homomorphism of the composition of $T$ and $S$ and $\mathrm{T'}$. Then the map isomorphism equivalence inverse composition projection of $u$ and $x_{3}$ is an isomorphism of the map of $u$ and $x_{3}$ and the composition of the inverse of the equivalence of $T$ and $\operatorname{mk}$ applied to $u$ and the composition of the projection of $\operatorname{mk}$ applied to $u$ and $\operatorname{pre}$ applied to $e$, $T$ and $S$ and the map of the identity morphism of $e$ and $x_{3}$.

Let $f$ be a homomorphism of $S$ and the action of $T$ and $Y$. Then $\operatorname{mk}$ applied to $f$ is a structured arrow of $S$ and $T$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{unit}$, $Y$ and $f$.

the identity structured arrow (from the docstring)

The identity structured arrow is an element of $\operatorname{IsInitial}$ applied to $\operatorname{mk}$ applied to the identity morphism of the action of $T$ and $Y$.

the postcomposition of f and g (from the name)

Let $f$ be a homomorphism of $S$ and the action of $T$ and $Y$. Let $g$ be a homomorphism of $Y$ and $\mathrm{Y'}$. Then the postcomposition of $f$ and $g$ is a homomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to the composition of $f$ and the map of $T$ and $g$.

the post of F and G (from the name)

Let $S$ be an element of $C$. Let $F$ be a functor of $B$ and $C$. Let $G$ be a functor of $C$ and $D$. Then the post of $F$ and $G$ is a functor of the set of structured arrows of $S$ and $F$ and the set of structured arrows of the action of $G$ and $S$ and the composition of $F$ and $G$.

the post isomorphism map of F and G (from the name)

Let $S$ be an element of $C$. Let $F$ be a functor of $B$ and $C$. Let $G$ be a functor of $C$ and $D$. Then the post isomorphism map of $F$ and $G$ is an isomorphism of the post of $F$ and $G$ and the map of the identity morphism of the action of $G$ and $S$ and the identity morphism of the composition of $F$ and $G$.

Let $S$ be an element of $D$. Let $F$ be a functor of $B$ and $C$. Let $G$ be a functor of $C$ and $D$. Then $\operatorname{pre}$ applied to $S$, $F$ and $G$ is a functor of the set of structured arrows of $S$ and the composition of $F$ and $G$ and the set of structured arrows of $S$ and $G$ defined as the right of $F$ and $G$.

the equivalence of F and f (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a structured arrow of $e$ and $G$. Then the equivalence of $F$ and $f$ is an equivalence of the set of structured arrows of $f$ and $\operatorname{pre}$ applied to $e$, $F$ and $G$ and the set of structured arrows of the right object of $f$ and $F$.

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

Let $F$ be a functor of $C$ and $D$. Let $f$ be a structured arrow of $e$ and $G$. Then the equivalence functor of $F$ and $f$ is a functor of the set of structured arrows of $f$ and $\operatorname{pre}$ applied to $e$, $F$ and $G$ and the set of structured arrows of the right object of $f$ and $F$.

the equivalence inverse of F and f (from the name)

Let $F$ be a functor of $C$ and $D$. Let $f$ be a structured arrow of $e$ and $G$. Then the equivalence inverse of $F$ and $f$ is a functor of the set of structured arrows of the right object of $f$ and $F$ and the set of structured arrows of $f$ and $\operatorname{pre}$ applied to $e$, $F$ and $G$.

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

Let $S$ be an element of $D$. Let $F$ be a functor of $B$ and $C$. Let $G$ be a functor of $C$ and $D$. Then the isomorphism map of $F$ and $G$ is an isomorphism of $\operatorname{pre}$ applied to $S$, $F$ and $G$ and the map of the identity morphism of $S$ and the identity morphism of the composition of $F$ and $G$.

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

Let $S$ be an element of $D$. Let $\mathrm{S'}$ be an element of $\mathrm{D'}$. Let $T$ be a functor of $C$ and $D$. Let $\mathrm{T'}$ be a functor of $\mathrm{C'}$ and $\mathrm{D'}$. Then the product equivalence of $T$ and $\mathrm{T'}$ is an equivalence of the set of structured arrows of $\ProdmkMACRoU {S}{\mathrm{S'}}$ and the product of $T$ and $\mathrm{T'}$ and $\mathrm{Prod}$ applied to the set of structured arrows of $S$ and $T$ and the set of structured arrows of $\mathrm{S'}$ and $\mathrm{T'}$.

the projection of S and T (from the name)

Let $S$ be an element of $D$. Let $T$ be a functor of $C$ and $D$. Then the projection of $S$ and $T$ is a functor of the set of structured arrows of $S$ and $T$ and $C$ defined as the second component of $\operatorname{fromPUnit}$ applied to $S$ and $T$.

the right object of X (from the docstring)

Let $X$ be a structured arrow of $S$ and $T$. Then the right object of $X$ is an element of $C$ defined as the right subobject of $X$.

the costructured arrow of F and d (from the name)

Let $F$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Then the costructured arrow of $F$ and $d$ is a functor of the set of opposites of the set of structured arrows of $d$ and $F$ and the set of costructured arrows of the opposite of $F$ and $\operatorname{op}$ applied to $d$.

the costructured arrow of F and d (from the name)

Let $F$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Then the costructured arrow of $F$ and $d$ is a functor of the set of opposites of the set of structured arrows of $\operatorname{op}$ applied to $d$ and the opposite of $F$ and the set of costructured arrows of $F$ and $d$.

the costructured arrow opposite equivalence of F and d (from the name)

Let $F$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Then the costructured arrow opposite equivalence of $F$ and $d$ is an equivalence of the set of opposites of the set of costructured arrows of $F$ and $d$ and the set of structured arrows of $\operatorname{op}$ applied to $d$ and the opposite of $F$.

the structured arrow opposite equivalence of F and d (from the name)

Let $F$ be a functor of $C$ and $D$. Let $d$ be an element of $D$. Then the structured arrow opposite equivalence of $F$ and $d$ is an equivalence of the set of opposites of the set of structured arrows of $d$ and $F$ and the set of costructured arrows of the opposite of $F$ and $\operatorname{op}$ applied to $d$.