Definitions: Mathlib.CategoryTheory, part 17 of 25

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

Let $F$ be a functor of $D$ and $\mathrm{D'}$. Let $c$ be an element of $C$. Let $d$ be an element of $D$. Then $\mathrm{CategoryTheory\_\_Functor\_\_LaxLeftLinear\_\_\_u3bc\_\_u2097\_}$ applied to $F$, $c$ and $d$ is a homomorphism of the action object of $c$ and the action of $F$ and $d$ and the action of $F$ and the action object of $c$ and $d$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $c$ and $d$.

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

Let $F$ be a functor of $D$ and $\mathrm{D'}$. Let $d$ be an element of $D$. Let $c$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_Functor\_\_LaxRightLinear\_\_\_u3bc\_\_u1d63\_}$ applied to $F$, $d$ and $c$ is a homomorphism of the action object of the action of $F$ and $d$ and $c$ and the action of $F$ and the action object of $d$ and $c$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $d$ and $c$.

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

the isomorphism of c and d (from the name)

Let $F$ be a functor of $D$ and $\mathrm{D'}$. Let $c$ be an element of $C$. Let $d$ be an element of $D$. Then the isomorphism of $c$ and $d$ is an isomorphism of the action object of $c$ and the action of $F$ and $d$ and the action of $F$ and the action object of $c$ and $d$.

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

Let $F$ be a functor of $D$ and $\mathrm{D'}$. Let $c$ be an element of $C$. Let $d$ be an element of $D$. Then $\mathrm{CategoryTheory\_\_Functor\_\_OplaxLeftLinear\_\_\_u3b4\_\_u2097\_}$ applied to $F$, $c$ and $d$ is a homomorphism of the action of $F$ and the action object of $c$ and $d$ and the action object of $c$ and the action of $F$ and $d$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $c$ and $d$.

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

Let $F$ be a functor of $D$ and $\mathrm{D'}$. Let $d$ be an element of $D$. Let $c$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_Functor\_\_OplaxRightLinear\_\_\_u3b4\_\_u1d63\_}$ applied to $F$, $d$ and $c$ is a homomorphism of the action of $F$ and the action object of $d$ and $c$ and the action object of the action of $F$ and $d$ and $c$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $d$ and $c$.

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

the isomorphism of d and c (from the name)

Let $F$ be a functor of $D$ and $\mathrm{D'}$. Let $d$ be an element of $D$. Let $c$ be an element of $C$. Then the isomorphism of $d$ and $c$ is an isomorphism of the action object of the action of $F$ and $d$ and $c$ and the action of $F$ and the action object of $d$ and $c$.

Let $A$ and $B$ be monoids of $C$. Then the elements of $\mathrm{Bimod}$ applied to $A$ and $B$ are a basic type.

the homomorphism of Q and L (from the name)

Let $P$ be an element of $\mathrm{Bimod}$ applied to $R$ and $S$. Let $Q$ be an element of $\mathrm{Bimod}$ applied to $S$ and $T$. Let $L$ be an element of $\mathrm{Bimod}$ applied to $T$ and $U$. Then the homomorphism of $Q$ and $L$ is a homomorphism of $\operatorname{X}$ applied to $\operatorname{tensorBimod}$ applied to $\operatorname{tensorBimod}$ applied to $P$ and $Q$ and $L$ and $\operatorname{X}$ applied to $\operatorname{tensorBimod}$ applied to $P$ and $\operatorname{tensorBimod}$ applied to $Q$ and $L$.

the inverse of Q and L (from the name)

Let $P$ be an element of $\mathrm{Bimod}$ applied to $R$ and $S$. Let $Q$ be an element of $\mathrm{Bimod}$ applied to $S$ and $T$. Let $L$ be an element of $\mathrm{Bimod}$ applied to $T$ and $U$. Then the inverse of $Q$ and $L$ is a homomorphism of $\operatorname{X}$ applied to $\operatorname{tensorBimod}$ applied to $P$ and $\operatorname{tensorBimod}$ applied to $Q$ and $L$ and $\operatorname{X}$ applied to $\operatorname{tensorBimod}$ applied to $\operatorname{tensorBimod}$ applied to $P$ and $Q$ and $L$.

homomorphism of M and N (from the name)

Let $M$ and $N$ be elements of $\mathrm{Bimod}$ applied to $A$ and $B$. 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}$.

the homomorphism of P (from the name)

Let $P$ be an element of $\mathrm{Bimod}$ applied to $R$ and $S$. Then the homomorphism of $P$ is a homomorphism of $\operatorname{X}$ applied to the regular of $R$ and $P$ and $\operatorname{X}$ applied to $P$.

the inverse of P (from the name)

Let $P$ be an element of $\mathrm{Bimod}$ applied to $R$ and $S$. Then the inverse of $P$ is a homomorphism of $\operatorname{X}$ applied to $P$ and $\operatorname{X}$ applied to the regular of $R$ and $P$ defined as the composition of the inverse of the left unitor of $\operatorname{X}$ applied to $P$ and the composition of the right whisker of the one and $\operatorname{X}$ applied to $P$ and the projection of the right whisker of $\operatorname{actRight}$ applied to the regular of $R$ and $\operatorname{X}$ applied to $P$ and the composition of the homomorphism of the associator of $\operatorname{X}$ applied to $R$ and $\operatorname{X}$ applied to $P$ and the left whisker of $\operatorname{X}$ applied to the regular of $R$ and $\operatorname{actLeft}$ applied to $P$.

the homomorphism of P (from the name)

Let $P$ be an element of $\mathrm{Bimod}$ applied to $R$ and $S$. Then the homomorphism of $P$ is a homomorphism of $\operatorname{X}$ applied to $P$ and the regular of $S$ and $\operatorname{X}$ applied to $P$.

the inverse of P (from the name)

Let $P$ be an element of $\mathrm{Bimod}$ applied to $R$ and $S$. Then the inverse of $P$ is a homomorphism of $\operatorname{X}$ applied to $P$ and $\operatorname{X}$ applied to $P$ and the regular of $S$ defined as the composition of the inverse of the right unitor of $\operatorname{X}$ applied to $P$ and the composition of the left whisker of $\operatorname{X}$ applied to $P$ and the one and the projection of the right whisker of $\operatorname{actRight}$ applied to $P$ and $\operatorname{X}$ applied to the regular of $S$ and the composition of the homomorphism of the associator of $\operatorname{X}$ applied to $S$ and $\operatorname{X}$ applied to the regular of $S$ and the left whisker of $\operatorname{X}$ applied to $P$ and $\operatorname{actLeft}$ applied to the regular of $S$.

Let $P$ be an element of $\mathrm{Bimod}$ applied to $R$ and $S$. Let $Q$ be an element of $\mathrm{Bimod}$ applied to $S$ and $T$. Then $\operatorname{X}$ applied to $P$ and $Q$ is an element of $C$ defined as the coequalizer of the right whisker of $\operatorname{actRight}$ applied to $P$ and $\operatorname{X}$ applied to $Q$ and the composition of the homomorphism of the associator of $\operatorname{X}$ applied to $S$ and $\operatorname{X}$ applied to $Q$ and the left whisker of $\operatorname{X}$ applied to $P$ and $\operatorname{actLeft}$ applied to $Q$.

Let $P$ be an element of $\mathrm{Bimod}$ applied to $R$ and $S$. Let $Q$ be an element of $\mathrm{Bimod}$ applied to $S$ and $T$. Then $\operatorname{actLeft}$ applied to $P$ and $Q$ is a homomorphism of the tensor object of $\operatorname{X}$ applied to $R$ and $\operatorname{X}$ applied to $P$ and $Q$ and $\operatorname{X}$ applied to $P$ and $Q$.

Let $P$ be an element of $\mathrm{Bimod}$ applied to $R$ and $S$. Let $Q$ be an element of $\mathrm{Bimod}$ applied to $S$ and $T$. Then $\operatorname{actRight}$ applied to $P$ and $Q$ is a homomorphism of the tensor object of $\operatorname{X}$ applied to $P$ and $Q$ and $\operatorname{X}$ applied to $T$ and $\operatorname{X}$ applied to $P$ and $Q$.

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

Let $\mathrm{self}$ be an element of $\mathrm{Bimod}$ applied to $A$ and $B$. Then $\operatorname{actLeft}$ applied to $\mathrm{self}$ is a homomorphism of the tensor object of $\operatorname{X}$ applied to $A$ and $\operatorname{X}$ applied to $\mathrm{self}$ and $\operatorname{X}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\mathrm{Bimod}$ applied to $A$ and $B$. Then $\operatorname{actRight}$ applied to $\mathrm{self}$ is a homomorphism of the tensor object of $\operatorname{X}$ applied to $\mathrm{self}$ and $\operatorname{X}$ applied to $B$ and $\operatorname{X}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

Let $L$ be an element of $\mathrm{Bimod}$ applied to $W$ and $X$. Let $M$ be an element of $\mathrm{Bimod}$ applied to $X$ and $Y$. Let $N$ be an element of $\mathrm{Bimod}$ applied to $Y$ and $Z$. Then $\operatorname{associatorBimod}$ applied to $L$, $M$ and $N$ is an isomorphism of $\operatorname{tensorBimod}$ applied to $\operatorname{tensorBimod}$ applied to $L$ and $M$ and $N$ and $\operatorname{tensorBimod}$ applied to $L$ and $\operatorname{tensorBimod}$ applied to $M$ and $N$ defined as the isomorphism of $\operatorname{mk}$ applied to the homomorphism of $M$ and $N$, the inverse of $M$ and $N$, $\mathrm{Bimod\_\_AssociatorBimod\_\_hom\_inv\_id}$ applied to $L$, $M$ and $N$ and $\mathrm{Bimod\_\_AssociatorBimod\_\_inv\_hom\_id}$ applied to $L$, $M$ and $N$.

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$.

Let $A$ be a monoid of $C$. Then $\operatorname{forget}$ applied to $A$ is a functor of $\mathrm{Bimod}$ applied to $A$ and $B$ and $C$.

the identity morphism of M (from the docstring)

Let $M$ be an element of $\mathrm{Bimod}$ applied to $A$ and $B$. Then the identity morphism of $M$ is a homomorphism of $M$ and $M$.

the isomorphism of f (from the name)

Let $f$ be an isomorphism of $\operatorname{X}$ applied to $P$ and $\operatorname{X}$ applied to $Q$ such that the composition of $\operatorname{actLeft}$ applied to $P$ and the homomorphism of $f$ is equal to the composition of the left whisker of $\operatorname{X}$ applied to $X$ and the homomorphism of $f$ and $\operatorname{actLeft}$ applied to $Q$ and the composition of $\operatorname{actRight}$ applied to $P$ and the homomorphism of $f$ is equal to the composition of the right whisker of the homomorphism of $f$ and $\operatorname{X}$ applied to $Y$ and $\operatorname{actRight}$ applied to $Q$. Then the isomorphism of $f$ is an isomorphism of $P$ and $Q$.

the left unitor of M (from the docstring)

Let $M$ be an element of $\mathrm{Bimod}$ applied to $X$ and $Y$. Then the left unitor of $M$ is an isomorphism of $\operatorname{tensorBimod}$ applied to the regular of $X$ and $M$ and $M$ defined as the isomorphism of $\operatorname{mk}$ applied to the homomorphism of $M$, the inverse of $M$, $\mathrm{Bimod\_\_LeftUnitorBimod\_\_hom\_inv\_id}$ applied to $M$ and $\mathrm{Bimod\_\_LeftUnitorBimod\_\_inv\_hom\_id}$ applied to $M$.

the regular of A (from the name)

Let $A$ be a monoid of $C$. Then the regular of $A$ is an element of $\mathrm{Bimod}$ applied to $A$ and $A$.

the right unitor of M (from the docstring)

Let $M$ be an element of $\mathrm{Bimod}$ applied to $X$ and $Y$. Then the right unitor of $M$ is an isomorphism of $\operatorname{tensorBimod}$ applied to $M$ and the regular of $Y$ and $M$ defined as the isomorphism of $\operatorname{mk}$ applied to the homomorphism of $M$, the inverse of $M$, $\mathrm{Bimod\_\_RightUnitorBimod\_\_hom\_inv\_id}$ applied to $M$ and $\mathrm{Bimod\_\_RightUnitorBimod\_\_inv\_hom\_id}$ applied to $M$.

Let $M$ be an element of $\mathrm{Bimod}$ applied to $X$ and $Y$. Let $N$ be an element of $\mathrm{Bimod}$ applied to $Y$ and $Z$. Then $\operatorname{tensorBimod}$ applied to $M$ and $N$ is an element of $\mathrm{Bimod}$ applied to $X$ and $Z$ defined as $\operatorname{mk}$ applied to $\operatorname{X}$ applied to $M$ and $N$, $\operatorname{actLeft}$ applied to $M$ and $N$, $\mathrm{Bimod\_\_TensorBimod\_\_one\_act\_left'}$ applied to $M$ and $N$, $\mathrm{Bimod\_\_TensorBimod\_\_left\_assoc'}$ applied to $M$ and $N$, $\operatorname{actRight}$ applied to $M$ and $N$, $\mathrm{Bimod\_\_TensorBimod\_\_actRight\_one'}$ applied to $M$ and $N$, $\mathrm{Bimod\_\_TensorBimod\_\_right\_assoc'}$ applied to $M$ and $N$ and $\mathrm{Bimod\_\_TensorBimod\_\_middle\_assoc'}$ applied to $M$ and $N$.

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

Let $M$ be an element of $\mathrm{Bimod}$ applied to $X$ and $Y$. Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the left whisker of $M$ and $f$ is a homomorphism of $\operatorname{tensorBimod}$ applied to $M$ and $x_{2}$ and $\operatorname{tensorBimod}$ applied to $M$ and $x_{3}$.

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

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $N$ be an element of $\mathrm{Bimod}$ applied to $Y$ and $Z$. Then the right whisker of $f$ and $N$ is a homomorphism of $\operatorname{tensorBimod}$ applied to $x_{2}$ and $N$ and $\operatorname{tensorBimod}$ applied to $x_{3}$ and $N$.

Let $C$ be a set. Then an element of $\operatorname{Bimon}$ applied to $C$ is an element of the function that maps $C$ to $\operatorname{Comon}$ applied to the set of monoids of $C$.

the equivalence (from the docstring)

The equivalence is an equivalence of $\operatorname{Bimon}$ applied to $C$ and the set of monoids of $\operatorname{Comon}$ applied to $C$.

the counit for the equivalence of M (from the docstring)

Let $M$ be a monoid of $\operatorname{Comon}$ applied to $C$. Then the counit for the equivalence of $M$ is an isomorphism of the action of the composition of $\operatorname{ofMonComon}$ applied to $C$ and $\operatorname{toMonComon}$ applied to $C$ and $M$ and $M$.

the unit for the equivalence of M (from the docstring)

Let $M$ be an element of $\operatorname{Bimon}$ applied to $C$. Then the unit for the equivalence of $M$ is an isomorphism of $M$ and the action of the composition of $\operatorname{toMonComon}$ applied to $C$ and $\operatorname{ofMonComon}$ applied to $C$ and $M$ defined as the isomorphism of $\operatorname{equivMonComonUnitIsoAppX}$ applied to $M$.

Let $C$ be a set. Then $\operatorname{forget}$ applied to $C$ is a functor of $\operatorname{Bimon}$ applied to $C$ and $C$ defined as the composition of the monoid of $C$ and $\operatorname{forget}$ applied to $C$.

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

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

the object level part of the backward direction of M (from the docstring)

Let $M$ be a monoid of $\operatorname{Comon}$ applied to $C$. Then the object level part of the backward direction of $M$ is an element of $\operatorname{Bimon}$ applied to $C$ defined as $\operatorname{mk}$ applied to $\operatorname{ofMonComonObjX}$ applied to $M$.

Let $C$ be a set. Then $\operatorname{toComon}$ applied to $C$ is a functor of $\operatorname{Bimon}$ applied to $C$ and $\operatorname{Comon}$ applied to $C$ defined as $\operatorname{mapComon}$ applied to $\operatorname{forget}$ applied to $C$.

the monoid of C (from the name)

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

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

the object level part of the forward direction of M (from the docstring)

Let $M$ be an element of $\operatorname{Bimon}$ applied to $C$. Then the object level part of the forward direction of $M$ is a monoid of $\operatorname{Comon}$ applied to $C$ defined as $\operatorname{mk}$ applied to the action of $\operatorname{toComon}$ applied to $C$ and $M$.

the bimonoid morphism of A (from the docstring)

Let $A$ be an element of $\operatorname{Bimon}$ applied to $C$. Then the bimonoid morphism of $A$ is a homomorphism of $A$ and the trivial bimonoid object of $C$ defined as $\operatorname{default}$.

the trivial bimonoid object of C (from the docstring)

Let $C$ be a set. Then the trivial bimonoid object of $C$ is an element of $\operatorname{Bimon}$ applied to $C$ defined as the trivial comonoid object of the set of monoids of $C$.

Let $A$ be an element of $\operatorname{Bimon}$ applied to $C$. Then $\operatorname{trivialTo}$ applied to $A$ is a homomorphism of the trivial bimonoid object of $C$ and $A$.

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

Let $f$ be a homomorphism of $M$ and $N$. Then we can say that $\operatorname{IsBimonHom}$ holds for $f$.

C is a braided category (from the name)

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

the braiding natural isomorphism of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $C$. Then the braiding natural isomorphism of $X$ and $Y$ is an isomorphism of the tensor object of $X$ and $Y$ and the tensor object of $Y$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $X$ and $Y$.

the braiding isomorphism of C (from the docstring)

Let $C$ be a set. Then the braiding isomorphism of $C$ is an isomorphism of the tensor product bifunctor of $C$ and the flip of the tensor product bifunctor of $C$.

the right tensor left isomorphism tensor of X (from the name)

Let $X$ be an element of $C$. Then the right tensor left isomorphism tensor of $X$ is an isomorphism of the left tensor of $X$ and the right tensor of $X$.

F is braided (from the name)

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

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

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

$\operatorname{forget}$ is a functor of $\operatorname{LaxBraidedFunctor}$ applied to $C$ and $D$ and $\operatorname{LaxMonoidalFunctor}$ applied to $C$ and $D$ defined as the induced functor of $\operatorname{toLaxMonoidalFunctor}$.

$\operatorname{fullyFaithfulForget}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{forget}$ defined as the induced functor of $\operatorname{toLaxMonoidalFunctor}$.

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{\_private\_\_Mathlib\_\_CategoryTheory\_\_Monoidal\_\_Braided\_\_Basic\_\_0\_\_\_auto\_137}$, $\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{\_private\_\_Mathlib\_\_CategoryTheory\_\_Monoidal\_\_Braided\_\_Basic\_\_0\_\_\_auto\_139}$ 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{\_private\_\_Mathlib\_\_CategoryTheory\_\_Monoidal\_\_Braided\_\_Basic\_\_0\_\_\_auto\_141}$. Then the isomorphism of $X_{2}$ is an isomorphism of $F$ and $G$ defined as the function that maps $\mathrm{tensor}$ to the unique isomorphism of $\operatorname{fullyFaithfulForget}$ and the isomorphism of $X_{2}$.

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

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

the tensor of x5 and x6 (from the name)

Let $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ be elements of $C$. Then the tensor of $x_{5}$ and $x_{6}$ is a homomorphism of the tensor object of the tensor object of $x_{3}$ and $x_{5}$ and the tensor object of $x_{4}$ and $x_{6}$ and the tensor object of the tensor object of $x_{3}$ and $x_{4}$ and the tensor object of $x_{5}$ and $x_{6}$ defined as the composition of the homomorphism of the associator of $x_{5}$ and the tensor object of $x_{4}$ and $x_{6}$ and the composition of the left whisker of $x_{3}$ and the inverse of the associator of $x_{4}$ and $x_{6}$ and the composition of the left whisker of $x_{3}$ and the right whisker of the inverse of the braiding natural isomorphism of $x_{4}$ and $x_{5}$ and $x_{6}$ and the composition of the left whisker of $x_{3}$ and the homomorphism of the associator of $x_{5}$ and $x_{6}$ and the inverse of the associator of $x_{4}$ and the tensor object of $x_{5}$ and $x_{6}$.

the tensor of x5 and x6 (from the name)

Let $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ be elements of $C$. Then the tensor of $x_{5}$ and $x_{6}$ is a homomorphism of the tensor object of the tensor object of $x_{3}$ and $x_{4}$ and the tensor object of $x_{5}$ and $x_{6}$ and the tensor object of the tensor object of $x_{3}$ and $x_{5}$ and the tensor object of $x_{4}$ and $x_{6}$ defined as the composition of the homomorphism of the associator of $x_{4}$ and the tensor object of $x_{5}$ and $x_{6}$ and the composition of the left whisker of $x_{3}$ and the inverse of the associator of $x_{5}$ and $x_{6}$ and the composition of the left whisker of $x_{3}$ and the right whisker of the homomorphism of the braiding natural isomorphism of $x_{4}$ and $x_{5}$ and $x_{6}$ and the composition of the left whisker of $x_{3}$ and the homomorphism of the associator of $x_{4}$ and $x_{6}$ and the inverse of the associator of $x_{5}$ and the tensor object of $x_{4}$ and $x_{6}$.

C is a symmetric category (from the name)

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

the functor of C (from the name)

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

the functor of C (from the name)

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

the functor of C (from the name)

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

the functor of C (from the name)

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

the functor of C (from the name)

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

the functor of C (from the name)

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

the functor of C (from the name)

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

the functor of C (from the name)

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

the functor of C (from the name)

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

the functor of C (from the name)

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

the middle left map in the forward hexagon identity of x2 (from the docstring)

Let $x_{2}$ be an isomorphism of the tensor product bifunctor of $C$ and the flip of the tensor product bifunctor of $C$. Then the middle left map in the forward hexagon identity of $x_{2}$ is a homomorphism of the functor of $C$ and the functor of $C$ defined as the component of the map of the functor and the homomorphism of $x_{2}$ and the tensor product bifunctor of $C$.

the bottom left map in the forward hexagon identity of C (from the docstring)

Let $C$ be a set. Then the bottom left map in the forward hexagon identity of $C$ is a homomorphism of the functor of $C$ and the functor of $C$.

the top right map in the forward hexagon identity of x2 (from the docstring)

Let $x_{2}$ be an isomorphism of the tensor product bifunctor of $C$ and the flip of the tensor product bifunctor of $C$. Then the top right map in the forward hexagon identity of $x_{2}$ is a homomorphism of the functor of $C$ and the functor of $C$ defined as the component of the map of the functor and the homomorphism of $x_{2}$ and the tensor product bifunctor of $C$.

the middle right map in the forward hexagon identity of C (from the docstring)

Let $C$ be a set. Then the middle right map in the forward hexagon identity of $C$ is a homomorphism of the functor of $C$ and the functor of $C$.

the bottom right map in the forward hexagon identity of x2 (from the docstring)

Let $x_{2}$ be an isomorphism of the tensor product bifunctor of $C$ and the flip of the tensor product bifunctor of $C$. Then the bottom right map in the forward hexagon identity of $x_{2}$ is a homomorphism of the functor of $C$ and the functor of $C$ defined as the map of the flip functor and the map of the flip functor of $C$ and the set of functors of $C$ and $C$ and the map of the action of the functor and the tensor product bifunctor of $C$ and the map of the flip functor of $C$ and $C$ and the homomorphism of $x_{2}$.

the middle left map in the reverse hexagon identity of x2 (from the docstring)

Let $x_{2}$ be an isomorphism of the tensor product bifunctor of $C$ and the flip of the tensor product bifunctor of $C$. Then the middle left map in the reverse hexagon identity of $x_{2}$ is a homomorphism of the functor of $C$ and the functor of $C$ defined as the map of the flip functor and the map of the flip functor of $C$ and the set of functors of $C$ and $C$ and the component of the map of the functor and the map of the flip functor of $C$ and $C$ and the homomorphism of $x_{2}$ and the tensor product bifunctor of $C$.

the bottom left map in the reverse hexagon identity of C (from the docstring)

Let $C$ be a set. Then the bottom left map in the reverse hexagon identity of $C$ is a homomorphism of the functor of $C$ and the functor of $C$ defined as the map of the flip functor and the map of the flip functor of $C$ and the set of functors of $C$ and $C$ and the inverse of the associator of $C$.

the top right map in the reverse hexagon identity of x2 (from the docstring)

Let $x_{2}$ be an isomorphism of the tensor product bifunctor of $C$ and the flip of the tensor product bifunctor of $C$. Then the top right map in the reverse hexagon identity of $x_{2}$ is a homomorphism of the functor of $C$ and the functor of $C$ defined as the map of the action of the functor and the tensor product bifunctor of $C$ and the homomorphism of $x_{2}$.

the middle right map in the reverse hexagon identity of C (from the docstring)

Let $C$ be a set. Then the middle right map in the reverse hexagon identity of $C$ is a homomorphism of the functor of $C$ and the functor of $C$.

the bottom right map in the reverse hexagon identity of x2 (from the docstring)

Let $x_{2}$ be an isomorphism of the tensor product bifunctor of $C$ and the flip of the tensor product bifunctor of $C$. Then the bottom right map in the reverse hexagon identity of $x_{2}$ is a homomorphism of the functor of $C$ and the functor of $C$ defined as the map of the flip functor and the component of the map of the functor and the homomorphism of $x_{2}$ and the tensor product bifunctor of $C$.

the flip tensor of sq (from the name)

Let $\mathrm{sq}$ be a pushout object object of $x_{7}$ and $x_{8}$. Then the flip tensor of $\mathrm{sq}$ is a pushout object object of $x_{8}$ and $x_{7}$ defined as the pushout object object of the flip of $\mathrm{sq}$ and the inverse of the braiding isomorphism of $C$.

C is a cartesian monoidal category (from the name)

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

the homomorphism equivalence to product (from the name)

The homomorphism equivalence to product is an equivalence from the set of homomorphisms of $Z$ and the tensor object of $X$ and $Y$ to $\mathrm{Prod}$ applied to the set of homomorphisms of $Z$ and $X$ and the set of homomorphisms of $Z$ and $Y$.

Let $F$ be a functor of $C$ and $D$. Let $A$ and $B$ be elements of $C$. Then $\operatorname{isLimitCartesianMonoidalCategoryOfPreservesLimits}$ applied to $F$, $A$ and $B$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the map of $F$ and the first projection from the product of $A$ and $B$ and the map of $F$ and the second projection from the product of $A$ and $B$ defined as $\operatorname{mapIsLimitOfPreservesOfIsLimit}$ applied to $F$, the first projection from the product of $A$ and $B$, the second projection from the product of $A$ and $B$ and $\operatorname{ofIsoLimit}$ applied to the monoidal product of $A$ and $B$ and $\operatorname{isoBinaryFanMk}$ applied to $\operatorname{mk}$ applied to the first projection from the product of $A$ and $B$ and the second projection from the product of $A$ and $B$.

the lift of f and g (from the name)

Let $f$ be a homomorphism of $T$ and $X$. Let $g$ be a homomorphism of $T$ and $Y$. Then the lift of $f$ and $g$ is a homomorphism of $T$ and the tensor object of $X$ and $Y$ defined as the lift of $f$ and $g$.

the lift equivalence (from the name)

The lift equivalence is an equivalence from $\mathrm{Prod}$ applied to the set of homomorphisms of $T$ and $X$ and the set of homomorphisms of $T$ and $Y$ to the set of homomorphisms of $T$ and the tensor object of $X$ and $Y$.

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{preservesTerminalIso}$ applied to $F$ is an isomorphism 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{conePointUniqueUpToIso}$ applied to $\operatorname{isLimitChangeEmptyCone}$ applied to $D$, $\operatorname{isLimitOfPreserves}$ applied to $F$ and the tensor unit, $\operatorname{asEmptyCone}$ applied to the action of $F$ and the tensor unity in the monoidal structure of $C$ and the identity of $\operatorname{pt}$ applied to the map cone of $F$ and $\operatorname{asEmptyCone}$ applied to the tensor unity in the monoidal structure of $C$ and the tensor unit.

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

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

the product comparison bifunctor natural isomorphism of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the product comparison bifunctor natural isomorphism of $F$ is an isomorphism of the composition of the tensor product bifunctor of $C$ and the action of the right whiskering of $C$ and $D$ and $F$ and the composition of $F$ and the composition of the tensor product bifunctor of $D$ and the action of the left whiskering of $D$ and $D$ and $F$ defined as $\operatorname{asIso}$ applied to the product comparison bifunctor natural transformation of $F$.

the product comparison bifunctor natural transformation of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the product comparison bifunctor natural transformation of $F$ is a homomorphism of the composition of the tensor product bifunctor of $C$ and the action of the right whiskering of $C$ and $D$ and $F$ and the composition of $F$ and the composition of the tensor product bifunctor of $D$ and the action of the left whiskering of $D$ and $D$ and $F$.

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

Let $F$ be a functor of $C$ and $D$. Let $A$ and $B$ be elements of $C$. Then the product comparison isomorphism of $A$ and $B$ is an isomorphism of the action of $F$ and the tensor object of $A$ and $B$ and the tensor object of the action of $F$ and $A$ and the action of $F$ and $B$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimitCartesianMonoidalCategoryOfPreservesLimits}$ applied to $F$, $A$ and $B$ and the monoidal product of the action of $F$ and $A$ and the action of $F$ and $B$.

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

Let $F$ be a functor of $C$ and $D$. Let $A$ be an element of $C$. Then the natural isomorphism of $F$ and $A$ is an isomorphism of the composition of the action of the tensor product bifunctor of $C$ and $A$ and $F$ and the composition of $F$ and the action of the tensor product bifunctor of $D$ and the action of $F$ and $A$ defined as $\operatorname{asIso}$ applied to the product comparison natural transformation of $F$ and $A$.

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

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

the tensor left isomorphism product of X (from the name)

Let $X$ be an element of $C$. Then the tensor left isomorphism product of $X$ is an isomorphism of the left tensor of $X$ and the action of the binary product functor and $X$.

the monoidal product of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $C$. Then the monoidal product of $X$ and $Y$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the first projection from the product of $X$ and $Y$ and the second projection from the product of $X$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $X$ and $Y$.

C is a semi cartesian monoidal category (from the name)

Let $C$ be a set. Then we can say that $C$ is a semi cartesian monoidal category.

the first projection from the product of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $C$. Then the first projection from the product of $X$ and $Y$ is a homomorphism of the tensor object of $X$ and $Y$ and $X$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $X$ and $Y$.

the tensor unit (from the docstring)

The tensor unit is an element of $\operatorname{IsTerminal}$ applied to the tensor unity in the monoidal structure of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the second projection from the product of X and Y (from the docstring)

Let $X$ and $Y$ be elements of $C$. Then the second projection from the product of $X$ and $Y$ is a homomorphism of the tensor object of $X$ and $Y$ and $Y$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $X$ and $Y$.

the unit of X (from the name)

Let $X$ be an element of $C$. Then the unit of $X$ is a homomorphism of $X$ and the tensor unity in the monoidal structure of $C$ defined as $\operatorname{from}$ applied to the tensor unit and $X$.

the chosen terminal (from the name)

The chosen terminal is a category defined as $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to the set of lift homomorphisms of $\operatorname{Discrete}$ applied to $\mathrm{Unit}$.

$\operatorname{chosenTerminalIsTerminal}$ is an element of $\operatorname{IsTerminal}$ applied to the chosen terminal.

$\operatorname{fromChosenTerminalEquiv}$ is an equivalence from the set of functors of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the chosen terminal and $C$ to $C$.

Let $X$ and $Y$ be categories. Then $\operatorname{isLimitProdCone}$ applied to $X$ and $Y$ is an element of $\operatorname{IsLimit}$ applied to the product cone of $X$ and $Y$.

the product cone of C and D (from the name)

Let $C$ and $D$ be categories. Then the product cone of $C$ and $D$ is an element of $\operatorname{BinaryFan}$ applied to $C$ and $D$ defined as $\operatorname{mk}$ applied to the category homomorphism of the first component of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $C$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $D$ and the category homomorphism of the second component of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $C$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $D$.

X is a commutative group object (from the name)

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

the Yoneda commutative group group (from the name)

The Yoneda commutative group group is a functor of the set of commutative groups of $C$ and the set of functors of the set of opposites of the set of groups of $C$ and the set of commutative group categories.

the Yoneda commutative group group object of G (from the name)

Let $G$ be a commutative group of $C$. Then the Yoneda commutative group group object of $G$ is a functor of the set of opposites of the set of groups of $C$ and the set of commutative group categories.

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

the comonoid equivalence (from the name)

The comonoid equivalence is an equivalence of $\operatorname{Comon}$ applied to $C$ and $C$.

Let $A$ be an element of $\operatorname{Comon}$ applied to $C$. Then $\operatorname{isoCartesianComon}$ applied to $A$ is an isomorphism of $A$ and the action of $\operatorname{cartesianComon}$ applied to $C$ and $\operatorname{X}$ applied to $A$.

the tensor object of x2 and x3 (from the name)

Let $x_{2}$ be an element of $\operatorname{RepresentableBy}$ applied to $F$ and $X$. Let $x_{3}$ be an element of $\operatorname{RepresentableBy}$ applied to $G$ and $Y$. Then the tensor object of $x_{2}$ and $x_{3}$ is an element of $\operatorname{RepresentableBy}$ applied to the tensor object of $F$ and $G$ and the tensor object of $X$ and $Y$.

the tensor object composition of G and H (from the name)

Let $F$ and $G$ be functors of $D$ and $C$. Let $H$ be a functor of $C$ and $E$. Then the tensor object composition of $G$ and $H$ is an isomorphism of the composition of the tensor object of $F$ and $G$ and $H$ and the tensor object of the composition of $F$ and $H$ and the composition of $G$ and $H$.

the commutator of G (from the docstring)

Let $G$ be an element of $C$. Then the commutator of $G$ is a homomorphism of the tensor object of $G$ and $G$ and $G$ defined as the sum of the first projection from the product of $G$ and $G$, the second projection from the product of $G$ and $G$, $\operatorname{neg}$ applied to the first projection from the product of $G$ and $G$ and $\operatorname{neg}$ applied to the second projection from the product of $G$ and $G$.

the additive conjugate of G (from the name)

Let $G$ be an element of $C$. Then the additive conjugate of $G$ is a homomorphism of the tensor object of $G$ and $G$ and $G$ defined as the sum of the first projection from the product of $G$ and $G$, the second projection from the product of $G$ and $G$ and $\operatorname{neg}$ applied to the first projection from the product of $G$ and $G$.

the commutator of G (from the docstring)

Let $G$ be an element of $C$. Then the commutator of $G$ is a homomorphism of the tensor object of $G$ and $G$ and $G$ defined as the product of the first projection from the product of $G$ and $G$, the second projection from the product of $G$ and $G$, $\operatorname{inv}$ applied to the first projection from the product of $G$ and $G$ and $\operatorname{inv}$ applied to the second projection from the product of $G$ and $G$.

the conjugate of G (from the name)

Let $G$ be an element of $C$. Then the conjugate of $G$ is a homomorphism of the tensor object of $G$ and $G$ and $G$ defined as the product of the first projection from the product of $G$ and $G$, the second projection from the product of $G$ and $G$ and $\operatorname{inv}$ applied to the first projection from the product of $G$ and $G$.

the Yoneda additive group (from the name)

The Yoneda additive group is a functor of the set of additive groups of $C$ and the set of functors of the set of opposites of $C$ and the set of additive group categories.

$\operatorname{yonedaAddGrpFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the Yoneda additive group.

the Yoneda additive group object of G (from the name)

Let $G$ be an element of $C$. Then the Yoneda additive group object of $G$ is a functor of the set of opposites of $C$ and the set of additive group categories.

the Yoneda additive group object isomorphism of F and x2 (from the name)

Let $X$ be an element of $C$. Let $F$ be a functor of the set of opposites of $C$ and the set of additive group categories. Let $x_{2}$ be an element of $\operatorname{RepresentableBy}$ applied to the composition of $F$ and the forgetful functor of the set of additive group categories and $X$. Then the Yoneda additive group object isomorphism of $F$ and $x_{2}$ is an isomorphism of the Yoneda additive group object of $X$ and $F$.

Let $G$ be an element of $C$. Then $\operatorname{yonedaAddGrpObjRepresentableBy}$ applied to $G$ is an element of $\operatorname{RepresentableBy}$ applied to the composition of the Yoneda additive group object of $G$ and the forgetful functor of the set of additive group categories and $G$ defined as $\operatorname{symm}$ applied to $\operatorname{representableByEquiv}$ and the identity of the action of the Yoneda and $G$.

the Yoneda group (from the name)

The Yoneda group is a functor of the set of groups of $C$ and the set of functors of the set of opposites of $C$ and the set of group categories.

$\operatorname{yonedaGrpFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the Yoneda group.

the Yoneda group object of G (from the name)

Let $G$ be an element of $C$. Then the Yoneda group object of $G$ is a functor of the set of opposites of $C$ and the set of group categories.

the Yoneda group object isomorphism of F and x2 (from the name)

Let $X$ be an element of $C$. Let $F$ be a functor of the set of opposites of $C$ and the set of group categories. Let $x_{2}$ be an element of $\operatorname{RepresentableBy}$ applied to the composition of $F$ and the forgetful functor of the set of group categories and $X$. Then the Yoneda group object isomorphism of $F$ and $x_{2}$ is an isomorphism of the Yoneda group object of $X$ and $F$.

Let $G$ be an element of $C$. Then $\operatorname{yonedaGrpObjRepresentableBy}$ applied to $G$ is an element of $\operatorname{RepresentableBy}$ applied to the composition of the Yoneda group object of $G$ and the forgetful functor of the set of group categories and $G$ defined as $\operatorname{symm}$ applied to $\operatorname{representableByEquiv}$ and the identity of the action of the Yoneda and $G$.

the additive action homomorphism of f and Z (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $Z$ be an element of $C$. Then the additive action homomorphism of $f$ and $Z$ is an additive action homomorphism of the set of homomorphisms of $Z$ and $X$ and the set of homomorphisms of $Z$ and $Y$ defined as $\operatorname{mk}$ applied to the function that maps $x_{5}$ to the composition of $x_{5}$ and $f$ and $\mathrm{CategoryTheory\_\_IsAddModHom\_\_map\_vadd}$ applied to $f$.

the multiplicative action homomorphism of f and Z (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $Z$ be an element of $C$. Then the multiplicative action homomorphism of $f$ and $Z$ is a multiplicative action homomorphism of the set of homomorphisms of $Z$ and $X$ and the set of homomorphisms of $Z$ and $Y$ defined as $\operatorname{mk}$ applied to the function that maps $x_{5}$ to the composition of $x_{5}$ and $f$ and $\mathrm{CategoryTheory\_\_IsModHom\_\_map\_smul}$ applied to $f$.

the trivial action of M and X (from the name)

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

the left product of M and X (from the name)

Let $M$ and $X$ be elements of $C$. Then the left product of $M$ and $X$ is a homomorphism of the tensor object of $M$ and $X$ and the tensor object of $X$ and $X$ defined as the lift of the scalar multiple and the second projection from the product of $M$ and $X$.

the homomorphism additive equivalence of F and hF (from the name)

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the homomorphism additive equivalence of $F$ and $\mathrm{hF}$ is an additive equivalence of the set of homomorphisms of $X$ and $M$ and the set of homomorphisms of the action of $F$ and $X$ and the action of $F$ and $M$.

the homomorphism multiplicative equivalence of F and hF (from the name)

Let $F$ be a functor of $C$ and $D$. Let $\mathrm{hF}$ be an element of $\operatorname{FullyFaithful}$ applied to $F$. Then the homomorphism multiplicative equivalence of $F$ and $\mathrm{hF}$ is a multiplicative equivalence of the set of homomorphisms of $X$ and $M$ and the set of homomorphisms of the action of $F$ and $X$ and the action of $F$ and $M$.

the homomorphism additive monoid homomorphism of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the homomorphism additive monoid homomorphism of $F$ is an additive monoid homomorphism of the set of homomorphisms of $X$ and $M$ and the set of homomorphisms of the action of $F$ and $X$ and the action of $F$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{map}$ applied to $F$ and $\mathrm{CategoryTheory\_\_Functor\_\_map\_zero'}$ applied to $F$ and $\mathrm{CategoryTheory\_\_Functor\_\_map\_add'}$ applied to $F$.

the homomorphism monoid homomorphism of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the homomorphism monoid homomorphism of $F$ is a monoid homomorphism of the set of homomorphisms of $X$ and $M$ and the set of homomorphisms of the action of $F$ and $X$ and the action of $F$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{map}$ applied to $F$ and $\mathrm{CategoryTheory\_\_Functor\_\_map\_one}$ applied to $F$ and $\mathrm{CategoryTheory\_\_Functor\_\_map\_mul}$ applied to $F$.

the right additive equivalence congruence of e and X (from the name)

Let $e$ be an isomorphism of $M$ and $N$. Let $X$ be an element of $C$. Then the right additive equivalence congruence of $e$ and $X$ is an additive equivalence of the set of homomorphisms of $X$ and $M$ and the set of homomorphisms of $X$ and $N$ defined as the additive monoid category isomorphism to additive equivalence of the application of the map isomorphism of the Yoneda additive monoid and the isomorphism of $e$ and $\operatorname{op}$ applied to $X$.

the right multiplicative equivalence congruence of e and X (from the name)

Let $e$ be an isomorphism of $M$ and $N$. Let $X$ be an element of $C$. Then the right multiplicative equivalence congruence of $e$ and $X$ is a multiplicative equivalence of the set of homomorphisms of $X$ and $M$ and the set of homomorphisms of $X$ and $N$ defined as the monoid category isomorphism to multiplicative equivalence of the application of the map isomorphism of the Yoneda monoid and the isomorphism of $e$ and $\operatorname{op}$ applied to $X$.

the additive monoid homomorphism of f and X (from the name)

Let $f$ be a homomorphism of $M$ and $N$. Let $X$ be an element of $C$. Then the additive monoid homomorphism of $f$ and $X$ is an additive monoid homomorphism of the set of homomorphisms of $X$ and $M$ and the set of homomorphisms of $X$ and $N$.

the monoid homomorphism of f and X (from the name)

Let $f$ be a homomorphism of $M$ and $N$. Let $X$ be an element of $C$. Then the monoid homomorphism of $f$ and $X$ is a monoid homomorphism of the set of homomorphisms of $X$ and $M$ and the set of homomorphisms of $X$ and $N$.

the Yoneda additive monoid (from the name)

The Yoneda additive monoid is a functor of the set of additive monoids of $C$ and the set of functors of the set of opposites of $C$ and the set of additive monoid categories.

$\operatorname{yonedaAddMonFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the Yoneda additive monoid.

the Yoneda additive monoid object of M (from the name)

Let $M$ be an element of $C$. Then the Yoneda additive monoid object of $M$ is a functor of the set of opposites of $C$ and the set of additive monoid categories.

the Yoneda additive monoid object isomorphism of F and x2 (from the name)

Let $X$ be an element of $C$. Let $F$ be a functor of the set of opposites of $C$ and the set of additive monoid categories. Let $x_{2}$ be an element of $\operatorname{RepresentableBy}$ applied to the composition of $F$ and the forgetful functor of the set of additive monoid categories and $X$. Then the Yoneda additive monoid object isomorphism of $F$ and $x_{2}$ is an isomorphism of the Yoneda additive monoid object of $X$ and $F$.

Let $M$ be an element of $C$. Then $\operatorname{yonedaAddMonObjRepresentableBy}$ applied to $M$ is an element of $\operatorname{RepresentableBy}$ applied to the composition of the Yoneda additive monoid object of $M$ and the forgetful functor of the set of additive monoid categories and $M$ defined as $\operatorname{symm}$ applied to $\operatorname{representableByEquiv}$ and the identity of the action of the Yoneda and $M$.

the Yoneda monoid (from the name)

The Yoneda monoid is a functor of the set of monoids of $C$ and the set of functors of the set of opposites of $C$ and the set of monoid categories.

$\operatorname{yonedaMonFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the Yoneda monoid.

the Yoneda monoid object of M (from the name)

Let $M$ be an element of $C$. Then the Yoneda monoid object of $M$ is a functor of the set of opposites of $C$ and the set of monoid categories.

the Yoneda monoid object isomorphism of F and x2 (from the name)

Let $X$ be an element of $C$. Let $F$ be a functor of the set of opposites of $C$ and the set of monoid categories. Let $x_{2}$ be an element of $\operatorname{RepresentableBy}$ applied to the composition of $F$ and the forgetful functor of the set of monoid categories and $X$. Then the Yoneda monoid object isomorphism of $F$ and $x_{2}$ is an isomorphism of the Yoneda monoid object of $X$ and $F$.

Let $M$ be an element of $C$. Then $\operatorname{yonedaMonObjRepresentableBy}$ applied to $M$ is an element of $\operatorname{RepresentableBy}$ applied to the composition of the Yoneda monoid object of $M$ and the forgetful functor of the set of monoid categories and $M$ defined as $\operatorname{symm}$ applied to $\operatorname{representableByEquiv}$ and the identity of the action of the Yoneda and $M$.

x4 is normal (from the name)

Let $x_{4}$ be a homomorphism of $H$ and $G$. Then we can say that $x_{4}$ is normal.

x4 is normal (from the name)

Let $x_{4}$ be a homomorphism of $H$ and $G$. Then we can say that $x_{4}$ is normal.

the Yoneda commutative ring (from the name)

The Yoneda commutative ring is a functor of the set of commutative ring object categories of $C$ and the set of functors of the set of opposites of $C$ and the set of categories of commutative rings.

the Yoneda commutative ring object of R (from the name)

Let $R$ be an element of $C$. Then the Yoneda commutative ring object of $R$ is a functor of the set of opposites of $C$ and the set of categories of commutative rings.

the Yoneda ring (from the name)

The Yoneda ring is a functor of the set of ring object categories of $C$ and the set of functors of the set of opposites of $C$ and the set of categories of rings.

the Yoneda ring object of R (from the name)

Let $R$ be an element of $C$. Then the Yoneda ring object of $R$ is a functor of the set of opposites of $C$ and the set of categories of rings.

the Yoneda embedding (from the docstring)

The Yoneda embedding is a functor of the set of groups of $C$ and the set of functors of the set of opposites of $C$ and the set of group categories.

the shrink Yoneda group object object equivalence (from the name)

The shrink Yoneda group object object equivalence is a multiplicative equivalence of the set of carriers of the action of the action of the Yoneda embedding and $M$ and $Y$ and the set of homomorphisms of the opposite of $Y$ and $\operatorname{X}$ applied to $M$ defined as the multiplicative equivalence.

the Yoneda embedding (from the docstring)

The Yoneda embedding is a functor of the set of monoids of $C$ and the set of functors of the set of opposites of $C$ and the set of monoid categories.

the shrink Yoneda monoid object object equivalence (from the name)

The shrink Yoneda monoid object object equivalence is a multiplicative equivalence of the set of carriers of the action of the action of the Yoneda embedding and $M$ and $Y$ and the set of homomorphisms of the opposite of $Y$ and $\operatorname{X}$ applied to $M$ defined as the multiplicative equivalence.

C is a monoidal category (from the name)

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

Let $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ be elements of $C$. Then $\operatorname{Pentagon}$ holds for $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$, if the composition of the right whisker of the homomorphism of the associator of $x_{3}$ and $x_{4}$ and $x_{5}$ and the composition of the homomorphism of the associator of the tensor object of $x_{3}$ and $x_{4}$ and $x_{5}$ and the left whisker of $x_{2}$ and the homomorphism of the associator of $x_{4}$ and $x_{5}$ is equal to the composition of the homomorphism of the associator of $x_{4}$ and $x_{5}$ and the homomorphism of the associator of $x_{3}$ and the tensor object of $x_{4}$ and $x_{5}$.

the associator of C (from the docstring)

Let $C$ be a set. Then the associator of $C$ is an isomorphism of the left associator tensor of $C$ and the right associator tensor of $C$.

the associator of C (from the docstring)

Let $C$ be a set. Then the associator of $C$ is an isomorphism of the bifunctor composition of the tensor product bifunctor of $C$ and the tensor product bifunctor of $C$ and the bifunctor composition of the tensor product bifunctor of $C$ and the tensor product bifunctor of $C$.

the tensor product bifunctor of C (from the docstring)

Let $C$ be a set. Then the tensor product bifunctor of $C$ is a functor of $C$ and the set of functors of $C$ and $C$.

the left associator tensor of C (from the name)

Let $C$ be a set. Then the left associator tensor of $C$ is a functor of $\mathrm{Prod}$ applied to $C$ and $\mathrm{Prod}$ applied to $C$ and $C$ and $C$.

the left unitor of C (from the docstring)

Let $C$ be a set. Then the left unitor of $C$ is an isomorphism of the left tensor unit of $C$ and the identity of $C$.

the right associator tensor of C (from the name)

Let $C$ be a set. Then the right associator tensor of $C$ is a functor of $\mathrm{Prod}$ applied to $C$ and $\mathrm{Prod}$ applied to $C$ and $C$ and $C$.

the right unitor of C (from the docstring)

Let $C$ be a set. Then the right unitor of $C$ is an isomorphism of the right tensor unit of $C$ and the identity of $C$.

the tensor of C (from the name)

Let $C$ be a set. Then the tensor of $C$ is a functor of $\mathrm{Prod}$ applied to $C$ and $C$ and $C$.

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

Let $f$ be an isomorphism of $X$ and $Y$. Let $g$ be an isomorphism of $\mathrm{X'}$ and $\mathrm{Y'}$. Then the tensor isomorphism of $f$ and $g$ is an isomorphism of the tensor object of $X$ and $\mathrm{X'}$ and the tensor object of $Y$ and $\mathrm{Y'}$.

the left tensor of X (from the name)

Let $X$ be an element of $C$. Then the left tensor of $X$ is a functor of $C$ and $C$ defined as the action of the tensor product bifunctor of $C$ and $X$.

the tensor left tensor of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the tensor left tensor of $X$ and $Y$ is an isomorphism of the left tensor of the tensor object of $X$ and $Y$ and the composition of the left tensor of $Y$ and the left tensor of $X$.

the right tensor of X (from the name)

Let $X$ be an element of $C$. Then the right tensor of $X$ is a functor of $C$ and $C$ defined as the action of the flip of the tensor product bifunctor of $C$ and $X$.

the tensor right tensor of X and Y (from the name)

Let $X$ and $Y$ be elements of $C$. Then the tensor right tensor of $X$ and $Y$ is an isomorphism of the right tensor of the tensor object of $X$ and $Y$ and the composition of the right tensor of $X$ and the right tensor of $Y$.

the left tensor unit of C (from the name)

Let $C$ be a set. Then the left tensor unit of $C$ is a functor of $C$ and $C$ defined as the left tensor of the tensor unity in the monoidal structure of $C$.

the right tensor unit of C (from the name)

Let $C$ be a set. Then the right tensor unit of $C$ is a functor of $C$ and $C$ defined as the right tensor of the tensor unity in the monoidal structure of $C$.

the left tensoring of C (from the name)

Let $C$ be a set. Then the left tensoring of $C$ is a functor of $C$ and the set of functors of $C$ and $C$ defined as the tensor product bifunctor of $C$.

the right tensoring of C (from the name)

Let $C$ be a set. Then the right tensoring of $C$ is a functor of $C$ and the set of functors of $C$ and $C$ defined as the flip of the tensor product bifunctor of $C$.

the left whiskering of X and f (from the docstring)

Let $X$ be an element of $C$. Let $f$ be an isomorphism of $Y$ and $Z$. Then the left whiskering of $X$ and $f$ is an isomorphism of the tensor object of $X$ and $Y$ and the tensor object of $X$ and $Z$.

the right whiskering of f and Z (from the docstring)

Let $f$ be an isomorphism of $X$ and $Y$. Let $Z$ be an element of $C$. Then the right whiskering of $f$ and $Z$ is an isomorphism of the tensor object of $X$ and $Z$ and the tensor object of $Y$ and $Z$.

the associator of Y and Z (from the name)

Let $X$, $Y$ and $Z$ be elements of $C$. Then the associator of $Y$ and $Z$ is an isomorphism of the tensor object of the tensor object of $X$ and $Y$ and $Z$ and the tensor object of $X$ and the tensor object of $Y$ and $Z$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$, $X$, $Y$ and $Z$.

the left unitor of X (from the name)

Let $X$ be an element of $C$. Then the left unitor of $X$ is an isomorphism of the tensor object of the tensor unity in the monoidal structure of $C$ and $X$ and $X$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$ and $X$.

the right unitor of X (from the name)

Let $X$ be an element of $C$. Then the right unitor of $X$ is an isomorphism of the tensor object of $X$ and the tensor unity in the monoidal structure of $C$ and $X$ defined as $\operatorname{proj7}$ applied to $\mathrm{self}$ and $X$.

the tensor homomorphism of f and g (from the name)

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the tensor homomorphism of $f$ and $g$ is a homomorphism of the tensor object of $x_{1}$ and $x_{3}$ and the tensor object of $x_{2}$ and $x_{4}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $f$ and $g$.

the tensor object of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $C$. Then the tensor object of $x_{1}$ and $x_{2}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

the tensor unity in the monoidal structure of C (from the docstring)

Let $C$ be a set. Then the tensor unity in the monoidal structure of $C$ is an element of $C$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

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

Let $X$ be an element of $C$. Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Then the left whisker of $X$ and $f$ is a homomorphism of the tensor object of $X$ and $x_{1}$ and the tensor object of $X$ and $x_{2}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $X$ and $f$.

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

Let $f$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $Y$ be an element of $C$. Then the right whisker of $f$ and $Y$ is a homomorphism of the tensor object of $x_{1}$ and $Y$ and the tensor object of $x_{2}$ and $Y$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $f$ and $Y$.

center of C (from the name)

Let $C$ be a set. Then a center of $C$ is an element of the function that maps $C$ to $\Sigma$ applied to the function that maps $X$ to the set of half braidings of $X$.

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be centers of $C$. Then the homomorphisms of $X$ and $Y$ are a basic type.

Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{fst}$ applied to $X$ and $\operatorname{fst}$ applied to $Y$ 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 centers of $C$ and $C$.

the isomorphism of f (from the name)

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

the center of C (from the name)

Let $C$ be a set. Then the center of $C$ is a functor of $C$ and the set of centers of $C$.

half braiding of X (from the name)

Let $X$ be an element of $C$. Then the half braidings of $X$ are a basic type.

Let $\mathrm{self}$ be a half braiding of $X$. Let $U$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_HalfBraiding\_\_\_u3b2\_}$ applied to $\mathrm{self}$ and $U$ is an isomorphism of the tensor object of $X$ and $U$ and the tensor object of $U$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $U$.

X is closed (from the name)

Let $X$ be an element of $C$. Then we can say that $X$ is closed.

the left adjoint (from the docstring)

The left adjoint is an adjunction of the left tensor of $X$ and the right adjoint of $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the right adjoint of X (from the name)

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

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

the composition of y and z (from the name)

Let $x_{2}$, $y$ and $z$ be elements of $C$. Then the composition of $y$ and $z$ is a homomorphism of the tensor object of the action of $\operatorname{ihom}$ applied to $x_{2}$ and $y$ and the action of $\operatorname{ihom}$ applied to $y$ and $z$ and the action of $\operatorname{ihom}$ applied to $x_{2}$ and $z$ defined as the curry of the composition transpose of $y$ and $z$.

the composition transpose of y and z (from the name)

Let $x_{2}$, $y$ and $z$ be elements of $C$. Then the composition transpose of $y$ and $z$ is a homomorphism of the tensor object of $x_{2}$ and the tensor object of the action of $\operatorname{ihom}$ applied to $x_{2}$ and $y$ and the action of $\operatorname{ihom}$ applied to $y$ and $z$ and $z$ defined as the composition of the inverse of the associator of the action of $\operatorname{ihom}$ applied to $x_{2}$ and $y$ and the action of $\operatorname{ihom}$ applied to $y$ and $z$ and the composition of the right whisker of the component of $\operatorname{ev}$ applied to $x_{2}$ and $y$ and the action of $\operatorname{ihom}$ applied to $y$ and $z$ and the component of $\operatorname{ev}$ applied to $y$ and $z$.

the curry of x3 (from the name)

Let $x_{3}$ be a homomorphism of the tensor object of $A$ and $Y$ and $X$. Then the curry of $x_{3}$ is a homomorphism of $Y$ and the action of $\operatorname{ihom}$ applied to $A$ and $X$ defined as the coercion of the homomorphism equivalence of $Y$ and $X$ and $x_{3}$.

the curry of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the curry of $f$ is a homomorphism of the tensor unity in the monoidal structure of $C$ and the action of $\operatorname{ihom}$ applied to $X$ and $Y$ defined as the curry of the composition of the homomorphism of the right unitor of $X$ and $f$.

the curry homomorphism equivalence (from the name)

The curry homomorphism equivalence is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of the tensor unity in the monoidal structure of $C$ and the action of $\operatorname{ihom}$ applied to $X$ and $Y$.

the identity of x2 (from the name)

Let $x_{2}$ be an element of $C$. Then the identity of $x_{2}$ is a homomorphism of the tensor unity in the monoidal structure of $C$ and the action of $\operatorname{ihom}$ applied to $x_{2}$ and $x_{2}$ defined as the curry of the homomorphism of the right unitor of $x_{2}$.

the internal homomorphism (from the name)

The internal homomorphism is a functor of the set of opposites of $C$ and the set of functors of $C$ and $C$.

the internal homomorphism adjunction (from the name)

The internal homomorphism adjunction is a parametrized adjunction of the tensor product bifunctor of $C$ and the internal homomorphism.

Let $f$ be a homomorphism of $B$ and $A$. Then $\operatorname{pre}$ applied to $f$ is a homomorphism of $\operatorname{ihom}$ applied to $A$ and $\operatorname{ihom}$ applied to $B$ defined as $\operatorname{conjugateEquiv}$ applied to the adjunction of $A$, the adjunction of $B$ and the map of the left tensoring of $C$ and $f$.

Let $x_{3}$ be a homomorphism of $Y$ and the action of $\operatorname{ihom}$ applied to $A$ and $X$. Then $\operatorname{uncurry}$ applied to $x_{3}$ is a homomorphism of the tensor object of $A$ and $Y$ and $X$ defined as the coercion of the inverse of the homomorphism equivalence of $Y$ and $X$ and $x_{3}$.

Let $g$ be a homomorphism of the tensor unity in the monoidal structure of $C$ and the action of $\operatorname{ihom}$ applied to $X$ and $Y$. Then $\operatorname{uncurry'}$ applied to $g$ is a homomorphism of $X$ and $Y$ defined as the composition of the inverse of the right unitor of $X$ and $\operatorname{uncurry}$ applied to $g$.

the unit isomorphism self of X (from the name)

Let $X$ be an element of $C$. Then the unit isomorphism self of $X$ is an isomorphism of the action of $\operatorname{ihom}$ applied to the tensor unity in the monoidal structure of $C$ and $X$ and $X$ defined as the inverse of the application of the unit natural isomorphism and $X$.

the unit natural isomorphism (from the name)

The unit natural isomorphism is an isomorphism of the identity of $C$ and $\operatorname{ihom}$ applied to the tensor unity in the monoidal structure of $C$ defined as $\operatorname{conjugateIsoEquiv}$ applied to the adjunction between the identity functor, the adjunction of the tensor unity in the monoidal structure of $C$ and the left unitor of $C$.

Let $A$ be an element of $C$. Then $\operatorname{ihom}$ applied to $A$ is a functor of $C$ and $C$ defined as the right adjoint of $A$.

the adjunction of A (from the name)

Let $A$ be an element of $C$. Then the adjunction of $A$ is an adjunction of the left tensor of $A$ and $\operatorname{ihom}$ applied to $A$ defined as the left adjoint.

the coevaluation natural transformation of A (from the docstring)

Let $A$ be an element of $C$. Then the coevaluation natural transformation of $A$ is a homomorphism of the identity of $C$ and the composition of the left tensor of $A$ and $\operatorname{ihom}$ applied to $A$ defined as the unit of the adjunction of $A$.

Let $A$ be an element of $C$. Then $\operatorname{ev}$ applied to $A$ is a homomorphism of the composition of $\operatorname{ihom}$ applied to $A$ and the left tensor of $A$ and the identity of $C$ defined as the counit of the adjunction of $A$.

Let $f$ be a homomorphism of $A$ and $Y$. Then $\operatorname{internalizeHom}$ applied to $f$ is a homomorphism of the tensor unity in the monoidal structure of $C$ and the action of $\operatorname{ihom}$ applied to $A$ and $Y$ defined as the curry of the composition of the first projection from the product of $A$ and the tensor unity in the monoidal structure of $C$ and $f$.

the multiplicative zero of t (from the name)

Let $t$ be an element of $\operatorname{IsInitial}$ applied to $I$. Then the multiplicative zero of $t$ is an isomorphism of the tensor object of $I$ and $A$ and $I$ defined as the composition of the braiding natural isomorphism of $I$ and $A$ and the zero product of $t$.

the power zero of t (from the name)

Let $t$ be an element of $\operatorname{IsInitial}$ applied to $I$. Then the power zero of $t$ is an isomorphism of the action of $\operatorname{ihom}$ applied to $I$ and $B$ and the tensor unity in the monoidal structure of $C$.

the zero product of t (from the name)

Let $t$ be an element of $\operatorname{IsInitial}$ applied to $I$. Then the zero product of $t$ is an isomorphism of the tensor object of $A$ and $I$ and $I$.

F is a monoidal closed functor (from the name)

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

the exponential comparison map of F and A (from the docstring)

Let $F$ be a functor of $C$ and $D$. Let $A$ be an element of $C$. Then the exponential comparison map of $F$ and $A$ is an element of $\operatorname{TwoSquare}$ applied to $\operatorname{ihom}$ applied to $A$, $F$, $F$ and $\operatorname{ihom}$ applied to the action of $F$ and $A$ defined as $\operatorname{mateEquiv}$ applied to the adjunction of $A$, the adjunction of the action of $F$ and $A$ and the inverse of the natural isomorphism of $F$ and $A$.

the Frobenius morphism of h and A (from the name)

Let $F$ be a functor of $C$ and $D$. Let $h$ be an adjunction of $L$ and $F$. Let $A$ be an element of $C$. Then the Frobenius morphism of $h$ and $A$ is an element of $\operatorname{TwoSquare}$ applied to the left tensor of the action of $F$ and $A$, $L$, $L$ and the left tensor of $A$ defined as the composition of the product comparison natural transformation of $L$ and the action of $F$ and $A$ and the left whisker of $L$ and the map of the tensor product bifunctor of $C$ and the component of the counit of $h$ and $A$.

the adjoint of F (from the name)

Let $F$ be a functor of $J$ and $C$. Then the adjoint of $F$ is an adjunction of the left tensor of $F$ and the action of the homomorphism functor of the set of functors of $J$ and $C$ and the set of functors of $J$ and $C$ and $\operatorname{op}$ applied to $F$.

the homomorphism equivalence (from the name)

The homomorphism equivalence is an equivalence from the set of homomorphisms of the tensor object of $x_{4}$ and $x_{5}$ and $x_{6}$ to the set of homomorphisms of $x_{5}$ and the functor enriched homomorphism of $x_{4}$ and $x_{6}$.

the adjoint of F (from the name)

Let $F$ be a functor of $C$ and the set of sets. Then the adjoint of $F$ is an adjunction of the left tensor of $F$ and the right adjoint of $F$.

the functor homomorphism equivalence of G and H (from the name)

Let $F$, $G$ and $H$ be functors of $C$ and the set of sets. Then the functor homomorphism equivalence of $G$ and $H$ is an equivalence from the set of homomorphisms of $G$ and the functor homomorphism of $F$ and $H$ to the set of homomorphisms of the tensor object of $F$ and $G$ and $H$ defined as the composition of the functor homomorphism equivalence of $H$ and $G$ and the homomorphism object equivalence of $H$ and $G$.

the right adjoint of F (from the name)

Let $F$ be a functor of $C$ and the set of sets. Then the right adjoint of $F$ is a functor of the set of functors of $C$ and the set of sets and the set of functors of $C$ and the set of sets.

i is a exponential ideal (from the name)

Let $i$ be a functor of $D$ and $C$. Then we can say that $i$ is an exponential ideal.

the bijection of B and X (from the name)

Let $i$ be a functor of $D$ and $C$. Let $A$ and $B$ be elements of $C$. Let $X$ be an element of $D$. Then the bijection of $B$ and $X$ is an equivalence from the set of homomorphisms of the action of the reflector of $i$ and the tensor object of $A$ and $B$ and $X$ to the set of homomorphisms of the tensor object of the action of the reflector of $i$ and $A$ and the action of the reflector of $i$ and $B$ and $X$.

Let $i$ be a functor of $D$ and $C$. Let $A$ be an element of $C$. Then $\operatorname{exponentialIdealReflective}$ applied to $i$ and $A$ is an isomorphism of the composition of $i$ and the composition of $\operatorname{ihom}$ applied to $A$ and the composition of the reflector of $i$ and $i$ and the composition of $i$ and $\operatorname{ihom}$ applied to $A$.

Let $x_{2}$, $y$ and $z$ be elements of $C$. Then $\operatorname{ihomCurry}$ applied to $x_{2}$, $y$ and $z$ is a homomorphism of the action of $\operatorname{ihom}$ applied to the tensor object of $x_{2}$ and $y$ and $z$ and the action of $\operatorname{ihom}$ applied to $y$ and the action of $\operatorname{ihom}$ applied to $x_{2}$ and $z$ defined as the curry of the curry of the composition of the inverse of the associator of $y$ and the action of $\operatorname{ihom}$ applied to the tensor object of $x_{2}$ and $y$ and $z$ and the component of $\operatorname{ev}$ applied to the tensor object of $x_{2}$ and $y$ and $z$.

Let $x_{2}$, $y$ and $z$ be elements of $C$. Then $\operatorname{ihomCurryIso}$ applied to $x_{2}$, $y$ and $z$ is an isomorphism of the action of $\operatorname{ihom}$ applied to the tensor object of $x_{2}$ and $y$ and $z$ and the action of $\operatorname{ihom}$ applied to $y$ and the action of $\operatorname{ihom}$ applied to $x_{2}$ and $z$ defined as $\operatorname{mk}$ applied to $\operatorname{ihomCurry}$ applied to $x_{2}$, $y$ and $z$, $\operatorname{ihomUncurry}$ applied to $x_{2}$, $y$ and $z$, $\mathrm{CategoryTheory\_\_MonoidalClosed\_\_ihomCurry\_ihomUncurry}$ applied to $x_{2}$, $y$ and $z$ and $\mathrm{CategoryTheory\_\_MonoidalClosed\_\_ihomUncurry\_ihomCurry}$ applied to $x_{2}$, $y$ and $z$.

Let $x_{2}$, $y$ and $z$ be elements of $C$. Then $\operatorname{ihomUncurry}$ applied to $x_{2}$, $y$ and $z$ is a homomorphism of the action of $\operatorname{ihom}$ applied to $y$ and the action of $\operatorname{ihom}$ applied to $x_{2}$ and $z$ and the action of $\operatorname{ihom}$ applied to the tensor object of $x_{2}$ and $y$ and $z$ defined as the curry of the composition of the homomorphism of the associator of $y$ and the action of $\operatorname{ihom}$ applied to $y$ and the action of $\operatorname{ihom}$ applied to $x_{2}$ and $z$ and the composition of the left whisker of $x_{2}$ and the component of $\operatorname{ev}$ applied to $y$ and the action of $\operatorname{ihom}$ applied to $x_{2}$ and $z$ and the component of $\operatorname{ev}$ applied to $x_{2}$ and $z$.

the adjunction of X (from the docstring)

Let $X$ be a set. Then the adjunction of $X$ is an adjunction of the left tensor of $X$ and the action of the Coyoneda and $\operatorname{op}$ applied to $X$.

the equivalence unit (from the name)

The equivalence unit is an equivalence of $C$ and $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$.

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

Let $\mathrm{self}$ be an element of $\operatorname{CommComon}$ applied to $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 $\mathrm{CategoryTheory\_\_CommComon\_\_forget\_u2082\_Comon}$ applied to $C$ is a functor of $\operatorname{CommComon}$ applied to $C$ and $\operatorname{Comon}$ applied to $C$ defined as the induced functor of $\operatorname{toComon}$.

Let $A$ be an element of $\operatorname{CommComon}$ applied to $C$. Then $\operatorname{toComon}$ applied to $A$ is an element of $\operatorname{Comon}$ applied to $C$ defined as $\operatorname{mk}$ applied to $\operatorname{X}$ applied to $A$.

the trivial commutative comonoid object of C (from the docstring)

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

the map commutative group of a (from the name)

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

commutative group of C (from the name)

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

Let $\mathrm{self}$ be a commutative 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 commutative groups of $C$ and $C$ defined as the composition of $\mathrm{CategoryTheory\_\_CommGrp\_\_forget\_u2082\_Grp}$ applied to $C$ and $\operatorname{forget}$ applied to $C$.

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_CommGrp\_\_forget\_u2082\_CommMon}$ applied to $C$ is a functor of the set of commutative groups of $C$ and the set of commutative monoids of $C$.

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

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_CommGrp\_\_fullyFaithfulForget\_u2082\_CommMon}$ applied to $C$ is an element of $\operatorname{FullyFaithful}$ applied to $\mathrm{CategoryTheory\_\_CommGrp\_\_forget\_u2082\_CommMon}$ applied to $C$.

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

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{\_private\_\_Mathlib\_\_CategoryTheory\_\_Monoidal\_\_CommGrp\_\_\_0\_\_\_auto\_93}$ 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{\_private\_\_Mathlib\_\_CategoryTheory\_\_Monoidal\_\_CommGrp\_\_\_0\_\_\_auto\_95}$. 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\_\_CommGrp\_\_fullyFaithfulForget\_u2082\_Grp}$ applied to $C$ and the isomorphism of $e$.

the commutative monoid of A (from the name)

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

the group of A (from the name)

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

the monoid of A (from the name)

Let $A$ be a commutative group of $C$. Then the monoid of $A$ is a monoid of $C$ defined as the monoid of the commutative monoid of $A$.

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

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

the map commutative group of e (from the name)

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

the map commutative group of hF (from the name)

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

the map commutative group of F (from the name)

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

the composition functor (from the docstring)

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

the map commutative group functor (from the name)

The map commutative 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 commutative groups of $C$ and the set of commutative groups of $D$.

the identity functor (from the docstring)

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

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

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

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

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

the map commutative monoid of a (from the name)

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

commutative monoid of C (from the name)

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

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

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

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

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_CommMon\_\_forget\_u2082\_Mon}$ applied to $C$ is a functor of the set of commutative monoids 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\_\_CommMon\_\_fullyFaithfulForget\_u2082\_Mon}$ applied to $C$ is an element of $\operatorname{FullyFaithful}$ applied to $\mathrm{CategoryTheory\_\_CommMon\_\_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 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 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\_\_CommMon\_\_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\_\_CommMon\_\_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$ defined as the unique isomorphism of $\mathrm{CategoryTheory\_\_CommMon\_\_fullyFaithfulForget\_u2082\_Mon}$ applied to $C$ and the isomorphism of $e$.

the monoid of A (from the name)

Let $A$ be a commutative monoid 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 commutative monoid object of C (from the docstring)

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

the map commutative monoid of e (from the name)

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

the map commutative monoid of hF (from the name)

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

the map commutative monoid of F (from the name)

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

the composition functor (from the docstring)

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

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

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

the identity functor (from the docstring)

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

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

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

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

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

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

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

Let $A$ be an element of $\operatorname{Comon}$ applied to $C$. Then $\operatorname{ComonToMonOpOpObj}$ applied to $A$ is a monoid of the set of opposites of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $\operatorname{X}$ applied to $A$.

the comonoid equivalence monoid opposite opposite of C (from the name)

Let $C$ be a set. Then the comonoid equivalence monoid opposite opposite of $C$ is an equivalence of $\operatorname{Comon}$ applied to $C$ and the set of opposites of the set of monoids of the set of opposites of $C$.

homomorphism of M and N (from the name)

Let $M$ and $N$ be elements of $\operatorname{Comon}$ applied to $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 $f$ and the counit morphism is equal to the counit morphism and $\mathrm{CategoryTheory\_\_Comon\_\_Hom\_\_mk'\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of $f$ and the comultiplication morphism is equal to the composition of the comultiplication morphism and the tensor homomorphism of $f$ and $f$ and $\mathrm{CategoryTheory\_\_Comon\_\_Hom\_\_mk'\_\_\_auto\_3}$. Then $\operatorname{mk'}$ applied to $f$, $\mathrm{f\_counit}$ and $\mathrm{f\_comul}$ is a homomorphism of $M$ and $N$ defined as $\operatorname{mk}$ applied to $f$.

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

the monoid opposite opposite to comonoid object of A (from the name)

Let $A$ be a monoid of the set of opposites of $C$. Then the monoid opposite opposite to comonoid object of $A$ is an element of $\operatorname{Comon}$ applied to $C$ defined as $\operatorname{mk}$ applied to the opposite of $\operatorname{X}$ applied to $A$.

Let $\mathrm{self}$ be an element of $\operatorname{Comon}$ applied to $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$.

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

the identity morphism of M (from the docstring)

Let $M$ be an element of $\operatorname{Comon}$ applied to $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 f (from the name)

Let $f$ 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 homomorphism of $f$ and the counit morphism is equal to the counit morphism and $\mathrm{CategoryTheory\_\_Comon\_\_mkIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $f$ and the comultiplication morphism is equal to the composition of the comultiplication morphism and the tensor homomorphism of the homomorphism of $f$ and the homomorphism of $f$ and $\mathrm{CategoryTheory\_\_Comon\_\_mkIso\_\_\_auto\_3}$. Then the isomorphism of $f$ is an isomorphism of $M$ and $N$.

the isomorphism of f (from the name)

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

the trivial comonoid object of C (from the docstring)

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

X is a comonoid object (from the name)

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

the comultiplication morphism (from the docstring)

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

the counit morphism (from the docstring)

The counit morphism is a homomorphism of $X$ 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$. Then $\operatorname{mapComon}$ applied to $F$ is a functor of $\operatorname{Comon}$ applied to $C$ and $\operatorname{Comon}$ applied to $D$.

X is a commutative comonoid object (from the name)

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

f is a comonoid homomorphism (from the name)

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

Let $M$ and $N$ be elements of $C$. Then an element of $\operatorname{Conv}$ applied to $M$ and $N$ is an element of the function that maps $M$ and $N$ to the set of homomorphisms of $M$ and $N$.

Let $F$ and $G$ be functors of $C$ and $V$. Then we can say that $\operatorname{DayConvolution}$ holds for $F$ and $G$.

the associator of G and H (from the name)

Let $F$, $G$ and $H$ be functors of $C$ and $V$. Then the associator of $G$ and $H$ is an isomorphism of the chosen convolution between the functors of the chosen convolution between the functors of $F$ and $G$ and $H$ and the chosen convolution between the functors of $F$ and the chosen convolution between the functors of $G$ and $H$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{ofIso}$ applied to $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayConvolution\_\_corepresentableBy\_u2082\_'}$ applied to $F$, $G$ and $H$ and the associator corepresenting isomorphism of $G$ and $H$ and $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayConvolution\_\_corepresentableBy\_u2082\_}$ applied to $F$, $G$ and $H$.

the associator corepresenting isomorphism of G and H (from the name)

Let $F$, $G$ and $H$ be functors of $C$ and $V$. Then the associator corepresenting isomorphism of $G$ and $H$ is an isomorphism of the composition of the action of the left whiskering of $C$ and $V$ and the tensor of $C$ and the composition of the action of the left whiskering of $\mathrm{Prod}$ applied to $C$ and $C$ and $V$ and the product of the tensor of $C$ and the identity of $C$ and the action of the Coyoneda and $\operatorname{op}$ applied to the external product of the external product of $F$ and $G$ and $H$ and the composition of the action of the left whiskering of $C$ and $V$ and the tensor of $C$ and the composition of the action of the left whiskering of $\mathrm{Prod}$ applied to $C$ and $C$ and $V$ and the product of the identity of $C$ and the tensor of $C$ and the action of the Coyoneda and $\operatorname{op}$ applied to the external product of $F$ and the external product of $G$ and $H$.

the chosen convolution between the functors of F and G (from the docstring)

Let $F$ and $G$ be functors of $C$ and $V$. Then the chosen convolution between the functors of $F$ and $G$ is a functor of $C$ and $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $F$ and $G$ be functors of $C$ and $V$. Then $\operatorname{corepresentableBy}$ applied to $F$ and $G$ is an element of $\operatorname{CorepresentableBy}$ applied to the composition of the action of the left whiskering of $C$ and $V$ and the tensor of $C$ and the action of the Coyoneda and $\operatorname{op}$ applied to the external product of $F$ and $G$ and the chosen convolution between the functors of $F$ and $G$.

Let $F$, $G$ and $H$ be functors of $C$ and $V$. Then $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayConvolution\_\_corepresentableBy\_u2082\_}$ applied to $F$, $G$ and $H$ is an element of $\operatorname{CorepresentableBy}$ applied to the composition of the action of the left whiskering of $C$ and $V$ and the tensor of $C$ and the composition of the action of the left whiskering of $\mathrm{Prod}$ applied to $C$ and $C$ and $V$ and the product of the identity of $C$ and the tensor of $C$ and the action of the Coyoneda and $\operatorname{op}$ applied to the external product of $F$ and the external product of $G$ and $H$ and the chosen convolution between the functors of $F$ and the chosen convolution between the functors of $G$ and $H$.

Let $F$, $G$ and $H$ be functors of $C$ and $V$. Then $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayConvolution\_\_corepresentableBy\_u2082\_'}$ applied to $F$, $G$ and $H$ is an element of $\operatorname{CorepresentableBy}$ applied to the composition of the action of the left whiskering of $C$ and $V$ and the tensor of $C$ and the composition of the action of the left whiskering of $\mathrm{Prod}$ applied to $C$ and $C$ and $V$ and the product of the tensor of $C$ and the identity of $C$ and the action of the Coyoneda and $\operatorname{op}$ applied to the external product of the external product of $F$ and $G$ and $H$ and the chosen convolution between the functors of the chosen convolution between the functors of $F$ and $G$ and $H$.

Let $F$ and $G$ be functors of $C$ and $V$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $\operatorname{mk}$ applied to the chosen convolution between the functors of $F$ and $G$ and the unit of $F$ and $G$. Proof. Let $F$ be arbitrary. Let $G$ be arbitrary. By self. By CategoryTheory__MonoidalCategory__DayConvolution__proj2.

the map of f and g (from the name)

Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Let $g$ be a homomorphism of $G$ and $\mathrm{G'}$. Then the map of $f$ and $g$ is a homomorphism of the chosen convolution between the functors of $F$ and $G$ and the chosen convolution between the functors of $\mathrm{F'}$ and $\mathrm{G'}$ defined as $\operatorname{descOfIsLeftKanExtension}$ applied to the chosen convolution between the functors of $F$ and $G$, the unit of $F$ and $G$, the chosen convolution between the functors of $\mathrm{F'}$ and $\mathrm{G'}$ and the composition of the map of the external product bifunctor of $C$ and $V$ and the homomorphism of $f$ and $g$ and the unit of $\mathrm{F'}$ and $\mathrm{G'}$.

Assume that $\operatorname{DayConvolution}$ holds for $F$ and $G$. Assume that $\operatorname{DayConvolution}$ holds for $F$ and $G$. Then $\operatorname{uniqueUpToIso}$ applied to $h$ and $\mathrm{h'}$ is an isomorphism of the chosen convolution between the functors of $F$ and $G$ and the chosen convolution between the functors of $F$ and $G$ defined as $\operatorname{leftKanExtensionUnique}$ applied to the chosen convolution between the functors of $F$ and $G$, the unit of $F$ and $G$, the chosen convolution between the functors of $F$ and $G$ and the unit of $F$ and $G$.

the unit of F and G (from the name)

Let $F$ and $G$ be functors of $C$ and $V$. Then the unit of $F$ and $G$ is a homomorphism of the external product of $F$ and $G$ and the composition of the tensor of $C$ and the chosen convolution between the functors of $F$ and $G$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

F is a day convolution unit (from the name)

Let $F$ be a functor of $C$ and $V$. Then we can say that $F$ is a day convolution unit.

$\operatorname{can}$ is a homomorphism of the tensor unity in the monoidal structure of $V$ and the action of $F$ and the tensor unity in the monoidal structure of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $U$ and $F$ be functors of $C$ and $V$. Then $\operatorname{corepresentableByLeft}$ applied to $U$ and $F$ is an element of $\operatorname{CorepresentableBy}$ applied to the composition of the action of the left whiskering of $C$ and $V$ and the tensor of $C$ and the composition of the action of the left whiskering of $\mathrm{Prod}$ applied to $C$ and $C$ and $V$ and the product of $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $C$ and the identity of $C$ and the action of the Coyoneda and $\operatorname{op}$ applied to the external product of $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $V$ and $F$ and the chosen convolution between the functors of $U$ and $F$.

Let $U$ and $F$ be functors of $C$ and $V$. Then $\operatorname{corepresentableByRight}$ applied to $U$ and $F$ is an element of $\operatorname{CorepresentableBy}$ applied to the composition of the action of the left whiskering of $C$ and $V$ and the tensor of $C$ and the composition of the action of the left whiskering of $\mathrm{Prod}$ applied to $C$ and $C$ and $V$ and the product of the identity of $C$ and $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $C$ and the action of the Coyoneda and $\operatorname{op}$ applied to the external product of $F$ and $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $V$ and the chosen convolution between the functors of $F$ and $U$.

the canonical map (from the docstring)

The canonical map is an element of $\operatorname{IsPointwiseLeftKanExtension}$ applied to $\operatorname{mk}$ applied to $F$ and $\operatorname{mk}$ applied to the function that maps $x_{4}$ to $\operatorname{can}$ and $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayConvolutionUnit\_\_\_proof\_2}$ applied to $F$ and $\operatorname{can}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the left unitor of U and F (from the name)

Let $U$ and $F$ be functors of $C$ and $V$. Then the left unitor of $U$ and $F$ is an isomorphism of the chosen convolution between the functors of $U$ and $F$ and $F$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{ofIso}$ applied to $\operatorname{corepresentableByLeft}$ applied to $U$ and $F$ and the left unitor corepresenting isomorphism of $F$ and $\operatorname{symm}$ applied to $\operatorname{corepresentableByEquiv}$ and the identity of the action of the Coyoneda and $\operatorname{op}$ applied to $F$.

the left unitor corepresenting isomorphism of F (from the name)

Let $F$ be a functor of $C$ and $V$. Then the left unitor corepresenting isomorphism of $F$ is an isomorphism of the composition of the action of the left whiskering of $C$ and $V$ and the tensor of $C$ and the composition of the action of the left whiskering of $\mathrm{Prod}$ applied to $C$ and $C$ and $V$ and the product of $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $C$ and the identity of $C$ and the action of the Coyoneda and $\operatorname{op}$ applied to the external product of $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $V$ and $F$ and the action of the Coyoneda and $\operatorname{op}$ applied to $F$.

the right unitor of U and F (from the name)

Let $U$ and $F$ be functors of $C$ and $V$. Then the right unitor of $U$ and $F$ is an isomorphism of the chosen convolution between the functors of $F$ and $U$ and $F$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{ofIso}$ applied to $\operatorname{corepresentableByRight}$ applied to $U$ and $F$ and the right unitor corepresenting isomorphism of $F$ and $\operatorname{symm}$ applied to $\operatorname{corepresentableByEquiv}$ and the identity of the action of the Coyoneda and $\operatorname{op}$ applied to $F$.

the right unitor corepresenting isomorphism of F (from the name)

Let $F$ be a functor of $C$ and $V$. Then the right unitor corepresenting isomorphism of $F$ is an isomorphism of the composition of the action of the left whiskering of $C$ and $V$ and the tensor of $C$ and the composition of the action of the left whiskering of $\mathrm{Prod}$ applied to $C$ and $C$ and $V$ and the product of the identity of $C$ and $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $C$ and the action of the Coyoneda and $\operatorname{op}$ applied to the external product of $F$ and $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $V$ and the action of the Coyoneda and $\operatorname{op}$ applied to $F$.

Let $U$ be a functor of $C$ and $V$. Then $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayConvolutionUnit\_\_\_u3c6\_}$ applied to $U$ is a homomorphism of $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $V$ and the composition of $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $C$ and $U$.

Let $C$, $V$ and $D$ be sets. Then we can say that $\operatorname{InducedLawfulDayConvolutionMonoidalCategoryStructCore}$ holds for $C$, $V$ and $D$.

the convolution unit application of y and #5 (from the name)

Let $V$ be a set. Let $d$ and $\mathrm{d'}$ be elements of $D$. Let $x_{5}$ and $y$ be elements of $C$. Then the convolution unit application of $x_{5}$ and $y$ is a homomorphism of the tensor object of the action of the action of the inclusion of $V$ and $D$ and $d$ and $x_{5}$ and the action of the action of the inclusion of $V$ and $D$ and $\mathrm{d'}$ and $y$ and the action of the action of the inclusion of $V$ and $D$ and the tensor object of $d$ and $\mathrm{d'}$ and the tensor object of $x_{5}$ and $y$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$, $d$, $\mathrm{d'}$, $x_{5}$ and $y$.

the fully faithful inclusion (from the name)

the tensor homomorphism of x9 and x10 (from the name)

Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{6}$. Let $x_{10}$ be a homomorphism of $x_{7}$ and $x_{8}$. Then the tensor homomorphism of $x_{9}$ and $x_{10}$ is a homomorphism of the tensor object of $x_{5}$ and $x_{7}$ and the tensor object of $x_{6}$ and $x_{8}$ defined as $\operatorname{proj7}$ applied to $\mathrm{self}$, $x_{9}$ and $x_{10}$.

the tensor object of x5 and x6 (from the name)

Let $C$ and $V$ be sets. Let $x_{5}$ and $x_{6}$ be elements of $D$. Then the tensor object of $x_{5}$ and $x_{6}$ is an element of $D$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $x_{5}$ and $x_{6}$.

the tensor object isomorphism convolution of d and #4 (from the name)

Let $C$ and $V$ be sets. Let $d$ and $\mathrm{d'}$ be elements of $D$. Then the tensor object isomorphism convolution of $d$ and $\mathrm{d'}$ is an isomorphism of the action of the inclusion of $V$ and $D$ and the tensor object of $d$ and $\mathrm{d'}$ and the chosen convolution between the functors of the action of the inclusion of $V$ and $D$ and $d$ and the action of the inclusion of $V$ and $D$ and $\mathrm{d'}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$, $d$ and $\mathrm{d'}$.

the tensor unit of V and D (from the name)

Let $C$, $V$ and $D$ be sets. Then the tensor unit of $V$ and $D$ is an element of $D$ defined as $\operatorname{proj9}$ applied to $\mathrm{self}$.

the inclusion of V and D (from the name)

Let $C$, $V$ and $D$ be sets. Then the inclusion of $V$ and $D$ is a functor of $D$ and the set of functors of $C$ and $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $C$, $V$ and $D$ be sets. Then we can say that $\operatorname{LawfulDayConvolutionMonoidalCategoryStruct}$ holds for $C$, $V$ and $D$.

the convolution extension unit of d and #4 (from the name)

Let $C$ and $V$ be sets. Let $d$ and $\mathrm{d'}$ be elements of $D$. Then the convolution extension unit of $d$ and $\mathrm{d'}$ is a homomorphism of the external product of the action of the inclusion of $V$ and $D$ and $d$ and the action of the inclusion of $V$ and $D$ and $\mathrm{d'}$ and the composition of the tensor of $C$ and the action of the inclusion of $V$ and $D$ and the tensor object of $d$ and $\mathrm{d'}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $d$ and $\mathrm{d'}$.

Let $d$ and $\mathrm{d'}$ be elements of $D$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $\operatorname{mk}$ applied to the action of the inclusion of $V$ and $D$ and the tensor object of $d$ and $\mathrm{d'}$ and the convolution extension unit of $d$ and $\mathrm{d'}$. Proof. Let $d$ be arbitrary. Let $\mathrm{d'}$ be arbitrary. By self. By d. By d'. By CategoryTheory__MonoidalCategory__LawfulDayConvolutionMonoidalCategoryStruct__proj2.

Let $C$, $V$ and $D$ be sets. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $\operatorname{mk}$ applied to the action of the inclusion of $V$ and $D$ and the tensor unity in the monoidal structure of $D$ and $\operatorname{mk}$ applied to the function that maps $x_{6}$ to the unit unit of $V$ and $D$ and $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_LawfulDayConvolutionMonoidalCategoryStruct\_\_\_proof\_2}$ applied to $C$, $V$, $D$, the inclusion of $V$ and $D$ and the unit unit of $V$ and $D$. Proof. Let $C$ be arbitrary. Let $V$ be arbitrary. Let $D$ be arbitrary. By self. By CategoryTheory__MonoidalCategory__LawfulDayConvolutionMonoidalCategoryStruct__proj4.

the unit unit of V and D (from the name)

Let $C$, $V$ and $D$ be sets. Then the unit unit of $V$ and $D$ is a homomorphism of the tensor unity in the monoidal structure of $V$ and the action of the action of the inclusion of $V$ and $D$ and the tensor unity in the monoidal structure of $D$ and the tensor unity in the monoidal structure of $C$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the inclusion of V and D (from the name)

Let $C$, $V$ and $D$ be sets. Then the inclusion of $V$ and $D$ is a functor of $D$ and the set of functors of $C$ and $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the braiding of F and G (from the name)

Let $F$ and $G$ be functors of $C$ and $V$. Then the braiding of $F$ and $G$ is an isomorphism of the chosen convolution between the functors of $F$ and $G$ and the chosen convolution between the functors of $G$ and $F$.

the braiding homomorphism corepresenting of F and G (from the name)

Let $F$ and $G$ be functors of $C$ and $V$. Then the braiding homomorphism corepresenting of $F$ and $G$ is a homomorphism of the external product of $F$ and $G$ and the composition of the tensor of $C$ and the chosen convolution between the functors of $G$ and $F$.

the braiding inverse corepresenting of F and G (from the name)

Let $F$ and $G$ be functors of $C$ and $V$. Then the braiding inverse corepresenting of $F$ and $G$ is a homomorphism of the external product of $G$ and $F$ and the composition of the tensor of $C$ and the chosen convolution between the functors of $F$ and $G$.

day convolution internal homomorphism of G and H (from the name)

Let $F$, $G$ and $H$ be functors of $C$ and $V$. Then the day convolution internal homomorphisms of $G$ and $H$ are a basic type.

Let $x_{6}$ be a day convolution internal homomorphism of the chosen convolution between the functors of $F$ and $G$ and $H$. Then $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayConvolutionInternalHom\_\_coev\_app}$ applied to $x_{6}$ is a homomorphism of $G$ and $H$.

Let $x_{6}$ be a day convolution internal homomorphism of $G$ and $H$. Then $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayConvolutionInternalHom\_\_ev\_app}$ applied to $x_{6}$ is a homomorphism of the chosen convolution between the functors of $F$ and $H$ and $G$.

Let $\mathrm{self}$ be a day convolution internal homomorphism of $G$ and $H$. Let $c$ be an element of $C$. Then $\operatorname{isLimitWedge}$ applied to $\mathrm{self}$ and $c$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the action of $H$ and $c$, $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayConvolutionInternalHom\_\_\_u3c0\_}$ applied to $c$ and $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayConvolutionInternalHom\_\_h\_u3c0\_}$ applied to $\mathrm{self}$ and $c$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $c$.

the map of f and x6 (from the name)

Let $x_{5}$ be a day convolution internal homomorphism of $G$ and $H$. Let $f$ be a homomorphism of $G$ and $\mathrm{G'}$. Let $x_{6}$ be a day convolution internal homomorphism of $\mathrm{G'}$ and $\mathrm{H'}$. Then the map of $f$ and $x_{6}$ is a homomorphism of $H$ and $\mathrm{H'}$.

the projection of c and j (from the name)

Let $\mathrm{self}$ be a day convolution internal homomorphism of $G$ and $H$. Let $c$ and $j$ be elements of $C$. Then the projection of $c$ and $j$ is a homomorphism of the action of $H$ and $c$ and the action of $\operatorname{ihom}$ applied to the action of $F$ and $j$ and the action of $G$ and the tensor object of $j$ and $c$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $c$ and $j$.

the day convolution internal homomorphism diagram functor of F (from the name)

Let $F$ be a functor of $C$ and $V$. Then the day convolution internal homomorphism diagram functor of $F$ is a functor of the set of functors of $C$ and $V$ and the set of functors of $C$ and the set of functors of the set of opposites of $C$ and the set of functors of $C$ and $V$.

day functor of C and V (from the name)

Let $C$ and $V$ be sets. Then the day functors of $C$ and $V$ are a basic type.

homomorphism of F and G (from the name)

Let $F$ and $G$ be day functors of $C$ and $V$. Then the homomorphisms of $F$ and $G$ are a basic type.

the underlying natural transformation of self (from the docstring)

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

the equivalence of C and V (from the name)

Let $C$ and $V$ be sets. Then the equivalence of $C$ and $V$ is an equivalence of the set of day functors of $C$ and $V$ and the set of functors of $C$ and $V$.

the underlying functor of self (from the docstring)

Let $\mathrm{self}$ be a day functor of $C$ and $V$. Then the underlying functor of $\mathrm{self}$ is a functor of $C$ and $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the isomorphism pointwise left Kan extension of F and G (from the name)

Let $F$ and $G$ be day functors of $C$ and $V$. Then the isomorphism pointwise left Kan extension of $F$ and $G$ is an isomorphism of the underlying functor of the tensor object of $F$ and $G$ and the pointwise left Kan extension of the tensor of $C$ and the external product of the underlying functor of $F$ and the underlying functor of $G$ defined as $\operatorname{leftKanExtensionUnique}$ applied to the underlying functor of the tensor object of $F$ and $G$, $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayFunctor\_\_\_u3b7\_}$ applied to $F$ and $G$, the pointwise left Kan extension of the tensor of $C$ and the external product of the underlying functor of $F$ and the underlying functor of $G$ and the pointwise left Kan extension unit of the tensor of $C$ and the external product of the underlying functor of $F$ and the underlying functor of $G$.

Let $x_{4}$ be a homomorphism of the external product of the underlying functor of $F$ and the underlying functor of $G$ and the composition of the tensor of $C$ and the underlying functor of $H$. Then $\operatorname{tensorDesc}$ applied to $x_{4}$ is a homomorphism of the tensor object of $F$ and $G$ and $H$ defined as $\operatorname{mk}$ applied to $\operatorname{descOfIsLeftKanExtension}$ applied to the underlying functor of the tensor object of $F$ and $G$, $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayFunctor\_\_\_u3b7\_}$ applied to $F$ and $G$, the underlying functor of $H$ and $x_{4}$.

Let $x_{4}$ be a homomorphism of the tensor unity in the monoidal structure of $V$ and the action of the underlying functor of $F$ and the tensor unity in the monoidal structure of $C$. Then $\operatorname{unitDesc}$ applied to $x_{4}$ is a homomorphism of the tensor unity in the monoidal structure of the set of day functors of $C$ and $V$ and $F$.

Let $F$ and $G$ be day functors of $C$ and $V$. Then $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayFunctor\_\_\_u3b7\_}$ applied to $F$ and $G$ is a homomorphism of the external product of the underlying functor of $F$ and the underlying functor of $G$ and the composition of the tensor of $C$ and the underlying functor of the tensor object of $F$ and $G$ defined as the convolution extension unit of $F$ and $G$.

Let $C$ and $V$ be sets. Then $\mathrm{CategoryTheory\_\_MonoidalCategory\_\_DayFunctor\_\_\_u3bd\_}$ applied to $C$ and $V$ is a homomorphism of the tensor unity in the monoidal structure of $V$ and the action of the underlying functor of the tensor unity in the monoidal structure of the set of day functors of $C$ and $V$ and the tensor unity in the monoidal structure of $C$ defined as the unit unit of $V$ and the set of day functors of $C$ and $V$.

the natural transformation of C and V (from the name)

Let $C$ and $V$ be sets. Then the natural transformation of $C$ and $V$ is a homomorphism of $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $V$ and the composition of $\operatorname{fromPUnit}$ applied to the tensor unity in the monoidal structure of $C$ and the underlying functor of the tensor unity in the monoidal structure of the set of day functors of $C$ and $V$.

the additive monoidal functor of F (from the name)

Let $F$ be an additive monoid homomorphism of $M$ and $N$. Then the additive monoidal functor of $F$ is a functor of $\operatorname{Discrete}$ applied to $M$ and $\operatorname{Discrete}$ applied to $N$ defined as the functor of the function that maps $X$ to $\operatorname{mk}$ applied to $F$ applied to $X$.

the additive monoidal functor composition of F and G (from the name)

Let $F$ be an additive monoid homomorphism of $M$ and $N$. Let $G$ be an additive monoid homomorphism of $N$ and $K$. Then the additive monoidal functor composition of $F$ and $G$ is an isomorphism of the composition of the additive monoidal functor of $F$ and the additive monoidal functor of $G$ and the additive monoidal functor of the composition of $G$ and $F$ defined as the identity of the composition of the additive monoidal functor of $F$ and the additive monoidal functor of $G$.

the monoidal functor of F (from the name)

Let $F$ be a monoid homomorphism of $M$ and $N$. Then the monoidal functor of $F$ is a functor of $\operatorname{Discrete}$ applied to $M$ and $\operatorname{Discrete}$ applied to $N$ defined as the functor of the function that maps $X$ to $\operatorname{mk}$ applied to $F$ applied to $X$.

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

Let $F$ be a monoid homomorphism of $M$ and $N$. Let $G$ be a monoid homomorphism of $N$ and $K$. Then the monoidal functor composition of $F$ and $G$ is an isomorphism of the composition of the monoidal functor of $F$ and the monoidal functor of $G$ and the monoidal functor of the composition of $G$ and $F$ defined as the identity of the composition of the monoidal functor of $F$ and the monoidal functor of $G$.

the equivalence of x3 and x4 (from the name)

Let $F$ be a functor of $M$ and the set of functors of $C$ and $C$. Let $m$ and $n$ be elements of $M$. Let $x_{3}$ be an isomorphism of the tensor object of $m$ and $n$ and the tensor unity in the monoidal structure of $M$. Let $x_{4}$ be an isomorphism of the tensor object of $n$ and $m$ and the tensor unity in the monoidal structure of $M$ such that the composition of the right whisker of the homomorphism of $x_{3}$ and $m$ and the homomorphism of the left unitor of $m$ is equal to the composition of the homomorphism of the associator of $n$ and $m$ and the composition of the left whisker of $m$ and the homomorphism of $x_{4}$ and the homomorphism of the right unitor of $m$. Then the equivalence of $x_{3}$ and $x_{4}$ is an equivalence of $C$ and $C$.

the unit of n and h (from the name)

Let $F$ be a functor of $M$ and the set of functors of $C$ and $C$. Let $m$ and $n$ be elements of $M$. Let $h$ be an isomorphism of the tensor object of $m$ and $n$ and the tensor unity in the monoidal structure of $M$. Then the unit of $n$ and $h$ is an isomorphism of the composition of the action of $F$ and $m$ and the action of $F$ and $n$ and the identity of $C$ defined as the composition of the isomorphism of $m$ and $n$ and the composition of the map isomorphism of $F$ and $h$ and the inverse of the isomorphism of $F$.

the external product of x6 and x7 (from the name)

Let $x_{6}$ be a functor of $x$ and $C$. Let $x_{7}$ be a functor of $x_{1}$ and $C$. Then the external product of $x_{6}$ and $x_{7}$ is a functor of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $C$ defined as the action of the external product bifunctor of $x_{1}$ and $C$ and $\ProdmkMACRoU {x_{6}}{x_{7}}$.

the external product bifunctor of x1 and C (from the name)

Let $x$, $x_{1}$ and $C$ be sets. Then the external product bifunctor of $x_{1}$ and $C$ is a functor of $\mathrm{Prod}$ applied to the set of functors of $x$ and $C$ and the set of functors of $x_{1}$ and $C$ and the set of functors of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $C$ defined as the action of $\operatorname{uncurry}$ and the action of the action of the postcomposition and $\operatorname{uncurry}$ and $\operatorname{externalProductBifunctorCurried}$ applied to $x$, $x_{1}$ and $C$.

Let $x$, $x_{1}$ and $C$ be sets. Then $\operatorname{externalProductBifunctorCurried}$ applied to $x$, $x_{1}$ and $C$ is a functor of the set of functors of $x$ and $C$ and the set of functors of the set of functors of $x_{1}$ and $C$ and the set of functors of $x$ and the set of functors of $x_{1}$ and $C$ defined as the action of the action of the postcomposition and the action of the evaluation of the set of functors of $C$ and the set of functors of $C$ and $C$ and the set of functors of $x$ and the set of functors of $x_{1}$ and $C$ and the tensor product bifunctor of $C$ and the left whiskering of $C$.

the external product composition diagonal isomorphism of x and C (from the name)

Let $x$ and $C$ be sets. Then the external product composition diagonal isomorphism of $x$ and $C$ is an isomorphism of the composition of the external product bifunctor of $x$ and $C$ and the action of the left whiskering of $\mathrm{Prod}$ applied to $x$ and $x$ and $C$ and the diagonal functor of $x$ and the tensor of the set of functors of $x$ and $C$.

the external product flip of x1 and C (from the name)

Let $x$, $x_{1}$ and $C$ be sets. Then the external product flip of $x_{1}$ and $C$ is an isomorphism of the action of the action of the postcomposition and the flip functor of $x_{1}$ and $C$ and $\operatorname{externalProductBifunctorCurried}$ applied to $x$, $x_{1}$ and $C$ and the flip of $\operatorname{externalProductBifunctorCurried}$ applied to $x_{1}$, $x$ and $C$.

the external product swap of x1 and C (from the name)

Let $x$, $x_{1}$ and $C$ be sets. Then the external product swap of $x_{1}$ and $C$ is an isomorphism of the composition of the external product bifunctor of $x_{1}$ and $C$ and the action of the left whiskering of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $C$ and the swap of $x_{1}$ and $x$ and the composition of the swap of the set of functors of $x$ and $C$ and the set of functors of $x_{1}$ and $C$ and the external product bifunctor of $x$ and $C$.

the product composition external product of x12 and x13 (from the name)

Let $x_{10}$ be a functor of $x_{6}$ and $x$. Let $x_{11}$ be a functor of $x$ and $C$. Let $x_{12}$ be a functor of $x_{7}$ and $x_{1}$. Let $x_{13}$ be a functor of $x_{1}$ and $C$. Then the product composition external product of $x_{12}$ and $x_{13}$ is an isomorphism of the composition of the product of $x_{10}$ and $x_{12}$ and the external product of $x_{11}$ and $x_{13}$ and the external product of the composition of $x_{10}$ and $x_{11}$ and the composition of $x_{12}$ and $x_{13}$.

the left extension unit of K and #3 (from the name)

Let $\mathrm{H'}$ be a functor of $\mathrm{D'}$ and $V$. Let $x_{5}$ be a homomorphism of $H$ and the composition of $L$ and $\mathrm{H'}$. Let $K$ be a functor of $E$ and $V$. Then the left extension unit of $x_{5}$ and $K$ is a homomorphism of the external product of $H$ and $K$ and the composition of the product of $L$ and the identity of $E$ and the external product of $\mathrm{H'}$ and $K$ defined as the map of the external product bifunctor of $E$ and $V$ and the homomorphism of $x_{5}$ and the inverse of the left unitor of $K$.

the right extension unit of K and #3 (from the name)

Let $\mathrm{H'}$ be a functor of $\mathrm{D'}$ and $V$. Let $x_{5}$ be a homomorphism of $H$ and the composition of $L$ and $\mathrm{H'}$. Let $K$ be a functor of $E$ and $V$. Then the right extension unit of $x_{5}$ and $K$ is a homomorphism of the external product of $K$ and $H$ and the composition of the product of the identity of $E$ and $L$ and the external product of $K$ and $\mathrm{H'}$ defined as the map of the external product bifunctor of $D$ and $V$ and the homomorphism of the inverse of the left unitor of $K$ and $x_{5}$.

Let $\mathrm{H'}$ be a functor of $\mathrm{D'}$ and $V$. Let $x_{5}$ be a homomorphism of $H$ and the composition of $L$ and $\mathrm{H'}$. Let $K$ be a functor of $E$ and $V$. Let $d$ be an element of $\mathrm{D'}$. Let $P$ be an element of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $\operatorname{mk}$ applied to $\mathrm{H'}$ and $x_{5}$ and $d$. Let $e$ be an element of $E$. Then $\operatorname{isPointwiseLeftKanExtensionAtExtensionUnitLeft}$ applied to $\mathrm{H'}$, $x_{5}$, $K$, $d$, $P$ and $e$ is an element of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $\operatorname{mk}$ applied to the external product of $\mathrm{H'}$ and $K$ and the left extension unit of $x_{5}$ and $K$ and $\ProdmkMACRoU {d}{e}$.

Let $\mathrm{H'}$ be a functor of $\mathrm{D'}$ and $V$. Let $x_{5}$ be a homomorphism of $H$ and the composition of $L$ and $\mathrm{H'}$. Let $K$ be a functor of $E$ and $V$. Let $d$ be an element of $\mathrm{D'}$. Let $P$ be an element of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $\operatorname{mk}$ applied to $\mathrm{H'}$ and $x_{5}$ and $d$. Let $e$ be an element of $E$. Then $\operatorname{isPointwiseLeftKanExtensionAtExtensionUnitRight}$ applied to $\mathrm{H'}$, $x_{5}$, $K$, $d$, $P$ and $e$ is an element of $\operatorname{IsPointwiseLeftKanExtensionAt}$ applied to $\operatorname{mk}$ applied to the external product of $K$ and $\mathrm{H'}$ and the right extension unit of $x_{5}$ and $K$ and $\ProdmkMACRoU {e}{d}$.

Let $\mathrm{H'}$ be a functor of $\mathrm{D'}$ and $V$. Let $x_{5}$ be a homomorphism of $H$ and the composition of $L$ and $\mathrm{H'}$. Let $K$ be a functor of $E$ and $V$. Let $P$ be an element of $\operatorname{IsPointwiseLeftKanExtension}$ applied to $\operatorname{mk}$ applied to $\mathrm{H'}$ and $x_{5}$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $\operatorname{mk}$ applied to the external product of $\mathrm{H'}$ and $K$ and the left extension unit of $x_{5}$ and $K$.

Let $\mathrm{H'}$ be a functor of $\mathrm{D'}$ and $V$. Let $x_{5}$ be a homomorphism of $H$ and the composition of $L$ and $\mathrm{H'}$. Let $K$ be a functor of $E$ and $V$. Let $P$ be an element of $\operatorname{IsPointwiseLeftKanExtension}$ applied to $\operatorname{mk}$ applied to $\mathrm{H'}$ and $x_{5}$. Then $\operatorname{IsPointwiseLeftKanExtension}$ holds for $\operatorname{mk}$ applied to the external product of $K$ and $\mathrm{H'}$ and the right extension unit of $x_{5}$ and $K$.