Definitions: Mathlib.CategoryTheory, part 2 of 25

L is coreflective (from the name)

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

Let $L$ be a functor of $C$ and $D$. Then $\operatorname{R}$ applied to $L$ is a functor of $D$ and $C$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the left adjoint (from the docstring)

The left adjoint is an adjunction of $L$ and $\operatorname{R}$ applied to $L$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

Let $j$ be a functor of $C$ and $D$. Then $\operatorname{fullyFaithfulOfCoreflective}$ applied to $j$ is an element of $\operatorname{FullyFaithful}$ applied to $j$ defined as $\operatorname{fullyFaithfulLOfIsIsoUnit}$ applied to the adjunction of $j$.

Let $i$ be a functor of $D$ and $C$. Then $\operatorname{fullyFaithfulOfReflective}$ applied to $i$ is an element of $\operatorname{FullyFaithful}$ applied to $i$ defined as $\operatorname{fullyFaithfulROfIsIsoCounit}$ applied to the adjunction of $i$.

R is reflective (from the name)

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

Let $R$ be a functor of $D$ and $C$. Then $\operatorname{L}$ applied to $R$ is a functor of $C$ and $D$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the right adjoint (from the docstring)

The right adjoint is an adjunction of $\operatorname{L}$ applied to $R$ and $R$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

Let $j$ be a functor of $C$ and $D$. Then $\operatorname{coreflector}$ applied to $j$ is a functor of $D$ and $C$ defined as $\operatorname{R}$ applied to $j$.

the adjunction of j (from the docstring)

Let $j$ be a functor of $C$ and $D$. Then the adjunction of $j$ is an adjunction of $j$ and $\operatorname{coreflector}$ applied to $j$ defined as the left adjoint.

the equivalence essential image (from the name)

The equivalence essential image is an equivalence of $D$ and the set of essential image subcategories of $i$.

the reflector of i (from the docstring)

Let $i$ be a functor of $D$ and $C$. Then the reflector of $i$ is a functor of $C$ and $D$ defined as $\operatorname{L}$ applied to $i$.

the adjunction of i (from the docstring)

Let $i$ be a functor of $D$ and $C$. Then the adjunction of $i$ is an adjunction of the reflector of $i$ and $i$ defined as the right adjoint.

Let $A$ be an element of $C$. Assume that $\operatorname{essImage}$ holds for $i$. Then $\operatorname{unitCompPartialBijective}$ applied to $A$ and $\mathrm{hB}$ is an equivalence from the set of homomorphisms of $A$ and $B$ to the set of homomorphisms of the action of $i$ and the action of the reflector of $i$ and $A$ and $B$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the homomorphism congruence of the identity of $A$ and the inverse of $\operatorname{getIso}$ applied to $\mathrm{hB}$ and $\operatorname{unitCompPartialBijectiveAux}$ applied to $A$ and the witness of $\mathrm{hB}$ and the homomorphism congruence of the identity of the action of $i$ and the action of the reflector of $i$ and $A$ and $\operatorname{getIso}$ applied to $\mathrm{hB}$.

Let $\mathrm{adj}$ be an adjunction of $\mathrm{L'}$ and $\mathrm{R'}$. Let $\mathrm{hiC}$ be an element of $\operatorname{FullyFaithful}$ applied to $\mathrm{iC}$. Let $\mathrm{hiD}$ be an element of $\operatorname{FullyFaithful}$ applied to $\mathrm{iD}$. Let $\mathrm{comm1}$ be an isomorphism of the composition of $\mathrm{iC}$ and $\mathrm{L'}$ and the composition of $L$ and $\mathrm{iD}$. Let $\mathrm{comm2}$ be an isomorphism of the composition of $\mathrm{iD}$ and $\mathrm{R'}$ and the composition of $R$ and $\mathrm{iC}$. Then $\operatorname{restrictFullyFaithful}$ applied to $\mathrm{adj}$, $\mathrm{hiC}$, $\mathrm{hiD}$, $\mathrm{comm1}$ and $\mathrm{comm2}$ is an adjunction of $L$ and $R$.

triple of G and H (from the name)

Let $F$ and $H$ be functors of $C$ and $D$. Let $G$ be a functor of $D$ and $C$. Then the triples of $G$ and $H$ are a basic type.

the adjoint of self (from the name)

Let $\mathrm{self}$ be a triple of $G$ and $H$. Then the adjoint of $\mathrm{self}$ is an adjunction of $F$ and $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the adjoint of self (from the name)

Let $\mathrm{self}$ be a triple of $G$ and $H$. Then the adjoint of $\mathrm{self}$ is an adjunction of $G$ and $H$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the fully faithful equivalence of t (from the name)

Let $t$ be a triple of $G$ and $H$. Then $\operatorname{leftToRight}$ applied to $t$ is a homomorphism of $F$ and $H$ defined as the composition of the inverse of the right unitor of $F$ and the composition of the left whisker of $F$ and the unit of the adjoint of $t$ and the composition of the inverse of the associator of $G$ and $H$ and the composition of the inverse of the right whisker of the unit of the adjoint of $t$ and $H$ and the homomorphism of the left unitor of $H$.

the opposite of t (from the name)

Let $t$ be a triple of $G$ and $H$. Then the opposite of $t$ is a triple of the opposite of $G$ and the opposite of $F$ defined as $\operatorname{mk}$ applied to the opposite of the adjoint of $t$ and the opposite of the adjoint of $t$.

Let $t$ be a triple of $G$ and $H$. Then $\operatorname{rightToLeft}$ applied to $t$ is a homomorphism of $H$ and $F$ defined as the preimage of the right whiskering of $\operatorname{ofFullyFaithful}$ applied to $G$ and $C$ and the composition of the counit of the adjoint of $t$ and the unit of the adjoint of $t$.

Let $\mathrm{adj1}$ be an adjunction of $F$ and $G$. Let $\mathrm{adj2}$ be an adjunction of $\mathrm{F'}$ and $G$. Then $\operatorname{leftAdjointUniq}$ applied to $\mathrm{adj1}$ and $\mathrm{adj2}$ is an isomorphism of $F$ and $\mathrm{F'}$ defined as the inverse of $\operatorname{symm}$ applied to the conjugate isomorphism equivalence of $\mathrm{adj1}$ and $\mathrm{adj2}$ and the identity of $G$.

Let $\mathrm{adj1}$ be an adjunction of $F$ and $G$. Let $\mathrm{adj2}$ be an adjunction of $F$ and $\mathrm{G'}$. Then $\operatorname{rightAdjointUniq}$ applied to $\mathrm{adj1}$ and $\mathrm{adj2}$ is an isomorphism of $G$ and $\mathrm{G'}$ defined as $\operatorname{conjugateIsoEquiv}$ applied to $\mathrm{adj1}$, $\mathrm{adj2}$ and the identity of $F$.

the left whisker of C and adj (from the name)

Let $C$ be a set. Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the left whisker of $C$ and $\mathrm{adj}$ is an adjunction of the action of the left whiskering of $D$ and $C$ and $G$ and the action of the left whiskering of $E$ and $C$ and $F$.

the right whisker of C and adj (from the name)

Let $C$ be a set. Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the right whisker of $C$ and $\mathrm{adj}$ is an adjunction of the action of the right whiskering of $D$ and $E$ and $F$ and the action of the right whiskering of $E$ and $D$ and $G$.

C is balanced (from the docstring)

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

adjoint of B (from the name)

Let $B$ be a set. Then the adjoints of $B$ are a basic type.

the associator of x2 and x3 (from the name)

Let $x_{1}$ be a homomorphism of $a$ and $b$. Let $x_{2}$ be a homomorphism of $b$ and $c$. Let $x_{3}$ be a homomorphism of $c$ and $d$. Then the associator of $x_{2}$ and $x_{3}$ is an isomorphism of the composition of the composition of $x_{1}$ and $x_{2}$ and $x_{3}$ and the composition of $x_{1}$ and the composition of $x_{2}$ and $x_{3}$.

the left unitor in the bicategory of x1 (from the docstring)

Let $x_{1}$ be a homomorphism of $a$ and $b$. Then the left unitor in the bicategory of $x_{1}$ is an isomorphism of the composition of the identity morphism of $a$ and $x_{1}$ and $x_{1}$.

the right unitor in the bicategory of x1 (from the docstring)

Let $x_{1}$ be a homomorphism of $a$ and $b$. Then the right unitor in the bicategory of $x_{1}$ is an isomorphism of the composition of $x_{1}$ and the identity morphism of $b$ and $x_{1}$.

the left whiskering in the bicategory of x1 and y (from the docstring)

Let $x_{1}$ be a homomorphism of $a$ and $b$. Let $y$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the left whiskering in the bicategory of $x_{1}$ and $y$ is a homomorphism of the composition of $x_{1}$ and $x_{2}$ and the composition of $x_{1}$ and $x_{3}$.

the right whiskering in the bicategory of x3 and x4 (from the docstring)

Let $x_{3}$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $x_{4}$ be a homomorphism of $b$ and $c$. Then the right whiskering in the bicategory of $x_{3}$ and $x_{4}$ is a homomorphism of the composition of $x_{1}$ and $x_{4}$ and the composition of $x_{2}$ and $x_{4}$.

homomorphism of a and b (from the name)

Let $a$ and $b$ be elements of $B$. Then the homomorphisms of $a$ and $b$ are a basic type.

the adjoint of self (from the name)

Let $\mathrm{self}$ be a homomorphism of $a$ and $b$. Then the adjoint of $\mathrm{self}$ is an adjunction of $\operatorname{l}$ applied to $\mathrm{self}$ and $\operatorname{r}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homomorphism of $a$ and $b$. Then $\operatorname{l}$ applied to $\mathrm{self}$ is a homomorphism of $a$ and $b$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homomorphism of $a$ and $b$. Then $\operatorname{r}$ applied to $\mathrm{self}$ is a homomorphism of $b$ and $a$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

homomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be homomorphisms of $a$ and $b$. Then the homomorphisms of $x_{1}$ and $x_{2}$ are a basic type.

Let $\mathrm{self}$ be a homomorphism of $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_Bicategory\_\_Adj\_\_Hom\_u2082\_\_\_\_u3c4\_l}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{l}$ applied to $x_{1}$ and $\operatorname{l}$ applied to $x_{2}$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_Adj\_\_Hom\_u2082\_\_\_proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homomorphism of $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_Bicategory\_\_Adj\_\_Hom\_u2082\_\_\_\_u3c4\_r}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{r}$ applied to $x_{2}$ and $\operatorname{r}$ applied to $x_{1}$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_Adj\_\_Hom\_u2082\_\_\_proj1}$ applied to $\mathrm{self}$.

$\mathrm{CategoryTheory\_\_Bicategory\_\_Adj\_\_forget\_u2081\_}$ is a pseudofunctor of the set of adjoints of $B$ and $B$.

the isomorphism of el and er (from the name)

Let $\mathrm{el}$ be an isomorphism of $\operatorname{l}$ applied to $x_{1}$ and $\operatorname{l}$ applied to $x_{2}$. Let $\mathrm{er}$ be an isomorphism of $\operatorname{r}$ applied to $x_{2}$ and $\operatorname{r}$ applied to $x_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that $\operatorname{conjugateEquiv}$ applied to the adjoint of $x_{2}$, the adjoint of $x_{1}$ and the homomorphism of $\mathrm{el}$ is equal to the homomorphism of $\mathrm{er}$ and $\mathrm{CategoryTheory\_\_Bicategory\_\_Adj\_\_iso\_u2082\_Mk\_\_\_auto\_1}$. Then the isomorphism of $\mathrm{el}$ and $\mathrm{er}$ is an isomorphism of $x_{1}$ and $x_{2}$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $x_{1}$ and $x_{2}$. Then the isomorphism of $e$ is an isomorphism of $\operatorname{l}$ applied to $x_{1}$ and $\operatorname{l}$ applied to $x_{2}$.

the object of self (from the name)

Let $\mathrm{self}$ be an adjoint of $B$. Then the object of $\mathrm{self}$ is an element of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $x_{1}$ and $x_{2}$. Then the isomorphism of $e$ is an isomorphism of $\operatorname{r}$ applied to $x_{1}$ and $\operatorname{r}$ applied to $x_{2}$.

