Definitions: Mathlib.CategoryTheory, part 18 of 25

free monoidal category of C (from the name)

Let $C$ be a set. Then the free monoidal categories of $C$ are a basic type.

homomorphism of x and x1 (from the name)

Let $x$ and $x_{1}$ be free monoidal categories of $C$. Then the homomorphisms of $x$ and $x_{1}$ are a basic type.

the composition of f and g (from the name)

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

Let $\mathrm{ctorIdx}$ be a natural number. Then the elements of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ are a basic type.

the identity of X (from the name)

Let $X$ be a free monoidal category of $C$. Then the identity of $X$ is a homomorphism of $X$ and $X$.

the homomorphism of X (from the name)

Let $X$ be a free monoidal category of $C$. Then the homomorphism of $X$ is a homomorphism of the tensor of the unit and $X$ and $X$.

the inverse of X (from the name)

Let $X$ be a free monoidal category of $C$. Then the inverse of $X$ is a homomorphism of $X$ and the tensor of the unit and $X$.

the tensor of f and g (from the name)

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

the left whisker of X and f (from the name)

Let $X$ be a free monoidal category of $C$. Let $f$ be a homomorphism of $x$ and $x_{1}$. Then the left whisker of $X$ and $f$ is a homomorphism of the tensor of $X$ and $x$ and the tensor of $X$ and $x_{1}$.

the right whisker of f and Y (from the name)

Let $f$ be a homomorphism of $x$ and $x_{1}$. Let $Y$ be a free monoidal category of $C$. Then the right whisker of $f$ and $Y$ is a homomorphism of the tensor of $x$ and $Y$ and the tensor of $x_{1}$ and $Y$.

the homomorphism of Y and Z (from the name)

Let $X$, $Y$ and $Z$ be free monoidal categories of $C$. Then the homomorphism of $Y$ and $Z$ is a homomorphism of the tensor of the tensor of $X$ and $Y$ and $Z$ and the tensor of $X$ and the tensor of $Y$ and $Z$.

the inverse of Y and Z (from the name)

Let $X$, $Y$ and $Z$ be free monoidal categories of $C$. Then the inverse of $Y$ and $Z$ is a homomorphism of the tensor of $X$ and the tensor of $Y$ and $Z$ and the tensor of the tensor of $X$ and $Y$ and $Z$.

the homomorphism of X (from the name)

Let $X$ be a free monoidal category of $C$. Then the homomorphism of $X$ is a homomorphism of the tensor of $X$ and the unit and $X$.

the inverse of X (from the name)

Let $X$ be a free monoidal category of $C$. Then the inverse of $X$ is a homomorphism of $X$ and the tensor of $X$ and the unit.

Let $x$ and $x_{1}$ be homomorphisms of $X$ and $Y$. Then we can say that $\operatorname{HomEquiv}$ holds for $x$ and $x_{1}$.

Assume that $\operatorname{HomEquiv}$ holds for $x$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x$ of $C$ to elements of $\mathrm{motive}$ applied to $\operatorname{of}$ applied to $x$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the unit and $\mathrm{PULift}$ applied to the set of functions from free monoidal categories $x_{1}$ of $C$ and free monoidal categories $x_{2}$ of $C$ to elements of $\mathrm{motive}$ applied to the tensor of $x_{1}$ and $x_{2}$.

the homomorphism of f (from the name)

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

Let $x$ be an element of $C$. Then $\operatorname{of}$ applied to $x$ is a free monoidal category of $C$.

the project of f (from the name)

Let $f$ be a function from elements of $C$ to elements of $D$. Then the project of $f$ is a functor of the set of free monoidal categories of $C$ and $D$.

the tensor of x and x1 (from the name)

Let $x$ and $x_{1}$ be free monoidal categories of $C$. Then the tensor of $x$ and $x_{1}$ is a free monoidal category of $C$.

the unit (from the name)

The unit is a free monoidal category of $C$.

the default (from the name)

The default is a free monoidal category of $C$ defined as the unit.

normal monoidal object of C (from the name)

Let $C$ be a set. Then the normal monoidal objects of $C$ are a basic type.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the unit and $\mathrm{PULift}$ applied to the set of functions from normal monoidal objects $x$ of $C$ and elements $x_{1}$ of $C$ to elements of $\mathrm{motive}$ applied to the tensor of $x$ and $x_{1}$.

the tensor of x and x1 (from the name)

Let $x$ be a normal monoidal object of $C$. Let $x_{1}$ be an element of $C$. Then the tensor of $x$ and $x_{1}$ is a normal monoidal object of $C$.

the unit (from the name)

The unit is a normal monoidal object of $C$.

the normalization functor for the free monoidal category over C (from the docstring)

Let $C$ be a set. Then the normalization functor for the free monoidal category over $C$ is a functor of the set of free monoidal categories of $C$ and $\operatorname{comp}$ applied to $\operatorname{Discrete}$, the set of elements of $\operatorname{NormalMonoidalObject}$ and $C$.

Let $C$ be a set. Then $\operatorname{fullNormalizeIso}$ applied to $C$ is an isomorphism of the identity of the set of free monoidal categories of $C$ and the composition of the normalization functor for the free monoidal category over $C$ and the inclusion.

the inclusion (from the name)

The inclusion is a functor of $\operatorname{comp}$ applied to $\operatorname{Discrete}$, the set of elements of $\operatorname{NormalMonoidalObject}$ and $C$ and the set of free monoidal categories of $C$ defined as the functor of $\operatorname{inclusionObj}$.

Let $C$ be a set. Then $\operatorname{normalize}$ applied to $C$ is a functor of the set of free monoidal categories of $C$ and the set of functors of $\operatorname{comp}$ applied to $\operatorname{Discrete}$, the set of elements of $\operatorname{NormalMonoidalObject}$ and $C$ and $\operatorname{comp}$ applied to $\operatorname{Discrete}$, the set of elements of $\operatorname{NormalMonoidalObject}$ and $C$.

Let $C$ be a set. Then $\operatorname{normalize'}$ applied to $C$ is a functor of the set of free monoidal categories of $C$ and the set of functors of $\operatorname{comp}$ applied to $\operatorname{Discrete}$, the set of elements of $\operatorname{NormalMonoidalObject}$ and $C$ and the set of free monoidal categories of $C$ defined as the composition of $\operatorname{normalize}$ applied to $C$ and the action of the right whiskering of $\operatorname{comp}$ applied to $\operatorname{Discrete}$, the set of elements of $\operatorname{NormalMonoidalObject}$ and $C$ and the set of free monoidal categories of $C$ and the inclusion.

Let $C$ be a set. Then $\operatorname{normalizeIso}$ applied to $C$ is an isomorphism of the tensor function of $C$ and $\operatorname{normalize'}$ applied to $C$.

Let $C$ be a set. Let $X$ be a free monoidal category of $C$. Let $n$ be a normal monoidal object of $C$. Then $\operatorname{normalizeIsoApp'}$ applied to $C$, $X$ and $n$ is an isomorphism of the tensor object of $\operatorname{inclusionObj}$ applied to $n$ and $X$ and $\operatorname{inclusionObj}$ applied to $\operatorname{normalizeObj}$ applied to $X$ and $n$ defined as $\operatorname{brecOn}$ applied to $X$, $\mathrm{CategoryTheory\_\_FreeMonoidalCategory\_\_normalizeIsoApp'\_\_\_f}$ applied to $C$ and $n$.

the tensor function of C (from the name)

Let $C$ be a set. Then the tensor function of $C$ is a functor of the set of free monoidal categories of $C$ and the set of functors of $\operatorname{comp}$ applied to $\operatorname{Discrete}$, the set of elements of $\operatorname{NormalMonoidalObject}$ and $C$ and the set of free monoidal categories of $C$.

adj is monoidal (from the name)

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then we can say that $\mathrm{adj}$ is monoidal.

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then $\operatorname{laxMonoidalEquivOplaxMonoidal}$ applied to $\mathrm{adj}$ is an element of $\EquivMACRoAE {\operatorname{LaxMonoidal} (G)}{\operatorname{OplaxMonoidal} (F)}$.

e is monoidal (from the docstring)

Let $e$ be an equivalence of $C$ and $D$. Then $e$ is monoidal, if the adjunction of $e$ is monoidal.

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

Let $x_{4}$ be an isomorphism of the tensor unity in the monoidal structure of $D$ and the action of $F$ and the tensor unity in the monoidal structure of $C$. Let $x_{5}$ be a function from elements $X_{5}$ of $C$ and elements $Y_{3}$ of $C$ to isomorphisms of the tensor object of the action of $F$ and $X_{5}$ and the action of $F$ and $Y_{3}$ and the action of $F$ and the tensor object of $X_{5}$ and $Y_{3}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $X_{4}$ of $C$, for all elements $Y_{2}$ of $C$, for all homomorphisms $f_{1}$ of $X_{4}$ and $Y_{2}$, for all elements $\mathrm{X'1}$ of $C$, the composition of the inverse of $x_{5}$ applied to $X_{4}$ and $\mathrm{X'1}$ and the right whisker of the map of $F$ and $f_{1}$ and the action of $F$ and $\mathrm{X'1}$ is equal to the composition of the map of $F$ and the right whisker of $f_{1}$ and $\mathrm{X'1}$ and the inverse of $x_{5}$ applied to $Y_{2}$ and $\mathrm{X'1}$ and $\mathrm{CategoryTheory\_\_Functor\_\_CoreMonoidal\_\_mk'\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for the proposition that for all elements $X_{3}$ of $C$, for all elements $Y_{1}$ of $C$, for all elements $\mathrm{X'}$ of $C$, for all homomorphisms $f$ of $X_{3}$ and $Y_{1}$, the composition of the inverse of $x_{5}$ applied to $\mathrm{X'}$ and $X_{3}$ and the left whisker of the action of $F$ and $\mathrm{X'}$ and the map of $F$ and $f$ is equal to the composition of the map of $F$ and the left whisker of $\mathrm{X'}$ and $f$ and the inverse of $x_{5}$ applied to $\mathrm{X'}$ and $Y_{1}$ and $\mathrm{CategoryTheory\_\_Functor\_\_CoreMonoidal\_\_mk'\_\_\_auto\_3}$, $\mathrm{autoParam}$ holds for the proposition that for all elements $X_{2}$ of $C$, for all elements $Y$ of $C$, for all elements $Z$ of $C$, the composition of the inverse of $x_{5}$ applied to the tensor object of $X_{2}$ and $Y$ and $Z$ and the composition of the right whisker of the inverse of $x_{5}$ applied to $X_{2}$ and $Y$ and the action of $F$ and $Z$ and the homomorphism of the associator of the action of $F$ and $Y$ and the action of $F$ and $Z$ is equal to the composition of the map of $F$ and the homomorphism of the associator of $Y$ and $Z$ and the composition of the inverse of $x_{5}$ applied to $X_{2}$ and the tensor object of $Y$ and $Z$ and the left whisker of the action of $F$ and $X_{2}$ and the inverse of $x_{5}$ applied to $Y$ and $Z$ and $\mathrm{CategoryTheory\_\_Functor\_\_CoreMonoidal\_\_mk'\_\_\_auto\_5}$, $\mathrm{autoParam}$ holds for the proposition that for all elements $X_{1}$ of $C$, the inverse of the left unitor of the action of $F$ and $X_{1}$ is equal to the composition of the map of $F$ and the inverse of the left unitor of $X_{1}$ and the composition of the inverse of $x_{5}$ applied to the tensor unity in the monoidal structure of $C$ and $X_{1}$ and the right whisker of the inverse of $x_{4}$ and the action of $F$ and $X_{1}$ and $\mathrm{CategoryTheory\_\_Functor\_\_CoreMonoidal\_\_mk'\_\_\_auto\_7}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $X$ of $C$, the inverse of the right unitor of the action of $F$ and $X$ is equal to the composition of the map of $F$ and the inverse of the right unitor of $X$ and the composition of the inverse of $x_{5}$ applied to $X$ and the tensor unity in the monoidal structure of $C$ and the left whisker of the action of $F$ and $X$ and the inverse of $x_{4}$ and $\mathrm{CategoryTheory\_\_Functor\_\_CoreMonoidal\_\_mk'\_\_\_auto\_9}$. Then $\operatorname{mk'}$ applied to $x_{4}$, $X_{5}$, $Y_{3}$, $x_{5}$, $h$, $h_{1}$, $\mathrm{oplax\_associativity}$, $\mathrm{oplax\_left\_unitality}$ and $\mathrm{oplax\_right\_unitality}$ is an element of $\operatorname{CoreMonoidal}$ applied to $F$.

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{ofLaxMonoidal}$ applied to $F$ is an element of $\operatorname{CoreMonoidal}$ applied to $F$.

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{ofOplaxMonoidal}$ applied to $F$ is an element of $\operatorname{CoreMonoidal}$ applied to $F$.

the isomorphism of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{CoreMonoidal}$ applied to $F$. Then the isomorphism of $\mathrm{self}$ is an isomorphism of the tensor unity in the monoidal structure of $D$ and the action of $F$ and the tensor unity in the monoidal structure of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the isomorphism of X and Y (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{CoreMonoidal}$ applied to $F$. Let $X$ and $Y$ be elements of $C$. Then the isomorphism of $X$ and $Y$ is an isomorphism of the tensor object of the action of $F$ and $X$ and the action of $F$ and $Y$ and the action of $F$ and the tensor object of $X$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $X$ and $Y$.

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

Let $F$ be a functor of $C$ and $D$. Then $\mathrm{CategoryTheory\_\_Functor\_\_LaxMonoidal\_\_\_u3b5\_}$ applied to $F$ is a homomorphism of the tensor unity in the monoidal structure of $D$ and the action of $F$ and the tensor unity in the monoidal structure of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $F$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then $\mathrm{CategoryTheory\_\_Functor\_\_LaxMonoidal\_\_\_u3bc\_}$ applied to $F$, $X$ and $Y$ is a homomorphism of the tensor object of the action of $F$ and $X$ and the action of $F$ and $Y$ and the action of $F$ and the tensor object of $X$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $X$ and $Y$.

F is monoidal (from the docstring)

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

the left commutative tensor of F and X (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then the left commutative tensor of $F$ and $X$ is an isomorphism of the composition of $F$ and the left tensor of the action of $F$ and $X$ and the composition of the left tensor of $X$ and $F$.

the right commutative tensor of F and X (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then the right commutative tensor of $F$ and $X$ is an isomorphism of the composition of $F$ and the right tensor of the action of $F$ and $X$ and the composition of the right tensor of $X$ and $F$.

the isomorphism of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the isomorphism of $F$ is an isomorphism of the tensor unity in the monoidal structure of $D$ and the action of $F$ and the tensor unity in the monoidal structure of $C$.

the isomorphism of X and Y (from the name)

Let $F$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then the isomorphism of $X$ and $Y$ is an isomorphism of the tensor object of the action of $F$ and $X$ and the action of $F$ and $Y$ and the action of $F$ and the tensor object of $X$ and $Y$.

the tensorator as a natural isomorphism of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the tensorator as a natural isomorphism of $F$ is an isomorphism of the composition of the product of $F$ and $F$ and the tensor of $D$ and the composition of the tensor of $C$ and $F$.

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

Let $F$ be a functor of $C$ and $D$. Let $X$ and $Y$ be elements of $C$. Then $\mathrm{CategoryTheory\_\_Functor\_\_OplaxMonoidal\_\_\_u3b4\_}$ applied to $F$, $X$ and $Y$ is a homomorphism of the action of $F$ and the tensor object of $X$ and $Y$ and the tensor object of the action of $F$ and $X$ and the action of $F$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $X$ and $Y$.

Let $F$ be a functor of $C$ and $D$. Then $\mathrm{CategoryTheory\_\_Functor\_\_OplaxMonoidal\_\_\_u3b7\_}$ applied to $F$ is a homomorphism of the action of $F$ and the tensor unity in the monoidal structure of $C$ and the tensor unity in the monoidal structure of $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $C$ and $D$ be sets. Then the elements of $\operatorname{LaxMonoidalFunctor}$ applied to $C$ and $D$ are a basic type.

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{of}$ applied to $F$ is an element of $\operatorname{LaxMonoidalFunctor}$ applied to $C$ and $D$ defined as $\operatorname{mk}$ applied to $F$ and $\mathrm{inferInstance}$.

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

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $x_{4}$ be a homomorphism of $\mathrm{F'}$ and $\mathrm{G'}$. Then the tensor homomorphism of $x_{3}$ and $x_{4}$ is a homomorphism of the tensor object of $F$ and $\mathrm{F'}$ and the tensor object of $G$ and $\mathrm{G'}$.

the tensor object of F and G (from the name)

Let $F$ and $G$ be functors of $C$ and $D$. Then the tensor object of $F$ and $G$ is a functor of $C$ and $D$.

the left whisker of F and x3 (from the name)

Let $F$ be a functor of $C$ and $D$. Let $x_{3}$ be a homomorphism of $\mathrm{F'}$ and $\mathrm{G'}$. Then the left whisker of $F$ and $x_{3}$ is a homomorphism of the tensor object of $F$ and $\mathrm{F'}$ and the tensor object of $F$ and $\mathrm{G'}$.

the right whisker of x3 and #2 (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $\mathrm{F'}$ be a functor of $C$ and $D$. Then the right whisker of $x_{3}$ and $\mathrm{F'}$ is a homomorphism of the tensor object of $F$ and $\mathrm{F'}$ and the tensor object of $G$ and $\mathrm{F'}$.

additive group of C (from the name)

Let $C$ be a set. Then the additive groups of $C$ are a basic type.

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

Let $C$ be a set. Then $\operatorname{forget}$ applied to $C$ is a functor of the set of additive groups of $C$ and $C$ defined as the composition of $\mathrm{CategoryTheory\_\_AddGrp\_\_forget\_u2082\_Mon}$ applied to $C$ and $\operatorname{forget}$ applied to $C$.

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_AddGrp\_\_forget\_u2082\_Mon}$ applied to $C$ is a functor of the set of additive groups of $C$ and the set of additive monoids of $C$ defined as the induced functor of $\operatorname{toAddMon}$.

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_AddGrp\_\_fullyFaithfulForget\_u2082\_Mon}$ applied to $C$ is an element of $\operatorname{FullyFaithful}$ applied to $\mathrm{CategoryTheory\_\_AddGrp\_\_forget\_u2082\_Mon}$ applied to $C$ defined as the induced functor of $\operatorname{toAddMon}$.

the homomorphism of f (from the name)

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

the homomorphism of f (from the name)

Let $f$ be a homomorphism of the additive monoid of $A$ and the additive monoid of $B$. Then the homomorphism of $f$ is a homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to $f$.

the homomorphism of f (from the name)

Let $f$ be a homomorphism of $\operatorname{X}$ applied to $A$ and $\operatorname{X}$ applied to $B$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the zero morphism and $f$ is equal to the zero morphism and $\mathrm{CategoryTheory\_\_AddGrp\_\_homMk''\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the sum and $f$ is equal to the composition of the tensor homomorphism of $f$ and $f$ and the sum and $\mathrm{CategoryTheory\_\_AddGrp\_\_homMk''\_\_\_auto\_3}$. Then the homomorphism of $f$ is a homomorphism of $A$ and $B$ defined as the homomorphism of $f$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $\operatorname{X}$ applied to $G$ and $\operatorname{X}$ applied to $H$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the zero morphism and the homomorphism of $e$ is equal to the zero morphism and $\mathrm{CategoryTheory\_\_AddGrp\_\_mkIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the sum and the homomorphism of $e$ is equal to the composition of the tensor homomorphism of the homomorphism of $e$ and the homomorphism of $e$ and the sum and $\mathrm{CategoryTheory\_\_AddGrp\_\_mkIso\_\_\_auto\_3}$. Then the isomorphism of $e$ is an isomorphism of $G$ and $H$ defined as the isomorphism of $e$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $G$ and $H$. Then the isomorphism of $e$ is an isomorphism of $\operatorname{mk}$ applied to $G$ and $\operatorname{mk}$ applied to $H$ defined as the unique isomorphism of $\mathrm{CategoryTheory\_\_AddGrp\_\_fullyFaithfulForget\_u2082\_Mon}$ applied to $C$ and the isomorphism of $e$.

the additive group of f (from the name)

Let $f$ be a homomorphism of $A$ and $B$. Then the additive group of $f$ is a homomorphism of $\operatorname{mk}$ applied to $A$ and $\operatorname{mk}$ applied to $B$ defined as the homomorphism of $f$.

the additive monoid of A (from the name)

Let $A$ be an additive group of $C$. Then the additive monoid of $A$ is an additive monoid of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{X}$ applied to $A$.

the trivial additive group object of C (from the docstring)

Let $C$ be a set. Then the trivial additive group object of $C$ is an additive group of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{X}$ applied to the trivial additive monoid object of $C$.

X is a additive group object (from the name)

Let $X$ be an element of $C$. Then we can say that $X$ is an additive group object.

Let $f$ be a homomorphism of the tensor unity in the monoidal structure of $C$ and $A$. Then $\operatorname{addRight}$ applied to $f$ is an isomorphism of $A$ and $A$.

the negation (from the docstring)

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

the map additive group of a (from the name)

Let $a$ be an adjunction of $F$ and $G$. Then the map additive group of $a$ is an adjunction of the map additive group of $F$ and the map additive group of $G$.

the map group of a (from the name)

Let $a$ be an adjunction of $F$ and $G$. Then the map group of $a$ is an adjunction of the map group of $F$ and the map group of $G$.

the map additive group of e (from the name)

Let $e$ be an equivalence of $C$ and $D$. Then the map additive group of $e$ is an equivalence of the set of additive groups of $C$ and the set of additive groups of $D$.

the map group of e (from the name)

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

the map additive group of hF (from the name)

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the map additive group of $\mathrm{hF}$ is an element of $\operatorname{FullyFaithful}$ applied to the map additive group of $F$.

the map group of hF (from the name)

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the map group of $\mathrm{hF}$ is an element of $\operatorname{FullyFaithful}$ applied to the map group of $F$.

the map additive group of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the map additive group of $F$ is a functor of the set of additive groups of $C$ and the set of additive groups of $D$.

the composition functor (from the docstring)

The composition functor is an isomorphism of the map additive group of the composition of $F$ and $G$ and the composition of the map additive group of $F$ and the map additive group of $G$.

the map additive group functor (from the name)

The map additive group functor is a functor of the set of left exact functors of $C$ and $D$ and the set of functors of the set of additive groups of $C$ and the set of additive groups of $D$.

the identity functor (from the docstring)

The identity functor is an isomorphism of the map additive group of the identity of $C$ and the identity of the set of additive groups of $C$.

the map additive group natural isomorphism of e (from the name)

Let $e$ be an isomorphism of $F$ and $\mathrm{F'}$. Then the map additive group natural isomorphism of $e$ is an isomorphism of the map additive group of $F$ and the map additive group of $\mathrm{F'}$.

the map additive group natural transformation of f (from the name)

Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the map additive group natural transformation of $f$ is a homomorphism of the map additive group of $F$ and the map additive group of $\mathrm{F'}$.

the map group of F (from the name)

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

the composition functor (from the docstring)

The composition functor is an isomorphism of the map group of the composition of $F$ and $G$ and the composition of the map group of $F$ and the map group of $G$.

the map group functor (from the name)

The map group functor is a functor of the set of left exact functors of $C$ and $D$ and the set of functors of the set of groups of $C$ and the set of groups of $D$.

the identity functor (from the docstring)

The identity functor is an isomorphism of the map group of the identity of $C$ and the identity of the set of groups of $C$.

the map group natural isomorphism of e (from the name)

Let $e$ be an isomorphism of $F$ and $\mathrm{F'}$. Then the map group natural isomorphism of $e$ is an isomorphism of the map group of $F$ and the map group of $\mathrm{F'}$.

the map group natural transformation of f (from the name)

Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the map group natural transformation of $f$ is a homomorphism of the map group of $F$ and the map group of $\mathrm{F'}$.

group of C (from the name)

Let $C$ be a set. Then the groups of $C$ are a basic type.

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

Let $C$ be a set. Then $\operatorname{forget}$ applied to $C$ is a functor of the set of groups of $C$ and $C$ defined as the composition of $\mathrm{CategoryTheory\_\_Grp\_\_forget\_u2082\_Mon}$ applied to $C$ and $\operatorname{forget}$ applied to $C$.

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_Grp\_\_forget\_u2082\_Mon}$ applied to $C$ is a functor of the set of groups of $C$ and the set of monoids of $C$ defined as the induced functor of $\operatorname{toMon}$.

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_Grp\_\_fullyFaithfulForget\_u2082\_Mon}$ applied to $C$ is an element of $\operatorname{FullyFaithful}$ applied to $\mathrm{CategoryTheory\_\_Grp\_\_forget\_u2082\_Mon}$ applied to $C$ defined as the induced functor of $\operatorname{toMon}$.

the homomorphism of f (from the name)

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

the homomorphism of f (from the name)

Let $f$ be a homomorphism of the monoid of $A$ and the monoid of $B$. Then the homomorphism of $f$ is a homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to $f$.

the homomorphism of f (from the name)

Let $f$ be a homomorphism of $\operatorname{X}$ applied to $A$ and $\operatorname{X}$ applied to $B$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the one and $f$ is equal to the one and $\mathrm{CategoryTheory\_\_Grp\_\_homMk''\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the product and $f$ is equal to the composition of the tensor homomorphism of $f$ and $f$ and the product and $\mathrm{CategoryTheory\_\_Grp\_\_homMk''\_\_\_auto\_3}$. Then the homomorphism of $f$ is a homomorphism of $A$ and $B$ defined as the homomorphism of $f$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $\operatorname{X}$ applied to $G$ and $\operatorname{X}$ applied to $H$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the one and the homomorphism of $e$ is equal to the one and $\mathrm{CategoryTheory\_\_Grp\_\_mkIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the product and the homomorphism of $e$ is equal to the composition of the tensor homomorphism of the homomorphism of $e$ and the homomorphism of $e$ and the product and $\mathrm{CategoryTheory\_\_Grp\_\_mkIso\_\_\_auto\_3}$. Then the isomorphism of $e$ is an isomorphism of $G$ and $H$ defined as the isomorphism of $e$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $G$ and $H$. Then the isomorphism of $e$ is an isomorphism of $\operatorname{mk}$ applied to $G$ and $\operatorname{mk}$ applied to $H$ defined as the unique isomorphism of $\mathrm{CategoryTheory\_\_Grp\_\_fullyFaithfulForget\_u2082\_Mon}$ applied to $C$ and the isomorphism of $e$.

the group of f (from the name)

Let $f$ be a homomorphism of $A$ and $B$. Then the group of $f$ is a homomorphism of $\operatorname{mk}$ applied to $A$ and $\operatorname{mk}$ applied to $B$ defined as the homomorphism of $f$.

the monoid of A (from the name)

Let $A$ be a group of $C$. Then the monoid of $A$ is a monoid of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{X}$ applied to $A$.

the trivial group object of C (from the docstring)

Let $C$ be a set. Then the trivial group object of $C$ is a group of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{X}$ applied to the trivial monoid object of $C$.

X is a group object (from the name)

Let $X$ be an element of $C$. Then we can say that $X$ is a group object.

the inverse (from the docstring)

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

the right multiplicative of f (from the name)

Let $f$ be a homomorphism of the tensor unity in the monoidal structure of $C$ and $A$. Then the right multiplicative of $f$ is an isomorphism of $A$ and $A$.

Hopf of C (from the name)

Let $C$ be a set. Then the Hopfs of $C$ are a basic type.

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

Let $A$ be a Hopf of $C$. Then $\operatorname{toBimon}$ applied to $A$ is an element of $\operatorname{Bimon}$ applied to $C$ defined as $\operatorname{mk'}$ applied to $\operatorname{X}$ applied to $A$.

X is a Hopf object (from the name)

Let $X$ be an element of $C$. Then we can say that $X$ is a Hopf object.

the antipode (from the docstring)

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

the counit for the equivalence (from the docstring)

The counit for the equivalence is an isomorphism of the composition of the inverse and the functor and the identity of the set of functors of $C$ and the set of commutative monoids of $D$.

the functor (from the name)

The functor is a functor of the set of commutative monoids of the set of functors of $C$ and $D$ and the set of functors of $C$ and the set of commutative monoids of $D$.

the inverse (from the name)

The inverse is a functor of the set of functors of $C$ and the set of commutative monoids of $D$ and the set of commutative monoids of the set of functors of $C$ and $D$.

the unit for the equivalence (from the docstring)

The unit for the equivalence is an isomorphism of the identity of the set of commutative monoids of the set of functors of $C$ and $D$ and the composition of the functor and the inverse.

the counit for the equivalence (from the docstring)

The counit for the equivalence is an isomorphism of the composition of $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Monoidal\_\_Internal\_\_FunctorCategory\_\_0\_\_CategoryTheory\_\_Monoidal\_\_ComonFunctorCategoryEquivalence\_\_inverse}$ and the functor and the identity of the set of functors of $C$ and $\operatorname{Comon}$ applied to $D$.

the functor (from the name)

The functor is a functor of $\operatorname{Comon}$ applied to the set of functors of $C$ and $D$ and the set of functors of $C$ and $\operatorname{Comon}$ applied to $D$.

the functor object of A (from the name)

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

the functor object object of A and X (from the name)

Let $A$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then the functor object object of $A$ and $X$ is an element of $\operatorname{Comon}$ applied to $D$ defined as $\operatorname{mk}$ applied to the action of $A$ and $X$.

the inverse object of F (from the name)

Let $F$ be a functor of $C$ and $\operatorname{Comon}$ applied to $D$. Then the inverse object of $F$ is an element of $\operatorname{Comon}$ applied to the set of functors of $C$ and $D$ defined as $\operatorname{mk}$ applied to the composition of $F$ and $\operatorname{forget}$ applied to $D$.

the counit for the equivalence (from the docstring)

The counit for the equivalence is an isomorphism of the composition of the inverse and the functor and the identity of the set of functors of $C$ and the set of monoids of $D$.

the functor (from the name)

The functor is a functor of the set of monoids of the set of functors of $C$ and $D$ and the set of functors of $C$ and the set of monoids of $D$.

the functor object of A (from the name)

Let $A$ be a functor of $C$ and $D$. Then the functor object of $A$ is a functor of $C$ and the set of monoids of $D$.

the functor object object of A and X (from the name)

Let $A$ be a functor of $C$ and $D$. Let $X$ be an element of $C$. Then the functor object object of $A$ and $X$ is a monoid of $D$ defined as $\operatorname{mk}$ applied to the action of $A$ and $X$.

the inverse (from the name)

The inverse is a functor of the set of functors of $C$ and the set of monoids of $D$ and the set of monoids of the set of functors of $C$ and $D$.

the inverse object of F (from the name)

Let $F$ be a functor of $C$ and the set of monoids of $D$. Then the inverse object of $F$ is a monoid of the set of functors of $C$ and $D$ defined as $\operatorname{mk}$ applied to the composition of $F$ and $\operatorname{forget}$ applied to $D$.

the unit for the equivalence (from the docstring)

The unit for the equivalence is an isomorphism of the identity of the set of monoids of the set of functors of $C$ and $D$ and the composition of the functor and the inverse.

the commutative monoid functor category equivalence of C and D (from the name)

Let $C$ and $D$ be sets. Then the commutative monoid functor category equivalence of $C$ and $D$ is an equivalence of the set of commutative monoids of the set of functors of $C$ and $D$ and the set of functors of $C$ and the set of commutative monoids of $D$.

the comonoid functor category equivalence of C and D (from the name)

Let $C$ and $D$ be sets. Then the comonoid functor category equivalence of $C$ and $D$ is an equivalence of $\operatorname{Comon}$ applied to the set of functors of $C$ and $D$ and the set of functors of $C$ and $\operatorname{Comon}$ applied to $D$.

the monoid functor category equivalence of C and D (from the name)

Let $C$ and $D$ be sets. Then the monoid functor category equivalence of $C$ and $D$ is an equivalence of the set of monoids of the set of functors of $C$ and $D$ and the set of functors of $C$ and the set of monoids of $D$.

Let $F$ be a functor of $J$ and the set of monoids of $C$. Let $c$ be a cone of the composition of $F$ and $\operatorname{forget}$ applied to $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{forgetMapConeLimitConeIso}$ applied to $F$, $c$ and $\mathrm{hc}$ is an isomorphism of the map cone of $\operatorname{forget}$ applied to $C$ and $\operatorname{limitCone}$ applied to $F$, $c$ and $\mathrm{hc}$ and $c$.

the limit of c and hc (from the name)

Let $F$ be a functor of $J$ and the set of monoids of $C$. Let $c$ be a cone of the composition of $F$ and $\operatorname{forget}$ applied to $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the limit of $c$ and $\mathrm{hc}$ is a monoid of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{pt}$ applied to $c$.

the limit cone lift to limit of c and hc (from the name)

Let $F$ be a functor of $J$ and the set of monoids of $C$. Let $c$ be a cone of the composition of $F$ and $\operatorname{forget}$ applied to $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then the limit cone lift to limit of $c$ and $\mathrm{hc}$ is a lift to limit of $c$ and $\mathrm{hc}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{limitCone}$ applied to $F$, $c$ and $\mathrm{hc}$ and $\operatorname{forgetMapConeLimitConeIso}$ applied to $F$, $c$ and $\mathrm{hc}$ and $\operatorname{limitConeIsLimit}$ applied to $F$, $c$ and $\mathrm{hc}$.

the functor (from the name)

The functor is a functor of the set of monoids of the set of module categories of $R$ and the set of algebra categories of $R$.

the inverse (from the name)

The inverse is a functor of the set of algebra categories of $R$ and the set of monoids of the set of module categories of $R$.

the monoid module equivalence algebra (from the name)

The monoid module equivalence algebra is an equivalence of the set of monoids of the set of module categories of $R$ and the set of algebra categories of $R$.

the equivalence (from the docstring)

The equivalence is an isomorphism of the composition of the functor and the forgetful functor of the set of algebra categories of $R$ and the set of module categories of $R$ and $\operatorname{forget}$ applied to the set of module categories of $R$.

the functor (from the name)

The functor is a functor of the set of commutative monoids of the set of sets and the set of commutative monoid categories.

the inverse (from the name)

The inverse is a functor of the set of commutative monoid categories and the set of commutative monoids of the set of sets.

the functor (from the name)

The functor is a functor of the set of monoids of the set of sets and the set of monoid categories.

the inverse (from the name)

The inverse is a functor of the set of monoid categories and the set of monoids of the set of sets.

the commutative monoid type equivalence commutative monoid (from the name)

The commutative monoid type equivalence commutative monoid is an equivalence of the set of commutative monoids of the set of sets and the set of commutative monoid categories.

$\mathrm{commMonTypeEquivalenceCommMonForget}$ is an isomorphism of the composition of the functor and the forgetful functor of the set of commutative monoid categories and the set of monoid categories and the composition of $\mathrm{CategoryTheory\_\_CommMon\_\_forget\_u2082\_Mon}$ applied to the set of sets and the functor defined as the identity of the composition of the functor and the forgetful functor of the set of commutative monoid categories and the set of monoid categories.

the monoid type equivalence monoid (from the name)

The monoid type equivalence monoid is an equivalence of the set of monoids of the set of sets and the set of monoid categories.

the equivalence (from the docstring)

The equivalence is an isomorphism of the composition of the functor and the forgetful functor of the set of monoid categories and $\operatorname{forget}$ applied to the set of sets.

the functor (from the name)

The functor is a functor of the set of commutative groups of the set of sets and the set of commutative group categories.

the inverse (from the name)

The inverse is a functor of the set of commutative group categories and the set of commutative groups of the set of sets.

the commutative group type equivalence commutative group (from the name)

The commutative group type equivalence commutative group is an equivalence of the set of commutative groups of the set of sets and the set of commutative group categories.

$\mathrm{commGrpTypeEquivalenceCommGrpForgetCommMon}$ is an isomorphism of the composition of the functor and the forgetful functor of the set of commutative group categories and the set of commutative monoid categories and the composition of $\mathrm{CategoryTheory\_\_CommGrp\_\_forget\_u2082\_CommMon}$ applied to the set of sets and the functor defined as the identity of the composition of the functor and the forgetful functor of the set of commutative group categories and the set of commutative monoid categories.

$\mathrm{commGrpTypeEquivalenceCommGrpForgetGrp}$ is an isomorphism of the composition of the functor and the forgetful functor of the set of commutative group categories and the set of group categories and the composition of $\mathrm{CategoryTheory\_\_CommGrp\_\_forget\_u2082\_Grp}$ applied to the set of sets and the functor defined as the identity of the composition of the functor and the forgetful functor of the set of commutative group categories and the set of group categories.

the functor (from the name)

The functor is a functor of the set of groups of the set of sets and the set of group categories.

the inverse (from the name)

The inverse is a functor of the set of group categories and the set of groups of the set of sets.

the group type equivalence group (from the name)

The group type equivalence group is an equivalence of the set of groups of the set of sets and the set of group categories.

$\mathrm{grpTypeEquivalenceGrpForget}$ is an isomorphism of the composition of the functor and the forgetful functor of the set of group categories and the set of monoid categories and the composition of $\mathrm{CategoryTheory\_\_Grp\_\_forget\_u2082\_Mon}$ applied to the set of sets and the functor defined as the identity of the composition of the functor and the forgetful functor of the set of group categories and the set of monoid categories.

Let $x_{7}$ be an element of $\operatorname{IsColimit}$ applied to $x_{6}$. Let $x_{12}$ be an element of $\operatorname{IsColimit}$ applied to $x_{11}$. Then $\operatorname{isColimitTensor}$ applied to $x_{7}$ and $x_{12}$ is an element of $\operatorname{IsColimit}$ applied to the tensor of $x_{6}$ and $x_{11}$.

the tensor of x6 and x10 (from the name)

Let $x_{6}$ be a cokernel cofork of $x_{5}$. Let $x_{10}$ be a cokernel cofork of $x_{9}$. Then the tensor of $x_{6}$ and $x_{10}$ is a cokernel cofork of $\operatorname{desc}$ applied to the right whisker of $x_{5}$ and $x_{8}$ and the left whisker of $x_{4}$ and $x_{9}$.

the tensor of x5 and x6 (from the name)

Let $x_{5}$ be a cocone of $x_{3}$. Let $x_{6}$ be a cocone of $x_{4}$. Then the tensor of $x_{5}$ and $x_{6}$ is a cocone of the tensor object of $x_{3}$ and $x_{4}$.

the tensor of x8 and x9 (from the name)

Let $x_{8}$ be a cocone of $x_{6}$. Let $x_{9}$ be a cocone of $x_{7}$. Then the tensor of $x_{8}$ and $x_{9}$ is a cocone of the external product of $x_{6}$ and $x_{7}$ defined as the map cocone of $x_{8}$ and $x_{9}$.

the tensor of x7 and x8 (from the name)

Let $x_{7}$ be an element of $\operatorname{IsColimit}$ applied to $x_{5}$. Let $x_{8}$ be an element of $\operatorname{IsColimit}$ applied to $x_{6}$. Then the tensor of $x_{7}$ and $x_{8}$ is an element of $\operatorname{IsColimit}$ applied to the tensor of $x_{5}$ and $x_{6}$.

the tensor of x10 and x11 (from the name)

Let $x_{10}$ be an element of $\operatorname{IsColimit}$ applied to $x_{8}$. Let $x_{11}$ be an element of $\operatorname{IsColimit}$ applied to $x_{9}$. Then the tensor of $x_{10}$ and $x_{11}$ is an element of $\operatorname{IsColimit}$ applied to the tensor of $x_{8}$ and $x_{9}$ defined as $\mathrm{CategoryTheory\_\_Limits\_\_isColimitOfPreserves\_u2082\_}$ applied to the tensor product bifunctor of $C$, $x_{10}$ and $x_{11}$.

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

Let $D$ be a set. Let $A$ be an element of $C$. Then the elements of $\operatorname{AddMod}$ applied to $D$ and $A$ are a basic type.

homomorphism of M and N (from the name)

Let $M$ and $N$ be elements of $\operatorname{AddMod}$ applied to $D$ and $A$. Then the homomorphisms of $M$ and $N$ are a basic type.

the homomorphism of self (from the name)

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

Let $f$ be a homomorphism of $\operatorname{X}$ applied to $M$ and $\operatorname{X}$ applied to $N$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the vector sum and $f$ is equal to the composition of the action of $A$ and $f$ and the vector sum and $\mathrm{CategoryTheory\_\_AddMod\_\_Hom\_\_mk'\_\_\_auto\_1}$. Then $\operatorname{mk'}$ applied to $f$ and $\mathrm{vadd\_hom}$ is a homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $f$.

Let $f$ be a homomorphism of $M$ and $N$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the vector sum and $f$ is equal to the composition of the action of $A$ and $f$ and the vector sum and $\mathrm{CategoryTheory\_\_AddMod\_\_Hom\_\_mk''\_\_\_auto\_1}$. Then $\operatorname{mk''}$ applied to $f$ and $\mathrm{vadd\_hom}$ is a homomorphism of $\operatorname{mk}$ applied to $M$ and $\operatorname{mk}$ applied to $N$ defined as $\operatorname{mk}$ applied to $f$.

Let $\mathrm{self}$ be an element of $\operatorname{AddMod}$ applied to $D$ and $A$. Then $\operatorname{X}$ applied to $\mathrm{self}$ is an element of $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the preimage of f (from the name)

Let $f$ be a homomorphism of $A$ and $B$. Then the preimage of $f$ is a functor of $\operatorname{AddMod}$ applied to $D$ and $B$ and $\operatorname{AddMod}$ applied to $D$ and $A$.

the composition of f and g (from the name)

Let $f$ be a homomorphism of $M$ and $N$. Let $g$ be a homomorphism of $N$ and $O$. Then the composition of $f$ and $g$ is a homomorphism of $M$ and $O$ defined as $\operatorname{mk}$ applied to the composition of the homomorphism of $f$ and the homomorphism of $g$.

Let $A$ be an element of $C$. Then $\operatorname{forget}$ applied to $A$ is a functor of $\operatorname{AddMod}$ applied to $D$ and $A$ and $D$.

the identity morphism of M (from the docstring)

Let $M$ be an element of $\operatorname{AddMod}$ applied to $D$ and $A$. Then the identity morphism of $M$ is a homomorphism of $M$ and $M$ defined as $\operatorname{mk}$ applied to the identity morphism of $\operatorname{X}$ applied to $M$.

the regular of A (from the name)

Let $A$ be an element of $C$. Then the regular of $A$ is an element of $\operatorname{AddMod}$ applied to $C$ and $A$ defined as $\operatorname{mk}$ applied to $A$.

Let $M$ be an element of $C$. Let $X$ be an element of $D$. Then we can say that $\operatorname{AddModObj}$ holds for $M$ and $X$.

the vector sum (from the name)

The vector sum is a homomorphism of the action object of $M$ and $X$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $A$ be an element of $C$. Let $f$ be a homomorphism of $\mathrm{M'}$ and $\mathrm{N'}$. Then we can say that $\operatorname{IsAddModHom}$ holds for $A$ and $f$.

Let $A$ be an element of $C$. Let $f$ be a homomorphism of $M$ and $N$. Then we can say that $\operatorname{IsModHom}$ holds for $A$ and $f$.

Let $D$ be a set. Let $A$ be an element of $C$. Then the elements of $\operatorname{Mod}$ applied to $D$ and $A$ are a basic type.

homomorphism of M and N (from the name)

Let $M$ and $N$ be elements of $\operatorname{Mod}$ applied to $D$ and $A$. Then the homomorphisms of $M$ and $N$ are a basic type.

the homomorphism of self (from the name)

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

Let $f$ be a homomorphism of $\operatorname{X}$ applied to $M$ and $\operatorname{X}$ applied to $N$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the scalar multiple and $f$ is equal to the composition of the action of $A$ and $f$ and the scalar multiple and $\mathrm{CategoryTheory\_\_Mod\_\_Hom\_\_mk'\_\_\_auto\_1}$. Then $\operatorname{mk'}$ applied to $f$ and $\mathrm{smul\_hom}$ is a homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $f$.

Let $f$ be a homomorphism of $M$ and $N$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the scalar multiple and $f$ is equal to the composition of the action of $A$ and $f$ and the scalar multiple and $\mathrm{CategoryTheory\_\_Mod\_\_Hom\_\_mk''\_\_\_auto\_1}$. Then $\operatorname{mk''}$ applied to $f$ and $\mathrm{smul\_hom}$ is a homomorphism of $\operatorname{mk}$ applied to $M$ and $\operatorname{mk}$ applied to $N$ defined as $\operatorname{mk}$ applied to $f$.

Let $\mathrm{self}$ be an element of $\operatorname{Mod}$ applied to $D$ and $A$. Then $\operatorname{X}$ applied to $\mathrm{self}$ is an element of $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the preimage of f (from the name)

Let $f$ be a homomorphism of $A$ and $B$. Then the preimage of $f$ is a functor of $\operatorname{Mod}$ applied to $D$ and $B$ and $\operatorname{Mod}$ applied to $D$ and $A$.

the composition of f and g (from the name)

Let $f$ be a homomorphism of $M$ and $N$. Let $g$ be a homomorphism of $N$ and $O$. Then the composition of $f$ and $g$ is a homomorphism of $M$ and $O$ defined as $\operatorname{mk}$ applied to the composition of the homomorphism of $f$ and the homomorphism of $g$.

Let $A$ be an element of $C$. Then $\operatorname{forget}$ applied to $A$ is a functor of $\operatorname{Mod}$ applied to $D$ and $A$ and $D$.

the identity morphism of M (from the docstring)

Let $M$ be an element of $\operatorname{Mod}$ applied to $D$ and $A$. Then the identity morphism of $M$ is a homomorphism of $M$ and $M$ defined as $\operatorname{mk}$ applied to the identity morphism of $\operatorname{X}$ applied to $M$.

the regular of A (from the name)

Let $A$ be an element of $C$. Then the regular of $A$ is an element of $\operatorname{Mod}$ applied to $C$ and $A$ defined as $\operatorname{mk}$ applied to $A$.

Let $M$ be an element of $C$. Let $X$ be an element of $D$. Then we can say that $\operatorname{ModObj}$ holds for $M$ and $X$.

the scalar multiple (from the name)

The scalar multiple is a homomorphism of the action object of $M$ and $X$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

additive monoid of C (from the name)

Let $C$ be a set. Then the additive monoids of $C$ are a basic type.

homomorphism of M and N (from the name)

Let $M$ and $N$ be additive monoids of $C$. Then the homomorphisms of $M$ and $N$ are a basic type.

the homomorphism of self (from the name)

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

Let $f$ be a homomorphism of $\operatorname{X}$ applied to $M$ and $\operatorname{X}$ applied to $N$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the zero morphism and $f$ is equal to the zero morphism and $\mathrm{CategoryTheory\_\_AddMon\_\_Hom\_\_mk'\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the sum and $f$ is equal to the composition of the tensor homomorphism of $f$ and $f$ and the sum and $\mathrm{CategoryTheory\_\_AddMon\_\_Hom\_\_mk'\_\_\_auto\_3}$. Then $\operatorname{mk'}$ applied to $f$, $\mathrm{zero\_f}$ and $\mathrm{add\_f}$ is a homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $f$.

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

the composition of f and g (from the name)

Let $f$ be a homomorphism of $M$ and $N$. Let $g$ be a homomorphism of $N$ and $O$. Then the composition of $f$ and $g$ is a homomorphism of $M$ and $O$ defined as $\operatorname{mk}$ applied to the composition of the homomorphism of $f$ and the homomorphism of $g$.

$\operatorname{equivLaxMonoidalFunctorPUnit}$ is an equivalence of $\operatorname{LaxMonoidalFunctor}$ applied to $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $C$ and the set of additive monoids of $C$.

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

the identity morphism of M (from the docstring)

Let $M$ be an additive monoid of $C$. Then the identity morphism of $M$ is a homomorphism of $M$ and $M$ defined as $\operatorname{mk}$ applied to the identity morphism of $\operatorname{X}$ applied to $M$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $\operatorname{X}$ applied to $M$ and $\operatorname{X}$ applied to $N$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the zero morphism and the homomorphism of $e$ is equal to the zero morphism and $\mathrm{CategoryTheory\_\_AddMon\_\_mkIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the sum and the homomorphism of $e$ is equal to the composition of the tensor homomorphism of the homomorphism of $e$ and the homomorphism of $e$ and the sum and $\mathrm{CategoryTheory\_\_AddMon\_\_mkIso\_\_\_auto\_3}$. Then the isomorphism of $e$ is an isomorphism of $M$ and $N$ defined as the isomorphism of $e$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $M$ and $N$. Then the isomorphism of $e$ is an isomorphism of $\operatorname{mk}$ applied to $M$ and $\operatorname{mk}$ applied to $N$.

the additive monoid of f (from the name)

Let $f$ be a homomorphism of $A$ and $B$. Then the additive monoid of $f$ is a homomorphism of $\operatorname{mk}$ applied to $A$ and $\operatorname{mk}$ applied to $B$ defined as $\operatorname{mk}$ applied to $f$.

the trivial additive monoid object of C (from the docstring)

Let $C$ be a set. Then the trivial additive monoid object of $C$ is an additive monoid of $C$ defined as $\operatorname{mk}$ applied to the tensor unity in the monoidal structure of $C$.

X is a additive monoid object (from the name)

Let $X$ be an element of $C$. Then we can say that $X$ is an additive monoid object.

the sum (from the name)

The sum is a homomorphism of the tensor object of $X$ and $X$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the zero morphism (from the docstring)

The zero morphism is a homomorphism of the tensor unity in the monoidal structure of $C$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the map additive monoid of a (from the name)

Let $a$ be an adjunction of $F$ and $G$. Then the map additive monoid of $a$ is an adjunction of the map additive monoid of $F$ and the map additive monoid of $G$.

the map monoid of a (from the name)

Let $a$ be an adjunction of $F$ and $G$. Then the map monoid of $a$ is an adjunction of the map monoid of $F$ and the map monoid of $G$.

the map additive monoid of e (from the name)

Let $e$ be an equivalence of $C$ and $D$. Then the map additive monoid of $e$ is an equivalence of the set of additive monoids of $C$ and the set of additive monoids of $D$.

the map monoid of e (from the name)

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

the map additive monoid of hF (from the name)

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the map additive monoid of $\mathrm{hF}$ is an element of $\operatorname{FullyFaithful}$ applied to the map additive monoid of $F$.

the map monoid of hF (from the name)

Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the map monoid of $\mathrm{hF}$ is an element of $\operatorname{FullyFaithful}$ applied to the map monoid of $F$.

the map additive monoid of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the map additive monoid of $F$ is a functor of the set of additive monoids of $C$ and the set of additive monoids of $D$.

the composition functor (from the docstring)

The composition functor is an isomorphism of the map additive monoid of the composition of $F$ and $G$ and the composition of the map additive monoid of $F$ and the map additive monoid of $G$.

the map additive monoid functor of C and D (from the name)

Let $C$ and $D$ be sets. Then the map additive monoid functor of $C$ and $D$ is a functor of $\operatorname{LaxMonoidalFunctor}$ applied to $C$ and $D$ and the set of functors of the set of additive monoids of $C$ and the set of additive monoids of $D$.

the identity functor (from the docstring)

The identity functor is an isomorphism of the map additive monoid of the identity of $C$ and the identity of the set of additive monoids of $C$.

the map additive monoid natural isomorphism of e (from the name)

Let $e$ be an isomorphism of $F$ and $\mathrm{F'}$. Then the map additive monoid natural isomorphism of $e$ is an isomorphism of the map additive monoid of $F$ and the map additive monoid of $\mathrm{F'}$.

the map additive monoid natural transformation of f (from the name)

Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the map additive monoid natural transformation of $f$ is a homomorphism of the map additive monoid of $F$ and the map additive monoid of $\mathrm{F'}$.

the map monoid of F (from the name)

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

the composition functor (from the docstring)

The composition functor is an isomorphism of the map monoid of the composition of $F$ and $G$ and the composition of the map monoid of $F$ and the map monoid of $G$.

the map monoid functor of C and D (from the name)

Let $C$ and $D$ be sets. Then the map monoid functor of $C$ and $D$ is a functor of $\operatorname{LaxMonoidalFunctor}$ applied to $C$ and $D$ and the set of functors of the set of monoids of $C$ and the set of monoids of $D$.

the identity functor (from the docstring)

The identity functor is an isomorphism of the map monoid of the identity of $C$ and the identity of the set of monoids of $C$.

the map monoid natural isomorphism of e (from the name)

Let $e$ be an isomorphism of $F$ and $\mathrm{F'}$. Then the map monoid natural isomorphism of $e$ is an isomorphism of the map monoid of $F$ and the map monoid of $\mathrm{F'}$.

the map monoid natural transformation of f (from the name)

Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the map monoid natural transformation of $f$ is a homomorphism of the map monoid of $F$ and the map monoid of $\mathrm{F'}$.

f is a additive monoid homomorphism (from the name)

Let $f$ be a homomorphism of $\mathrm{M'}$ and $\mathrm{N'}$. Then we can say that $f$ is an additive monoid homomorphism.

X is a commutative additive monoid object (from the name)

Let $X$ be an element of $C$. Then we can say that $X$ is a commutative additive monoid object.

X is a commutative monoid object (from the name)

Let $X$ be an element of $C$. Then we can say that $X$ is a commutative monoid object.

f is a monoid homomorphism (from the name)

Let $f$ be a homomorphism of $M$ and $N$. Then we can say that $f$ is a monoid homomorphism.

monoid of C (from the name)

Let $C$ be a set. Then the monoids of $C$ are a basic type.

homomorphism of M and N (from the name)

Let $M$ and $N$ be monoids of $C$. Then the homomorphisms of $M$ and $N$ are a basic type.

the homomorphism of self (from the name)

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

Let $f$ be a homomorphism of $\operatorname{X}$ applied to $M$ and $\operatorname{X}$ applied to $N$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the one and $f$ is equal to the one and $\mathrm{CategoryTheory\_\_Mon\_\_Hom\_\_mk'\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the product and $f$ is equal to the composition of the tensor homomorphism of $f$ and $f$ and the product and $\mathrm{CategoryTheory\_\_Mon\_\_Hom\_\_mk'\_\_\_auto\_3}$. Then $\operatorname{mk'}$ applied to $f$, $\mathrm{one\_f}$ and $\mathrm{mul\_f}$ is a homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $f$.

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

the composition of f and g (from the name)

Let $f$ be a homomorphism of $M$ and $N$. Let $g$ be a homomorphism of $N$ and $O$. Then the composition of $f$ and $g$ is a homomorphism of $M$ and $O$ defined as $\operatorname{mk}$ applied to the composition of the homomorphism of $f$ and the homomorphism of $g$.

$\operatorname{equivLaxMonoidalFunctorPUnit}$ is an equivalence of $\operatorname{LaxMonoidalFunctor}$ applied to $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $C$ and the set of monoids of $C$.

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

the identity morphism of M (from the docstring)

Let $M$ be a monoid of $C$. Then the identity morphism of $M$ is a homomorphism of $M$ and $M$ defined as $\operatorname{mk}$ applied to the identity morphism of $\operatorname{X}$ applied to $M$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $\operatorname{X}$ applied to $M$ and $\operatorname{X}$ applied to $N$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the one and the homomorphism of $e$ is equal to the one and $\mathrm{CategoryTheory\_\_Mon\_\_mkIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the product and the homomorphism of $e$ is equal to the composition of the tensor homomorphism of the homomorphism of $e$ and the homomorphism of $e$ and the product and $\mathrm{CategoryTheory\_\_Mon\_\_mkIso\_\_\_auto\_3}$. Then the isomorphism of $e$ is an isomorphism of $M$ and $N$ defined as the isomorphism of $e$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $M$ and $N$. Then the isomorphism of $e$ is an isomorphism of $\operatorname{mk}$ applied to $M$ and $\operatorname{mk}$ applied to $N$.

the monoid of f (from the name)

Let $f$ be a homomorphism of $A$ and $B$. Then the monoid of $f$ is a homomorphism of $\operatorname{mk}$ applied to $A$ and $\operatorname{mk}$ applied to $B$ defined as $\operatorname{mk}$ applied to $f$.

the trivial monoid object of C (from the docstring)

Let $C$ be a set. Then the trivial monoid object of $C$ is a monoid of $C$ defined as $\operatorname{mk}$ applied to the tensor unity in the monoidal structure of $C$.

X is a monoid object (from the name)

Let $X$ be an element of $C$. Then we can say that $X$ is a monoid object.

the product (from the name)

The product is a homomorphism of the tensor object of $X$ and $X$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the one (from the name)

The one is a homomorphism of the tensor unity in the monoidal structure of $C$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $x_{4}$ be an isomorphism of the tensor unity in the monoidal structure of $D$ and the action of $F$ and the tensor unity in the monoidal structure of $C$. Let $x_{5}$ be an isomorphism of the curried tensor of $F$ and the curried tensor post of $F$ such that the composition of the left maps in the associativity hexagon of the homomorphism of $x_{5}$ is equal to the composition of the right maps in the associativity hexagon of the homomorphism of $x_{5}$, the left map in the left unitality square of $F$ is equal to the composition of the top map in the left unitality square of the homomorphism of $x_{4}$ and the composition of the component of the homomorphism of $x_{5}$ and the tensor unity in the monoidal structure of $C$ and the bottom map in the left unitality square of $F$ and the left map in the right unitality square of $F$ is equal to the composition of the top map in the right unitality square of the homomorphism of $x_{4}$ and the composition of the component of the map of the flip functor of $C$ and $D$ and the homomorphism of $x_{5}$ and the tensor unity in the monoidal structure of $C$ and the bottom map in the right unitality square of $F$. Then $\operatorname{ofBifunctor}$ applied to $x_{4}$, $x_{5}$, $\mathrm{associativity}$, $\mathrm{left\_unitality}$ and $\mathrm{right\_unitality}$ is an element of $\operatorname{CoreMonoidal}$ applied to $F$.

the bottom map in the right unitality square of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the bottom map in the right unitality square of $F$ is a homomorphism of the composition of the action of the flip of the tensor product bifunctor of $C$ and the tensor unity in the monoidal structure of $C$ and $F$ and $F$ defined as the right whisker of the homomorphism of the right unitor of $C$ and $F$.

the bottom map in the left unitality square of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the bottom map in the left unitality square of $F$ is a homomorphism of the composition of the action of the tensor product bifunctor of $C$ and the tensor unity in the monoidal structure of $C$ and $F$ and $F$ defined as the right whisker of the homomorphism of the left unitor of $C$ and $F$.

the composition of the left maps in the associativity hexagon of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the curried tensor of $F$ and the curried tensor post of $F$. Then the composition of the left maps in the associativity hexagon of $x_{4}$ is a homomorphism of the curried tensor of $F$ and the curried tensor post post of $F$ defined as the composition of the top left map in the associativity hexagon of $x_{4}$ and the composition of the middle left map in the associativity hexagon of $x_{4}$ and the bottom left map in the associativity hexagon of $F$.

the top left map in the associativity hexagon of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the curried tensor of $F$ and the curried tensor post of $F$. Then the top left map in the associativity hexagon of $x_{4}$ is a homomorphism of the curried tensor of $F$ and the curried tensor post of $F$ defined as the component of the map of the functor and $x_{4}$ and $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_curriedTensorInsertFunctor\_u2082\_}$ applied to $F$.

the middle left map in the associativity hexagon of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the curried tensor of $F$ and the curried tensor post of $F$. Then the middle left map in the associativity hexagon of $x_{4}$ is a homomorphism of the curried tensor post of $F$ and the curried tensor post post of $F$ defined as the map of the action of the functor and the tensor product bifunctor of $C$ and $x_{4}$.

the bottom left map in the associativity hexagon of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the bottom left map in the associativity hexagon of $F$ is a homomorphism of the curried tensor post post of $F$ and the curried tensor post post of $F$ defined as the map of the action of the postcomposition and $F$ and the homomorphism of the associator of $C$.

the left map in the right unitality square of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the left map in the right unitality square of $F$ is a homomorphism of the composition of $F$ and the right tensor unit of $D$ and $F$ defined as the left whisker of $F$ and the homomorphism of the right unitor of $D$.

the left map in the left unitality square of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the left map in the left unitality square of $F$ is a homomorphism of the composition of $F$ and the left tensor unit of $D$ and $F$ defined as the left whisker of $F$ and the homomorphism of the left unitor of $D$.

the composition of the right maps in the associativity hexagon of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the curried tensor of $F$ and the curried tensor post of $F$. Then the composition of the right maps in the associativity hexagon of $x_{4}$ is a homomorphism of the curried tensor of $F$ and the curried tensor post post of $F$ defined as the composition of the top right map in the associativity hexagon of $F$ and the composition of the middle right map in the associativity hexagon of $x_{4}$ and the bottom right map in the associativity hexagon of $x_{4}$.

the top right map in the associativity hexagon of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the top right map in the associativity hexagon of $F$ is a homomorphism of the curried tensor of $F$ and the curried tensor of $F$ defined as the map of the action of the action of the action of the left whiskering of $D$ and $F$ and $F$ and $F$ and the homomorphism of the associator of $D$.

the middle right map in the associativity hexagon of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the curried tensor of $F$ and the curried tensor post of $F$. Then the middle right map in the associativity hexagon of $x_{4}$ is a homomorphism of the curried tensor of $F$ and the curried tensor post of $F$ defined as the map of the action of the functor and $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_curriedTensorInsertFunctor\_u2081\_}$ applied to $F$ and $x_{4}$.

the bottom right map in the associativity hexagon of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the curried tensor of $F$ and the curried tensor post of $F$. Then the bottom right map in the associativity hexagon of $x_{4}$ is a homomorphism of the curried tensor post of $F$ and the curried tensor post post of $F$ defined as the component of the map of the functor and $x_{4}$ and the tensor product bifunctor of $C$.

the top map in the right unitality square of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the tensor unity in the monoidal structure of $D$ and the action of $F$ and the tensor unity in the monoidal structure of $C$. Then the top map in the right unitality square of $x_{4}$ is a homomorphism of the composition of $F$ and the right tensor unit of $D$ and the action of the flip of the curried tensor of $F$ and the tensor unity in the monoidal structure of $C$ defined as the left whisker of $F$ and the map of the flip of the tensor product bifunctor of $D$ and $x_{4}$.

the top map in the left unitality square of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the tensor unity in the monoidal structure of $D$ and the action of $F$ and the tensor unity in the monoidal structure of $C$. Then the top map in the left unitality square of $x_{4}$ is a homomorphism of the composition of $F$ and the left tensor unit of $D$ and the action of the curried tensor of $F$ and the tensor unity in the monoidal structure of $C$ defined as the left whisker of $F$ and the map of the tensor product bifunctor of $D$ and $x_{4}$.

the bottom map in the oplax right unitality square of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the action of $F$ and the tensor unity in the monoidal structure of $C$ and the tensor unity in the monoidal structure of $D$. Then the bottom map in the oplax right unitality square of $x_{4}$ is a homomorphism of the action of the flip of the curried tensor of $F$ and the tensor unity in the monoidal structure of $C$ and the composition of $F$ and the right tensor unit of $D$ defined as the left whisker of $F$ and the map of the flip of the tensor product bifunctor of $D$ and $x_{4}$.

the bottom map in the oplax left unitality square of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the action of $F$ and the tensor unity in the monoidal structure of $C$ and the tensor unity in the monoidal structure of $D$. Then the bottom map in the oplax left unitality square of $x_{4}$ is a homomorphism of the action of the curried tensor of $F$ and the tensor unity in the monoidal structure of $C$ and the composition of $F$ and the left tensor unit of $D$ defined as the left whisker of $F$ and the map of the tensor product bifunctor of $D$ and $x_{4}$.

the first map of x4 (from the name)

Let $x_{4}$ be a homomorphism of the curried tensor post of $F$ and the curried tensor of $F$. Then the first map of $x_{4}$ is a homomorphism of the curried tensor post post of $F$ and the curried tensor of $F$ defined as the composition of the top left map in the oplax associativity hexagon of $x_{4}$ and the composition of the middle left map in the oplax associativity hexagon of $x_{4}$ and the bottom left map in the oplax associativity hexagon of $F$.

the top left map in the oplax associativity hexagon of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the curried tensor post of $F$ and the curried tensor of $F$. Then the top left map in the oplax associativity hexagon of $x_{4}$ is a homomorphism of the curried tensor post post of $F$ and the curried tensor post of $F$ defined as the map of the action of the functor and the tensor product bifunctor of $C$ and $x_{4}$.

the middle left map in the oplax associativity hexagon of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the curried tensor post of $F$ and the curried tensor of $F$. Then the middle left map in the oplax associativity hexagon of $x_{4}$ is a homomorphism of the curried tensor post of $F$ and the curried tensor of $F$ defined as the component of the map of the functor and $x_{4}$ and $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_curriedTensorInsertFunctor\_u2082\_}$ applied to $F$.

the bottom left map in the oplax associativity hexagon of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the bottom left map in the oplax associativity hexagon of $F$ is a homomorphism of the curried tensor of $F$ and the curried tensor of $F$ defined as the map of the action of the action of the action of the left whiskering of $D$ and $F$ and $F$ and $F$ and the homomorphism of the associator of $D$.

the left map in the oplax right unitality square of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the left map in the oplax right unitality square of $F$ is a homomorphism of $F$ and the composition of $F$ and the right tensor unit of $D$ defined as the left whisker of $F$ and the inverse of the right unitor of $D$.

the left map in the oplax left unitality square of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the left map in the oplax left unitality square of $F$ is a homomorphism of $F$ and the composition of $F$ and the left tensor unit of $D$ defined as the left whisker of $F$ and the inverse of the left unitor of $D$.

the second map of x4 (from the name)

Let $x_{4}$ be a homomorphism of the curried tensor post of $F$ and the curried tensor of $F$. Then the second map of $x_{4}$ is a homomorphism of the curried tensor post post of $F$ and the curried tensor of $F$ defined as the composition of the top right map in the oplax associativity hexagon of $F$ and the composition of the middle right map in the oplax associativity hexagon of $x_{4}$ and the bottom right map in the oplax associativity hexagon of $x_{4}$.

the top right map in the oplax associativity hexagon of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the top right map in the oplax associativity hexagon of $F$ is a homomorphism of the curried tensor post post of $F$ and the curried tensor post post of $F$ defined as the map of the action of the postcomposition and $F$ and the homomorphism of the associator of $C$.

the middle right map in the oplax associativity hexagon of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the curried tensor post of $F$ and the curried tensor of $F$. Then the middle right map in the oplax associativity hexagon of $x_{4}$ is a homomorphism of the curried tensor post post of $F$ and the curried tensor post of $F$ defined as the component of the map of the functor and $x_{4}$ and the tensor product bifunctor of $C$.

the bottom right map in the oplax associativity hexagon of x4 (from the docstring)

Let $x_{4}$ be a homomorphism of the curried tensor post of $F$ and the curried tensor of $F$. Then the bottom right map in the oplax associativity hexagon of $x_{4}$ is a homomorphism of the curried tensor post of $F$ and the curried tensor of $F$ defined as the map of the action of the functor and $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_curriedTensorInsertFunctor\_u2081\_}$ applied to $F$ and $x_{4}$.

the top map in the oplax right unitality square of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the top map in the oplax right unitality square of $F$ is a homomorphism of $F$ and the composition of the action of the flip of the tensor product bifunctor of $C$ and the tensor unity in the monoidal structure of $C$ and $F$ defined as the right whisker of the inverse of the right unitor of $C$ and $F$.

the top map in the oplax left unitality square of F (from the docstring)

Let $F$ be a functor of $C$ and $D$. Then the top map in the oplax left unitality square of $F$ is a homomorphism of $F$ and the composition of the action of the tensor product bifunctor of $C$ and the tensor unity in the monoidal structure of $C$ and $F$ defined as the right whisker of the inverse of the left unitor of $C$ and $F$.

the curried tensor isomorphism post of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the curried tensor isomorphism post of $F$ is an isomorphism of the curried tensor of $F$ and the curried tensor post of $F$.

Let $F$ be a functor of $C$ and $D$. Then $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_curriedTensorInsertFunctor\_u2081\_}$ applied to $F$ is a functor of $C$ and the set of functors of $D$ and $D$ defined as the action of the action of the action of the left whiskering of $D$ and $F$ and the identity of $D$ and the tensor product bifunctor of $D$.

Let $F$ be a functor of $C$ and $D$. Then $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_curriedTensorInsertFunctor\_u2082\_}$ applied to $F$ is a functor of $D$ and the set of functors of $C$ and $D$ defined as the action of the action of the action of the left whiskering of $D$ and the identity of $D$ and $F$ and the tensor product bifunctor of $D$.

the curried tensor post of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the curried tensor post of $F$ is a functor of $C$ and the set of functors of $C$ and $D$ defined as the action of the action of the postcomposition and $F$ and the tensor product bifunctor of $C$.

the curried tensor post functor (from the name)

The curried tensor post functor is a functor of the set of functors of $C$ and $D$ and the set of functors of $C$ and the set of functors of $C$ and $D$ defined as the action of the flip of the postcomposition and the tensor product bifunctor of $C$.

the curried tensor post post of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the curried tensor post post of $F$ is a functor of $C$ and the set of functors of $C$ and the set of functors of $C$ and $D$ defined as the bifunctor composition of the tensor product bifunctor of $C$ and the curried tensor post of $F$.

the curried tensor post post of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the curried tensor post post of $F$ is a functor of $C$ and the set of functors of $C$ and the set of functors of $C$ and $D$ defined as the bifunctor composition of the curried tensor post of $F$ and the tensor product bifunctor of $C$.

the curried tensor post of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the curried tensor post of $F$ is a functor of $C$ and the set of functors of $C$ and the set of functors of $C$ and $D$ defined as the bifunctor composition of the tensor product bifunctor of $C$ and the curried tensor of $F$.

the curried tensor of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the curried tensor of $F$ is a functor of $C$ and the set of functors of $C$ and $D$ defined as the action of the action of the action of the left whiskering of $D$ and $F$ and $F$ and the tensor product bifunctor of $D$.

the curried tensor functor (from the name)

The curried tensor functor is a functor of the set of functors of $C$ and $D$ and the set of functors of $C$ and the set of functors of $C$ and $D$.

the curried tensor post of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the curried tensor post of $F$ is a functor of $C$ and the set of functors of $C$ and the set of functors of $C$ and $D$ defined as the bifunctor composition of the curried tensor of $F$ and the tensor product bifunctor of $C$.

the curried tensor of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the curried tensor of $F$ is a functor of $C$ and the set of functors of $C$ and the set of functors of $C$ and $D$ defined as the bifunctor composition of the curried tensor of $F$ and $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_curriedTensorInsertFunctor\_u2082\_}$ applied to $F$.

the curried tensor of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the curried tensor of $F$ is a functor of $C$ and the set of functors of $C$ and the set of functors of $C$ and $D$ defined as the bifunctor composition of $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_curriedTensorInsertFunctor\_u2081\_}$ applied to $F$ and the curried tensor of $F$.

the first map of tensor and associator (from the name)

Let $\mathrm{tensor}$ be a functor of $C$ and the set of functors of $C$ and $C$. Let $\mathrm{associator}$ be an isomorphism of the bifunctor composition of $\mathrm{tensor}$ and $\mathrm{tensor}$ and the bifunctor composition of $\mathrm{tensor}$ and $\mathrm{tensor}$. Then the first map of $\mathrm{tensor}$ and $\mathrm{associator}$ is a homomorphism of the source of $\mathrm{tensor}$ and the target of $\mathrm{tensor}$ defined as the composition of the map of the action of the postcomposition and $\mathrm{tensor}$ and the homomorphism of $\mathrm{associator}$ and the composition of the component of the map of the functor and the homomorphism of $\mathrm{associator}$ and $\mathrm{tensor}$ and the map of the action of the functor and $\mathrm{tensor}$ and the homomorphism of $\mathrm{associator}$.

the second map of tensor and associator (from the name)

Let $\mathrm{tensor}$ be a functor of $C$ and the set of functors of $C$ and $C$. Let $\mathrm{associator}$ be an isomorphism of the bifunctor composition of $\mathrm{tensor}$ and $\mathrm{tensor}$ and the bifunctor composition of $\mathrm{tensor}$ and $\mathrm{tensor}$. Then the second map of $\mathrm{tensor}$ and $\mathrm{associator}$ is a homomorphism of the source of $\mathrm{tensor}$ and the target of $\mathrm{tensor}$ defined as the composition of the map of the action of the functor and $\mathrm{tensor}$ and the homomorphism of $\mathrm{associator}$ and the component of the map of the functor and the homomorphism of $\mathrm{associator}$ and $\mathrm{tensor}$.

the source of tensor (from the name)

Let $\mathrm{tensor}$ be a functor of $C$ and the set of functors of $C$ and $C$. Then the source of $\mathrm{tensor}$ is a functor of $C$ and the set of functors of $C$ and the set of functors of $C$ and the set of functors of $C$ and $C$ defined as the action of the action of the postcomposition and $\mathrm{tensor}$ and the bifunctor composition of $\mathrm{tensor}$ and $\mathrm{tensor}$.

the target of tensor (from the name)

Let $\mathrm{tensor}$ be a functor of $C$ and the set of functors of $C$ and $C$. Then the target of $\mathrm{tensor}$ is a functor of $C$ and the set of functors of $C$ and the set of functors of $C$ and the set of functors of $C$ and $C$ defined as the trifunctor composition of $\mathrm{tensor}$ and the bifunctor composition of $\mathrm{tensor}$ and $\mathrm{tensor}$.

the associator map of unit and associator (from the name)

Let $\mathrm{tensor}$ be a functor of $C$ and the set of functors of $C$ and $C$. Let $\mathrm{unit}$ be an element of $C$. Let $\mathrm{associator}$ be an isomorphism of the bifunctor composition of $\mathrm{tensor}$ and $\mathrm{tensor}$ and the bifunctor composition of $\mathrm{tensor}$ and $\mathrm{tensor}$. Then the associator map of $\mathrm{unit}$ and $\mathrm{associator}$ is a homomorphism of the source of $\mathrm{tensor}$ and $\mathrm{unit}$ and the middle of $\mathrm{tensor}$ and $\mathrm{unit}$.

the first map of associator and leftUnitor (from the name)

Let $\mathrm{tensor}$ be a functor of $C$ and the set of functors of $C$ and $C$. Let $\mathrm{unit}$ be an element of $C$. Let $\mathrm{associator}$ be an isomorphism of the bifunctor composition of $\mathrm{tensor}$ and $\mathrm{tensor}$ and the bifunctor composition of $\mathrm{tensor}$ and $\mathrm{tensor}$. Let $\mathrm{leftUnitor}$ be an isomorphism of the action of $\mathrm{tensor}$ and $\mathrm{unit}$ and the identity of $C$. Then the first map of $\mathrm{associator}$ and $\mathrm{leftUnitor}$ is a homomorphism of the source of $\mathrm{tensor}$ and $\mathrm{unit}$ and $\mathrm{tensor}$ defined as the composition of the associator map of $\mathrm{unit}$ and $\mathrm{associator}$ and the left unitor map of $\mathrm{unit}$ and $\mathrm{leftUnitor}$.

the left unitor map of unit and leftUnitor (from the name)

Let $\mathrm{tensor}$ be a functor of $C$ and the set of functors of $C$ and $C$. Let $\mathrm{unit}$ be an element of $C$. Let $\mathrm{leftUnitor}$ be an isomorphism of the action of $\mathrm{tensor}$ and $\mathrm{unit}$ and the identity of $C$. Then the left unitor map of $\mathrm{unit}$ and $\mathrm{leftUnitor}$ is a homomorphism of the middle of $\mathrm{tensor}$ and $\mathrm{unit}$ and $\mathrm{tensor}$.

the middle of tensor and unit (from the name)

Let $\mathrm{tensor}$ be a functor of $C$ and the set of functors of $C$ and $C$. Let $\mathrm{unit}$ be an element of $C$. Then the middle of $\mathrm{tensor}$ and $\mathrm{unit}$ is a functor of $C$ and the set of functors of $C$ and $C$ defined as the composition of $\mathrm{tensor}$ and the action of the flip of the right whiskering of $C$ and $C$ and the action of $\mathrm{tensor}$ and $\mathrm{unit}$.

the second map of unit and rightUnitor (from the name)

Let $\mathrm{tensor}$ be a functor of $C$ and the set of functors of $C$ and $C$. Let $\mathrm{unit}$ be an element of $C$. Let $\mathrm{rightUnitor}$ be an isomorphism of the action of the flip of $\mathrm{tensor}$ and $\mathrm{unit}$ and the identity of $C$. Then the second map of $\mathrm{unit}$ and $\mathrm{rightUnitor}$ is a homomorphism of the source of $\mathrm{tensor}$ and $\mathrm{unit}$ and $\mathrm{tensor}$.

the source of tensor and unit (from the name)

Let $\mathrm{tensor}$ be a functor of $C$ and the set of functors of $C$ and $C$. Let $\mathrm{unit}$ be an element of $C$. Then the source of $\mathrm{tensor}$ and $\mathrm{unit}$ is a functor of $C$ and the set of functors of $C$ and $C$ defined as the composition of the action of the flip of $\mathrm{tensor}$ and $\mathrm{unit}$ and $\mathrm{tensor}$.

homomorphism of F and G (from the name)

Let $F$ and $G$ be elements of $\operatorname{LaxMonoidalFunctor}$ applied to $C$ and $D$. Then the homomorphisms of $F$ and $G$ are a basic type.

the homomorphism of self (from the name)

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

the homomorphism of f (from the name)

Let $f$ be a homomorphism of $\operatorname{toFunctor}$ applied to $F$ and $\operatorname{toFunctor}$ applied to $G$. Then the homomorphism of $f$ is a homomorphism of $F$ and $G$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $\operatorname{toFunctor}$ applied to $F$ and $\operatorname{toFunctor}$ applied to $G$. Then the isomorphism of $e$ is an isomorphism of $F$ and $G$.

the isomorphism of e (from the name)

Let $e$ be a function from elements $X_{2}$ of $C$ to isomorphisms of the action of $\operatorname{toFunctor}$ applied to $F$ and $X_{2}$ and the action of $\operatorname{toFunctor}$ applied to $G$ and $X_{2}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $X_{1}$ of $C$, for all elements $Y_{1}$ of $C$, for all homomorphisms $f$ of $X_{1}$ and $Y_{1}$, the composition of the map of $\operatorname{toFunctor}$ applied to $F$ and $f$ and the homomorphism of $e$ applied to $Y_{1}$ is equal to the composition of the homomorphism of $e$ applied to $X_{1}$ and the map of $\operatorname{toFunctor}$ applied to $G$ and $f$ and $\mathrm{CategoryTheory\_\_LaxMonoidalFunctor\_\_isoOfComponents\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for the proposition that the composition of $\mathrm{CategoryTheory\_\_Functor\_\_LaxMonoidal\_\_\_u3b5\_}$ applied to $\operatorname{toFunctor}$ applied to $F$ and the homomorphism of $e$ applied to the tensor unity in the monoidal structure of $C$ is equal to $\mathrm{CategoryTheory\_\_Functor\_\_LaxMonoidal\_\_\_u3b5\_}$ applied to $\operatorname{toFunctor}$ applied to $G$ and $\mathrm{CategoryTheory\_\_LaxMonoidalFunctor\_\_isoOfComponents\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $X$ of $C$, for all elements $Y$ of $C$, the composition of $\mathrm{CategoryTheory\_\_Functor\_\_LaxMonoidal\_\_\_u3bc\_}$ applied to $\operatorname{toFunctor}$ applied to $F$, $X$ and $Y$ and the homomorphism of $e$ applied to the tensor object of $X$ and $Y$ is equal to the composition of the tensor homomorphism of the homomorphism of $e$ applied to $X$ and the homomorphism of $e$ applied to $Y$ and $\mathrm{CategoryTheory\_\_Functor\_\_LaxMonoidal\_\_\_u3bc\_}$ applied to $\operatorname{toFunctor}$ applied to $G$, $X$ and $Y$ and $\mathrm{CategoryTheory\_\_LaxMonoidalFunctor\_\_isoOfComponents\_\_\_auto\_5}$. Then the isomorphism of $X_{2}$ is an isomorphism of $F$ and $G$ defined as the function that maps $\mathrm{tensor}$ to the isomorphism of the natural isomorphism of $X_{2}$ and the function that maps $x_{4}$ and $x_{5}$ to $e$ applied to $x_{4}$ and $x_{5}$.

x6 is monoidal (from the docstring)

Let $x_{6}$ be a homomorphism of $x_{4}$ and $x_{5}$. Then we can say that $x_{6}$ is monoidal.

Let $f$ be an isomorphism of $X$ and $Y$. Then $\operatorname{mop}$ applied to $f$ is an isomorphism of $\operatorname{mop}$ applied to $X$ and $\operatorname{mop}$ applied to $Y$ defined as the map isomorphism of $\operatorname{mopFunctor}$ applied to $C$ and $f$.

Let $f$ be an isomorphism of $X$ and $Y$. Then $\operatorname{unmop}$ applied to $f$ is an isomorphism of $\operatorname{unmop}$ applied to $X$ and $\operatorname{unmop}$ applied to $Y$ defined as the map isomorphism of $\operatorname{unmopFunctor}$ applied to $C$ and $f$.

monoidal opposite of C (from the name)

Let $C$ be a set. Then the monoidal opposites of $C$ are a basic type.

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

Let $C$ be a set. Then $\operatorname{mopMopEquivalence}$ applied to $C$ is an equivalence of the set of monoidal opposites of the set of monoidal opposites of $C$ and $C$ defined as the composition of $\operatorname{unmopEquiv}$ applied to the set of monoidal opposites of $C$ and $\operatorname{unmopEquiv}$ applied to $C$.

the tensor isomorphism of C (from the name)

Let $C$ be a set. Then the tensor isomorphism of $C$ is an isomorphism of the tensor of the set of monoidal opposites of $C$ and the composition of the product of $\operatorname{unmopFunctor}$ applied to $C$ and $\operatorname{unmopFunctor}$ applied to $C$ and the composition of the swap of $C$ and $C$ and the composition of the tensor of $C$ and $\operatorname{mopFunctor}$ applied to $C$ defined as the identity of the tensor of the set of monoidal opposites of $C$.

the tensor left isomorphism of X (from the name)

Let $X$ be a monoidal opposite of $C$. Then the tensor left isomorphism of $X$ is an isomorphism of the left tensor of $X$ and the composition of $\operatorname{unmopFunctor}$ applied to $C$ and the composition of the right tensor of $\operatorname{unmop}$ applied to $X$ and $\operatorname{mopFunctor}$ applied to $C$ defined as the identity of the left tensor of $X$.

Let $X$ be an element of $C$. Then $\operatorname{tensorLeftMopIso}$ applied to $X$ is an isomorphism of the left tensor of $\operatorname{mop}$ applied to $X$ and the composition of $\operatorname{unmopFunctor}$ applied to $C$ and the composition of the right tensor of $X$ and $\operatorname{mopFunctor}$ applied to $C$ defined as the identity of the left tensor of $\operatorname{mop}$ applied to $X$.

Let $X$ be a monoidal opposite of $C$. Then $\operatorname{tensorLeftUnmopIso}$ applied to $X$ is an isomorphism of the left tensor of $\operatorname{unmop}$ applied to $X$ and the composition of $\operatorname{mopFunctor}$ applied to $C$ and the composition of the right tensor of $X$ and $\operatorname{unmopFunctor}$ applied to $C$ defined as the identity of the left tensor of $\operatorname{unmop}$ applied to $X$.

the tensor right isomorphism of X (from the name)

Let $X$ be a monoidal opposite of $C$. Then the tensor right isomorphism of $X$ is an isomorphism of the right tensor of $X$ and the composition of $\operatorname{unmopFunctor}$ applied to $C$ and the composition of the left tensor of $\operatorname{unmop}$ applied to $X$ and $\operatorname{mopFunctor}$ applied to $C$ defined as the identity of the right tensor of $X$.

Let $X$ be an element of $C$. Then $\operatorname{tensorRightMopIso}$ applied to $X$ is an isomorphism of the right tensor of $\operatorname{mop}$ applied to $X$ and the composition of $\operatorname{unmopFunctor}$ applied to $C$ and the composition of the left tensor of $X$ and $\operatorname{mopFunctor}$ applied to $C$ defined as the identity of the right tensor of $\operatorname{mop}$ applied to $X$.

Let $X$ be a monoidal opposite of $C$. Then $\operatorname{tensorRightUnmopIso}$ applied to $X$ is an isomorphism of the right tensor of $\operatorname{unmop}$ applied to $X$ and the composition of $\operatorname{mopFunctor}$ applied to $C$ and the composition of the left tensor of $X$ and $\operatorname{unmopFunctor}$ applied to $C$ defined as the identity of the right tensor of $\operatorname{unmop}$ applied to $X$.

Let $\mathrm{self}$ be a monoidal opposite of $C$. Then $\operatorname{unmop}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $C$ be a set. Then $\operatorname{unmopEquiv}$ applied to $C$ is an equivalence of the set of monoidal opposites of $C$ and $C$ defined as the inverse of $\operatorname{mopEquiv}$ applied to $C$.

Let $C$ be a set. Then $\operatorname{mopFunctor}$ applied to $C$ is a functor of $C$ and the set of monoidal opposites of $C$.

Let $C$ be a set. Then $\operatorname{unmopFunctor}$ applied to $C$ is a functor of the set of monoidal opposites of $C$ and $C$.

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

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

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

$\operatorname{mopEquivCompForgetIso}$ is an isomorphism of the composition of the functor of $\operatorname{mopEquiv}$ applied to $C$ and $\operatorname{forget}$ applied to the set of monoidal opposites of $C$ and the composition of $\operatorname{forget}$ applied to $C$ and the functor of $\operatorname{mopEquiv}$ applied to $C$ defined as the identity of the composition of the functor of $\operatorname{mopEquiv}$ applied to $C$ and $\operatorname{forget}$ applied to the set of monoidal opposites of $C$.

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

the left distributor of X and f (from the name)

Let $X$ be an element of $C$. Let $f$ be a function from elements of $J$ to elements of $C$. Then the left distributor of $X$ and $f$ is an isomorphism of the tensor object of $X$ and the biproduct of $f$ and the biproduct of the function that maps $j$ to the tensor object of $X$ and $f$ applied to $j$ defined as the map biproduct of the left tensor of $X$ and $f$.

the right distributor of f and X (from the name)

Let $f$ be a function from elements of $J$ to elements of $C$. Let $X$ be an element of $C$. Then the right distributor of $f$ and $X$ is an isomorphism of the tensor object of the biproduct of $f$ and $X$ and the biproduct of the function that maps $j$ to the tensor object of $f$ applied to $j$ and $X$ defined as the map biproduct of the right tensor of $X$ and $f$.

the arrow isomorphism of X and i (from the docstring)

Let $X$ be an arrow of $C$. Let $i$ be an element of $\operatorname{IsInitial}$ applied to $I$. Then the arrow isomorphism of $X$ and $i$ is an isomorphism of the action of the action of the pullback homomorphism and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $\operatorname{to}$ applied to $i$ and $W$ and $X$ and $\operatorname{mk}$ applied to the map of $\operatorname{ihom}$ applied to $W$ and the homomorphism of $X$.

the arrow isomorphism of X and t (from the docstring)

Let $X$ be an arrow of $C$. Let $t$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then the arrow isomorphism of $X$ and $t$ is an isomorphism of the action of the action of the pullback homomorphism and $\operatorname{op}$ applied to $X$ and $\operatorname{mk}$ applied to $\operatorname{from}$ applied to $t$ and $W$ and $\operatorname{mk}$ applied to the component of $\operatorname{pre}$ applied to the homomorphism of $X$ and $W$.

the associator of x3 and x4 (from the name)

Let $x_{2}$, $x_{3}$ and $x_{4}$ be arrows of $C$. Then the associator of $x_{3}$ and $x_{4}$ is an isomorphism of the action of the action of the pushout product and the action of the action of the pushout product and $x_{2}$ and $x_{3}$ and $x_{4}$ and the action of the action of the pushout product and $x_{2}$ and the action of the action of the pushout product and $x_{3}$ and $x_{4}$.

the braiding of x3 and x4 (from the name)

Let $x_{3}$ and $x_{4}$ be arrows of $C$. Then the braiding of $x_{3}$ and $x_{4}$ is an isomorphism of the action of the action of the pushout product and $x_{3}$ and $x_{4}$ and the action of the action of the pushout product and $x_{4}$ and $x_{3}$.

Let $X$ be an arrow of $C$. Let $i$ be an element of $\operatorname{IsInitial}$ applied to $I$. Let $t$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then $\operatorname{isInitialIsTerminalIso}$ applied to $X$, $i$ and $t$ is an isomorphism of the action of the action of the pushout product and $X$ and $\operatorname{mk}$ applied to $\operatorname{to}$ applied to $i$ and $T$ and $X$.

Let $X$ be an arrow of $C$. Let $i$ be an element of $\operatorname{IsInitial}$ applied to $I$. Let $t$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then $\operatorname{isInitialIsTerminalIso'}$ applied to $X$, $i$ and $t$ is an isomorphism of the action of the action of the pushout product and $X$ and $\operatorname{mk}$ applied to $\operatorname{from}$ applied to $t$ and $I$ and $X$.

the arrow isomorphism of X and i (from the docstring)

Let $X$ be an arrow of $C$. Let $i$ be an element of $\operatorname{IsInitial}$ applied to $I$. Then the arrow isomorphism of $X$ and $i$ is an isomorphism of the action of the action of the pushout product and $X$ and $\operatorname{mk}$ applied to $\operatorname{to}$ applied to $i$ and $W$ and $\operatorname{mk}$ applied to the right whisker of the homomorphism of $X$ and $W$.

the arrow isomorphism of X and i (from the docstring)

Let $X$ be an arrow of $C$. Let $i$ be an element of $\operatorname{IsInitial}$ applied to $I$. Then the arrow isomorphism of $X$ and $i$ is an isomorphism of the action of the action of the pushout product and $\operatorname{mk}$ applied to $\operatorname{to}$ applied to $i$ and $W$ and $X$ and $\operatorname{mk}$ applied to the left whisker of $W$ and the homomorphism of $X$.

the left unitor of X (from the name)

Let $X$ be an arrow of $C$. Then the left unitor of $X$ is an isomorphism of the action of the action of the pushout product and $\operatorname{mk}$ applied to $\operatorname{to}$ applied to the tensor unity in the monoidal structure of $C$ and $X$ and $X$ defined as the composition of the braiding of $\operatorname{mk}$ applied to $\operatorname{to}$ applied to the tensor unity in the monoidal structure of $C$ and $X$ and the right unitor of $X$.

the right unitor of X (from the name)

Let $X$ be an arrow of $C$. Then the right unitor of $X$ is an isomorphism of the action of the action of the pushout product and $X$ and $\operatorname{mk}$ applied to $\operatorname{to}$ applied to the tensor unity in the monoidal structure of $C$ and $X$.

the whisker left isomorphism of x2 and x3 (from the name)

Let $x_{2}$ and $x_{3}$ be arrows of $C$. Then the whisker left isomorphism of $x_{2}$ and $x_{3}$ is an isomorphism of $\operatorname{mk}$ applied to the left whisker of $W$ and the homomorphism of the action of the action of the pushout product and $x_{2}$ and $x_{3}$ and the action of the action of the pushout product and $\operatorname{mk}$ applied to the left whisker of $W$ and the homomorphism of $x_{2}$ and $x_{3}$.

the whisker right isomorphism of x2 and x3 (from the name)

Let $x_{2}$ and $x_{3}$ be arrows of $C$. Then the whisker right isomorphism of $x_{2}$ and $x_{3}$ is an isomorphism of $\operatorname{mk}$ applied to the right whisker of the homomorphism of the action of the action of the pushout product and $x_{2}$ and $x_{3}$ and $W$ and the action of the action of the pushout product and $x_{2}$ and $\operatorname{mk}$ applied to the right whisker of the homomorphism of $x_{3}$ and $W$.

the pullback homomorphism (from the name)

The pullback homomorphism is a functor of the set of opposites of the set of arrows of $C$ and the set of functors of the set of arrows of $C$ and the set of arrows of $C$ defined as $\operatorname{leibnizPullback}$ applied to the internal homomorphism.

the pushout product (from the name)

The pushout product is a functor of the set of arrows of $C$ and the set of functors of the set of arrows of $C$ and the set of arrows of $C$ defined as $\operatorname{leibnizPushout}$ applied to the tensor product bifunctor of $C$.

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

the coevaluation of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the coevaluation of $X$ and $Y$ is a homomorphism of the tensor unity in the monoidal structure of $C$ and the tensor object of $X$ and $Y$ defined as the coevaluation.

the coevaluation (from the name)

The coevaluation is a homomorphism of the tensor unity in the monoidal structure of $C$ and the tensor object of $X$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the evaluation of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the evaluation of $X$ and $Y$ is a homomorphism of the tensor object of $Y$ and $X$ and the tensor unity in the monoidal structure of $C$ defined as the evaluation.

the evaluation (from the name)

The evaluation is a homomorphism of the tensor object of $Y$ and $X$ and the tensor unity in the monoidal structure of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Y has left duals (from the name)

Let $Y$ be an element of $C$. Then we can say that $Y$ has left duals.

the left dual of the object of Y (from the docstring)

Let $Y$ be an element of $C$. Then the left dual of the object of $Y$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

X has right duals (from the name)

Let $X$ be an element of $C$. Then we can say that $X$ has right duals.

the right dual of X (from the name)

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

C is a left rigid category (from the name)

Let $C$ be a set. Then we can say that $C$ is a left rigid category.

C is a right rigid category (from the name)

Let $C$ be a set. Then we can say that $C$ is a right rigid category.

C is a rigid category (from the name)

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

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{leftAdjointMate}$ applied to $f$ is a homomorphism of the left dual of the object of $Y$ and the left dual of the object of $X$ defined as the composition of the inverse of the left unitor of the left dual of the object of $Y$ and the composition of the right whisker of the coevaluation of the left dual of the object of $X$ and $X$ and the left dual of the object of $Y$ and the composition of the right whisker of the left whisker of the left dual of the object of $X$ and $f$ and the left dual of the object of $Y$ and the composition of the homomorphism of the associator of $Y$ and the left dual of the object of $Y$ and the composition of the left whisker of the left dual of the object of $X$ and the evaluation of the left dual of the object of $Y$ and $Y$ and the homomorphism of the right unitor of the left dual of the object of $X$.

the left dual isomorphism of x4 and x5 (from the name)

Assume that $\operatorname{ExactPairing}$ holds for $x_{2}$ and $Y$. Assume that $\operatorname{ExactPairing}$ holds for $x_{3}$ and $Y$. Then the left dual isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $x_{2}$ and $x_{3}$.

the left dual of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $C$. Then the left dual of $X$ and $Y$ is an isomorphism of the left dual of the object of the tensor object of $X$ and $Y$ and the tensor object of the left dual of the object of $Y$ and the left dual of the object of $X$ defined as the left dual isomorphism of $\operatorname{exact}$ and $\operatorname{tensor}$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{rightAdjointMate}$ applied to $f$ is a homomorphism of the right dual of $Y$ and the right dual of $X$ defined as the composition of the inverse of the right unitor of the right dual of $Y$ and the composition of the left whisker of the right dual of $Y$ and the coevaluation of $X$ and the right dual of $X$ and the composition of the left whisker of the right dual of $Y$ and the right whisker of $f$ and the right dual of $X$ and the composition of the inverse of the associator of $Y$ and the right dual of $X$ and the composition of the right whisker of the evaluation of $Y$ and the right dual of $Y$ and the right dual of $X$ and the homomorphism of the left unitor of the right dual of $X$.

the right dual isomorphism of x4 and x5 (from the name)

Assume that $\operatorname{ExactPairing}$ holds for $X$ and $x_{2}$. Assume that $\operatorname{ExactPairing}$ holds for $X$ and $x_{3}$. Then the right dual isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $x_{2}$ and $x_{3}$.

the right dual of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $C$. Then the right dual of $X$ and $Y$ is an isomorphism of the right dual of the tensor object of $X$ and $Y$ and the tensor object of the right dual of $Y$ and the right dual of $X$ defined as the right dual isomorphism of $\operatorname{exact}$ and $\operatorname{tensor}$.

the tensor left adjunction of Y and #2 (from the name)

Let $Y$ and $\mathrm{Y'}$ be elements of $C$. Then the tensor left adjunction of $Y$ and $\mathrm{Y'}$ is an adjunction of the left tensor of $\mathrm{Y'}$ and the left tensor of $Y$ defined as $\operatorname{mkOfHomEquiv}$ applied to $\operatorname{mk}$ applied to the function that maps $X$ and $Z$ to the tensor left homomorphism equivalence of $\mathrm{Y'}$ and $Z$, the function that maps $x_{3}$, $x_{4}$, $x_{5}$, $f$ and $g$ to $\mathrm{CategoryTheory\_\_tensorLeftHomEquiv\_symm\_naturality}$ applied to $f$ and $g$ and the function that maps $x_{6}$, $x_{7}$, $x_{8}$, $f_{1}$ and $g_{1}$ to $\mathrm{CategoryTheory\_\_tensorLeftHomEquiv\_naturality}$ applied to $f_{1}$ and $g_{1}$.

the tensor left homomorphism equivalence of Z and #4 (from the name)

Let $X$, $Y$, $\mathrm{Y'}$ and $Z$ be elements of $C$. Then the tensor left homomorphism equivalence of $\mathrm{Y'}$ and $Z$ is an equivalence from the set of homomorphisms of the tensor object of $\mathrm{Y'}$ and $X$ and $Z$ to the set of homomorphisms of $X$ and the tensor object of $Y$ and $Z$.

the tensor right adjunction of Y and #2 (from the name)

Let $Y$ and $\mathrm{Y'}$ be elements of $C$. Then the tensor right adjunction of $Y$ and $\mathrm{Y'}$ is an adjunction of the right tensor of $Y$ and the right tensor of $\mathrm{Y'}$ defined as $\operatorname{mkOfHomEquiv}$ applied to $\operatorname{mk}$ applied to the function that maps $X$ and $Z$ to the tensor right homomorphism equivalence of $\mathrm{Y'}$ and $Z$, the function that maps $x_{3}$, $x_{4}$, $x_{5}$, $f$ and $g$ to $\mathrm{CategoryTheory\_\_tensorRightHomEquiv\_symm\_naturality}$ applied to $f$ and $g$ and the function that maps $x_{6}$, $x_{7}$, $x_{8}$, $f_{1}$ and $g_{1}$ to $\mathrm{CategoryTheory\_\_tensorRightHomEquiv\_naturality}$ applied to $f_{1}$ and $g_{1}$.

the tensor right homomorphism equivalence of Z and #4 (from the name)

Let $X$, $Y$, $\mathrm{Y'}$ and $Z$ be elements of $C$. Then the tensor right homomorphism equivalence of $\mathrm{Y'}$ and $Z$ is an equivalence from the set of homomorphisms of the tensor object of $X$ and $Y$ and $Z$ to the set of homomorphisms of $X$ and the tensor object of $Z$ and $\mathrm{Y'}$.

the left dual functor of C (from the name)

Let $C$ be a set. Then the left dual functor of $C$ is a functor of $C$ and the set of monoidal opposites of the set of opposites of $C$.

the right dual functor of C (from the name)

Let $C$ be a set. Then the right dual functor of $C$ is a functor of $C$ and the set of monoidal opposites of the set of opposites of $C$.

R is a commutative ring object (from the name)

Let $R$ be an element of $C$. Then we can say that $R$ is a commutative ring object.

commutative ring object category of C (from the name)

Let $C$ be a set. Then the commutative ring object categories of $C$ are a basic type.

homomorphism of x3 and x4 (from the name)

Let $x_{3}$ and $x_{4}$ be commutative ring object categories of $C$. Then the homomorphisms of $x_{3}$ and $x_{4}$ are a basic type.

the homomorphism of self (from the name)

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

Let $\mathrm{self}$ be a commutative ring object category of $C$. Then $\operatorname{X}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

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

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_CommRingObjCat\_\_forget\_u2082\_RingObjCat}$ applied to $C$ is a functor of the set of commutative ring object categories of $C$ and the set of ring object categories of $C$.

the forgetful functor of C (from the docstring)

Let $C$ be a set. Then the forgetful functor of $C$ is an element of $\operatorname{FullyFaithful}$ applied to $\mathrm{CategoryTheory\_\_CommRingObjCat\_\_forget\_u2082\_RingObjCat}$ applied to $C$.

f is a ring homomorphism (from the name)

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Then we can say that $f$ is a ring homomorphism.

R is a ring object (from the name)

Let $R$ be an element of $C$. Then we can say that $R$ is a ring object.

ring object category of C (from the name)

Let $C$ be a set. Then the ring object categories of $C$ are a basic type.

homomorphism of x3 and x4 (from the name)

Let $x_{3}$ and $x_{4}$ be ring object categories of $C$. Then the homomorphisms of $x_{3}$ and $x_{4}$ are a basic type.

the homomorphism of self (from the name)

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

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

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

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_RingObjCat\_\_forget\_u2082\_AddMon}$ applied to $C$ is a functor of the set of ring object categories of $C$ and the set of additive monoids of $C$.

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_RingObjCat\_\_forget\_u2082\_Mon}$ applied to $C$ is a functor of the set of ring object categories of $C$ and the set of monoids of $C$.

the monoid homomorphism of F (from the name)

Let $F$ be a functor of $C$ and $D$. Assume that $C$ is skeletal. Assume that $D$ is skeletal. Then the monoid homomorphism of $F$ is a monoid homomorphism of $C$ and $D$.

the multiplicative equivalence of e (from the name)

Let $e$ be an equivalence of $C$ and $D$. Assume that $C$ is skeletal. Assume that $D$ is skeletal. Then the multiplicative equivalence of $e$ is a multiplicative equivalence of $C$ and $D$.

the monoid homomorphism of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the monoid homomorphism of $F$ is a monoid homomorphism of the set of skeletons of $C$ and the set of skeletons of $D$ defined as the monoid homomorphism of the map skeleton of $F$.

the multiplicative equivalence of e (from the name)

Let $e$ be an equivalence of $C$ and $D$. Then the multiplicative equivalence of $e$ is a multiplicative equivalence of the set of skeletons of $C$ and the set of skeletons of $D$ defined as the multiplicative equivalence of the composition of the composition of the skeleton equivalence of $C$ and $e$ and the inverse of the skeleton equivalence of $D$.

Let $P$ be an object property of $C$. Then we can say that $\operatorname{ContainsUnit}$ holds for $P$.

P is monoidal (from the name)

Let $P$ be an object property of $C$. Then we can say that $P$ is monoidal.

Let $P$ be an object property of $C$. Then we can say that $\operatorname{IsMonoidalClosed}$ holds for $P$.

Let $x_{2}$, $x_{3}$ and $Q$ be object properties of $C$. Then we can say that $\operatorname{TensorLE}$ holds for $x_{2}$, $x_{3}$ and $Q$.

Let $C$ be a set. Let $n$ be a natural number. Then $\operatorname{Tor}$ applied to $C$ and $n$ is a functor of $C$ and the set of functors of $C$ and $C$.

Let $C$ be a set. Let $n$ be a natural number. Then $\operatorname{Tor'}$ applied to $C$ and $n$ is a functor of $C$ and the set of functors of $C$ and $C$.