adjunction of f and g (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $a$. Then the adjunctions of $f$ and $g$ are a basic type.

the composition of x5 and x6 (from the name)

Let $x_{5}$ be an adjunction of $x_{1}$ and $x_{2}$. Let $x_{6}$ be an adjunction of $x_{3}$ and $x_{4}$. Then the composition of $x_{5}$ and $x_{6}$ is an adjunction of the composition of $x_{1}$ and $x_{3}$ and the composition of $x_{4}$ and $x_{2}$.

the counit of self (from the docstring)

Let $\mathrm{self}$ be an adjunction of $f$ and $g$. Then the counit of $\mathrm{self}$ is a homomorphism of the composition of $g$ and $f$ and the identity morphism of $b$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the identity of a (from the name)

Let $a$ be an element of $B$. Then the identity of $a$ is an adjunction of the identity morphism of $a$ and the identity morphism of $a$.

the adjunction of f (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Then the adjunction of $f$ is an adjunction of $f$ and the right adjoint of $f$ defined as the adjoint of $\operatorname{getRightAdjoint}$ applied to $f$.

the adjunction of f (from the name)

Let $f$ be a homomorphism of $b$ and $a$. Then the adjunction of $f$ is an adjunction of the left adjoint of $f$ and $f$ defined as the adjoint of $\operatorname{getLeftAdjoint}$ applied to $f$.

the unit of self (from the docstring)

Let $\mathrm{self}$ be an adjunction of $f$ and $g$. Then the unit of $\mathrm{self}$ is a homomorphism of the identity morphism of $a$ and the composition of $f$ and $g$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

equivalence of a and b (from the name)

Let $a$ and $b$ be elements of $B$. Then the equivalences of $a$ and $b$ are a basic type.

the adjoint of e (from the name)

Let $e$ be an equivalence of $a$ and $b$. Then the adjoint of $e$ is an adjunction of the homomorphism of $e$ and the inverse of $e$ defined as $\operatorname{mk}$ applied to the homomorphism of the unit of $e$, the homomorphism of the counit of $e$, $\mathrm{CategoryTheory\_\_Bicategory\_\_Equivalence\_\_left\_triangle\_hom}$ applied to $e$ and $\mathrm{CategoryTheory\_\_Bicategory\_\_Equivalence\_\_right\_triangle\_hom}$ applied to $e$.

the counit of self (from the name)

Let $\mathrm{self}$ be an equivalence of $a$ and $b$. Then the counit of $\mathrm{self}$ is an isomorphism of the composition of the inverse of $\mathrm{self}$ and the homomorphism of $\mathrm{self}$ and the identity morphism of $b$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the homomorphism of self (from the name)

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

the identity of a (from the name)

Let $a$ be an element of $B$. Then the identity of $a$ is an equivalence of $a$ and $a$.

the inverse of self (from the name)

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

Let $x_{1}$ be an isomorphism of the identity morphism of $a$ and the composition of $f$ and $g$. Let $x_{2}$ be an isomorphism of the composition of $g$ and $f$ and the identity morphism of $b$. Then $\operatorname{mkOfAdjointifyCounit}$ applied to $x_{1}$ and $x_{2}$ is an equivalence of $a$ and $b$ defined as $\operatorname{mk}$ applied to $f$, $g$, $x_{1}$, $\operatorname{adjointifyCounit}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{CategoryTheory\_\_Bicategory\_\_adjointifyCounit\_left\_triangle}$ applied to $x_{1}$ and $x_{2}$.

the unit of self (from the name)

Let $\mathrm{self}$ be an equivalence of $a$ and $b$. Then the unit of $\mathrm{self}$ is an isomorphism of the identity morphism of $a$ and the composition of the homomorphism of $\mathrm{self}$ and the inverse of $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

left is a left adjoint (from the name)

Let $\mathrm{left}$ be a homomorphism of $a$ and $b$. Then we can say that $\mathrm{left}$ is a left adjoint.

right is a right adjoint (from the name)

Let $\mathrm{right}$ be a homomorphism of $b$ and $a$. Then we can say that $\mathrm{right}$ is a right adjoint.

left adjoint of right (from the name)

Let $\mathrm{right}$ be a homomorphism of $b$ and $a$. Then the left adjoints of $\mathrm{right}$ are a basic type.

the adjoint of self (from the name)

Let $\mathrm{self}$ be a left adjoint of $\mathrm{right}$. Then the adjoint of $\mathrm{self}$ is an adjunction of the left adjoint to $\mathrm{self}$ and $\mathrm{right}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the left adjoint to self (from the docstring)

Let $\mathrm{self}$ be a left adjoint of $\mathrm{right}$. Then the left adjoint to $\mathrm{self}$ is a homomorphism of $a$ and $b$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

right adjoint of left (from the name)

Let $\mathrm{left}$ be a homomorphism of $a$ and $b$. Then the right adjoints of $\mathrm{left}$ are a basic type.

the adjoint of self (from the name)

Let $\mathrm{self}$ be a right adjoint of $\mathrm{left}$. Then the adjoint of $\mathrm{self}$ is an adjunction of $\mathrm{left}$ and the right adjoint to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the right adjoint to self (from the docstring)

Let $\mathrm{self}$ be a right adjoint of $\mathrm{left}$. Then the right adjoint to $\mathrm{self}$ is a homomorphism of $b$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $f$ be a homomorphism of $b$ and $a$. Then $\operatorname{getLeftAdjoint}$ applied to $f$ is a left adjoint of $f$ defined as $\operatorname{choice}$ applied to $\operatorname{nonempty}$.

Let $f$ be a homomorphism of $a$ and $b$. Then $\operatorname{getRightAdjoint}$ applied to $f$ is a right adjoint of $f$ defined as $\operatorname{choice}$ applied to $\operatorname{nonempty}$.

the left adjoint of f (from the docstring)

Let $f$ be a homomorphism of $b$ and $a$. Then the left adjoint of $f$ is a homomorphism of $a$ and $b$ defined as the left adjoint to $\operatorname{getLeftAdjoint}$ applied to $f$.

the left zigzag of x1 and x2 (from the name)

Let $x_{1}$ be a homomorphism of the identity morphism of $a$ and the composition of $f$ and $g$. Let $x_{2}$ be a homomorphism of the composition of $g$ and $f$ and the identity morphism of $b$. Then the left zigzag of $x_{1}$ and $x_{2}$ is a homomorphism of the composition of the identity morphism of $a$ and $f$ and the composition of $f$ and the identity morphism of $b$ defined as $\operatorname{bicategoricalComp}$ applied to the right whisker of $x_{1}$ and $f$ and the left whisker of $f$ and $x_{2}$.

the left zigzag isomorphism of x1 and x2 (from the name)

Let $x_{1}$ be an isomorphism of the identity morphism of $a$ and the composition of $f$ and $g$. Let $x_{2}$ be an isomorphism of the composition of $g$ and $f$ and the identity morphism of $b$. Then the left zigzag isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of the composition of the identity morphism of $a$ and $f$ and the composition of $f$ and the identity morphism of $b$ defined as $\operatorname{bicategoricalIsoComp}$ applied to the right whiskering of $x_{1}$ and $f$ and the left whiskering of $f$ and $x_{2}$.

the right adjoint of f (from the docstring)

Let $f$ be a homomorphism of $a$ and $b$. Then the right adjoint of $f$ is a homomorphism of $b$ and $a$ defined as the right adjoint to $\operatorname{getRightAdjoint}$ applied to $f$.

the right zigzag of x1 and x2 (from the name)

Let $x_{1}$ be a homomorphism of the identity morphism of $a$ and the composition of $f$ and $g$. Let $x_{2}$ be a homomorphism of the composition of $g$ and $f$ and the identity morphism of $b$. Then the right zigzag of $x_{1}$ and $x_{2}$ is a homomorphism of the composition of $g$ and the identity morphism of $a$ and the composition of the identity morphism of $b$ and $g$ defined as $\operatorname{bicategoricalComp}$ applied to the left whisker of $g$ and $x_{1}$ and the right whisker of $x_{2}$ and $g$.

the right zigzag isomorphism of x1 and x2 (from the name)

Let $x_{1}$ be an isomorphism of the identity morphism of $a$ and the composition of $f$ and $g$. Let $x_{2}$ be an isomorphism of the composition of $g$ and $f$ and the identity morphism of $b$. Then the right zigzag isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of the composition of $g$ and the identity morphism of $a$ and the composition of the identity morphism of $b$ and $g$ defined as $\operatorname{bicategoricalIsoComp}$ applied to the left whiskering of $g$ and $x_{1}$ and the right whiskering of $x_{2}$ and $g$.

the map adjunction of F and adj (from the name)

Let $F$ be a pseudofunctor of $B$ and $C$. Let $\mathrm{adj}$ be an adjunction of $f$ and $g$. Then the map adjunction of $F$ and $\mathrm{adj}$ is an adjunction of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $g$.

the map adjunction of F and adj (from the name)

Let $F$ be a strict pseudofunctor of $B$ and $C$. Let $\mathrm{adj}$ be an adjunction of $f$ and $g$. Then the map adjunction of $F$ and $\mathrm{adj}$ is an adjunction of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\operatorname{toPseudofunctor}$ applied to $\operatorname{toStrictlyUnitaryPseudofunctor}$ applied to $F$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\operatorname{toPseudofunctor}$ applied to $\operatorname{toStrictlyUnitaryPseudofunctor}$ applied to $F$ and $g$ defined as the map adjunction of $\operatorname{toPseudofunctor}$ applied to $\operatorname{toStrictlyUnitaryPseudofunctor}$ applied to $F$ and $\mathrm{adj}$.

the adjunction of adj (from the name)

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the adjunction of $\mathrm{adj}$ is an adjunction of the functor of $F$ and the functor of $G$.

the category of adj (from the name)

Let $\mathrm{adj}$ be an adjunction of $F$ and $G$. Then the category of $\mathrm{adj}$ is an adjunction of the category homomorphism of $F$ and the category homomorphism of $G$.

the homomorphism equivalence of adj (from the name)

Let $\mathrm{adj}$ be an adjunction of $l$ and $r$. Then the homomorphism equivalence of $\mathrm{adj}$ is an equivalence from the set of homomorphisms of $g$ and the composition of $l$ and $h$ to the set of homomorphisms of the composition of $r$ and $g$ and $h$.

the homomorphism equivalence of adj (from the name)

Let $\mathrm{adj}$ be an adjunction of $l$ and $r$. Then the homomorphism equivalence of $\mathrm{adj}$ is an equivalence from the set of homomorphisms of the composition of $g$ and $l$ and $h$ to the set of homomorphisms of $g$ and the composition of $h$ and $r$.

the conjugate equivalence of x5 and x6 (from the name)

Let $x_{5}$ be an adjunction of $x_{1}$ and $x_{3}$. Let $x_{6}$ be an adjunction of $x_{2}$ and $x_{4}$. Then the conjugate equivalence of $x_{5}$ and $x_{6}$ is an equivalence from the set of homomorphisms of $x_{2}$ and $x_{1}$ to the set of homomorphisms of $x_{3}$ and $x_{4}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of the homomorphism congruence of the left unitor of $x_{2}$ and the right unitor of $x_{1}$ and $\operatorname{mateEquiv}$ applied to $x_{5}$ and $x_{6}$ and the homomorphism congruence of the right unitor of $x_{3}$ and the left unitor of $x_{4}$.

the conjugate isomorphism equivalence of x5 and x6 (from the name)

Let $x_{5}$ be an adjunction of $x_{1}$ and $x_{3}$. Let $x_{6}$ be an adjunction of $x_{2}$ and $x_{4}$. Then the conjugate isomorphism equivalence of $x_{5}$ and $x_{6}$ is an equivalence from the set of isomorphisms of $x_{2}$ and $x_{1}$ to the set of isomorphisms of $x_{3}$ and $x_{4}$.

the vertical composition of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{1}$. Let $x_{5}$ be a homomorphism of the composition of $g$ and $x_{3}$ and the composition of $x_{2}$ and $h$. Then the vertical composition of $x_{4}$ and $x_{5}$ is a homomorphism of the composition of $g$ and $x_{3}$ and the composition of $x_{1}$ and $h$ defined as the composition of $x_{5}$ and the right whisker of $x_{4}$ and $h$.

the composition of x16 and x17 (from the name)

Let $x_{14}$ be a homomorphism of the composition of $x_{2}$ and $x_{10}$ and the composition of $x_{8}$ and $x_{3}$. Let $x_{15}$ be a homomorphism of the composition of $x_{3}$ and $x_{11}$ and the composition of $x_{9}$ and $x_{4}$. Let $x_{16}$ be a homomorphism of the composition of $x_{5}$ and $x_{12}$ and the composition of $x_{10}$ and $x_{6}$. Let $x_{17}$ be a homomorphism of the composition of $x_{6}$ and $x_{13}$ and the composition of $x_{11}$ and $x_{7}$. Then the composition of $x_{16}$ and $x_{17}$ is a homomorphism of the composition of the composition of $x_{2}$ and $x_{5}$ and the composition of $x_{12}$ and $x_{13}$ and the composition of the composition of $x_{8}$ and $x_{9}$ and the composition of $x_{4}$ and $x_{7}$ defined as the vertical composition of $\operatorname{hcomp}$ applied to $x_{14}$ and $x_{15}$ and $\operatorname{hcomp}$ applied to $x_{16}$ and $x_{17}$.

Let $x_{5}$ be a homomorphism of the composition of $g$ and $x_{2}$ and the composition of $x_{1}$ and $h$. Let $x_{6}$ be a homomorphism of the composition of $h$ and $x_{4}$ and the composition of $x_{3}$ and $k$. Then $\operatorname{hcomp}$ applied to $x_{5}$ and $x_{6}$ is a homomorphism of the composition of $g$ and the composition of $x_{2}$ and $x_{4}$ and the composition of the composition of $x_{1}$ and $x_{3}$ and $k$ defined as the composition of the inverse of the associator of $x_{2}$ and $x_{4}$ and the composition of the right whisker of $x_{5}$ and $x_{4}$ and the composition of the homomorphism of the associator of $h$ and $x_{4}$ and the composition of the left whisker of $x_{1}$ and $x_{6}$ and the inverse of the associator of $x_{3}$ and $k$.

the vertical composition of x8 and x9 (from the name)

Let $x_{8}$ be a homomorphism of the composition of $x_{1}$ and $x_{6}$ and the composition of $x_{5}$ and $x_{3}$. Let $x_{9}$ be a homomorphism of the composition of $x_{2}$ and $x_{7}$ and the composition of $x_{6}$ and $x_{4}$. Then the vertical composition of $x_{8}$ and $x_{9}$ is a homomorphism of the composition of the composition of $x_{1}$ and $x_{2}$ and $x_{7}$ and the composition of $x_{5}$ and the composition of $x_{3}$ and $x_{4}$ defined as the composition of the homomorphism of the associator of $x_{2}$ and $x_{7}$ and the composition of the left whisker of $x_{1}$ and $x_{9}$ and the composition of the inverse of the associator of $x_{6}$ and $x_{4}$ and the composition of the right whisker of $x_{8}$ and $x_{4}$ and the homomorphism of the associator of $x_{3}$ and $x_{4}$.

the vertical composition of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of the composition of $g$ and $x_{2}$ and the composition of $x_{1}$ and $h$. Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{2}$. Then the vertical composition of $x_{4}$ and $x_{5}$ is a homomorphism of the composition of $g$ and $x_{3}$ and the composition of $x_{1}$ and $h$ defined as the composition of the left whisker of $g$ and $x_{5}$ and $x_{4}$.

Let $x_{5}$ be an adjunction of $x_{1}$ and $x_{2}$. Let $x_{6}$ be an adjunction of $x_{3}$ and $x_{4}$. Then $\operatorname{mateEquiv}$ applied to $x_{5}$ and $x_{6}$ is an equivalence from the set of homomorphisms of the composition of $g$ and $x_{3}$ and the composition of $x_{1}$ and $h$ to the set of homomorphisms of the composition of $x_{2}$ and $g$ and the composition of $h$ and $x_{4}$ defined as the composition of the homomorphism equivalence of $x_{6}$ and the composition of the homomorphism congruence of the identity of $g$ and the associator of $h$ and $x_{4}$ and the homomorphism equivalence of $x_{5}$.

the vertical composition of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $x_{5}$ be a homomorphism of the composition of $x_{2}$ and $g$ and the composition of $h$ and $x_{3}$. Then the vertical composition of $x_{4}$ and $x_{5}$ is a homomorphism of the composition of $x_{1}$ and $g$ and the composition of $h$ and $x_{3}$ defined as the composition of the right whisker of $x_{4}$ and $g$ and $x_{5}$.

the composition of x16 and x17 (from the name)

Let $x_{14}$ be a homomorphism of the composition of $x_{8}$ and $x_{2}$ and the composition of $x_{3}$ and $x_{10}$. Let $x_{15}$ be a homomorphism of the composition of $x_{9}$ and $x_{3}$ and the composition of $x_{4}$ and $x_{11}$. Let $x_{16}$ be a homomorphism of the composition of $x_{10}$ and $x_{5}$ and the composition of $x_{6}$ and $x_{12}$. Let $x_{17}$ be a homomorphism of the composition of $x_{11}$ and $x_{6}$ and the composition of $x_{7}$ and $x_{13}$. Then the composition of $x_{16}$ and $x_{17}$ is a homomorphism of the composition of the composition of $x_{9}$ and $x_{8}$ and the composition of $x_{2}$ and $x_{5}$ and the composition of the composition of $x_{4}$ and $x_{7}$ and the composition of $x_{13}$ and $x_{12}$ defined as the vertical composition of $\operatorname{hcomp}$ applied to $x_{14}$ and $x_{15}$ and $\operatorname{hcomp}$ applied to $x_{16}$ and $x_{17}$.

Let $x_{5}$ be a homomorphism of the composition of $x_{1}$ and $g$ and the composition of $h$ and $x_{2}$. Let $x_{6}$ be a homomorphism of the composition of $x_{3}$ and $h$ and the composition of $k$ and $x_{4}$. Then $\operatorname{hcomp}$ applied to $x_{5}$ and $x_{6}$ is a homomorphism of the composition of the composition of $x_{3}$ and $x_{1}$ and $g$ and the composition of $k$ and the composition of $x_{4}$ and $x_{2}$ defined as the composition of the homomorphism of the associator of $x_{1}$ and $g$ and the composition of the left whisker of $x_{3}$ and $x_{5}$ and the composition of the inverse of the associator of $h$ and $x_{2}$ and the composition of the right whisker of $x_{6}$ and $x_{2}$ and the homomorphism of the associator of $x_{4}$ and $x_{2}$.

the vertical composition of x8 and x9 (from the name)

Let $x_{8}$ be a homomorphism of the composition of $x_{5}$ and $x_{1}$ and the composition of $x_{3}$ and $x_{6}$. Let $x_{9}$ be a homomorphism of the composition of $x_{6}$ and $x_{2}$ and the composition of $x_{4}$ and $x_{7}$. Then the vertical composition of $x_{8}$ and $x_{9}$ is a homomorphism of the composition of $x_{5}$ and the composition of $x_{1}$ and $x_{2}$ and the composition of the composition of $x_{3}$ and $x_{4}$ and $x_{7}$ defined as the composition of the inverse of the associator of $x_{1}$ and $x_{2}$ and the composition of the right whisker of $x_{8}$ and $x_{2}$ and the composition of the homomorphism of the associator of $x_{6}$ and $x_{2}$ and the composition of the left whisker of $x_{3}$ and $x_{9}$ and the inverse of the associator of $x_{4}$ and $x_{7}$.

the vertical composition of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of the composition of $x_{1}$ and $g$ and the composition of $h$ and $x_{2}$. Let $x_{5}$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the vertical composition of $x_{4}$ and $x_{5}$ is a homomorphism of the composition of $x_{1}$ and $g$ and the composition of $h$ and $x_{3}$ defined as the composition of $x_{4}$ and the left whisker of $h$ and $x_{5}$.

B is a bicategory (from the name)

Let $B$ be a set. Then we can say that $B$ is a bicategory.

the associator of g and h (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $c$. Let $h$ be a homomorphism of $c$ and $d$. Then the associator of $g$ and $h$ is an isomorphism of the composition of the composition of $f$ and $g$ and $h$ and the composition of $f$ and the composition of $g$ and $h$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$, $f$, $g$ and $h$.

the left associator natural isomorphism of g and h (from the name)

Let $a$ be an element of $B$. Let $g$ be a homomorphism of $b$ and $c$. Let $h$ be a homomorphism of $c$ and $d$. Then the left associator natural isomorphism of $g$ and $h$ is an isomorphism of the composition of the action of $\operatorname{postcomposing}$ applied to $a$, $b$ and $c$ and $g$ and the action of $\operatorname{postcomposing}$ applied to $a$, $c$ and $d$ and $h$ and the action of $\operatorname{postcomposing}$ applied to $a$, $b$ and $d$ and the composition of $g$ and $h$.

the associator natural isomorphism middle of f and h (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Let $h$ be a homomorphism of $c$ and $d$. Then the associator natural isomorphism middle of $f$ and $h$ is an isomorphism of the composition of the action of $\operatorname{precomposing}$ applied to $a$, $b$ and $c$ and $f$ and the action of $\operatorname{postcomposing}$ applied to $a$, $c$ and $d$ and $h$ and the composition of the action of $\operatorname{postcomposing}$ applied to $b$, $c$ and $d$ and $h$ and the action of $\operatorname{precomposing}$ applied to $a$, $b$ and $d$ and $f$.

the right associator natural isomorphism of g and d (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $c$. Let $d$ be an element of $B$. Then the right associator natural isomorphism of $g$ and $d$ is an isomorphism of the action of $\operatorname{precomposing}$ applied to $a$, $c$ and $d$ and the composition of $f$ and $g$ and the composition of the action of $\operatorname{precomposing}$ applied to $b$, $c$ and $d$ and $g$ and the action of $\operatorname{precomposing}$ applied to $a$, $b$ and $d$ and $f$.

the left unitor of f (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Then the left unitor of $f$ is an isomorphism of the composition of the identity morphism of $a$ and $f$ and $f$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$ and $f$.

the left unitor natural isomorphism of a and b (from the name)

Let $a$ and $b$ be elements of $B$. Then the left unitor natural isomorphism of $a$ and $b$ is an isomorphism of the action of $\operatorname{precomposing}$ applied to $a$, $a$ and $b$ and the identity morphism of $a$ and the identity of the set of homomorphisms of $a$ and $b$.

the postcomposition of a and f (from the name)

Let $a$ be an element of $B$. Let $f$ be a homomorphism of $b$ and $c$. Then the postcomposition of $a$ and $f$ is a functor of the set of homomorphisms of $a$ and $b$ and the set of homomorphisms of $a$ and $c$.

Let $a$, $b$ and $c$ be elements of $B$. Then $\operatorname{postcomposing}$ applied to $a$, $b$ and $c$ is a functor of the set of homomorphisms of $b$ and $c$ and the set of functors of the set of homomorphisms of $a$ and $b$ and the set of homomorphisms of $a$ and $c$.

the precomposition of c and f (from the name)

Let $c$ be an element of $B$. Let $f$ be a homomorphism of $a$ and $b$. Then the precomposition of $c$ and $f$ is a functor of the set of homomorphisms of $b$ and $c$ and the set of homomorphisms of $a$ and $c$.

Let $a$, $b$ and $c$ be elements of $B$. Then $\operatorname{precomposing}$ applied to $a$, $b$ and $c$ is a functor of the set of homomorphisms of $a$ and $b$ and the set of functors of the set of homomorphisms of $b$ and $c$ and the set of homomorphisms of $a$ and $c$.

the right unitor of f (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Then the right unitor of $f$ is an isomorphism of the composition of $f$ and the identity morphism of $b$ and $f$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$ and $f$.

the right unitor natural isomorphism of a and b (from the name)

Let $a$ and $b$ be elements of $B$. Then the right unitor natural isomorphism of $a$ and $b$ is an isomorphism of the action of $\operatorname{postcomposing}$ applied to $a$, $b$ and $b$ and the identity morphism of $b$ and the identity of the set of homomorphisms of $a$ and $b$.

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

Let $f$ be a homomorphism of $a$ and $b$. Let $x$ be a homomorphism of $g$ and $h$. Then the left whisker of $f$ and $x$ is a homomorphism of the composition of $f$ and $g$ and the composition of $f$ and $h$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $f$ and $x$.

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

Let $f$ be a homomorphism of $a$ and $b$. Let $x_{1}$ be an isomorphism of $g$ and $h$. Then the left whiskering of $f$ and $x_{1}$ is an isomorphism of the composition of $f$ and $g$ and the composition of $f$ and $h$.

the right whisker of x and h (from the name)

Let $x$ be a homomorphism of $f$ and $g$. Let $h$ be a homomorphism of $b$ and $c$. Then the right whisker of $x$ and $h$ is a homomorphism of the composition of $f$ and $h$ and the composition of $g$ and $h$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $x$ and $h$.

the right whiskering of x1 and h (from the docstring)

Let $x_{1}$ be an isomorphism of $f$ and $g$. Let $h$ be a homomorphism of $b$ and $c$. Then the right whiskering of $x_{1}$ and $h$ is an isomorphism of the composition of $f$ and $h$ and the composition of $g$ and $h$.

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

the composition of x1 and x2 (from the name)

Let $x_{1}$ be a homomorphism of $f$ and $\mathrm{f'}$. Let $x_{2}$ be a homomorphism of $g$ and $\mathrm{g'}$. Then the composition of $x_{1}$ and $x_{2}$ is a homomorphism of the composition of $f$ and $g$ and the composition of $\mathrm{f'}$ and $\mathrm{g'}$ defined as the map of the functor of the composition of $b$ and $c$ and $\ProdmkMACRoU {x_{1}}{x_{2}}$.

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

homomorphism of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the homomorphisms of $f$ and $g$ are a basic type.

the base of x2 (from the name)

Let $x_{2}$ be a homomorphism of $f$ and $g$. Then the base of $x_{2}$ is a homomorphism of $\operatorname{homEquiv}$ applied to $f$ and $\operatorname{homEquiv}$ applied to $g$ defined as the base of $x_{2}$.

the base of self (from the name)

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

Let $x_{2}$ be a homomorphism of $\operatorname{homEquiv}$ applied to $f$ and $\operatorname{homEquiv}$ applied to $g$. Then $\operatorname{mk}$ applied to $x_{2}$ is a homomorphism of $f$ and $g$ defined as $\operatorname{mk'}$ applied to $x_{2}$.

the composition of x2 and x3 (from the name)

Let $x_{2}$ be a homomorphism of $f$ and $\mathrm{f'}$. Let $x_{3}$ be a homomorphism of $g$ and $\mathrm{g'}$. Then the composition of $x_{2}$ and $x_{3}$ is a homomorphism of the composition of $f$ and $g$ and the composition of $\mathrm{f'}$ and $\mathrm{g'}$.

the homomorphism equivalence (from the name)

The homomorphism equivalence is an equivalence from the set of homomorphisms of $a$ and $b$ to the set of homomorphisms of the base of $a$ and the base of $b$ defined as the composition of the homomorphism equivalence of the set of categories and the composition of the equivalence functor of the tensor unity in the monoidal structure of the set of categories and the homomorphism of $a$ and $b$ and $\operatorname{fromChosenTerminalEquiv}$.

the base of a (from the name)

Let $a$ be an element of $\operatorname{CatEnrichedOrdinary}$ applied to $C$. Then the base of $a$ is an element of $\operatorname{CatEnriched}$ applied to $C$ defined as $a$.

the inclusion of B (from the name)

Let $B$ be a set. Then the inclusion of $B$ is a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of paths of $B$ and the set of free bicategories of $B$.

the inclusion path of a and b (from the name)

Let $a$ and $b$ be elements of $B$. Then the inclusion path of $a$ and $b$ is a functor of $\operatorname{Discrete}$ applied to the set of paths of $a$ and $b$ and the set of homomorphisms of $a$ and $b$ defined as the functor of $\operatorname{inclusionPathAux}$.

Let $B$ be a set. Then $\operatorname{normalize}$ applied to $B$ is a pseudofunctor of the set of free bicategories of $B$ and $\operatorname{LocallyDiscrete}$ applied to the set of paths of $B$.

Let $a$ and $b$ be elements of $B$. Then $\operatorname{normalizeEquiv}$ applied to $a$ and $b$ is an equivalence of the set of homomorphisms of $a$ and $b$ and $\operatorname{Discrete}$ applied to the set of paths of $a$ and $b$.

Let $p$ be a path of $a$ and $b$. Let $f$ be a homomorphism of $b$ and $c$. Then $\operatorname{normalizeIso}$ applied to $p$ and $f$ is an isomorphism of the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{preinclusion}$ applied to $B$ and $\operatorname{mk}$ applied to $p$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{preinclusion}$ applied to $B$ and $\operatorname{mk}$ applied to $\operatorname{normalizeAux}$ applied to $p$ and $f$ defined as $\operatorname{brecOn}$ applied to $f$, $\mathrm{CategoryTheory\_\_FreeBicategory\_\_normalizeIso\_\_\_f}$ and $p$.

Let $B$ be a set. Then $\operatorname{preinclusion}$ applied to $B$ is a prelax functor of $\operatorname{LocallyDiscrete}$ applied to the set of paths of $B$ and the set of free bicategories of $B$.

Let $X$ be an element of $C$. Then an element of $\operatorname{EndMonoidal}$ applied to $X$ is an element of the function that maps $X$ to the set of homomorphisms of $X$ and $X$.

Assume that $\EqtMACRoH {x_{1}}{y}$. Assume that $\EqtMACRoH {y}{z}$. Then $\operatorname{eqToHomTransIso}$ applied to $h$ and $h_{1}$ is an isomorphism of $\operatorname{eqToHom}$ applied to $\operatorname{trans}$ applied to $h$ and $h_{1}$ and the composition of $\operatorname{eqToHom}$ applied to $h$ and $\operatorname{eqToHom}$ applied to $h_{1}$.

left extension of f and g (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Then a left extension of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of structured arrows of $g$ and the precomposition of $c$ and $f$.

Let $g$ be a homomorphism of $a$ and $c$. Then $\operatorname{alongId}$ applied to $g$ is a left extension of the identity morphism of $a$ and $g$ defined as $\operatorname{mk}$ applied to $g$ and the inverse of the left unitor of $g$.

the extension of t (from the name)

Let $t$ be a left extension of $f$ and $g$. Then the extension of $t$ is a homomorphism of $b$ and $c$ defined as the right object of $t$.

the homomorphism of x1 and w (from the name)

Let $x_{1}$ be a homomorphism of the extension of $s$ and the extension of $t$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the unit of $s$ and the left whisker of $f$ and $x_{1}$ is equal to the unit of $t$ and $\mathrm{CategoryTheory\_\_Bicategory\_\_LeftExtension\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $x_{1}$ and $w$ is a homomorphism of $s$ and $t$ defined as the homomorphism of $x_{1}$ and $w$.

the map isomorphism of ef and eg (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$ is an equivalence of the set of left extensions of $f$ and $g$ and the set of left extensions of $\mathrm{f'}$ and $\mathrm{g'}$ defined as the composition of the map natural isomorphism of the map isomorphism of $\operatorname{precomposing}$ applied to $a$, $b$ and $c$ and $\mathrm{ef}$ and the map isomorphism of $\mathrm{eg}$.

Let $h$ be a homomorphism of $b$ and $c$. Let $\mathrm{unit}$ be a homomorphism of $g$ and the composition of $f$ and $h$. Then $\operatorname{mk}$ applied to $h$ and $\mathrm{unit}$ is a left extension of $f$ and $g$ defined as $\operatorname{mk}$ applied to $\mathrm{unit}$.

the left extension of t (from the name)

Let $t$ be a left extension of $f$ and the composition of $g$ and the identity morphism of $c$. Then the left extension of $t$ is a left extension of $f$ and $g$ defined as $\operatorname{mk}$ applied to the extension of $t$ and the composition of the inverse of the right unitor of $g$ and the unit of $t$.

the left extension of eg and t (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Let $t$ be a left extension of $f$ and $g$. Then the left extension of $\mathrm{eg}$ and $t$ is a left extension of $\mathrm{f'}$ and $\mathrm{g'}$ defined as the action of the functor of the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$ and $t$.

the unit of t (from the name)

Let $t$ be a left extension of $f$ and $g$. Then the unit of $t$ is a homomorphism of $g$ and the composition of $f$ and the extension of $t$ defined as the homomorphism of $t$.

the whisker of t and h (from the name)

Let $t$ be a left extension of $f$ and $g$. Let $h$ be a homomorphism of $c$ and $x_{1}$. Then the whisker of $t$ and $h$ is a left extension of $f$ and the composition of $g$ and $h$ defined as $\operatorname{mk}$ applied to the composition of the extension of $t$ and $h$ and the composition of the right whisker of the unit of $t$ and $h$ and the homomorphism of the associator of the extension of $t$ and $h$.

the whisker homomorphism of i and h (from the name)

Let $i$ be a homomorphism of $s$ and $t$. Let $h$ be a homomorphism of $c$ and $x_{1}$. Then the whisker homomorphism of $i$ and $h$ is a homomorphism of the whisker of $s$ and $h$ and the whisker of $t$ and $h$.

Let $s$ be a left extension of $f$ and the composition of $g$ and the identity morphism of $c$. Let $x_{1}$ be a homomorphism of $s$ and the whisker of $t$ and the identity morphism of $c$. Then $\operatorname{whiskerIdCancel}$ applied to $s$ and $x_{1}$ is a homomorphism of the left extension of $s$ and $t$.

the whisker isomorphism of i and h (from the name)

Let $i$ be an isomorphism of $s$ and $t$. Let $h$ be a homomorphism of $c$ and $x_{1}$. Then the whisker isomorphism of $i$ and $h$ is an isomorphism of the whisker of $s$ and $h$ and the whisker of $t$ and $h$.

the whisker of t (from the name)

Let $t$ be a left extension of $f$ and $g$. Then the whisker of $t$ is an isomorphism of the left extension of the whisker of $t$ and the identity morphism of $c$ and $t$.

the whisker of t and h (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Let $t$ be a left extension of $f$ and $g$. Let $h$ be a homomorphism of $c$ and $x_{1}$. Then the whisker of $t$ and $h$ is an isomorphism of the left extension of the right whiskering of $\mathrm{eg}$ and $h$ and the whisker of $t$ and $h$ and the whisker of the left extension of $\mathrm{eg}$ and $t$ and $h$.

the whiskering of h (from the name)

Let $h$ be a homomorphism of $c$ and $x_{1}$. Then the whiskering of $h$ is a functor of the set of left extensions of $f$ and $g$ and the set of left extensions of $f$ and the composition of $g$ and $h$.

left lift of f and g (from the name)

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Then a left lift of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of structured arrows of $g$ and the postcomposition of $c$ and $f$.

Let $g$ be a homomorphism of $c$ and $a$. Then $\operatorname{alongId}$ applied to $g$ is a left lift of the identity morphism of $a$ and $g$ defined as $\operatorname{mk}$ applied to $g$ and the inverse of the right unitor of $g$.

the homomorphism of x1 and w (from the name)

Let $x_{1}$ be a homomorphism of the lift of $s$ and the lift of $t$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the unit of $s$ and the right whisker of $x_{1}$ and $f$ is equal to the unit of $t$ and $\mathrm{CategoryTheory\_\_Bicategory\_\_LeftLift\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $x_{1}$ and $w$ is a homomorphism of $s$ and $t$ defined as the homomorphism of $x_{1}$ and $w$.

the lift of t (from the name)

Let $t$ be a left lift of $f$ and $g$. Then the lift of $t$ is a homomorphism of $c$ and $b$ defined as the right object of $t$.

the map isomorphism of ef and eg (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$ is an equivalence of the set of left lifts of $f$ and $g$ and the set of left lifts of $\mathrm{f'}$ and $\mathrm{g'}$ defined as the composition of the map natural isomorphism of the map isomorphism of $\operatorname{postcomposing}$ applied to $c$, $b$ and $a$ and $\mathrm{ef}$ and the map isomorphism of $\mathrm{eg}$.

Let $h$ be a homomorphism of $c$ and $b$. Let $\mathrm{unit}$ be a homomorphism of $g$ and the composition of $h$ and $f$. Then $\operatorname{mk}$ applied to $h$ and $\mathrm{unit}$ is a left lift of $f$ and $g$ defined as $\operatorname{mk}$ applied to $\mathrm{unit}$.

the left lift of t (from the name)

Let $t$ be a left lift of $f$ and the composition of the identity morphism of $c$ and $g$. Then the left lift of $t$ is a left lift of $f$ and $g$ defined as $\operatorname{mk}$ applied to the lift of $t$ and the composition of the inverse of the left unitor of $g$ and the unit of $t$.

the left lift of eg and t (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Let $t$ be a left lift of $f$ and $g$. Then the left lift of $\mathrm{eg}$ and $t$ is a left lift of $\mathrm{f'}$ and $\mathrm{g'}$ defined as the action of the functor of the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$ and $t$.

the unit of t (from the name)

Let $t$ be a left lift of $f$ and $g$. Then the unit of $t$ is a homomorphism of $g$ and the composition of the lift of $t$ and $f$ defined as the homomorphism of $t$.

the whisker of t and h (from the name)

Let $t$ be a left lift of $f$ and $g$. Let $h$ be a homomorphism of $x_{1}$ and $c$. Then the whisker of $t$ and $h$ is a left lift of $f$ and the composition of $h$ and $g$ defined as $\operatorname{mk}$ applied to the composition of $h$ and the lift of $t$ and the composition of the left whisker of $h$ and the unit of $t$ and the inverse of the associator of the lift of $t$ and $f$.

the whisker homomorphism of i and h (from the name)

Let $i$ be a homomorphism of $s$ and $t$. Let $h$ be a homomorphism of $x_{1}$ and $c$. Then the whisker homomorphism of $i$ and $h$ is a homomorphism of the whisker of $s$ and $h$ and the whisker of $t$ and $h$.

Let $s$ be a left lift of $f$ and the composition of the identity morphism of $c$ and $g$. Let $x_{1}$ be a homomorphism of $s$ and the whisker of $t$ and the identity morphism of $c$. Then $\operatorname{whiskerIdCancel}$ applied to $s$ and $x_{1}$ is a homomorphism of the left lift of $s$ and $t$.

the whisker isomorphism of i and h (from the name)

Let $i$ be an isomorphism of $s$ and $t$. Let $h$ be a homomorphism of $x_{1}$ and $c$. Then the whisker isomorphism of $i$ and $h$ is an isomorphism of the whisker of $s$ and $h$ and the whisker of $t$ and $h$.

the whisker of t (from the name)

Let $t$ be a left lift of $f$ and $g$. Then the whisker of $t$ is an isomorphism of the left lift of the whisker of $t$ and the identity morphism of $c$ and $t$.

the whisker of t and h (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Let $t$ be a left lift of $f$ and $g$. Let $h$ be a homomorphism of $x_{1}$ and $c$. Then the whisker of $t$ and $h$ is an isomorphism of the left lift of the left whiskering of $h$ and $\mathrm{eg}$ and the whisker of $t$ and $h$ and the whisker of the left lift of $\mathrm{eg}$ and $t$ and $h$.

the whiskering of h (from the name)

Let $h$ be a homomorphism of $x_{1}$ and $c$. Then the whiskering of $h$ is a functor of the set of left lifts of $f$ and $g$ and the set of left lifts of $f$ and the composition of $h$ and $g$.

right extension of f and g (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Then a right extension of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of costructured arrows of the precomposition of $c$ and $f$ and $g$.

Let $g$ be a homomorphism of $a$ and $c$. Then $\operatorname{alongId}$ applied to $g$ is a right extension of the identity morphism of $a$ and $g$ defined as $\operatorname{mk}$ applied to $g$ and the homomorphism of the left unitor of $g$.

the counit of t (from the name)

Let $t$ be a right extension of $f$ and $g$. Then the counit of $t$ is a homomorphism of the composition of $f$ and the extension of $t$ and $g$ defined as the homomorphism of $t$.

the extension of t (from the name)

Let $t$ be a right extension of $f$ and $g$. Then the extension of $t$ is a homomorphism of $b$ and $c$ defined as the left object of $t$.

the homomorphism of x1 and w (from the name)

Let $x_{1}$ be a homomorphism of the extension of $s$ and the extension of $t$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the left whisker of $f$ and $x_{1}$ and the counit of $t$ is equal to the counit of $s$ and $\mathrm{CategoryTheory\_\_Bicategory\_\_RightExtension\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $x_{1}$ and $w$ is a homomorphism of $s$ and $t$ defined as the homomorphism of $x_{1}$ and $w$.

the map isomorphism of ef and eg (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$ is an equivalence of the set of right extensions of $f$ and $g$ and the set of right extensions of $\mathrm{f'}$ and $\mathrm{g'}$ defined as the composition of the map natural isomorphism of the map isomorphism of $\operatorname{precomposing}$ applied to $a$, $b$ and $c$ and $\mathrm{ef}$ and the map isomorphism of $\mathrm{eg}$.

Let $h$ be a homomorphism of $b$ and $c$. Let $\mathrm{counit}$ be a homomorphism of the composition of $f$ and $h$ and $g$. Then $\operatorname{mk}$ applied to $h$ and $\mathrm{counit}$ is a right extension of $f$ and $g$ defined as $\operatorname{mk}$ applied to $\mathrm{counit}$.

the right extension of t (from the name)

Let $t$ be a right extension of $f$ and the composition of $g$ and the identity morphism of $c$. Then the right extension of $t$ is a right extension of $f$ and $g$ defined as $\operatorname{mk}$ applied to the extension of $t$ and the composition of the counit of $t$ and the homomorphism of the right unitor of $g$.

the right extension of eg and t (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Let $t$ be a right extension of $f$ and $g$. Then the right extension of $\mathrm{eg}$ and $t$ is a right extension of $\mathrm{f'}$ and $\mathrm{g'}$ defined as the action of the functor of the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$ and $t$.

the whisker of t and h (from the name)

Let $t$ be a right extension of $f$ and $g$. Let $h$ be a homomorphism of $c$ and $x_{1}$. Then the whisker of $t$ and $h$ is a right extension of $f$ and the composition of $g$ and $h$ defined as $\operatorname{mk}$ applied to the composition of the extension of $t$ and $h$ and the composition of the inverse of the associator of the extension of $t$ and $h$ and the right whisker of the counit of $t$ and $h$.

the whisker homomorphism of i and h (from the name)

Let $i$ be a homomorphism of $s$ and $t$. Let $h$ be a homomorphism of $c$ and $x_{1}$. Then the whisker homomorphism of $i$ and $h$ is a homomorphism of the whisker of $s$ and $h$ and the whisker of $t$ and $h$.

Let $t$ be a right extension of $f$ and the composition of $g$ and the identity morphism of $c$. Let $x_{1}$ be a homomorphism of the whisker of $s$ and the identity morphism of $c$ and $t$. Then $\operatorname{whiskerIdCancel}$ applied to $t$ and $x_{1}$ is a homomorphism of $s$ and the right extension of $t$.

the whisker isomorphism of i and h (from the name)

Let $i$ be an isomorphism of $s$ and $t$. Let $h$ be a homomorphism of $c$ and $x_{1}$. Then the whisker isomorphism of $i$ and $h$ is an isomorphism of the whisker of $s$ and $h$ and the whisker of $t$ and $h$.

the whisker of t (from the name)

Let $t$ be a right extension of $f$ and $g$. Then the whisker of $t$ is an isomorphism of the right extension of the whisker of $t$ and the identity morphism of $c$ and $t$.

the whisker of t and h (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Let $t$ be a right extension of $f$ and $g$. Let $h$ be a homomorphism of $c$ and $x_{1}$. Then the whisker of $t$ and $h$ is an isomorphism of the right extension of the right whiskering of $\mathrm{eg}$ and $h$ and the whisker of $t$ and $h$ and the whisker of the right extension of $\mathrm{eg}$ and $t$ and $h$.

the whiskering of h (from the name)

Let $h$ be a homomorphism of $c$ and $x_{1}$. Then the whiskering of $h$ is a functor of the set of right extensions of $f$ and $g$ and the set of right extensions of $f$ and the composition of $g$ and $h$.

right lift of f and g (from the name)

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Then a right lift of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of costructured arrows of the postcomposition of $c$ and $f$ and $g$.

Let $g$ be a homomorphism of $c$ and $a$. Then $\operatorname{alongId}$ applied to $g$ is a right lift of the identity morphism of $a$ and $g$ defined as $\operatorname{mk}$ applied to $g$ and the homomorphism of the right unitor of $g$.

the counit of t (from the name)

Let $t$ be a right lift of $f$ and $g$. Then the counit of $t$ is a homomorphism of the composition of the lift of $t$ and $f$ and $g$ defined as the homomorphism of $t$.

the homomorphism of x1 and w (from the name)

Let $x_{1}$ be a homomorphism of the lift of $s$ and the lift of $t$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the right whisker of $x_{1}$ and $f$ and the counit of $t$ is equal to the counit of $s$ and $\mathrm{CategoryTheory\_\_Bicategory\_\_RightLift\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $x_{1}$ and $w$ is a homomorphism of $s$ and $t$ defined as the homomorphism of $x_{1}$ and $w$.

the lift of t (from the name)

Let $t$ be a right lift of $f$ and $g$. Then the lift of $t$ is a homomorphism of $c$ and $b$ defined as the left object of $t$.

the map isomorphism of ef and eg (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$ is an equivalence of the set of right lifts of $f$ and $g$ and the set of right lifts of $\mathrm{f'}$ and $\mathrm{g'}$ defined as the composition of the map natural isomorphism of the map isomorphism of $\operatorname{postcomposing}$ applied to $c$, $b$ and $a$ and $\mathrm{ef}$ and the map isomorphism of $\mathrm{eg}$.

Let $h$ be a homomorphism of $c$ and $b$. Let $\mathrm{counit}$ be a homomorphism of the composition of $h$ and $f$ and $g$. Then $\operatorname{mk}$ applied to $h$ and $\mathrm{counit}$ is a right lift of $f$ and $g$ defined as $\operatorname{mk}$ applied to $\mathrm{counit}$.

the right lift of t (from the name)

Let $t$ be a right lift of $f$ and the composition of the identity morphism of $c$ and $g$. Then the right lift of $t$ is a right lift of $f$ and $g$ defined as $\operatorname{mk}$ applied to the lift of $t$ and the composition of the counit of $t$ and the homomorphism of the left unitor of $g$.

the right lift of eg and t (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Let $t$ be a right lift of $f$ and $g$. Then the right lift of $\mathrm{eg}$ and $t$ is a right lift of $\mathrm{f'}$ and $\mathrm{g'}$ defined as the action of the functor of the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$ and $t$.

the whisker of t and h (from the name)

Let $t$ be a right lift of $f$ and $g$. Let $h$ be a homomorphism of $x_{1}$ and $c$. Then the whisker of $t$ and $h$ is a right lift of $f$ and the composition of $h$ and $g$ defined as $\operatorname{mk}$ applied to the composition of $h$ and the lift of $t$ and the composition of the homomorphism of the associator of the lift of $t$ and $f$ and the left whisker of $h$ and the counit of $t$.

the whisker homomorphism of i and h (from the name)

Let $i$ be a homomorphism of $s$ and $t$. Let $h$ be a homomorphism of $x_{1}$ and $c$. Then the whisker homomorphism of $i$ and $h$ is a homomorphism of the whisker of $s$ and $h$ and the whisker of $t$ and $h$.

Let $t$ be a right lift of $f$ and the composition of the identity morphism of $c$ and $g$. Let $x_{1}$ be a homomorphism of the whisker of $s$ and the identity morphism of $c$ and $t$. Then $\operatorname{whiskerIdCancel}$ applied to $t$ and $x_{1}$ is a homomorphism of $s$ and the right lift of $t$.

the whisker isomorphism of i and h (from the name)

Let $i$ be an isomorphism of $s$ and $t$. Let $h$ be a homomorphism of $x_{1}$ and $c$. Then the whisker isomorphism of $i$ and $h$ is an isomorphism of the whisker of $s$ and $h$ and the whisker of $t$ and $h$.

the whisker of t (from the name)

Let $t$ be a right lift of $f$ and $g$. Then the whisker of $t$ is an isomorphism of the right lift of the whisker of $t$ and the identity morphism of $c$ and $t$.

the whisker of t and h (from the name)

Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Let $t$ be a right lift of $f$ and $g$. Let $h$ be a homomorphism of $x_{1}$ and $c$. Then the whisker of $t$ and $h$ is an isomorphism of the right lift of the left whiskering of $h$ and $\mathrm{eg}$ and the whisker of $t$ and $h$ and the whisker of the right lift of $\mathrm{eg}$ and $t$ and $h$.

the whiskering of h (from the name)

Let $h$ be a homomorphism of $x_{1}$ and $c$. Then the whiskering of $h$ is a functor of the set of right lifts of $f$ and $g$ and the set of right lifts of $f$ and the composition of $h$ and $g$.

free bicategory of B (from the name)

Let $B$ be a set. Then a free bicategory of $B$ is an element of the function that maps $B$ to $B$.

homomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $B$. Then the homomorphisms of $x_{1}$ and $x_{2}$ are a basic type.

the composition of f and g (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $c$. Then the composition of $f$ and $g$ is a homomorphism of $a$ and $c$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $a$ of $B$ and elements $b$ of $B$ and homomorphisms $f$ of $a$ and $b$ to elements of $\mathrm{motive}$ applied to $a$, $b$ and $\operatorname{of}$ applied to $f$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to the set of functions from elements $a_{1}$ of $B$ to elements of $\mathrm{motive}$ applied to $a_{1}$, $a_{1}$ and the identity of $a_{1}$ and $\mathrm{PULift}$ applied to the set of functions from elements $a_{2}$ of $B$ and elements $b_{1}$ of $B$ and elements $c$ of $B$ and homomorphisms $f_{1}$ of $a_{2}$ and $b_{1}$ and homomorphisms $g$ of $b_{1}$ and $c$ to elements of $\mathrm{motive}$ applied to $a_{2}$, $c$ and the composition of $f_{1}$ and $g$.

the identity of a (from the name)

Let $a$ be an element of $B$. Then the identity of $a$ is a homomorphism of $a$ and $a$.

Let $f$ be a homomorphism of $a$ and $b$. Then $\operatorname{of}$ applied to $f$ is a homomorphism of $a$ and $b$.

homomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be homomorphisms of $a$ and $b$. Then the homomorphisms of $x_{1}$ and $x_{2}$ are a basic type.

the associator of g and h (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $c$. Let $h$ be a homomorphism of $c$ and $d$. Then the associator of $g$ and $h$ is a homomorphism of the composition of the composition of $f$ and $g$ and $h$ and the composition of $f$ and the composition of $g$ and $h$.

the associator inverse of g and h (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $c$. Let $h$ be a homomorphism of $c$ and $d$. Then the associator inverse of $g$ and $h$ is a homomorphism of the composition of $f$ and the composition of $g$ and $h$ and the composition of the composition of $f$ and $g$ and $h$.

Let $\mathrm{ctorIdx}$ be a natural number. Then the elements of $\mathrm{CategoryTheory\_\_FreeBicategory\_\_Hom\_u2082\_\_\_ctorElimType}$ applied to $\mathrm{ctorIdx}$ are a basic type.

the identity of f (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Then the identity of $f$ is a homomorphism of $f$ and $f$.

the left unitor of f (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Then the left unitor of $f$ is a homomorphism of the composition of the identity morphism of $a$ and $f$ and $f$.

the left unitor inverse of f (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Then the left unitor inverse of $f$ is a homomorphism of $f$ and the composition of the identity morphism of $a$ and $f$.

Let $x_{1}$ be a homomorphism of $f$ and $g$. Then $\mathrm{CategoryTheory\_\_FreeBicategory\_\_Hom\_u2082\_\_\_mk}$ applied to $x_{1}$ is a homomorphism of $f$ and $g$ defined as $\operatorname{mk}$ applied to $\operatorname{Rel}$ and $x_{1}$.

the right unitor of f (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Then the right unitor of $f$ is a homomorphism of the composition of $f$ and the identity morphism of $b$ and $f$.

the right unitor inverse of f (from the name)

Let $f$ be a homomorphism of $a$ and $b$. Then the right unitor inverse of $f$ is a homomorphism of $f$ and the composition of $f$ and the identity morphism of $b$.

the vertical composition of x1 and x2 (from the name)

Let $x_{1}$ be a homomorphism of $f$ and $g$. Let $x_{2}$ be a homomorphism of $g$ and $h$. Then the vertical composition of $x_{1}$ and $x_{2}$ is a homomorphism of $f$ and $h$.

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

Let $f$ be a homomorphism of $a$ and $b$. Let $x_{1}$ be a homomorphism of $g$ and $h$. Then the left whisker of $f$ and $x_{1}$ is a homomorphism of the composition of $f$ and $g$ and the composition of $f$ and $h$.

the right whisker of h and x1 (from the name)

Let $h$ be a homomorphism of $b$ and $c$. Let $x_{1}$ be a homomorphism of $f$ and $g$. Then the right whisker of $h$ and $x_{1}$ is a homomorphism of the composition of $f$ and $h$ and the composition of $g$ and $h$.

Let $x_{1}$ and $x_{2}$ be homomorphisms of $f$ and $g$. Then we can say that $\operatorname{Rel}$ holds for $x_{1}$ and $x_{2}$.

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

the lift of F (from the name)

Let $F$ be a prefunctor of $B$ and $C$. Then the lift of $F$ is a pseudofunctor of the set of free bicategories of $B$ and $C$.

$\operatorname{of}$ is a prefunctor of $B$ and the set of free bicategories of $B$ defined as $\operatorname{mk}$ applied to $\mathrm{id}$ and the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{of}$.

object property of F (from the name)

Let $F$ be a pseudofunctor of $B$ and the set of categories. Then the object properties of $F$ are a basic type.

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

P is closed under map object (from the name)

Let $P$ be an object property of $F$. Then we can say that $P$ is closed under map object.

object of P and X (from the name)

Let $P$ be an object property of $F$. Let $X$ be an element of $B$. Then an object of $P$ and $X$ is an element of the function that maps $P$ and $X$ to the set of full subcategories of $\operatorname{prop}$ applied to $P$ and $X$.

Let $P$ be an object property of $F$. Then $\operatorname{fullsubcategory}$ applied to $P$ is a pseudofunctor of $B$ and the set of categories.

the map of P and f (from the name)

Let $P$ be an object property of $F$. Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $P$ and $f$ is a functor of the set of objects of $P$ and $X$ and the set of objects of $P$ and $Y$.

the map of P and x1 (from the name)

Let $P$ be an object property of $F$. Let $x_{1}$ be a homomorphism of $f$ and $g$. Then the map of $P$ and $x_{1}$ is a homomorphism of the map of $P$ and $f$ and the map of $P$ and $g$ defined as the preimage of the right whiskering of the inclusion of $\operatorname{prop}$ applied to $P$ and $Y$ and the set of objects of $P$ and $X$ and the left whisker of the inclusion of $\operatorname{prop}$ applied to $P$ and $X$ and the natural transformation of the map of $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $x_{1}$.

Let $\mathrm{self}$ be an object property of $F$. Let $X$ be an element of $B$. Then there is an object property of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $X$. Proof. Let $\mathrm{self}$ be arbitrary. Let $X$ be arbitrary. By self. By X. By CategoryTheory__Pseudofunctor__ObjectProperty__proj0.

the inclusion of P (from the docstring)

Let $P$ be an object property of $F$. Then the inclusion of $P$ is a strong composition of $\operatorname{fullsubcategory}$ applied to $P$ and $F$.

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

pseudo of F (from the name)

Let $F$ be an element of $\operatorname{LaxFunctor}$ applied to $B$ and $C$. Then the pseudos of $F$ are a basic type.

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

Let $\mathrm{self}$ be a pseudo of $F$. Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $c$. Then the map composition isomorphism of $f$ and $g$ is an isomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and the composition of $f$ and $g$ and the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $g$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $f$ and $g$.

the map identity isomorphism of self and a (from the name)

Let $\mathrm{self}$ be a pseudo of $F$. Let $a$ be an element of $B$. Then the map identity isomorphism of $\mathrm{self}$ and $a$ is an isomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and the identity morphism of $a$ and the identity morphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

the composition of F and G (from the name)

Let $F$ be an element of $\operatorname{LaxFunctor}$ applied to $B$ and $C$. Let $G$ be an element of $\operatorname{LaxFunctor}$ applied to $C$ and $D$. Then the composition of $F$ and $G$ is an element of $\operatorname{LaxFunctor}$ applied to $B$ and $D$.

the identity of B (from the name)

Let $B$ be a set. Then the identity of $B$ is an element of $\operatorname{LaxFunctor}$ applied to $B$ and $B$.

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

Let $\mathrm{self}$ be an element of $\operatorname{LaxFunctor}$ applied to $B$ and $C$. Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $c$. Then the map composition of $f$ and $g$ is a homomorphism of the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and $g$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and the composition of $f$ and $g$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $f$ and $g$.

the map composition of g and fg (from the name)

Let $F$ be an element of $\operatorname{LaxFunctor}$ applied to $B$ and $C$. Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $\mathrm{fg}$ be a homomorphism of $x_{2}$ and $x_{4}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $f$ and $g$ is equal to $\mathrm{fg}$ and $\mathrm{CategoryTheory\_\_LaxFunctor\_\_mapComp'\_\_\_auto\_1}$. Then the map composition of $g$ and $\mathrm{fg}$ is a homomorphism of the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $g$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\mathrm{fg}$.

the map identity of self and a (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{LaxFunctor}$ applied to $B$ and $C$. Let $a$ be an element of $B$. Then the map identity of $\mathrm{self}$ and $a$ is a homomorphism of the identity morphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and $a$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and the identity morphism of $a$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $a$.

the map identity of F and f (from the name)

Let $F$ be an element of $\operatorname{LaxFunctor}$ applied to $B$ and $C$. Let $f$ be a homomorphism of $b$ and $b$ such that $\mathrm{autoParam}$ holds for the proposition that $f$ is equal to the identity morphism of $b$ and $\mathrm{CategoryTheory\_\_LaxFunctor\_\_mapId'\_\_\_auto\_1}$. Then the map identity of $F$ and $f$ is a homomorphism of the identity morphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $b$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$.

the oplax functor of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the oplax functor of $F$ is an oplax functor of $\operatorname{LocallyDiscrete}$ applied to $C$ and $\operatorname{LocallyDiscrete}$ applied to $D$ defined as the oplax functor associated with a pseudofunctor of the pseudofunctor of $F$.

the oplax functor of F (from the name)

Let $F$ be a functor of $I$ and $B$. Then the oplax functor of $F$ is an oplax functor of $\operatorname{LocallyDiscrete}$ applied to $I$ and $B$ defined as the oplax functor associated with a pseudofunctor of the pseudofunctor of $F$.

the pseudofunctor of F (from the name)

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

the pseudofunctor of F (from the name)

Let $F$ be a functor of $I$ and $B$. Then the pseudofunctor of $F$ is a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to $I$ and $B$.

the pseudofunctor of b1 and mapId (from the name)

Let $\mathrm{obj}$ be a function from elements of $x$ to elements of $C$. Let $\mathrm{map}$ be a function from elements $b_{1}$ of $x$ and elements $\mathrm{b'}$ of $x$ and homomorphisms of $b_{1}$ and $\mathrm{b'}$ to homomorphisms of $\mathrm{obj}$ applied to $b_{1}$ and $\mathrm{obj}$ applied to $\mathrm{b'}$. Let $\mathrm{mapId}$ be a function from elements $b$ of $x$ to isomorphisms of $\mathrm{map}$ applied to $b$, $b$ and the identity morphism of $b$ and the identity morphism of $\mathrm{obj}$ applied to $b$. Let $\mathrm{mapComp}$ be a function from elements $x_{11}$ of $x$ and elements $x_{12}$ of $x$ and elements $x_{13}$ of $x$ and homomorphisms $f_{3}$ of $x_{11}$ and $x_{12}$ and homomorphisms $g_{1}$ of $x_{12}$ and $x_{13}$ to isomorphisms of $\mathrm{map}$ applied to $x_{11}$, $x_{13}$ and the composition of $f_{3}$ and $g_{1}$ and the composition of $\mathrm{map}$ applied to $x_{11}$, $x_{12}$ and $f_{3}$ and $\mathrm{map}$ applied to $x_{12}$, $x_{13}$ and $g_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{7}$ of $x$, for all elements $x_{8}$ of $x$, for all elements $x_{9}$ of $x$, for all elements $x_{10}$ of $x$, for all homomorphisms $f_{2}$ of $x_{7}$ and $x_{8}$, for all homomorphisms $g$ of $x_{8}$ and $x_{9}$, for all homomorphisms $h_{3}$ of $x_{9}$ and $x_{10}$, the composition of the homomorphism of $\mathrm{mapComp}$ applied to $x_{7}$, $x_{9}$, $x_{10}$, the composition of $f_{2}$ and $g$ and $h_{3}$ and the composition of the right whisker of the homomorphism of $\mathrm{mapComp}$ applied to $x_{7}$, $x_{8}$, $x_{9}$, $f_{2}$ and $g$ and $\mathrm{map}$ applied to $x_{9}$, $x_{10}$ and $h_{3}$ and the composition of the homomorphism of the associator of $\mathrm{map}$ applied to $x_{8}$, $x_{9}$ and $g$ and $\mathrm{map}$ applied to $x_{9}$, $x_{10}$ and $h_{3}$ and the composition of the left whisker of $\mathrm{map}$ applied to $x_{7}$, $x_{8}$ and $f_{2}$ and the inverse of $\mathrm{mapComp}$ applied to $x_{8}$, $x_{9}$, $x_{10}$, $g$ and $h_{3}$ and the inverse of $\mathrm{mapComp}$ applied to $x_{7}$, $x_{8}$, $x_{10}$, $f_{2}$ and the composition of $g$ and $h_{3}$ is equal to $\operatorname{eqToHom}$ applied to $\mathrm{CategoryTheory\_\_LocallyDiscrete\_\_mkPseudofunctor\_\_\_proof\_7}$ applied to $\mathrm{obj}$, $\mathrm{map}$, $f_{2}$, $g$ and $h_{3}$ and $\mathrm{CategoryTheory\_\_LocallyDiscrete\_\_mkPseudofunctor\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{5}$ of $x$, for all elements $x_{6}$ of $x$, for all homomorphisms $f_{1}$ of $x_{5}$ and $x_{6}$, the composition of the homomorphism of $\mathrm{mapComp}$ applied to $x_{5}$, $x_{5}$, $x_{6}$, the identity morphism of $x_{5}$ and $f_{1}$ and the composition of the right whisker of the homomorphism of $\mathrm{mapId}$ applied to $x_{5}$ and $\mathrm{map}$ applied to $x_{5}$, $x_{6}$ and $f_{1}$ and the homomorphism of the left unitor of $\mathrm{map}$ applied to $x_{5}$, $x_{6}$ and $f_{1}$ is equal to $\operatorname{eqToHom}$ applied to $\mathrm{CategoryTheory\_\_LocallyDiscrete\_\_mkPseudofunctor\_\_\_proof\_8}$ applied to $\mathrm{obj}$, $\mathrm{map}$ and $f_{1}$ and $\mathrm{CategoryTheory\_\_LocallyDiscrete\_\_mkPseudofunctor\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{3}$ of $x$, for all elements $x_{4}$ of $x$, for all homomorphisms $f$ of $x_{3}$ and $x_{4}$, the composition of the homomorphism of $\mathrm{mapComp}$ applied to $x_{3}$, $x_{4}$, $x_{4}$, $f$ and the identity morphism of $x_{4}$ and the composition of the left whisker of $\mathrm{map}$ applied to $x_{3}$, $x_{4}$ and $f$ and the homomorphism of $\mathrm{mapId}$ applied to $x_{4}$ and the homomorphism of the right unitor of $\mathrm{map}$ applied to $x_{3}$, $x_{4}$ and $f$ is equal to $\operatorname{eqToHom}$ applied to $\mathrm{CategoryTheory\_\_LocallyDiscrete\_\_mkPseudofunctor\_\_\_proof\_9}$ applied to $\mathrm{obj}$, $\mathrm{map}$ and $f$ and $\mathrm{CategoryTheory\_\_LocallyDiscrete\_\_mkPseudofunctor\_\_\_auto\_5}$. Then the pseudofunctor of $\mathrm{b'}$ and $\mathrm{map}$ is a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to $x$ and $C$.

the oplax functor of b1 and mapId (from the name)

Let $\mathrm{obj}$ be a function from elements of $B$ to elements of $C$. Let $\mathrm{map}$ be a function from elements $b_{1}$ of $B$ and elements $\mathrm{b'}$ of $B$ and homomorphisms of $b_{1}$ and $\mathrm{b'}$ to homomorphisms of $\mathrm{obj}$ applied to $b_{1}$ and $\mathrm{obj}$ applied to $\mathrm{b'}$. Let $\mathrm{mapId}$ be a function from elements $b$ of $B$ to homomorphisms of $\mathrm{map}$ applied to $b$, $b$ and the identity morphism of $b$ and the identity morphism of $\mathrm{obj}$ applied to $b$. Let $\mathrm{mapComp}$ be a function from elements $x_{10}$ of $B$ and elements $x_{11}$ of $B$ and elements $x_{12}$ of $B$ and homomorphisms $f_{3}$ of $x_{10}$ and $x_{11}$ and homomorphisms $g_{1}$ of $x_{11}$ and $x_{12}$ to homomorphisms of $\mathrm{map}$ applied to $x_{10}$, $x_{12}$ and the composition of $f_{3}$ and $g_{1}$ and the composition of $\mathrm{map}$ applied to $x_{10}$, $x_{11}$ and $f_{3}$ and $\mathrm{map}$ applied to $x_{11}$, $x_{12}$ and $g_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{6}$ of $B$, for all elements $x_{7}$ of $B$, for all elements $x_{8}$ of $B$, for all elements $x_{9}$ of $B$, for all homomorphisms $f_{2}$ of $x_{6}$ and $x_{7}$, for all homomorphisms $g$ of $x_{7}$ and $x_{8}$, for all homomorphisms $h_{4}$ of $x_{8}$ and $x_{9}$, the composition of $\operatorname{eqToHom}$ applied to $\mathrm{CategoryTheory\_\_pseudofunctorOfIsLocallyDiscrete\_\_\_proof\_7}$ applied to $\mathrm{obj}$, $\mathrm{map}$, $f_{2}$, $g$ and $h_{4}$ and the composition of $\mathrm{mapComp}$ applied to $x_{6}$, $x_{7}$, $x_{9}$, $f_{2}$ and the composition of $g$ and $h_{4}$ and the left whisker of $\mathrm{map}$ applied to $x_{6}$, $x_{7}$ and $f_{2}$ and $\mathrm{mapComp}$ applied to $x_{7}$, $x_{8}$, $x_{9}$, $g$ and $h_{4}$ is equal to the composition of $\mathrm{mapComp}$ applied to $x_{6}$, $x_{8}$, $x_{9}$, the composition of $f_{2}$ and $g$ and $h_{4}$ and the composition of the right whisker of $\mathrm{mapComp}$ applied to $x_{6}$, $x_{7}$, $x_{8}$, $f_{2}$ and $g$ and $\mathrm{map}$ applied to $x_{8}$, $x_{9}$ and $h_{4}$ and the homomorphism of the associator of $\mathrm{map}$ applied to $x_{7}$, $x_{8}$ and $g$ and $\mathrm{map}$ applied to $x_{8}$, $x_{9}$ and $h_{4}$ and $\mathrm{CategoryTheory\_\_oplaxFunctorOfIsLocallyDiscrete\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{4}$ of $B$, for all elements $x_{5}$ of $B$, for all homomorphisms $f_{1}$ of $x_{4}$ and $x_{5}$, the composition of $\mathrm{mapComp}$ applied to $x_{4}$, $x_{4}$, $x_{5}$, the identity morphism of $x_{4}$ and $f_{1}$ and the composition of the right whisker of $\mathrm{mapId}$ applied to $x_{4}$ and $\mathrm{map}$ applied to $x_{4}$, $x_{5}$ and $f_{1}$ and the homomorphism of the left unitor of $\mathrm{map}$ applied to $x_{4}$, $x_{5}$ and $f_{1}$ is equal to $\operatorname{eqToHom}$ applied to $\mathrm{CategoryTheory\_\_pseudofunctorOfIsLocallyDiscrete\_\_\_proof\_8}$ applied to $\mathrm{obj}$, $\mathrm{map}$ and $f_{1}$ and $\mathrm{CategoryTheory\_\_oplaxFunctorOfIsLocallyDiscrete\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{2}$ of $B$, for all elements $x_{3}$ of $B$, for all homomorphisms $f$ of $x_{2}$ and $x_{3}$, the composition of $\mathrm{mapComp}$ applied to $x_{2}$, $x_{3}$, $x_{3}$, $f$ and the identity morphism of $x_{3}$ and the composition of the left whisker of $\mathrm{map}$ applied to $x_{2}$, $x_{3}$ and $f$ and $\mathrm{mapId}$ applied to $x_{3}$ and the homomorphism of the right unitor of $\mathrm{map}$ applied to $x_{2}$, $x_{3}$ and $f$ is equal to $\operatorname{eqToHom}$ applied to $\mathrm{CategoryTheory\_\_pseudofunctorOfIsLocallyDiscrete\_\_\_proof\_9}$ applied to $\mathrm{obj}$, $\mathrm{map}$ and $f$ and $\mathrm{CategoryTheory\_\_oplaxFunctorOfIsLocallyDiscrete\_\_\_auto\_5}$. Then the oplax functor of $\mathrm{b'}$ and $\mathrm{map}$ is an oplax functor of $B$ and $C$.

the pseudofunctor of b1 and mapId (from the name)

Let $\mathrm{obj}$ be a function from elements of $B$ to elements of $C$. Let $\mathrm{map}$ be a function from elements $b_{1}$ of $B$ and elements $\mathrm{b'}$ of $B$ and homomorphisms of $b_{1}$ and $\mathrm{b'}$ to homomorphisms of $\mathrm{obj}$ applied to $b_{1}$ and $\mathrm{obj}$ applied to $\mathrm{b'}$. Let $\mathrm{mapId}$ be a function from elements $b$ of $B$ to isomorphisms of $\mathrm{map}$ applied to $b$, $b$ and the identity morphism of $b$ and the identity morphism of $\mathrm{obj}$ applied to $b$. Let $\mathrm{mapComp}$ be a function from elements $x_{10}$ of $B$ and elements $x_{11}$ of $B$ and elements $x_{12}$ of $B$ and homomorphisms $f_{3}$ of $x_{10}$ and $x_{11}$ and homomorphisms $g_{1}$ of $x_{11}$ and $x_{12}$ to isomorphisms of $\mathrm{map}$ applied to $x_{10}$, $x_{12}$ and the composition of $f_{3}$ and $g_{1}$ and the composition of $\mathrm{map}$ applied to $x_{10}$, $x_{11}$ and $f_{3}$ and $\mathrm{map}$ applied to $x_{11}$, $x_{12}$ and $g_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{6}$ of $B$, for all elements $x_{7}$ of $B$, for all elements $x_{8}$ of $B$, for all elements $x_{9}$ of $B$, for all homomorphisms $f_{2}$ of $x_{6}$ and $x_{7}$, for all homomorphisms $g$ of $x_{7}$ and $x_{8}$, for all homomorphisms $h_{4}$ of $x_{8}$ and $x_{9}$, the composition of the homomorphism of $\mathrm{mapComp}$ applied to $x_{6}$, $x_{8}$, $x_{9}$, the composition of $f_{2}$ and $g$ and $h_{4}$ and the composition of the right whisker of the homomorphism of $\mathrm{mapComp}$ applied to $x_{6}$, $x_{7}$, $x_{8}$, $f_{2}$ and $g$ and $\mathrm{map}$ applied to $x_{8}$, $x_{9}$ and $h_{4}$ and the composition of the homomorphism of the associator of $\mathrm{map}$ applied to $x_{7}$, $x_{8}$ and $g$ and $\mathrm{map}$ applied to $x_{8}$, $x_{9}$ and $h_{4}$ and the composition of the left whisker of $\mathrm{map}$ applied to $x_{6}$, $x_{7}$ and $f_{2}$ and the inverse of $\mathrm{mapComp}$ applied to $x_{7}$, $x_{8}$, $x_{9}$, $g$ and $h_{4}$ and the inverse of $\mathrm{mapComp}$ applied to $x_{6}$, $x_{7}$, $x_{9}$, $f_{2}$ and the composition of $g$ and $h_{4}$ is equal to $\operatorname{eqToHom}$ applied to $\mathrm{CategoryTheory\_\_pseudofunctorOfIsLocallyDiscrete\_\_\_proof\_7}$ applied to $\mathrm{obj}$, $\mathrm{map}$, $f_{2}$, $g$ and $h_{4}$ and $\mathrm{CategoryTheory\_\_pseudofunctorOfIsLocallyDiscrete\_\_\_auto\_1}$, $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{4}$ of $B$, for all elements $x_{5}$ of $B$, for all homomorphisms $f_{1}$ of $x_{4}$ and $x_{5}$, the composition of the homomorphism of $\mathrm{mapComp}$ applied to $x_{4}$, $x_{4}$, $x_{5}$, the identity morphism of $x_{4}$ and $f_{1}$ and the composition of the right whisker of the homomorphism of $\mathrm{mapId}$ applied to $x_{4}$ and $\mathrm{map}$ applied to $x_{4}$, $x_{5}$ and $f_{1}$ and the homomorphism of the left unitor of $\mathrm{map}$ applied to $x_{4}$, $x_{5}$ and $f_{1}$ is equal to $\operatorname{eqToHom}$ applied to $\mathrm{CategoryTheory\_\_pseudofunctorOfIsLocallyDiscrete\_\_\_proof\_8}$ applied to $\mathrm{obj}$, $\mathrm{map}$ and $f_{1}$ and $\mathrm{CategoryTheory\_\_pseudofunctorOfIsLocallyDiscrete\_\_\_auto\_3}$ and $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{2}$ of $B$, for all elements $x_{3}$ of $B$, for all homomorphisms $f$ of $x_{2}$ and $x_{3}$, the composition of the homomorphism of $\mathrm{mapComp}$ applied to $x_{2}$, $x_{3}$, $x_{3}$, $f$ and the identity morphism of $x_{3}$ and the composition of the left whisker of $\mathrm{map}$ applied to $x_{2}$, $x_{3}$ and $f$ and the homomorphism of $\mathrm{mapId}$ applied to $x_{3}$ and the homomorphism of the right unitor of $\mathrm{map}$ applied to $x_{2}$, $x_{3}$ and $f$ is equal to $\operatorname{eqToHom}$ applied to $\mathrm{CategoryTheory\_\_pseudofunctorOfIsLocallyDiscrete\_\_\_proof\_9}$ applied to $\mathrm{obj}$, $\mathrm{map}$ and $f$ and $\mathrm{CategoryTheory\_\_pseudofunctorOfIsLocallyDiscrete\_\_\_auto\_5}$. Then the pseudofunctor of $\mathrm{b'}$ and $\mathrm{map}$ is a pseudofunctor of $B$ and $C$.

oplax functor of B and C (from the name)

Let $B$ and $C$ be sets. Then the oplax functors of $B$ and $C$ are a basic type.

pseudo of F (from the name)

Let $F$ be an oplax functor of $B$ and $C$. Then the pseudos of $F$ are a basic type.

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

Let $\mathrm{self}$ be a pseudo of $F$. Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $c$. Then the map composition isomorphism of $f$ and $g$ is an isomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and the composition of $f$ and $g$ and the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $g$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $f$ and $g$.

the map identity isomorphism of self and a (from the name)

Let $\mathrm{self}$ be a pseudo of $F$. Let $a$ be an element of $B$. Then the map identity isomorphism of $\mathrm{self}$ and $a$ is an isomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and the identity morphism of $a$ and the identity morphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

the composition of F and G (from the name)

Let $F$ be an oplax functor of $B$ and $C$. Let $G$ be an oplax functor of $C$ and $D$. Then the composition of $F$ and $G$ is an oplax functor of $B$ and $D$.

the identity oplax functor of B (from the docstring)

Let $B$ be a set. Then the identity oplax functor of $B$ is an oplax functor of $B$ and $B$.

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

Let $\mathrm{self}$ be an oplax functor of $B$ and $C$. Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $c$. Then the map composition of $f$ and $g$ is a homomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and the composition of $f$ and $g$ and the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and $g$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $f$ and $g$.

the map composition of g and fg (from the name)

Let $F$ be an oplax functor of $B$ and $C$. Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $\mathrm{fg}$ be a homomorphism of $x_{2}$ and $x_{4}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $f$ and $g$ is equal to $\mathrm{fg}$ and $\mathrm{CategoryTheory\_\_OplaxFunctor\_\_mapComp'\_\_\_auto\_1}$. Then the map composition of $g$ and $\mathrm{fg}$ is a homomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\mathrm{fg}$ and the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $g$.

the map identity of self and a (from the name)

Let $\mathrm{self}$ be an oplax functor of $B$ and $C$. Let $a$ be an element of $B$. Then the map identity of $\mathrm{self}$ and $a$ is a homomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and the identity morphism of $a$ and the identity morphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and $a$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $a$.

the map identity of F and f (from the name)

Let $F$ be an oplax functor of $B$ and $C$. Let $f$ be a homomorphism of $b$ and $b$ such that $\mathrm{autoParam}$ holds for the proposition that $f$ is equal to the identity morphism of $b$ and $\mathrm{CategoryTheory\_\_OplaxFunctor\_\_mapId'\_\_\_auto\_1}$. Then the map identity of $F$ and $f$ is a homomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the identity morphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $b$.

prelax functor of B and C (from the name)

Let $B$ and $C$ be sets. Then the prelax functors of $B$ and $C$ are a basic type.

the composition of F and G (from the name)

Let $F$ be a prelax functor of $B$ and $C$. Let $G$ be a prelax functor of $C$ and $D$. Then the composition of $F$ and $G$ is a prelax functor of $B$ and $D$.

the identity prelax functor of B (from the docstring)

Let $B$ be a set. Then the identity prelax functor of $B$ is a prelax functor of $B$ and $B$.

the map functor of a and b (from the name)

Let $F$ be a prelax functor of $B$ and $C$. Let $a$ and $b$ be elements of $B$. Then the map functor of $a$ and $b$ is a functor of the set of homomorphisms of $a$ and $b$ and the set of homomorphisms of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $F$ and $a$ and the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $F$ and $b$.

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

Let $F$ be a prelax functor of $B$ and $C$. Let $x_{2}$ be an isomorphism of $f$ and $g$. Then the map isomorphism of $F$ and $x_{2}$ is an isomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $F$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $F$ and $g$ defined as the map isomorphism of the map functor of $a$ and $b$ and $x_{2}$.

Let $F$ be a function from elements of $B$ to elements of $C$. Let $\mathrm{F'}$ be a function from elements $a$ of $B$ and elements $b$ of $B$ to functors of the set of homomorphisms of $a$ and $b$ and the set of homomorphisms of $F$ applied to $a$ and $F$ applied to $b$. Then $\operatorname{mkOfHomFunctors}$ applied to $F$, $a$, $b$ and $\mathrm{F'}$ is a prelax functor of $B$ and $C$.

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

the composition of F and G (from the name)

Let $F$ be an element of $\operatorname{PrelaxFunctorStruct}$ applied to $B$ and $C$. Let $G$ be an element of $\operatorname{PrelaxFunctorStruct}$ applied to $C$ and $D$. Then the composition of $F$ and $G$ is an element of $\operatorname{PrelaxFunctorStruct}$ applied to $B$ and $D$ defined as $\operatorname{mk}$ applied to the composition of $\operatorname{toPrefunctor}$ applied to $F$ and $\operatorname{toPrefunctor}$ applied to $G$ and the function that maps $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$ and $x_{10}$ to the map of $G$ and the map of $F$ and $x_{10}$.

the identity of B (from the name)

Let $B$ be a set. Then the identity of $B$ is an element of $\operatorname{PrelaxFunctorStruct}$ applied to $B$ and $B$ defined as $\operatorname{mk}$ applied to the identity of $B$ and the function that maps $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$ and $x_{6}$ to $x_{6}$.

the map of self and x4 (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{PrelaxFunctorStruct}$ applied to $B$ and $C$. Let $x_{4}$ be a homomorphism of $f$ and $g$. Then the map of $\mathrm{self}$ and $x_{4}$ is a homomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\mathrm{self}$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\mathrm{self}$ and $g$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{4}$.

Let $F$ be a function from elements of $B$ to elements of $C$. Let $\mathrm{F'}$ be a function from elements $a$ of $B$ and elements $b$ of $B$ to prefunctors of the set of homomorphisms of $a$ and $b$ and the set of homomorphisms of $F$ applied to $a$ and $F$ applied to $b$. Then $\operatorname{mkOfHomPrefunctors}$ applied to $F$, $a$, $b$ and $\mathrm{F'}$ is an element of $\operatorname{PrelaxFunctorStruct}$ applied to $B$ and $C$ defined as the function that maps $b$ and $\mathrm{F'}$ to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $F$ and the function that maps $a$ and $b$ to $\operatorname{obj}$ applied to $a$ applied to $a$ and $b$, the function that maps $a_{1}$, $b_{1}$, $x_{4}$ and $x_{5}$ to $\operatorname{map}$ applied to $a$ applied to $a_{1}$ and $b_{1}$, $b$ and $\mathrm{F'}$.

pseudofunctor of B and C (from the name)

Let $B$ and $C$ be sets. Then the pseudofunctors of $B$ and $C$ are a basic type.

the composition of F and G (from the name)

Let $F$ be a pseudofunctor of $B$ and $C$. Let $G$ be a pseudofunctor of $C$ and $D$. Then the composition of $F$ and $G$ is a pseudofunctor of $B$ and $D$.

the identity pseudofunctor of B (from the docstring)

Let $B$ be a set. Then the identity pseudofunctor of $B$ is a pseudofunctor of $B$ and $B$.

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

Let $\mathrm{self}$ be a pseudofunctor of $B$ and $C$. Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $c$. Then the map composition of $f$ and $g$ is an isomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and the composition of $f$ and $g$ and the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and $g$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $f$ and $g$.

the map composition of g and fg (from the name)

Let $F$ be a pseudofunctor of $B$ and $C$. Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $\mathrm{fg}$ be a homomorphism of $x_{2}$ and $x_{4}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $f$ and $g$ is equal to $\mathrm{fg}$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_mapComp'\_\_\_auto\_1}$. Then the map composition of $g$ and $\mathrm{fg}$ is an isomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\mathrm{fg}$ and the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $g$.

the map identity of self and a (from the name)

Let $\mathrm{self}$ be a pseudofunctor of $B$ and $C$. Let $a$ be an element of $B$. Then the map identity of $\mathrm{self}$ and $a$ is an isomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and the identity morphism of $a$ and the identity morphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\mathrm{self}$ and $a$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $a$.

the map identity of F and f (from the name)

Let $F$ be a pseudofunctor of $B$ and $C$. Let $f$ be a homomorphism of $b$ and $b$ such that $\mathrm{autoParam}$ holds for the proposition that $f$ is equal to the identity morphism of $b$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_mapId'\_\_\_auto\_1}$. Then the map identity of $F$ and $f$ is an isomorphism of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the identity morphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $b$.

Let $F$ be an element of $\operatorname{LaxFunctor}$ applied to $B$ and $C$. Let $\mathrm{F'}$ be a pseudo of $F$. Then $\operatorname{mkOfLax}$ applied to $F$ and $\mathrm{F'}$ is a pseudofunctor of $B$ and $C$.

Let $F$ be an element of $\operatorname{LaxFunctor}$ applied to $B$ and $C$. Then $\operatorname{mkOfLax'}$ applied to $F$ is a pseudofunctor of $B$ and $C$.

Let $F$ be an oplax functor of $B$ and $C$. Let $\mathrm{F'}$ be a pseudo of $F$. Then $\operatorname{mkOfOplax}$ applied to $F$ and $\mathrm{F'}$ is a pseudofunctor of $B$ and $C$.

Let $F$ be an oplax functor of $B$ and $C$. Then $\operatorname{mkOfOplax'}$ applied to $F$ is a pseudofunctor of $B$ and $C$.

Let $F$ be a pseudofunctor of $B$ and $C$. Then $\operatorname{toLax}$ applied to $F$ is an element of $\operatorname{LaxFunctor}$ applied to $B$ and $C$.

the oplax functor associated with a pseudofunctor of F (from the docstring)

Let $F$ be a pseudofunctor of $B$ and $C$. Then the oplax functor associated with a pseudofunctor of $F$ is an oplax functor of $B$ and $C$.

strict pseudofunctor of B and C (from the name)

Let $B$ and $C$ be sets. Then the strict pseudofunctors of $B$ and $C$ are a basic type.

the composition of F and G (from the name)

Let $F$ be a strict pseudofunctor of $B$ and $C$. Let $G$ be a strict pseudofunctor of $C$ and $D$. Then the composition of $F$ and $G$ is a strict pseudofunctor of $B$ and $D$.

the identity of B (from the docstring)

Let $B$ be a set. Then the identity of $B$ is a strict pseudofunctor of $B$ and $B$.

Let $S$ be a strict pseudofunctor of $B$ and $C$. Then $\operatorname{mk'}$ applied to $S$ is a strict pseudofunctor of $B$ and $C$.

Let $S$ be a strict pseudofunctor of $B$ and $C$. Then $\operatorname{mk''}$ applied to $S$ is a strict pseudofunctor of $B$ and $C$.

the functor of F (from the name)

Let $F$ be a strict pseudofunctor of $B$ and $C$. Then the functor of $F$ is a functor of $B$ and $C$.

strict pseudofunctor of B and C (from the name)

Let $B$ and $C$ be sets. Then the strict pseudofunctors of $B$ and $C$ are a basic type.

strict pseudofunctor of B and C (from the name)

Let $B$ and $C$ be sets. Then the strict pseudofunctors of $B$ and $C$ are a basic type.

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

the composition of F and G (from the name)

Let $F$ be an element of $\operatorname{StrictlyUnitaryLaxFunctor}$ applied to $B$ and $C$. Let $G$ be an element of $\operatorname{StrictlyUnitaryLaxFunctor}$ applied to $C$ and $D$. Then the composition of $F$ and $G$ is an element of $\operatorname{StrictlyUnitaryLaxFunctor}$ applied to $B$ and $D$.

the identity of B (from the docstring)

Let $B$ be a set. Then the identity of $B$ is an element of $\operatorname{StrictlyUnitaryLaxFunctor}$ applied to $B$ and $B$.

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

Let $F$ be an element of $\operatorname{StrictlyUnitaryLaxFunctor}$ applied to $B$ and $C$. Let $x_{2}$ be an element of $B$. Then the map identity isomorphism of $F$ and $x_{2}$ is an isomorphism of the identity morphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\operatorname{toLaxFunctor}$ applied to $F$ and $x_{2}$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $\operatorname{toLaxFunctor}$ applied to $F$ and the identity morphism of $x_{2}$.

Let $S$ be an element of $\operatorname{StrictlyUnitaryLaxFunctorCore}$ applied to $B$ and $C$. Then $\operatorname{mk'}$ applied to $S$ is an element of $\operatorname{StrictlyUnitaryLaxFunctor}$ applied to $B$ and $C$.

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

the map of self and x2 (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{StrictlyUnitaryLaxFunctorCore}$ applied to $B$ and $C$. Let $x_{2}$ be a homomorphism of $X$ and $Y$. Then the map of $\mathrm{self}$ and $x_{2}$ is a homomorphism of the object of $\mathrm{self}$ and $X$ and the object of $\mathrm{self}$ and $Y$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.

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

Let $\mathrm{self}$ be an element of $\operatorname{StrictlyUnitaryLaxFunctorCore}$ applied to $B$ and $C$. Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $b$ and $c$. Then the map composition of $f$ and $g$ is a homomorphism of the composition of the map of $\mathrm{self}$ and $f$ and the map of $\mathrm{self}$ and $g$ and the map of $\mathrm{self}$ and the composition of $f$ and $g$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$, $f$ and $g$.

the map of self and x2 (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{StrictlyUnitaryLaxFunctorCore}$ applied to $B$ and $C$. Let $x_{2}$ be a homomorphism of $f$ and $g$. Then the map of $\mathrm{self}$ and $x_{2}$ is a homomorphism of the map of $\mathrm{self}$ and $f$ and the map of $\mathrm{self}$ and $g$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $x_{2}$.

the object of self and x2 (from the name)

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

strictly unitary pseudofunctor of B and C (from the name)

the composition of F and G (from the name)

the identity of B (from the docstring)

strictly unitary pseudofunctor of B and C (from the name)

the map of self and x2 (from the name)

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

the map of self and x2 (from the name)

the object of self and x2 (from the name)

the associator of x3 and x4 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a homomorphism of $G$ and $H$. Let $x_{4}$ be a homomorphism of $H$ and $I$. Then the associator of $x_{3}$ and $x_{4}$ is an isomorphism of the composition of the composition of $x_{2}$ and $x_{3}$ and $x_{4}$ and the composition of $x_{2}$ and the composition of $x_{3}$ and $x_{4}$.

the left unitor of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the left unitor of $x_{2}$ is an isomorphism of the composition of the identity morphism of $F$ and $x_{2}$ and $x_{2}$.

the right unitor of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the right unitor of $x_{2}$ is an isomorphism of the composition of $x_{2}$ and the identity morphism of $G$ and $x_{2}$.

the left whisker of x2 and x5 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the left whisker of $x_{2}$ and $x_{5}$ is a homomorphism of the composition of $x_{2}$ and $x_{3}$ and the composition of $x_{2}$ and $x_{4}$.

the right whisker of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{5}$ be a homomorphism of $G$ and $H$. Then the right whisker of $x_{4}$ and $x_{5}$ is a homomorphism of the composition of $x_{2}$ and $x_{5}$ and the composition of $x_{3}$ and $x_{5}$.

the associator of x3 and x4 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a homomorphism of $G$ and $H$. Let $x_{4}$ be a homomorphism of $H$ and $I$. Then the associator of $x_{3}$ and $x_{4}$ is an isomorphism of the composition of the composition of $x_{2}$ and $x_{3}$ and $x_{4}$ and the composition of $x_{2}$ and the composition of $x_{3}$ and $x_{4}$.

the left unitor of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the left unitor of $x_{2}$ is an isomorphism of the composition of the identity morphism of $F$ and $x_{2}$ and $x_{2}$.

the right unitor of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the right unitor of $x_{2}$ is an isomorphism of the composition of $x_{2}$ and the identity morphism of $G$ and $x_{2}$.

the left whisker of x2 and x5 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the left whisker of $x_{2}$ and $x_{5}$ is a homomorphism of the composition of $x_{2}$ and $x_{3}$ and the composition of $x_{2}$ and $x_{4}$.

the right whisker of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{5}$ be a homomorphism of $G$ and $H$. Then the right whisker of $x_{4}$ and $x_{5}$ is a homomorphism of the composition of $x_{2}$ and $x_{5}$ and the composition of $x_{3}$ and $x_{5}$.

the associator of x3 and x4 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a homomorphism of $G$ and $H$. Let $x_{4}$ be a homomorphism of $H$ and $I$. Then the associator of $x_{3}$ and $x_{4}$ is an isomorphism of the composition of the composition of $x_{2}$ and $x_{3}$ and $x_{4}$ and the composition of $x_{2}$ and the composition of $x_{3}$ and $x_{4}$.

the left unitor of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the left unitor of $x_{2}$ is an isomorphism of the composition of the identity morphism of $F$ and $x_{2}$ and $x_{2}$.

the right unitor of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the right unitor of $x_{2}$ is an isomorphism of the composition of $x_{2}$ and the identity morphism of $G$ and $x_{2}$.

the left whisker of x2 and x5 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the left whisker of $x_{2}$ and $x_{5}$ is a homomorphism of the composition of $x_{2}$ and $x_{3}$ and the composition of $x_{2}$ and $x_{4}$.

the right whisker of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{5}$ be a homomorphism of $G$ and $H$. Then the right whisker of $x_{4}$ and $x_{5}$ is a homomorphism of the composition of $x_{2}$ and $x_{5}$ and the composition of $x_{3}$ and $x_{5}$.

the associator of x3 and x4 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a homomorphism of $G$ and $H$. Let $x_{4}$ be a homomorphism of $H$ and $I$. Then the associator of $x_{3}$ and $x_{4}$ is an isomorphism of the composition of the composition of $x_{2}$ and $x_{3}$ and $x_{4}$ and the composition of $x_{2}$ and the composition of $x_{3}$ and $x_{4}$.

the left unitor of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the left unitor of $x_{2}$ is an isomorphism of the composition of the identity morphism of $F$ and $x_{2}$ and $x_{2}$.

the right unitor of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the right unitor of $x_{2}$ is an isomorphism of the composition of $x_{2}$ and the identity morphism of $G$ and $x_{2}$.

the left whisker of x2 and x5 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the left whisker of $x_{2}$ and $x_{5}$ is a homomorphism of the composition of $x_{2}$ and $x_{3}$ and the composition of $x_{2}$ and $x_{4}$.

the right whisker of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{5}$ be a homomorphism of $G$ and $H$. Then the right whisker of $x_{4}$ and $x_{5}$ is a homomorphism of the composition of $x_{2}$ and $x_{5}$ and the composition of $x_{3}$ and $x_{5}$.

the associator of x3 and x4 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a homomorphism of $G$ and $H$. Let $x_{4}$ be a homomorphism of $H$ and $I$. Then the associator of $x_{3}$ and $x_{4}$ is an isomorphism of the composition of the composition of $x_{2}$ and $x_{3}$ and $x_{4}$ and the composition of $x_{2}$ and the composition of $x_{3}$ and $x_{4}$.

the left unitor of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the left unitor of $x_{2}$ is an isomorphism of the composition of the identity morphism of $F$ and $x_{2}$ and $x_{2}$.

the right unitor of x2 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the right unitor of $x_{2}$ is an isomorphism of the composition of $x_{2}$ and the identity morphism of $G$ and $x_{2}$.

the left whisker of x2 and x5 (from the name)

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{5}$ be a homomorphism of $x_{3}$ and $x_{4}$. Then the left whisker of $x_{2}$ and $x_{5}$ is a homomorphism of the composition of $x_{2}$ and $x_{3}$ and the composition of $x_{2}$ and $x_{4}$.

the right whisker of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $x_{2}$ and $x_{3}$. Let $x_{5}$ be a homomorphism of $G$ and $H$. Then the right whisker of $x_{4}$ and $x_{5}$ is a homomorphism of the composition of $x_{2}$ and $x_{5}$ and the composition of $x_{3}$ and $x_{5}$.

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $x$ and the set of categories. Then the elements of $\operatorname{CoGrothendieck}$ applied to $F$ are a basic type.

homomorphism of X and Y (from the name)

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

the base of self (from the name)

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

the morphism in the fiber over the domain of self (from the docstring)

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

the underlying object in the base category of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{CoGrothendieck}$ applied to $F$. Then the underlying object in the base category of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

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

Let $\mathrm{self}$ be an element of $\operatorname{CoGrothendieck}$ applied to $F$. Then the object in the fiber of the base object of $\mathrm{self}$ is an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to the underlying object in the base category of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $x$ and the set of categories. Then $\operatorname{forget}$ applied to $F$ is a functor of $\operatorname{CoGrothendieck}$ applied to $F$ and $x$.

the map of x2 (from the name)

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

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

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a homomorphism of $G$ and $H$. Then the map composition isomorphism of $x_{2}$ and $x_{3}$ is an isomorphism of the map of the composition of $x_{2}$ and $x_{3}$ and the composition of the map of $x_{2}$ and the map of $x_{3}$.

the map identity isomorphism of F (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $x$ and the set of categories. Then the map identity isomorphism of $F$ is an isomorphism of the map of the identity morphism of $F$ and the identity of $\operatorname{CoGrothendieck}$ applied to $F$.

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

homomorphism of X and Y (from the name)

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

the base of self (from the name)

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

the morphism in the fiber over the domain of self (from the docstring)

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

the underlying object in the base category of self (from the docstring)

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

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

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

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

the map of x2 (from the name)

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

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

Let $x_{2}$ be a homomorphism of $F$ and $G$. Let $x_{3}$ be a homomorphism of $G$ and $H$. Then the map composition isomorphism of $x_{2}$ and $x_{3}$ is an isomorphism of the map of the composition of $x_{2}$ and $x_{3}$ and the composition of the map of $x_{2}$ and the map of $x_{3}$.

the map identity isomorphism of F (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to $x$ and the set of categories. Then the map identity isomorphism of $F$ is an isomorphism of the map of the identity morphism of $F$ and the identity of $\operatorname{Grothendieck}$ applied to $F$.

induced bicategory of C and _F (from the name)

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

homomorphism of X and Y (from the name)

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

the homomorphism of self (from the name)

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

homomorphism of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the homomorphisms of $f$ and $g$ are a basic type.

the homomorphism of self (from the name)

Let $\mathrm{self}$ be a homomorphism of $f$ and $g$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of the homomorphism of $f$ and the homomorphism of $g$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_InducedBicategory\_\_Hom\_u2082\_\_\_proj0}$ applied to $\mathrm{self}$.

$\operatorname{forget}$ is a strict pseudofunctor of the set of induced bicategories of $C$ and $F$ and $C$.

the isomorphism of x1 (from the name)

Let $x_{1}$ be an isomorphism of the homomorphism of $f$ and the homomorphism of $g$. Then the isomorphism of $x_{1}$ is an isomorphism of $f$ and $g$.

the homomorphism of f (from the name)

Let $f$ be a homomorphism of $F$ applied to $X$ and $F$ applied to $Y$. Then the homomorphism of $f$ is a homomorphism of $X$ and $Y$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_InducedBicategory\_\_Hom\_\_\_mkInternal}$ applied to $f$.

the homomorphism of x1 (from the name)

Let $x_{1}$ be a homomorphism of $f$ and $g$. Then the homomorphism of $x_{1}$ is a homomorphism of the homomorphism of $f$ and the homomorphism of $g$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_InducedBicategory\_\_Hom\_u2082\_\_\_mk}$ applied to $x_{1}$.

Let $\mathrm{adj}$ be an adjunction of $f$ and $u$. Then $\operatorname{IsAbsKan}$ holds for $\operatorname{mk}$ applied to $u$ and the unit of $\mathrm{adj}$.

Let $\mathrm{adj}$ be an adjunction of $f$ and $u$. Then $\operatorname{IsAbsKan}$ holds for $\operatorname{mk}$ applied to $f$ and the unit of $\mathrm{adj}$.

the adjunction of t and H (from the name)

Let $t$ be a left extension of $f$ and the identity morphism of $a$. Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Then the adjunction of $t$ and $H$ is an adjunction of $f$ and the extension of $t$ defined as the adjunction of $\operatorname{isKan}$ applied to $H$ and $H$ applied to $b$ and $f$.

the adjunction of H and #2 (from the name)

Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $\mathrm{H'}$ be an element of $\operatorname{IsKan}$ applied to the whisker of $t$ and $f$. Then the adjunction of $H$ and $\mathrm{H'}$ is an adjunction of $f$ and the extension of $t$.

Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $\mathrm{adj}$ be an adjunction of $h$ and $u$. Then $\operatorname{isKanOfWhiskerLeftAdjoint}$ applied to $H$ and $\mathrm{adj}$ is an element of $\operatorname{IsKan}$ applied to the whisker of $t$ and $h$.

the adjunction of t and H (from the name)

Let $t$ be a left lift of $u$ and the identity morphism of $a$. Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Then the adjunction of $t$ and $H$ is an adjunction of the lift of $t$ and $u$ defined as the adjunction of $\operatorname{isKan}$ applied to $H$ and $H$ applied to $b$ and $u$.

the adjunction of H and #2 (from the name)

Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $\mathrm{H'}$ be an element of $\operatorname{IsKan}$ applied to the whisker of $t$ and $u$. Then the adjunction of $H$ and $\mathrm{H'}$ is an adjunction of the lift of $t$ and $u$.

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Then we can say that $\operatorname{HasAbsLeftKanExtension}$ holds for $f$ and $g$.

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Then we can say that $\operatorname{HasAbsLeftKanLift}$ holds for $f$ and $g$.

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Then we can say that $\operatorname{HasLeftKanExtension}$ holds for $f$ and $g$.

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Then we can say that $\operatorname{HasLeftKanLift}$ holds for $f$ and $g$.

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Let $h_{1}$ be a homomorphism of $c$ and $x_{1}$. Then we can say that $\operatorname{CommuteWith}$ holds for $f$, $g$ and $h_{1}$.

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Let $h_{1}$ be a homomorphism of $c$ and $x_{1}$. Then $\operatorname{isKan}$ applied to $f$, $g$ and $h_{1}$ is an element of $\operatorname{IsKan}$ applied to the whisker of $\operatorname{lanLeftExtension}$ applied to $f$ and $g$ and $h_{1}$ defined as $\operatorname{choice}$ applied to $\operatorname{commute}$.

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Let $t$ be a left extension of $f$ and $g$. Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $h_{1}$ be a homomorphism of $c$ and $x_{1}$. Then $\operatorname{isKanWhisker}$ applied to $f$, $g$, $t$, $H$ and $h_{1}$ is an element of $\operatorname{IsKan}$ applied to the whisker of $t$ and $h_{1}$ defined as the whisker of $h_{1}$ and $\operatorname{isKan}$ applied to $f$, $g$ and $h_{1}$.

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Let $h_{1}$ be a homomorphism of $c$ and $x_{1}$. Then $\operatorname{lanCompIso}$ applied to $f$, $g$ and $h_{1}$ is an isomorphism of $\operatorname{lan}$ applied to $f$ and the composition of $g$ and $h_{1}$ and the composition of $\operatorname{lan}$ applied to $f$ and $g$ and $h_{1}$ defined as the right isomorphism of $\operatorname{lanCompIsoWhisker}$ applied to $f$, $g$ and $h_{1}$.

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Let $h_{1}$ be a homomorphism of $c$ and $x_{1}$. Then $\operatorname{lanCompIsoWhisker}$ applied to $f$, $g$ and $h_{1}$ is an isomorphism of $\operatorname{lanLeftExtension}$ applied to $f$ and the composition of $g$ and $h_{1}$ and the whisker of $\operatorname{lanLeftExtension}$ applied to $f$ and $g$ and $h_{1}$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{lanIsKan}$ applied to $f$ and the composition of $g$ and $h_{1}$ and $\operatorname{isKan}$ applied to $f$, $g$ and $h_{1}$.

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Let $h_{1}$ be a homomorphism of $x_{1}$ and $c$. Then we can say that $\operatorname{CommuteWith}$ holds for $f$, $g$ and $h_{1}$.

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Let $h_{1}$ be a homomorphism of $x_{1}$ and $c$. Then $\operatorname{isKan}$ applied to $f$, $g$ and $h_{1}$ is an element of $\operatorname{IsKan}$ applied to the whisker of $\operatorname{lanLiftLeftLift}$ applied to $f$ and $g$ and $h_{1}$ defined as $\operatorname{choice}$ applied to $\operatorname{commute}$.

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Let $t$ be a left lift of $f$ and $g$. Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $h_{1}$ be a homomorphism of $x_{1}$ and $c$. Then $\operatorname{isKanWhisker}$ applied to $f$, $g$, $t$, $H$ and $h_{1}$ is an element of $\operatorname{IsKan}$ applied to the whisker of $t$ and $h_{1}$ defined as the whisker of $h_{1}$ and $\operatorname{isKan}$ applied to $f$, $g$ and $h_{1}$.

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Let $h_{1}$ be a homomorphism of $x_{1}$ and $c$. Then $\operatorname{lanLiftCompIso}$ applied to $f$, $g$ and $h_{1}$ is an isomorphism of $\operatorname{lanLift}$ applied to $f$ and the composition of $h_{1}$ and $g$ and the composition of $h_{1}$ and $\operatorname{lanLift}$ applied to $f$ and $g$ defined as the right isomorphism of $\operatorname{lanLiftCompIsoWhisker}$ applied to $f$, $g$ and $h_{1}$.

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Let $h_{1}$ be a homomorphism of $x_{1}$ and $c$. Then $\operatorname{lanLiftCompIsoWhisker}$ applied to $f$, $g$ and $h_{1}$ is an isomorphism of $\operatorname{lanLiftLeftLift}$ applied to $f$ and the composition of $h_{1}$ and $g$ and the whisker of $\operatorname{lanLiftLeftLift}$ applied to $f$ and $g$ and $h_{1}$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{lanLiftIsKan}$ applied to $f$ and the composition of $h_{1}$ and $g$ and $\operatorname{isKan}$ applied to $f$, $g$ and $h_{1}$.

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Then $\operatorname{lan}$ applied to $f$ and $g$ is a homomorphism of $b$ and $c$ defined as the extension of $\operatorname{lanLeftExtension}$ applied to $f$ and $g$.

Let $s$ be a left extension of $f$ and $g$. Then $\operatorname{lanDesc}$ applied to $s$ is a homomorphism of $\operatorname{lan}$ applied to $f$ and $g$ and the extension of $s$ defined as $\operatorname{desc}$ applied to $\operatorname{lanIsKan}$ applied to $f$ and $g$ and $s$.

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Then $\operatorname{lanIsKan}$ applied to $f$ and $g$ is an element of $\operatorname{IsKan}$ applied to $\operatorname{lanLeftExtension}$ applied to $f$ and $g$ defined as $\operatorname{initialIsInitial}$.

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Then $\operatorname{lanLeftExtension}$ applied to $f$ and $g$ is a left extension of $f$ and $g$ defined as $\operatorname{initial}$ applied to the set of left extensions of $f$ and $g$.

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Then $\operatorname{lanLift}$ applied to $f$ and $g$ is a homomorphism of $c$ and $b$ defined as the lift of $\operatorname{lanLiftLeftLift}$ applied to $f$ and $g$.

Let $s$ be a left lift of $f$ and $g$. Then $\operatorname{lanLiftDesc}$ applied to $s$ is a homomorphism of $\operatorname{lanLift}$ applied to $f$ and $g$ and the lift of $s$ defined as $\operatorname{desc}$ applied to $\operatorname{lanLiftIsKan}$ applied to $f$ and $g$ and $s$.

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Then $\operatorname{lanLiftIsKan}$ applied to $f$ and $g$ is an element of $\operatorname{IsKan}$ applied to $\operatorname{lanLiftLeftLift}$ applied to $f$ and $g$ defined as $\operatorname{initialIsInitial}$.

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Then $\operatorname{lanLiftLeftLift}$ applied to $f$ and $g$ is a left lift of $f$ and $g$ defined as $\operatorname{initial}$ applied to the set of left lifts of $f$ and $g$.

the unit for the left Kan lift of f and g (from the docstring)

Let $f$ be a homomorphism of $b$ and $a$. Let $g$ be a homomorphism of $c$ and $a$. Then the unit for the left Kan lift of $f$ and $g$ is a homomorphism of $g$ and the composition of $\operatorname{lanLift}$ applied to $f$ and $g$ and $f$ defined as the unit of $\operatorname{lanLiftLeftLift}$ applied to $f$ and $g$.

the unit for the left Kan extension of f and g (from the docstring)

Let $f$ be a homomorphism of $a$ and $b$. Let $g$ be a homomorphism of $a$ and $c$. Then the unit for the left Kan extension of $f$ and $g$ is a homomorphism of $g$ and the composition of $f$ and $\operatorname{lan}$ applied to $f$ and $g$ defined as the unit of $\operatorname{lanLeftExtension}$ applied to $f$ and $g$.