Definitions: Mathlib.CategoryTheory, part 3 of 25

CategoryTheory.Bicategory.LeftExtension.IsAbsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, type

Wording

no wording

English

Let $t$ be a left extension of $f$ and $g$. Then an element of $\operatorname{IsAbsKan}$ applied to $t$ is an element of the function that maps $t$ to the set of functions from elements $x_{1}$ of $B$ and homomorphisms $h$ of $c$ and $x_{1}$ to elements of $\operatorname{IsKan}$ applied to the whisker of $t$ and $h$.

CategoryTheory.Bicategory.LeftExtension.IsAbsKan.descdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Let $s$ be a left extension of $f$ and the composition of $g$ and $h$. Then $\operatorname{desc}$ applied to $H$ and $s$ is a homomorphism of the composition of the extension of $t$ and $h$ and the extension of $s$ defined as $\operatorname{desc}$ applied to $H$ applied to $x_{1}$ and $h$ and $s$.

CategoryTheory.Bicategory.LeftExtension.IsAbsKan.isKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Then $\operatorname{isKan}$ applied to $H$ is an element of $\operatorname{IsKan}$ applied to $t$ defined as $\operatorname{ofIsoKan}$ applied to $\operatorname{ofCompId}$ applied to the whisker of $t$ and the identity morphism of $c$ and $H$ applied to $c$ and the identity morphism of $c$ and the whisker of $t$.

CategoryTheory.Bicategory.LeftExtension.IsAbsKan.ofIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then $\operatorname{IsAbsKan}$ holds for the left extension of $\mathrm{eg}$ and $t$. Proof. Let $H$ be arbitrary. Let $\mathrm{ef}$ be arbitrary. Let $\mathrm{eg}$ be arbitrary. Let $x_{1}$ be arbitrary. Let $h$ be arbitrary. By x1. By h. By H. By ef. By eg. By h. By CategoryTheory__Bicategory__whiskerRightIso. By CategoryTheory__Bicategory__LeftExtension__IsKan__ofIso. By t. By h. By CategoryTheory__Bicategory__LeftExtension__whiskerOfIso. By CategoryTheory__Bicategory__LeftExtension__IsKan__ofIsoKan.

CategoryTheory.Bicategory.LeftExtension.IsAbsKan.ofIsoAbsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $P$ be an element of $\operatorname{IsAbsKan}$ applied to $s$. Let $i$ be an isomorphism of $s$ and $t$. Then $\operatorname{IsAbsKan}$ holds for $t$. Proof. Let $P$ be arbitrary. Let $i$ be arbitrary. Let $x_{1}$ be arbitrary. Let $h$ be arbitrary. By x1. By h. By P. By i. By h. By CategoryTheory__Bicategory__LeftExtension__whiskerIso. By CategoryTheory__Bicategory__LeftExtension__IsKan__ofIsoKan.

CategoryTheory.Bicategory.LeftExtension.IsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, type

Wording

no wording

English

Let $t$ be a left extension of $f$ and $g$. Then an element of $\operatorname{IsKan}$ applied to $t$ is an element of the function that maps $t$ to $\operatorname{IsUniversal}$ applied to $t$.

CategoryTheory.Bicategory.LeftExtension.IsKan.descdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $s$ be a left extension of $f$ and $g$. Then $\operatorname{desc}$ applied to $H$ and $s$ is a homomorphism of the extension of $t$ and the extension of $s$ defined as $\operatorname{desc}$ applied to $H$ and $s$.

CategoryTheory.Bicategory.LeftExtension.IsKan.mkdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $\mathrm{desc}$ be a function from left extensions $s_{1}$ of $f$ and $g$ to homomorphisms of $t$ and $s_{1}$ such that for all left extensions $s$ of $f$ and $g$, for all homomorphisms $x_{1}$ of $t$ and $s$, $\EqtMACRoH {x_{1}}{\mathrm{desc} (s)}$. Then $\operatorname{mk}$ applied to $s_{1}$, $\mathrm{desc}$ and $w$ is an element of $\operatorname{IsKan}$ applied to $t$ defined as the function that maps $w$ to $\operatorname{ofUniqueHom}$ applied to $s_{1}$, $\mathrm{desc}$ and $w$.

CategoryTheory.Bicategory.LeftExtension.IsKan.ofCompIddefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $t$ be a left extension of $f$ and the composition of $g$ and the identity morphism of $c$. Let $P$ be an element of $\operatorname{IsKan}$ applied to $t$. Then $\operatorname{ofCompId}$ applied to $t$ and $P$ is an element of $\operatorname{IsKan}$ applied to the left extension of $t$.

CategoryTheory.Bicategory.LeftExtension.IsKan.ofIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then $\operatorname{ofIso}$ applied to $H$, $\mathrm{ef}$ and $\mathrm{eg}$ is an element of $\operatorname{IsKan}$ applied to the left extension of $\mathrm{eg}$ and $t$ defined as $\operatorname{isInitialObj}$ applied to the functor of the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$, $t$ and $H$.

CategoryTheory.Bicategory.LeftExtension.IsKan.ofIsoKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $P$ be an element of $\operatorname{IsKan}$ applied to $s$. Let $i$ be an isomorphism of $s$ and $t$. Then $\operatorname{ofIsoKan}$ applied to $P$ and $i$ is an element of $\operatorname{IsKan}$ applied to $t$ defined as $\operatorname{ofIso}$ applied to $P$ and $i$.

CategoryTheory.Bicategory.LeftExtension.IsKan.uniqueUpToIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $P$ be an element of $\operatorname{IsKan}$ applied to $s$. Let $Q$ be an element of $\operatorname{IsKan}$ applied to $t$. Then $\operatorname{uniqueUpToIso}$ applied to $P$ and $Q$ is an isomorphism of $s$ and $t$ defined as $\operatorname{uniqueUpToIso}$ applied to $P$ and $Q$.

CategoryTheory.Bicategory.LeftExtension.IsKan.whiskerOfCommutedefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

the whisker of h and P (from the name)

English

Let $s$ and $t$ be left extensions of $f$ and $g$. Let $i$ be an isomorphism of $s$ and $t$. Let $h$ be a homomorphism of $c$ and $x_{1}$. Let $P$ be an element of $\operatorname{IsKan}$ applied to the whisker of $s$ and $h$. Then the whisker of $h$ and $P$ is an element of $\operatorname{IsKan}$ applied to the whisker of $t$ and $h$ defined as $\operatorname{ofIsoKan}$ applied to $P$ and the whisker isomorphism of $i$ and $h$.

CategoryTheory.Bicategory.LeftLift.IsAbsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, type

Wording

no wording

English

Let $t$ be a left lift of $f$ and $g$. Then an element of $\operatorname{IsAbsKan}$ applied to $t$ is an element of the function that maps $t$ to the set of functions from elements $x_{1}$ of $B$ and homomorphisms $h$ of $x_{1}$ and $c$ to elements of $\operatorname{IsKan}$ applied to the whisker of $t$ and $h$.

CategoryTheory.Bicategory.LeftLift.IsAbsKan.descdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Let $s$ be a left lift of $f$ and the composition of $h$ and $g$. Then $\operatorname{desc}$ applied to $H$ and $s$ is a homomorphism of the composition of $h$ and the lift of $t$ and the lift of $s$ defined as $\operatorname{desc}$ applied to $H$ applied to $x_{1}$ and $h$ and $s$.

CategoryTheory.Bicategory.LeftLift.IsAbsKan.isKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Then $\operatorname{isKan}$ applied to $H$ is an element of $\operatorname{IsKan}$ applied to $t$ defined as $\operatorname{ofIsoKan}$ applied to $\operatorname{ofIdComp}$ applied to the whisker of $t$ and the identity morphism of $c$ and $H$ applied to $c$ and the identity morphism of $c$ and the whisker of $t$.

CategoryTheory.Bicategory.LeftLift.IsAbsKan.ofIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then $\operatorname{IsAbsKan}$ holds for the left lift of $\mathrm{eg}$ and $t$. Proof. Let $H$ be arbitrary. Let $\mathrm{ef}$ be arbitrary. Let $\mathrm{eg}$ be arbitrary. Let $x_{1}$ be arbitrary. Let $h$ be arbitrary. By x1. By h. By H. By ef. By h. By eg. By CategoryTheory__Bicategory__whiskerLeftIso. By CategoryTheory__Bicategory__LeftLift__IsKan__ofIso. By t. By h. By CategoryTheory__Bicategory__LeftLift__whiskerOfIso. By CategoryTheory__Bicategory__LeftLift__IsKan__ofIsoKan.

CategoryTheory.Bicategory.LeftLift.IsAbsKan.ofIsoAbsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $P$ be an element of $\operatorname{IsAbsKan}$ applied to $s$. Let $i$ be an isomorphism of $s$ and $t$. Then $\operatorname{IsAbsKan}$ holds for $t$. Proof. Let $P$ be arbitrary. Let $i$ be arbitrary. Let $x_{1}$ be arbitrary. Let $h$ be arbitrary. By x1. By h. By P. By i. By h. By CategoryTheory__Bicategory__LeftLift__whiskerIso. By CategoryTheory__Bicategory__LeftLift__IsKan__ofIsoKan.

CategoryTheory.Bicategory.LeftLift.IsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, type

Wording

no wording

English

Let $t$ be a left lift of $f$ and $g$. Then an element of $\operatorname{IsKan}$ applied to $t$ is an element of the function that maps $t$ to $\operatorname{IsUniversal}$ applied to $t$.

CategoryTheory.Bicategory.LeftLift.IsKan.descdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $s$ be a left lift of $f$ and $g$. Then $\operatorname{desc}$ applied to $H$ and $s$ is a homomorphism of the lift of $t$ and the lift of $s$ defined as $\operatorname{desc}$ applied to $H$ and $s$.

CategoryTheory.Bicategory.LeftLift.IsKan.mkdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $\mathrm{desc}$ be a function from left lifts $s_{1}$ of $f$ and $g$ to homomorphisms of $t$ and $s_{1}$ such that for all left lifts $s$ of $f$ and $g$, for all homomorphisms $x_{1}$ of $t$ and $s$, $\EqtMACRoH {x_{1}}{\mathrm{desc} (s)}$. Then $\operatorname{mk}$ applied to $s_{1}$, $\mathrm{desc}$ and $w$ is an element of $\operatorname{IsKan}$ applied to $t$ defined as the function that maps $w$ to $\operatorname{ofUniqueHom}$ applied to $s_{1}$, $\mathrm{desc}$ and $w$.

CategoryTheory.Bicategory.LeftLift.IsKan.ofIdCompdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $t$ be a left lift of $f$ and the composition of the identity morphism of $c$ and $g$. Let $P$ be an element of $\operatorname{IsKan}$ applied to $t$. Then $\operatorname{ofIdComp}$ applied to $t$ and $P$ is an element of $\operatorname{IsKan}$ applied to the left lift of $t$.

CategoryTheory.Bicategory.LeftLift.IsKan.ofIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then $\operatorname{ofIso}$ applied to $H$, $\mathrm{ef}$ and $\mathrm{eg}$ is an element of $\operatorname{IsKan}$ applied to the left lift of $\mathrm{eg}$ and $t$ defined as $\operatorname{isInitialObj}$ applied to the functor of the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$, $t$ and $H$.

CategoryTheory.Bicategory.LeftLift.IsKan.ofIsoKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

CategoryTheory.Bicategory.LeftLift.IsKan.whiskerOfCommutedefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

the whisker of h and P (from the name)

English

Let $s$ and $t$ be left lifts of $f$ and $g$. Let $i$ be an isomorphism of $s$ and $t$. Let $h$ be a homomorphism of $x_{1}$ and $c$. Let $P$ be an element of $\operatorname{IsKan}$ applied to the whisker of $s$ and $h$. Then the whisker of $h$ and $P$ is an element of $\operatorname{IsKan}$ applied to the whisker of $t$ and $h$ defined as $\operatorname{ofIsoKan}$ applied to $P$ and the whisker isomorphism of $i$ and $h$.

CategoryTheory.Bicategory.RightExtension.IsAbsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, type

Wording

no wording

English

Let $t$ be a right extension of $f$ and $g$. Then an element of $\operatorname{IsAbsKan}$ applied to $t$ is an element of the function that maps $t$ to the set of functions from elements $x_{1}$ of $B$ and homomorphisms $h$ of $c$ and $x_{1}$ to elements of $\operatorname{IsKan}$ applied to the whisker of $t$ and $h$.

CategoryTheory.Bicategory.RightExtension.IsAbsKan.descdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Let $s$ be a right extension of $f$ and the composition of $g$ and $h$. Then $\operatorname{desc}$ applied to $H$ and $s$ is a homomorphism of the extension of $s$ and the composition of the extension of $t$ and $h$ defined as $\operatorname{desc}$ applied to $H$ applied to $x_{1}$ and $h$ and $s$.

CategoryTheory.Bicategory.RightExtension.IsAbsKan.isKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

CategoryTheory.Bicategory.RightExtension.IsAbsKan.ofIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then $\operatorname{IsAbsKan}$ holds for the right extension of $\mathrm{eg}$ and $t$. Proof. Let $H$ be arbitrary. Let $\mathrm{ef}$ be arbitrary. Let $\mathrm{eg}$ be arbitrary. Let $x_{1}$ be arbitrary. Let $h$ be arbitrary. By x1. By h. By H. By ef. By eg. By h. By CategoryTheory__Bicategory__whiskerRightIso. By CategoryTheory__Bicategory__RightExtension__IsKan__ofIso. By t. By h. By CategoryTheory__Bicategory__RightExtension__whiskerOfIso. By CategoryTheory__Bicategory__RightExtension__IsKan__ofIsoKan.

CategoryTheory.Bicategory.RightExtension.IsAbsKan.ofIsoAbsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $P$ be an element of $\operatorname{IsAbsKan}$ applied to $s$. Let $i$ be an isomorphism of $s$ and $t$. Then $\operatorname{IsAbsKan}$ holds for $t$. Proof. Let $P$ be arbitrary. Let $i$ be arbitrary. Let $x_{1}$ be arbitrary. Let $h$ be arbitrary. By x1. By h. By P. By i. By h. By CategoryTheory__Bicategory__RightExtension__whiskerIso. By CategoryTheory__Bicategory__RightExtension__IsKan__ofIsoKan.

CategoryTheory.Bicategory.RightExtension.IsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, type

Wording

no wording

English

Let $t$ be a right extension of $f$ and $g$. Then an element of $\operatorname{IsKan}$ applied to $t$ is an element of the function that maps $t$ to $\operatorname{IsUniversal}$ applied to $t$.

CategoryTheory.Bicategory.RightExtension.IsKan.descdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $s$ be a right extension of $f$ and $g$. Then $\operatorname{desc}$ applied to $H$ and $s$ is a homomorphism of the extension of $s$ and the extension of $t$ defined as the lift of $H$ and $s$.

CategoryTheory.Bicategory.RightExtension.IsKan.mkdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $\mathrm{desc}$ be a function from right extensions $s_{1}$ of $f$ and $g$ to homomorphisms of $s_{1}$ and $t$ such that for all right extensions $s$ of $f$ and $g$, for all homomorphisms $x_{1}$ of $s$ and $t$, $\EqtMACRoH {x_{1}}{\mathrm{desc} (s)}$. Then $\operatorname{mk}$ applied to $s_{1}$, $\mathrm{desc}$ and $w$ is an element of $\operatorname{IsKan}$ applied to $t$ defined as the function that maps $w$ to $\operatorname{ofUniqueHom}$ applied to $s_{1}$, $\mathrm{desc}$ and $w$.

CategoryTheory.Bicategory.RightExtension.IsKan.ofCompIddefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $t$ be a right extension of $f$ and the composition of $g$ and the identity morphism of $c$. Let $P$ be an element of $\operatorname{IsKan}$ applied to $t$. Then $\operatorname{ofCompId}$ applied to $t$ and $P$ is an element of $\operatorname{IsKan}$ applied to the right extension of $t$.

CategoryTheory.Bicategory.RightExtension.IsKan.ofIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then $\operatorname{ofIso}$ applied to $H$, $\mathrm{ef}$ and $\mathrm{eg}$ is an element of $\operatorname{IsKan}$ applied to the right extension of $\mathrm{eg}$ and $t$ defined as $\operatorname{isTerminalObj}$ applied to the functor of the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$, $t$ and $H$.

CategoryTheory.Bicategory.RightExtension.IsKan.ofIsoKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

CategoryTheory.Bicategory.RightExtension.IsKan.uniqueUpToIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

CategoryTheory.Bicategory.RightExtension.IsKan.whiskerOfCommutedefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

the whisker of h and P (from the name)

English

Let $s$ and $t$ be right extensions of $f$ and $g$. Let $i$ be an isomorphism of $s$ and $t$. Let $h$ be a homomorphism of $c$ and $x_{1}$. Let $P$ be an element of $\operatorname{IsKan}$ applied to the whisker of $s$ and $h$. Then the whisker of $h$ and $P$ is an element of $\operatorname{IsKan}$ applied to the whisker of $t$ and $h$ defined as $\operatorname{ofIsoKan}$ applied to $P$ and the whisker isomorphism of $i$ and $h$.

CategoryTheory.Bicategory.RightLift.IsAbsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, type

Wording

no wording

English

Let $t$ be a right lift of $f$ and $g$. Then an element of $\operatorname{IsAbsKan}$ applied to $t$ is an element of the function that maps $t$ to the set of functions from elements $x_{1}$ of $B$ and homomorphisms $h$ of $x_{1}$ and $c$ to elements of $\operatorname{IsKan}$ applied to the whisker of $t$ and $h$.

CategoryTheory.Bicategory.RightLift.IsAbsKan.descdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Let $s$ be a right lift of $f$ and the composition of $h$ and $g$. Then $\operatorname{desc}$ applied to $H$ and $s$ is a homomorphism of the lift of $s$ and the composition of $h$ and the lift of $t$ defined as $\operatorname{desc}$ applied to $H$ applied to $x_{1}$ and $h$ and $s$.

CategoryTheory.Bicategory.RightLift.IsAbsKan.isKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Then $\operatorname{isKan}$ applied to $H$ is an element of $\operatorname{IsKan}$ applied to $t$ defined as $\operatorname{ofIsoKan}$ applied to $\operatorname{ofIdComp}$ applied to the whisker of $t$ and the identity morphism of $c$ and $H$ applied to $c$ and the identity morphism of $c$ and the whisker of $t$.

CategoryTheory.Bicategory.RightLift.IsAbsKan.ofIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsAbsKan}$ applied to $t$. Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then $\operatorname{IsAbsKan}$ holds for the right lift of $\mathrm{eg}$ and $t$. Proof. Let $H$ be arbitrary. Let $\mathrm{ef}$ be arbitrary. Let $\mathrm{eg}$ be arbitrary. Let $x_{1}$ be arbitrary. Let $h$ be arbitrary. By x1. By h. By H. By ef. By h. By eg. By CategoryTheory__Bicategory__whiskerLeftIso. By CategoryTheory__Bicategory__RightLift__IsKan__ofIso. By t. By h. By CategoryTheory__Bicategory__RightLift__whiskerOfIso. By CategoryTheory__Bicategory__RightLift__IsKan__ofIsoKan.

CategoryTheory.Bicategory.RightLift.IsAbsKan.ofIsoAbsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $P$ be an element of $\operatorname{IsAbsKan}$ applied to $s$. Let $i$ be an isomorphism of $s$ and $t$. Then $\operatorname{IsAbsKan}$ holds for $t$. Proof. Let $P$ be arbitrary. Let $i$ be arbitrary. Let $x_{1}$ be arbitrary. Let $h$ be arbitrary. By x1. By h. By P. By i. By h. By CategoryTheory__Bicategory__RightLift__whiskerIso. By CategoryTheory__Bicategory__RightLift__IsKan__ofIsoKan.

CategoryTheory.Bicategory.RightLift.IsKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, type

Wording

no wording

English

Let $t$ be a right lift of $f$ and $g$. Then an element of $\operatorname{IsKan}$ applied to $t$ is an element of the function that maps $t$ to $\operatorname{IsUniversal}$ applied to $t$.

CategoryTheory.Bicategory.RightLift.IsKan.descdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $s$ be a right lift of $f$ and $g$. Then $\operatorname{desc}$ applied to $H$ and $s$ is a homomorphism of the lift of $s$ and the lift of $t$ defined as the lift of $H$ and $s$.

CategoryTheory.Bicategory.RightLift.IsKan.mkdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $\mathrm{desc}$ be a function from right lifts $s_{1}$ of $f$ and $g$ to homomorphisms of $s_{1}$ and $t$ such that for all right lifts $s$ of $f$ and $g$, for all homomorphisms $x_{1}$ of $s$ and $t$, $\EqtMACRoH {x_{1}}{\mathrm{desc} (s)}$. Then $\operatorname{mk}$ applied to $s_{1}$, $\mathrm{desc}$ and $w$ is an element of $\operatorname{IsKan}$ applied to $t$ defined as the function that maps $w$ to $\operatorname{ofUniqueHom}$ applied to $s_{1}$, $\mathrm{desc}$ and $w$.

CategoryTheory.Bicategory.RightLift.IsKan.ofIdCompdefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $t$ be a right lift of $f$ and the composition of the identity morphism of $c$ and $g$. Let $P$ be an element of $\operatorname{IsKan}$ applied to $t$. Then $\operatorname{ofIdComp}$ applied to $t$ and $P$ is an element of $\operatorname{IsKan}$ applied to the right lift of $t$.

CategoryTheory.Bicategory.RightLift.IsKan.ofIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

Let $H$ be an element of $\operatorname{IsKan}$ applied to $t$. Let $\mathrm{ef}$ be an isomorphism of $f$ and $\mathrm{f'}$. Let $\mathrm{eg}$ be an isomorphism of $g$ and $\mathrm{g'}$. Then $\operatorname{ofIso}$ applied to $H$, $\mathrm{ef}$ and $\mathrm{eg}$ is an element of $\operatorname{IsKan}$ applied to the right lift of $\mathrm{eg}$ and $t$ defined as $\operatorname{isTerminalObj}$ applied to the functor of the map isomorphism of $\mathrm{ef}$ and $\mathrm{eg}$, $t$ and $H$.

CategoryTheory.Bicategory.RightLift.IsKan.ofIsoKandefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

CategoryTheory.Bicategory.RightLift.IsKan.uniqueUpToIsodefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

no wording

English

CategoryTheory.Bicategory.RightLift.IsKan.whiskerOfCommutedefMathlib.CategoryTheory.Bicategory.Kan.IsKan, function or constant

Wording

the whisker of h and P (from the name)

English

Let $s$ and $t$ be right lifts of $f$ and $g$. Let $i$ be an isomorphism of $s$ and $t$. Let $h$ be a homomorphism of $x_{1}$ and $c$. Let $P$ be an element of $\operatorname{IsKan}$ applied to the whisker of $s$ and $h$. Then the whisker of $h$ and $P$ is an element of $\operatorname{IsKan}$ applied to the whisker of $t$ and $h$ defined as $\operatorname{ofIsoKan}$ applied to $P$ and the whisker isomorphism of $i$ and $h$.

Mathlib.CategoryTheory.Bicategory.LocallyDiscrete

CategoryTheory.Bicategory.IsLocallyDiscretedefMathlib.CategoryTheory.Bicategory.LocallyDiscrete, predicate

Wording

B is locally discrete (from the docstring)

English

generation took over the time limit

CategoryTheory.LocallyDiscretestructureMathlib.CategoryTheory.Bicategory.LocallyDiscrete, type

Wording

no wording

English

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

CategoryTheory.LocallyDiscrete.asdefMathlib.CategoryTheory.Bicategory.LocallyDiscrete, function or constant

Wording

no wording

English

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

CategoryTheory.LocallyDiscrete.locallyDiscreteEquivdefMathlib.CategoryTheory.Bicategory.LocallyDiscrete, function or constant

Wording

the locally discrete equivalence (from the name)

English

generation took over the time limit

Quiver.Hom.toLocdefMathlib.CategoryTheory.Bicategory.LocallyDiscrete, function or constant

Wording

no wording

English

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

Mathlib.CategoryTheory.Bicategory.LocallyGroupoid

CategoryTheory.Bicategory.IsLocallyGroupoiddefMathlib.CategoryTheory.Bicategory.LocallyGroupoid, predicate

Wording

B is locally groupoidal (from the docstring)

English

generation took over the time limit

CategoryTheory.Bicategory.PithstructureMathlib.CategoryTheory.Bicategory.LocallyGroupoid, type

Wording

no wording

English

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

CategoryTheory.Bicategory.Pith.asdefMathlib.CategoryTheory.Bicategory.LocallyGroupoid, function or constant

Wording

no wording

English

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

CategoryTheory.Bicategory.Pith.inclusiondefMathlib.CategoryTheory.Bicategory.LocallyGroupoid, function or constant

Wording

the inclusion of B (from the name)

English

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

CategoryTheory.Bicategory.Pith.pseudofunctorToPithdefMathlib.CategoryTheory.Bicategory.LocallyGroupoid, function or constant

Wording

no wording

English

Let $F$ be a pseudofunctor of $\mathrm{B'}$ and $B$. Then $\operatorname{pseudofunctorToPith}$ applied to $F$ is a pseudofunctor of $\mathrm{B'}$ and $\operatorname{Pith}$ applied to $B$.

CategoryTheory.Bicategory.Pith.pseudofunctorToPithCompInclusionStrongIsoHomdefMathlib.CategoryTheory.Bicategory.LocallyGroupoid, function or constant

Wording

no wording

English

Let $F$ be a pseudofunctor of $\mathrm{B'}$ and $B$. Then $\operatorname{pseudofunctorToPithCompInclusionStrongIsoHom}$ applied to $F$ is a strong composition of the composition of $\operatorname{pseudofunctorToPith}$ applied to $F$ and the inclusion of $B$ and $F$.

CategoryTheory.Bicategory.Pith.pseudofunctorToPithCompInclusionStrongIsoInvdefMathlib.CategoryTheory.Bicategory.LocallyGroupoid, function or constant

Wording

no wording

English

Let $F$ be a pseudofunctor of $\mathrm{B'}$ and $B$. Then $\operatorname{pseudofunctorToPithCompInclusionStrongIsoInv}$ applied to $F$ is a strong composition of $F$ and the composition of $\operatorname{pseudofunctorToPith}$ applied to $F$ and the inclusion of $B$.

CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoiddefMathlib.CategoryTheory.Bicategory.LocallyGroupoid, function or constant

Wording

the pseudofunctor of F (from the name)

English

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

CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoiddefMathlib.CategoryTheory.Bicategory.LocallyGroupoid, function or constant

Wording

the pseudofunctor of F (from the name)

English

Let $F$ be an oplax functor of $\mathrm{B'}$ and $B$. Then the pseudofunctor of $F$ is a pseudo of $F$.

Mathlib.CategoryTheory.Bicategory.Modification.Lax

CategoryTheory.Lax.LaxTrans.HomstructureMathlib.CategoryTheory.Bicategory.Modification.Lax, type

Wording

homomorphism of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the homomorphisms of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Lax.LaxTrans.Hom.asdefMathlib.CategoryTheory.Bicategory.Modification.Lax, function or constant

Wording

no wording

English

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

CategoryTheory.Lax.LaxTrans.ModificationstructureMathlib.CategoryTheory.Bicategory.Modification.Lax, type

Wording

modification of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the modifications of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Lax.LaxTrans.Modification.appdefMathlib.CategoryTheory.Bicategory.Modification.Lax, function or constant

Wording

the modification of self and a (from the name)

English

Let $\mathrm{self}$ be a modification of $x_{2}$ and $x_{3}$. Let $a$ be an element of $B$. Then the modification of $\mathrm{self}$ and $a$ is a homomorphism of $\operatorname{LaxTrans}$ applied to $x_{2}$ and $a$ and $\operatorname{LaxTrans}$ applied to $x_{3}$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

CategoryTheory.Lax.LaxTrans.Modification.iddefMathlib.CategoryTheory.Bicategory.Modification.Lax, function or constant

Wording

the identity modification of x2 (from the docstring)

English

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

CategoryTheory.Lax.LaxTrans.Modification.vcompdefMathlib.CategoryTheory.Bicategory.Modification.Lax, function or constant

Wording

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

English

Let $x_{5}$ be a modification of $x_{2}$ and $x_{3}$. Let $x_{6}$ be a modification of $x_{3}$ and $x_{4}$. Then the vertical composition of $x_{5}$ and $x_{6}$ is a modification of $x_{2}$ and $x_{4}$.

CategoryTheory.Lax.LaxTrans.isoMkdefMathlib.CategoryTheory.Bicategory.Modification.Lax, function or constant

Wording

the isomorphism of app and a1 (from the name)

English

Let $\mathrm{app}$ be a function from elements $a_{1}$ of $B$ to isomorphisms of $\operatorname{LaxTrans}$ applied to $x_{2}$ and $a_{1}$ and $\operatorname{LaxTrans}$ applied to $x_{3}$ and $a_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $a$ and $b$ of $B$, for all homomorphisms $f$ of $a$ and $b$, the composition of the right whisker of the homomorphism of $\mathrm{app}$ applied to $a$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $f$ and the naturality of $x_{3}$ and $f$ is equal to the composition of the naturality of $x_{2}$ and $f$ and the left whisker of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the homomorphism of $\mathrm{app}$ applied to $b$ and $\mathrm{CategoryTheory\_\_Lax\_\_LaxTrans\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $a_{1}$ and $\mathrm{app}$ is an isomorphism of $x_{2}$ and $x_{3}$.

CategoryTheory.Lax.OplaxTrans.HomstructureMathlib.CategoryTheory.Bicategory.Modification.Lax, type

Wording

homomorphism of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the homomorphisms of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Lax.OplaxTrans.Hom.asdefMathlib.CategoryTheory.Bicategory.Modification.Lax, function or constant

Wording

no wording

English

CategoryTheory.Lax.OplaxTrans.ModificationstructureMathlib.CategoryTheory.Bicategory.Modification.Lax, type

Wording

modification of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the modifications of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Lax.OplaxTrans.Modification.appdefMathlib.CategoryTheory.Bicategory.Modification.Lax, function or constant

Wording

the modification of self and a (from the name)

English

Let $\mathrm{self}$ be a modification of $x_{2}$ and $x_{3}$. Let $a$ be an element of $B$. Then the modification of $\mathrm{self}$ and $a$ is a homomorphism of the oplax composition of $x_{2}$ and $a$ and the oplax composition of $x_{3}$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

CategoryTheory.Lax.OplaxTrans.Modification.iddefMathlib.CategoryTheory.Bicategory.Modification.Lax, function or constant

Wording

the identity modification of x2 (from the docstring)

English

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

CategoryTheory.Lax.OplaxTrans.Modification.vcompdefMathlib.CategoryTheory.Bicategory.Modification.Lax, function or constant

Wording

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

English

CategoryTheory.Lax.OplaxTrans.isoMkdefMathlib.CategoryTheory.Bicategory.Modification.Lax, function or constant

Wording

the isomorphism of app and a1 (from the name)

English

Let $\mathrm{app}$ be a function from elements $a_{1}$ of $B$ to isomorphisms of the oplax composition of $x_{2}$ and $a_{1}$ and the oplax composition of $x_{3}$ and $a_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $a$ and $b$ of $B$, for all homomorphisms $f$ of $a$ and $b$, the composition of the left whisker of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the homomorphism of $\mathrm{app}$ applied to $b$ and the naturality of $x_{3}$ and $f$ is equal to the composition of the naturality of $x_{2}$ and $f$ and the right whisker of the homomorphism of $\mathrm{app}$ applied to $a$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $f$ and $\mathrm{CategoryTheory\_\_Lax\_\_OplaxTrans\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $a_{1}$ and $\mathrm{app}$ is an isomorphism of $x_{2}$ and $x_{3}$.

Mathlib.CategoryTheory.Bicategory.Modification.Oplax

CategoryTheory.Oplax.LaxTrans.HomstructureMathlib.CategoryTheory.Bicategory.Modification.Oplax, type

Wording

homomorphism of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the homomorphisms of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Oplax.LaxTrans.Hom.asdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

no wording

English

CategoryTheory.Oplax.LaxTrans.ModificationstructureMathlib.CategoryTheory.Bicategory.Modification.Oplax, type

Wording

modification of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the modifications of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Oplax.LaxTrans.Modification.appdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

the modification of self and a (from the name)

English

CategoryTheory.Oplax.LaxTrans.Modification.iddefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

the identity modification of x2 (from the docstring)

English

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

CategoryTheory.Oplax.LaxTrans.Modification.vcompdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

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

English

CategoryTheory.Oplax.LaxTrans.isoMkdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

the isomorphism of app and a1 (from the name)

English

Let $\mathrm{app}$ be a function from elements $a_{1}$ of $B$ to isomorphisms of $\operatorname{LaxTrans}$ applied to $x_{2}$ and $a_{1}$ and $\operatorname{LaxTrans}$ applied to $x_{3}$ and $a_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $a$ and $b$ of $B$, for all homomorphisms $f$ of $a$ and $b$, the composition of the right whisker of the homomorphism of $\mathrm{app}$ applied to $a$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $f$ and the naturality of $x_{3}$ and $f$ is equal to the composition of the naturality of $x_{2}$ and $f$ and the left whisker of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the homomorphism of $\mathrm{app}$ applied to $b$ and $\mathrm{CategoryTheory\_\_Oplax\_\_LaxTrans\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $a_{1}$ and $\mathrm{app}$ is an isomorphism of $x_{2}$ and $x_{3}$.

CategoryTheory.Oplax.OplaxTrans.HomstructureMathlib.CategoryTheory.Bicategory.Modification.Oplax, type

Wording

homomorphism of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the homomorphisms of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Oplax.OplaxTrans.Hom.asdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

no wording

English

CategoryTheory.Oplax.OplaxTrans.ModificationstructureMathlib.CategoryTheory.Bicategory.Modification.Oplax, type

Wording

modification of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the modifications of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Oplax.OplaxTrans.Modification.appdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

the modification of self and a (from the name)

English

CategoryTheory.Oplax.OplaxTrans.Modification.iddefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

the identity modification of x2 (from the docstring)

English

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

CategoryTheory.Oplax.OplaxTrans.Modification.vcompdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

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

English

CategoryTheory.Oplax.OplaxTrans.isoMkdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

the isomorphism of app and a1 (from the name)

English

Let $\mathrm{app}$ be a function from elements $a_{1}$ of $B$ to isomorphisms of the oplax composition of $x_{2}$ and $a_{1}$ and the oplax composition of $x_{3}$ and $a_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $a$ and $b$ of $B$, for all homomorphisms $f$ of $a$ and $b$, the composition of the left whisker of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the homomorphism of $\mathrm{app}$ applied to $b$ and the naturality of $x_{3}$ and $f$ is equal to the composition of the naturality of $x_{2}$ and $f$ and the right whisker of the homomorphism of $\mathrm{app}$ applied to $a$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $f$ and $\mathrm{CategoryTheory\_\_Oplax\_\_OplaxTrans\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $a_{1}$ and $\mathrm{app}$ is an isomorphism of $x_{2}$ and $x_{3}$.

CategoryTheory.Oplax.StrongTrans.HomstructureMathlib.CategoryTheory.Bicategory.Modification.Oplax, type

Wording

homomorphism of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the homomorphisms of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Oplax.StrongTrans.Hom.asdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

no wording

English

CategoryTheory.Oplax.StrongTrans.ModificationstructureMathlib.CategoryTheory.Bicategory.Modification.Oplax, type

Wording

modification of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the modifications of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Oplax.StrongTrans.Modification.appdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

the modification of self and a (from the name)

English

Let $\mathrm{self}$ be a modification of $x_{2}$ and $x_{3}$. Let $a$ be an element of $B$. Then the modification of $\mathrm{self}$ and $a$ is a homomorphism of the strong composition of $x_{2}$ and $a$ and the strong composition of $x_{3}$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

CategoryTheory.Oplax.StrongTrans.Modification.equivOplaxdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

the equivalence oplax (from the name)

English

The equivalence oplax is an equivalence from the set of modifications of the underlying oplax natural transformation of $x_{2}$ and the underlying oplax natural transformation of $x_{3}$ to the set of modifications of $x_{2}$ and $x_{3}$.

CategoryTheory.Oplax.StrongTrans.Modification.iddefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

the identity modification of x2 (from the docstring)

English

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

CategoryTheory.Oplax.StrongTrans.Modification.mkOfOplaxdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

no wording

English

Let $x_{4}$ be a modification of the underlying oplax natural transformation of $x_{2}$ and the underlying oplax natural transformation of $x_{3}$. Then $\operatorname{mkOfOplax}$ applied to $x_{4}$ is a modification of $x_{2}$ and $x_{3}$.

CategoryTheory.Oplax.StrongTrans.Modification.toOplaxdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

the oplax of x4 (from the name)

English

Let $x_{4}$ be a modification of $x_{2}$ and $x_{3}$. Then the oplax of $x_{4}$ is a modification of the underlying oplax natural transformation of $x_{2}$ and the underlying oplax natural transformation of $x_{3}$.

CategoryTheory.Oplax.StrongTrans.Modification.vcompdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

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

English

CategoryTheory.Oplax.StrongTrans.isoMkdefMathlib.CategoryTheory.Bicategory.Modification.Oplax, function or constant

Wording

the isomorphism of app and a1 (from the name)

English

Let $\mathrm{app}$ be a function from elements $a_{1}$ of $B$ to isomorphisms of the strong composition of $x_{2}$ and $a_{1}$ and the strong composition of $x_{3}$ and $a_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $a$ and $b$ of $B$, for all homomorphisms $f$ of $a$ and $b$, the composition of the left whisker of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the homomorphism of $\mathrm{app}$ applied to $b$ and the homomorphism of the naturality of $x_{3}$ and $f$ is equal to the composition of the homomorphism of the naturality of $x_{2}$ and $f$ and the right whisker of the homomorphism of $\mathrm{app}$ applied to $a$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $f$ and $\mathrm{CategoryTheory\_\_Oplax\_\_StrongTrans\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $a_{1}$ and $\mathrm{app}$ is an isomorphism of $x_{2}$ and $x_{3}$.

Mathlib.CategoryTheory.Bicategory.Modification.Pseudo

CategoryTheory.Pseudofunctor.StrongTrans.HomstructureMathlib.CategoryTheory.Bicategory.Modification.Pseudo, type

Wording

homomorphism of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the homomorphisms of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Pseudofunctor.StrongTrans.Hom.asdefMathlib.CategoryTheory.Bicategory.Modification.Pseudo, function or constant

Wording

no wording

English

CategoryTheory.Pseudofunctor.StrongTrans.ModificationstructureMathlib.CategoryTheory.Bicategory.Modification.Pseudo, type

Wording

modification of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be homomorphisms of $F$ and $G$. Then the modifications of $x_{2}$ and $x_{3}$ are a basic type.

CategoryTheory.Pseudofunctor.StrongTrans.Modification.appdefMathlib.CategoryTheory.Bicategory.Modification.Pseudo, function or constant

Wording

the modification of self and a (from the name)

English

CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplaxdefMathlib.CategoryTheory.Bicategory.Modification.Pseudo, function or constant

Wording

the equivalence oplax (from the name)

English

The equivalence oplax is an equivalence from the set of modifications of the oplax of $x_{2}$ and the oplax of $x_{3}$ to the set of modifications of $x_{2}$ and $x_{3}$.

CategoryTheory.Pseudofunctor.StrongTrans.Modification.iddefMathlib.CategoryTheory.Bicategory.Modification.Pseudo, function or constant

Wording

the identity modification of x2 (from the docstring)

English

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

CategoryTheory.Pseudofunctor.StrongTrans.Modification.mkOfOplaxdefMathlib.CategoryTheory.Bicategory.Modification.Pseudo, function or constant

Wording

no wording

English

Let $x_{4}$ be a modification of the oplax of $x_{2}$ and the oplax of $x_{3}$. Then $\operatorname{mkOfOplax}$ applied to $x_{4}$ is a modification of $x_{2}$ and $x_{3}$.

CategoryTheory.Pseudofunctor.StrongTrans.Modification.toOplaxdefMathlib.CategoryTheory.Bicategory.Modification.Pseudo, function or constant

Wording

the oplax of x4 (from the name)

English

Let $x_{4}$ be a modification of $x_{2}$ and $x_{3}$. Then the oplax of $x_{4}$ is a modification of the oplax of $x_{2}$ and the oplax of $x_{3}$.

CategoryTheory.Pseudofunctor.StrongTrans.Modification.vcompdefMathlib.CategoryTheory.Bicategory.Modification.Pseudo, function or constant

Wording

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

English

CategoryTheory.Pseudofunctor.StrongTrans.isoMkdefMathlib.CategoryTheory.Bicategory.Modification.Pseudo, function or constant

Wording

the isomorphism of app and a1 (from the name)

English

Let $\mathrm{app}$ be a function from elements $a_{1}$ of $B$ to isomorphisms of the strong composition of $x_{2}$ and $a_{1}$ and the strong composition of $x_{3}$ and $a_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $a$ and $b$ of $B$, for all homomorphisms $f$ of $a$ and $b$, the composition of the left whisker of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the homomorphism of $\mathrm{app}$ applied to $b$ and the homomorphism of the naturality of $x_{3}$ and $f$ is equal to the composition of the homomorphism of the naturality of $x_{2}$ and $f$ and the right whisker of the homomorphism of $\mathrm{app}$ applied to $a$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $f$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_StrongTrans\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $a_{1}$ and $\mathrm{app}$ is an isomorphism of $x_{2}$ and $x_{3}$.

Mathlib.CategoryTheory.Bicategory.Monad.Basic

CategoryTheory.Bicategory.ComonaddefMathlib.CategoryTheory.Bicategory.Monad.Basic, type

Wording

comonad of t (from the name)

English

Let $t$ be a homomorphism of $a$ and $a$. Then a comonad of $t$ is an element of the function that maps $t$ to the proposition that $t$ is a comonoid object.

CategoryTheory.Bicategory.Comonad.comuldefMathlib.CategoryTheory.Bicategory.Monad.Basic, function or constant

Wording

no wording

English

$\operatorname{comul}$ is a homomorphism of $t$ and the composition of $t$ and $t$ defined as the comultiplication morphism.

CategoryTheory.Bicategory.Comonad.counitdefMathlib.CategoryTheory.Bicategory.Monad.Basic, function or constant

Wording

the counit (from the name)

English

The counit is a homomorphism of $t$ and the identity morphism of $a$ defined as the counit morphism.

CategoryTheory.Bicategory.Comonad.toOplaxdefMathlib.CategoryTheory.Bicategory.Monad.Basic, function or constant

Wording

the oplax of t (from the name)

English

Let $t$ be a homomorphism of $a$ and $a$. Then the oplax of $t$ is an oplax functor of $\operatorname{LocallyDiscrete}$ applied to $\operatorname{Discrete}$ applied to $\mathrm{Unit}$ and $B$.

CategoryTheory.Bicategory.OplaxTrans.ComonadBicatdefMathlib.CategoryTheory.Bicategory.Monad.Basic, type

Wording

no wording

English

Let $B$ be a set. Then an element of $\operatorname{ComonadBicat}$ applied to $B$ is an element of the function that maps $B$ to the set of oplax functors of $\operatorname{LocallyDiscrete}$ applied to $\operatorname{Discrete}$ applied to $\mathrm{Unit}$ and $B$.

CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.homdefMathlib.CategoryTheory.Bicategory.Monad.Basic, function or constant

Wording

the homomorphism of m (from the name)

English

Let $m$ be an element of $\operatorname{ComonadBicat}$ applied to $B$. Then the homomorphism of $m$ is a homomorphism of the object in $m$ and the object in $m$ defined as the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to the oplax functor from the trivial bicategory to $m$ and the identity morphism of $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{unit}$.

CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonaddefMathlib.CategoryTheory.Bicategory.Monad.Basic, function or constant

Wording

no wording

English

Let $t$ be a homomorphism of $a$ and $a$. Then $\operatorname{mkOfComonad}$ applied to $t$ is an element of $\operatorname{ComonadBicat}$ applied to $B$ defined as the oplax of $t$.

CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.objdefMathlib.CategoryTheory.Bicategory.Monad.Basic, function or constant

Wording

the object in m (from the docstring)

English

Let $m$ be an element of $\operatorname{ComonadBicat}$ applied to $B$. Then the object in $m$ is an element of $B$ defined as the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to the oplax functor from the trivial bicategory to $m$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{unit}$.

CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.toOplaxdefMathlib.CategoryTheory.Bicategory.Monad.Basic, function or constant

Wording

the oplax functor from the trivial bicategory to m (from the docstring)

English

Let $m$ be an element of $\operatorname{ComonadBicat}$ applied to $B$. Then the oplax functor from the trivial bicategory to $m$ is an oplax functor of $\operatorname{LocallyDiscrete}$ applied to $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ and $B$ defined as $m$.

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

CategoryTheory.Lax.LaxTransstructureMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, type

Wording

no wording

English

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

CategoryTheory.Lax.LaxTrans.StrongCorestructureMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, type

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the elements of $\operatorname{StrongCore}$ applied to $x_{2}$ are a basic type.

CategoryTheory.Lax.LaxTrans.StrongCore.naturalitydefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the naturality of self and f (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{StrongCore}$ applied to $x_{2}$. Let $f$ be a homomorphism of $a$ and $b$. Then the naturality of $\mathrm{self}$ and $f$ is an isomorphism of the composition of $\operatorname{LaxTrans}$ applied to $x_{2}$ and $a$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $f$ and the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and $\operatorname{LaxTrans}$ applied to $x_{2}$ and $b$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $f$.

CategoryTheory.Lax.LaxTrans.appdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{LaxTrans}$ applied to $F$ and $G$. Let $a$ be an element of $B$. Then $\operatorname{LaxTrans}$ applied to $\mathrm{self}$ and $a$ is a homomorphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $a$ and the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

CategoryTheory.Lax.LaxTrans.iddefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the identity of F (from the name)

English

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

CategoryTheory.Lax.LaxTrans.naturalitydefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the naturality of self and f (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{LaxTrans}$ applied to $F$ and $G$. Let $f$ be a homomorphism of $a$ and $b$. Then the naturality of $\mathrm{self}$ and $f$ is a homomorphism of the composition of $\operatorname{LaxTrans}$ applied to $\mathrm{self}$ and $a$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $f$ and the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and $\operatorname{LaxTrans}$ applied to $\mathrm{self}$ and $b$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $f$.

CategoryTheory.Lax.LaxTrans.vCompdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the composition of x2 and x3 (from the name)

English

Let $x_{2}$ be an element of $\operatorname{LaxTrans}$ applied to $F$ and $G$. Let $x_{3}$ be an element of $\operatorname{LaxTrans}$ applied to $G$ and $H$. Then the composition of $x_{2}$ and $x_{3}$ is an element of $\operatorname{LaxTrans}$ applied to $F$ and $H$ defined as $\operatorname{mk}$ applied to the function that maps $a$ to $\operatorname{vCompApp}$ applied to $x_{2}$, $x_{3}$ and $a$, the function that maps $x_{4}$ and $x_{5}$ to $\operatorname{vCompNaturality}$ applied to $x_{2}$ and $x_{3}$, the function that maps $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ to $\mathrm{CategoryTheory\_\_Lax\_\_LaxTrans\_\_vComp\_naturality\_naturality}$ applied to $x_{2}$ and $x_{3}$, $\mathrm{CategoryTheory\_\_Lax\_\_LaxTrans\_\_vComp\_naturality\_id}$ applied to $x_{2}$ and $x_{3}$ and the function that maps $x_{10}$, $x_{11}$ and $x_{12}$ to $\mathrm{CategoryTheory\_\_Lax\_\_LaxTrans\_\_vComp\_naturality\_comp}$ applied to $x_{2}$ and $x_{3}$.

CategoryTheory.Lax.OplaxTransstructureMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, type

Wording

oplax composition of F and G (from the name)

English

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

CategoryTheory.Lax.OplaxTrans.appdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the oplax composition of self and a (from the name)

English

Let $\mathrm{self}$ be an oplax composition of $F$ and $G$. Let $a$ be an element of $B$. Then the oplax composition of $\mathrm{self}$ and $a$ is a homomorphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $a$ and the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

CategoryTheory.Lax.OplaxTrans.iddefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the identity oplax transformation of F (from the docstring)

English

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

CategoryTheory.Lax.OplaxTrans.naturalitydefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the naturality of self and f (from the name)

English

Let $\mathrm{self}$ be an oplax composition of $F$ and $G$. Let $f$ be a homomorphism of $a$ and $b$. Then the naturality of $\mathrm{self}$ and $f$ 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 oplax composition of $\mathrm{self}$ and $b$ and the composition of the oplax composition of $\mathrm{self}$ and $a$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $f$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $f$.

CategoryTheory.Lax.OplaxTrans.vCompdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the composition of x2 and x3 (from the name)

English

Let $x_{2}$ be an oplax composition of $F$ and $G$. Let $x_{3}$ be an oplax composition of $G$ and $H$. Then the composition of $x_{2}$ and $x_{3}$ is an oplax composition of $F$ and $H$ defined as $\operatorname{mk}$ applied to $\operatorname{vCompApp}$ applied to $x_{2}$ and $x_{3}$, the function that maps $x_{4}$ and $x_{5}$ to $\operatorname{vCompNaturality}$ applied to $x_{2}$ and $x_{3}$, the function that maps $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ to $\mathrm{CategoryTheory\_\_Lax\_\_OplaxTrans\_\_vComp\_naturality\_naturality}$ applied to $x_{2}$ and $x_{3}$, $\mathrm{CategoryTheory\_\_Lax\_\_OplaxTrans\_\_vComp\_naturality\_id}$ applied to $x_{2}$ and $x_{3}$ and the function that maps $x_{10}$, $x_{11}$ and $x_{12}$ to $\mathrm{CategoryTheory\_\_Lax\_\_OplaxTrans\_\_vComp\_naturality\_comp}$ applied to $x_{2}$ and $x_{3}$.

CategoryTheory.Lax.StrongTransstructureMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, type

Wording

strong composition of F and G (from the name)

English

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

CategoryTheory.Lax.StrongTrans.appdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the strong composition of self and a (from the name)

English

Let $\mathrm{self}$ be a strong composition of $F$ and $G$. Let $a$ be an element of $B$. Then the strong composition of $\mathrm{self}$ and $a$ is a homomorphism of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $a$ and the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

CategoryTheory.Lax.StrongTrans.iddefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the identity strong natural transformation of F (from the docstring)

English

Let $F$ be an element of $\operatorname{LaxFunctor}$ applied to $B$ and $C$. Then the identity strong natural transformation of $F$ is a strong composition of $F$ and $F$.

CategoryTheory.Lax.StrongTrans.mkOfLaxdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $\operatorname{LaxTrans}$ applied to $F$ and $G$. Let $x_{3}$ be an element of $\operatorname{StrongCore}$ applied to $x_{2}$. Then $\operatorname{mkOfLax}$ applied to $x_{2}$ and $x_{3}$ is a strong composition of $F$ and $G$.

CategoryTheory.Lax.StrongTrans.mkOfLax'defMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $\operatorname{LaxTrans}$ applied to $F$ and $G$. Then $\operatorname{mkOfLax'}$ applied to $x_{2}$ is a strong composition of $F$ and $G$.

CategoryTheory.Lax.StrongTrans.naturalitydefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the naturality of self and f (from the name)

English

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

CategoryTheory.Lax.StrongTrans.toLaxdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

no wording

English

Let $x_{2}$ be a strong composition of $F$ and $G$. Then $\operatorname{toLax}$ applied to $x_{2}$ is an element of $\operatorname{LaxTrans}$ applied to $F$ and $G$.

CategoryTheory.Lax.StrongTrans.vCompdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax, function or constant

Wording

the composition of x2 and x3 (from the name)

English

Let $x_{2}$ be a strong composition of $F$ and $G$. Let $x_{3}$ be a strong composition of $G$ and $H$. Then the composition of $x_{2}$ and $x_{3}$ is a strong composition of $F$ and $H$.

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

CategoryTheory.Oplax.LaxTransstructureMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, type

Wording

no wording

English

Let $F$ and $G$ be oplax functors of $B$ and $C$. Then the elements of $\operatorname{LaxTrans}$ applied to $F$ and $G$ are a basic type.

CategoryTheory.Oplax.LaxTrans.appdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

no wording

English

CategoryTheory.Oplax.LaxTrans.iddefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

the identity of F (from the name)

English

Let $F$ be an oplax functor of $B$ and $C$. Then the identity of $F$ is an element of $\operatorname{LaxTrans}$ applied to $F$ and $F$.

CategoryTheory.Oplax.LaxTrans.naturalitydefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

the naturality of self and f (from the name)

English

CategoryTheory.Oplax.LaxTrans.vCompdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

the composition of x2 and x3 (from the name)

English

Let $x_{2}$ be an element of $\operatorname{LaxTrans}$ applied to $F$ and $G$. Let $x_{3}$ be an element of $\operatorname{LaxTrans}$ applied to $G$ and $H$. Then the composition of $x_{2}$ and $x_{3}$ is an element of $\operatorname{LaxTrans}$ applied to $F$ and $H$ defined as $\operatorname{mk}$ applied to the function that maps $a$ to $\operatorname{vCompApp}$ applied to $x_{2}$, $x_{3}$ and $a$, the function that maps $x_{4}$ and $x_{5}$ to $\operatorname{vCompNaturality}$ applied to $x_{2}$ and $x_{3}$, the function that maps $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ to $\mathrm{CategoryTheory\_\_Oplax\_\_LaxTrans\_\_vComp\_naturality\_naturality}$ applied to $x_{2}$ and $x_{3}$, $\mathrm{CategoryTheory\_\_Oplax\_\_LaxTrans\_\_vComp\_naturality\_id}$ applied to $x_{2}$ and $x_{3}$ and the function that maps $x_{10}$, $x_{11}$ and $x_{12}$ to $\mathrm{CategoryTheory\_\_Oplax\_\_LaxTrans\_\_vComp\_naturality\_comp}$ applied to $x_{2}$ and $x_{3}$.

CategoryTheory.Oplax.OplaxTransstructureMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, type

Wording

oplax composition of F and G (from the name)

English

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

CategoryTheory.Oplax.OplaxTrans.StrongCorestructureMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, type

Wording

no wording

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the elements of $\operatorname{StrongCore}$ applied to $x_{2}$ are a basic type.

CategoryTheory.Oplax.OplaxTrans.StrongCore.naturalitydefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

the naturality of self and f (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{StrongCore}$ applied to $x_{2}$. Let $f$ be a homomorphism of $a$ and $b$. Then the naturality of $\mathrm{self}$ and $f$ is an isomorphism of the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$ and the oplax composition of $x_{2}$ and $b$ and the composition of the oplax composition of $x_{2}$ and $a$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $G$ and $f$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $f$.

CategoryTheory.Oplax.OplaxTrans.appdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

the oplax composition of self and a (from the name)

English

CategoryTheory.Oplax.OplaxTrans.iddefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

the identity oplax transformation of F (from the docstring)

English

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

CategoryTheory.Oplax.OplaxTrans.naturalitydefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

the naturality of self and f (from the name)

English

CategoryTheory.Oplax.OplaxTrans.vcompdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

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

English

Let $x_{2}$ be an oplax composition of $F$ and $G$. Let $x_{3}$ be an oplax composition of $G$ and $H$. Then the vertical composition of $x_{2}$ and $x_{3}$ is an oplax composition of $F$ and $H$.

CategoryTheory.Oplax.StrongTransstructureMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, type

Wording

strong composition of F and G (from the name)

English

Let $F$ and $G$ be oplax functors of $B$ and $C$. Then the strong compositions of $F$ and $G$ are a basic type.

CategoryTheory.Oplax.StrongTrans.appdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

the strong composition of self and a (from the name)

English

CategoryTheory.Oplax.StrongTrans.iddefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

the identity strong natural transformation of F (from the docstring)

English

Let $F$ be an oplax functor of $B$ and $C$. Then the identity strong natural transformation of $F$ is a strong composition of $F$ and $F$.

CategoryTheory.Oplax.StrongTrans.mkOfOplaxdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

no wording

English

Let $x_{2}$ be an oplax composition of $F$ and $G$. Let $x_{3}$ be an element of $\operatorname{StrongCore}$ applied to $x_{2}$. Then $\operatorname{mkOfOplax}$ applied to $x_{2}$ and $x_{3}$ is a strong composition of $F$ and $G$.

CategoryTheory.Oplax.StrongTrans.mkOfOplax'defMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

no wording

English

Let $x_{2}$ be an oplax composition of $F$ and $G$. Then $\operatorname{mkOfOplax'}$ applied to $x_{2}$ is a strong composition of $F$ and $G$.

CategoryTheory.Oplax.StrongTrans.naturalitydefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

the naturality of self and f (from the name)

English

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

CategoryTheory.Oplax.StrongTrans.toOplaxdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

the underlying oplax natural transformation of x2 (from the docstring)

English

Let $x_{2}$ be a strong composition of $F$ and $G$. Then the underlying oplax natural transformation of $x_{2}$ is an oplax composition of $F$ and $G$.

CategoryTheory.Oplax.StrongTrans.vcompdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax, function or constant

Wording

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

English

Let $x_{2}$ be a strong composition of $F$ and $G$. Let $x_{3}$ be a strong composition of $G$ and $H$. Then the vertical composition of $x_{2}$ and $x_{3}$ is a strong composition of $F$ and $H$.

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

CategoryTheory.Pseudofunctor.StrongTransstructureMathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo, type

Wording

strong composition of F and G (from the name)

English

Let $F$ and $G$ be pseudofunctors of $B$ and $C$. Then the strong compositions of $F$ and $G$ are a basic type.

CategoryTheory.Pseudofunctor.StrongTrans.appdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo, function or constant

Wording

the strong composition of self and a (from the name)

English

CategoryTheory.Pseudofunctor.StrongTrans.iddefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo, function or constant

Wording

the identity strong transformation of F (from the docstring)

English

Let $F$ be a pseudofunctor of $B$ and $C$. Then the identity strong transformation of $F$ is a strong composition of $F$ and $F$.

CategoryTheory.Pseudofunctor.StrongTrans.mkOfOplaxdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo, function or constant

Wording

no wording

English

Let $x_{2}$ be a strong composition of the oplax functor associated with a pseudofunctor of $F$ and the oplax functor associated with a pseudofunctor of $G$. Then $\operatorname{mkOfOplax}$ applied to $x_{2}$ is a strong composition of $F$ and $G$.

CategoryTheory.Pseudofunctor.StrongTrans.naturalitydefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo, function or constant

Wording

the naturality of self and f (from the name)

English

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

CategoryTheory.Pseudofunctor.StrongTrans.toOplaxdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo, function or constant

Wording

the oplax of x2 (from the name)

English

Let $x_{2}$ be a strong composition of $F$ and $G$. Then the oplax of $x_{2}$ is a strong composition of the oplax functor associated with a pseudofunctor of $F$ and the oplax functor associated with a pseudofunctor of $G$.

CategoryTheory.Pseudofunctor.StrongTrans.vcompdefMathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo, function or constant

Wording

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

English

Let $x_{2}$ be a strong composition of $F$ and $G$. Let $x_{3}$ be a strong composition of $G$ and $H$. Then the vertical composition of $x_{2}$ and $x_{3}$ is a strong composition of $F$ and $H$ defined as $\operatorname{mkOfOplax}$ applied to the vertical composition of the oplax of $x_{2}$ and the oplax of $x_{3}$.

Mathlib.CategoryTheory.Bicategory.Opposites

Bicategory.Opposite.Hom2structureMathlib.CategoryTheory.Bicategory.Opposites, type

Wording

homomorphism of f and g (from the name)

English

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

Bicategory.Opposite.Hom2.unop2defMathlib.CategoryTheory.Bicategory.Opposites, function or constant

Wording

the opposite of self (from the name)

English

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

Bicategory.Opposite.op2defMathlib.CategoryTheory.Bicategory.Opposites, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be a homomorphism of $f$ and $g$. Then the opposite of $x_{1}$ is a homomorphism of the opposite in $f$ and the opposite in $g$ defined as $\operatorname{op2'}$ applied to $x_{1}$.

Bicategory.Opposite.opFunctordefMathlib.CategoryTheory.Bicategory.Opposites, function or constant

Wording

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

English

Let $a$ and $b$ be elements of $B$. Then the opposite functor of $a$ and $b$ is a functor of the set of homomorphisms of $a$ and $b$ and the set of homomorphisms of $\operatorname{op}$ applied to $b$ and $\operatorname{op}$ applied to $a$.

Bicategory.Opposite.unopFunctordefMathlib.CategoryTheory.Bicategory.Opposites, function or constant

Wording

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

English

Let $a$ and $b$ be opposites of $B$. Then the opposite functor of $a$ and $b$ is a functor of the set of homomorphisms of $a$ and $b$ and the set of homomorphisms of the opposite of $b$ and the opposite of $a$.

CategoryTheory.Iso.op2defMathlib.CategoryTheory.Bicategory.Opposites, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be an isomorphism of $f$ and $g$. Then the opposite of $x_{1}$ is an isomorphism of the opposite in $f$ and the opposite in $g$ defined as the map isomorphism of the opposite functor of $a$ and $b$ and $x_{1}$.

CategoryTheory.Iso.op2_unopdefMathlib.CategoryTheory.Bicategory.Opposites, function or constant

Wording

the opposite opposite of x1 (from the name)

English

Let $x_{1}$ be an isomorphism of the opposite of $f$ and the opposite of $g$. Then the opposite opposite of $x_{1}$ is an isomorphism of $f$ and $g$ defined as the map isomorphism of the opposite functor of the opposite of $b$ and the opposite of $a$ and $x_{1}$.

CategoryTheory.Iso.unop2defMathlib.CategoryTheory.Bicategory.Opposites, function or constant

Wording

the opposite of x1 (from the name)

English

Let $x_{1}$ be an isomorphism of $f$ and $g$. Then the opposite of $x_{1}$ is an isomorphism of the opposite of $f$ and the opposite of $g$ defined as the map isomorphism of the opposite functor of $a$ and $b$ and $x_{1}$.

CategoryTheory.Iso.unop2_opdefMathlib.CategoryTheory.Bicategory.Opposites, function or constant

Wording

the opposite opposite of x1 (from the name)

English

Let $x_{1}$ be an isomorphism of the opposite in $f$ and the opposite in $g$. Then the opposite opposite of $x_{1}$ is an isomorphism of $f$ and $g$ defined as the map isomorphism of the opposite functor of $\operatorname{op}$ applied to $b$ and $\operatorname{op}$ applied to $a$ and $x_{1}$.

Mathlib.CategoryTheory.Bicategory.Product

CategoryTheory.Bicategory.Prod.fstdefMathlib.CategoryTheory.Bicategory.Product, function or constant

Wording

the first component of B and C (from the name)

English

Let $B$ and $C$ be sets. Then the first component of $B$ and $C$ is a strict pseudofunctor of $\mathrm{Prod}$ applied to $B$ and $C$ and $B$.

CategoryTheory.Bicategory.Prod.sectLdefMathlib.CategoryTheory.Bicategory.Product, function or constant

Wording

no wording

English

generation took over the time limit

CategoryTheory.Bicategory.Prod.sectRdefMathlib.CategoryTheory.Bicategory.Product, function or constant

Wording

no wording

English

generation took over the time limit

CategoryTheory.Bicategory.Prod.snddefMathlib.CategoryTheory.Bicategory.Product, function or constant

Wording

the second component of B and C (from the name)

English

Let $B$ and $C$ be sets. Then the second component of $B$ and $C$ is a strict pseudofunctor of $\mathrm{Prod}$ applied to $B$ and $C$ and $C$.

CategoryTheory.Bicategory.Prod.swapdefMathlib.CategoryTheory.Bicategory.Product, function or constant

Wording

the swap of B and C (from the name)

English

Let $B$ and $C$ be sets. Then the swap of $B$ and $C$ is a strict pseudofunctor of $\mathrm{Prod}$ applied to $B$ and $C$ and $\mathrm{Prod}$ applied to $C$ and $B$.

Mathlib.CategoryTheory.Bicategory.RetractArrow

CategoryTheory.Bicategory.RetractArrow₁structureMathlib.CategoryTheory.Bicategory.RetractArrow, type

Wording

retract arrow of f and #2 (from the name)

English

Let $\mathrm{f'}$ be a homomorphism of $\mathrm{X'}$ and $\mathrm{Y'}$. Let $f$ be a homomorphism of $X$ and $Y$. Then the retract arrows of $\mathrm{f'}$ and $f$ are a basic type.

CategoryTheory.Bicategory.RetractArrow₁.commidefMathlib.CategoryTheory.Bicategory.RetractArrow, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a retract arrow of $\mathrm{f'}$ and $f$. Then $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_commi}$ applied to $\mathrm{self}$ is an isomorphism of the composition of $\mathrm{f'}$ and $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_i\_u2082\_}$ applied to $\mathrm{self}$ and the composition of $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_i\_u2081\_}$ applied to $\mathrm{self}$ and $f$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_proj6}$ applied to $\mathrm{self}$.

CategoryTheory.Bicategory.RetractArrow₁.commrdefMathlib.CategoryTheory.Bicategory.RetractArrow, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a retract arrow of $\mathrm{f'}$ and $f$. Then $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_commr}$ applied to $\mathrm{self}$ is an isomorphism of the composition of $f$ and $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_r\_u2082\_}$ applied to $\mathrm{self}$ and the composition of $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_r\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{f'}$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_proj7}$ applied to $\mathrm{self}$.

CategoryTheory.Bicategory.RetractArrow₁.equivalencedefMathlib.CategoryTheory.Bicategory.RetractArrow, function or constant

Wording

the equivalence of r (from the name)

English

Let $r$ be a retract arrow of $\mathrm{f'}$ and the homomorphism of $f$. Then the equivalence of $r$ is an equivalence of $\mathrm{X'}$ and $\mathrm{Y'}$.

CategoryTheory.Bicategory.RetractArrow₁.id₁defMathlib.CategoryTheory.Bicategory.RetractArrow, function or constant

Wording

the identity of self (from the name)

English

Let $\mathrm{self}$ be a retract arrow of $\mathrm{f'}$ and $f$. Then the identity of $\mathrm{self}$ is an isomorphism of the composition of $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_i\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_r\_u2081\_}$ applied to $\mathrm{self}$ and the identity morphism of $\mathrm{X'}$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_proj4}$ applied to $\mathrm{self}$.

CategoryTheory.Bicategory.RetractArrow₁.id₂defMathlib.CategoryTheory.Bicategory.RetractArrow, function or constant

Wording

the identity of self (from the name)

English

Let $\mathrm{self}$ be a retract arrow of $\mathrm{f'}$ and $f$. Then the identity of $\mathrm{self}$ is an isomorphism of the composition of $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_i\_u2082\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_r\_u2082\_}$ applied to $\mathrm{self}$ and the identity morphism of $\mathrm{Y'}$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_proj5}$ applied to $\mathrm{self}$.

CategoryTheory.Bicategory.RetractArrow₁.i₁defMathlib.CategoryTheory.Bicategory.RetractArrow, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a retract arrow of $\mathrm{f'}$ and $f$. Then $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_i\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{X'}$ and $X$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Bicategory.RetractArrow₁.i₂defMathlib.CategoryTheory.Bicategory.RetractArrow, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a retract arrow of $\mathrm{f'}$ and $f$. Then $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_i\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{Y'}$ and $Y$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_proj2}$ applied to $\mathrm{self}$.

CategoryTheory.Bicategory.RetractArrow₁.mapdefMathlib.CategoryTheory.Bicategory.RetractArrow, function or constant

Wording

the map of r and F (from the name)

English

Let $r$ be a retract arrow of $\mathrm{f'}$ and $f$. Let $F$ be a pseudofunctor of $C$ and $D$. Then the map of $r$ and $F$ is a retract arrow of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\mathrm{f'}$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $f$.

CategoryTheory.Bicategory.RetractArrow₁.r₁defMathlib.CategoryTheory.Bicategory.RetractArrow, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a retract arrow of $\mathrm{f'}$ and $f$. Then $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_r\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $X$ and $\mathrm{X'}$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Bicategory.RetractArrow₁.r₂defMathlib.CategoryTheory.Bicategory.RetractArrow, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a retract arrow of $\mathrm{f'}$ and $f$. Then $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_r\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of $Y$ and $\mathrm{Y'}$ defined as $\mathrm{CategoryTheory\_\_Bicategory\_\_RetractArrow\_u2081\_\_\_proj3}$ applied to $\mathrm{self}$.

CategoryTheory.RetractArrow.toLocdefMathlib.CategoryTheory.Bicategory.RetractArrow, function or constant

Wording

no wording

English

Let $r$ be a retract arrow of $\mathrm{f'}$ and $f$. Then $\operatorname{toLoc}$ applied to $r$ is a retract arrow of $\operatorname{toLoc}$ applied to $\mathrm{f'}$ and $\operatorname{toLoc}$ applied to $f$.

Mathlib.CategoryTheory.Bicategory.SingleObj

CategoryTheory.MonoidalSingleObjdefMathlib.CategoryTheory.Bicategory.SingleObj, type

Wording

monoidal single object of C (from the name)

English

Let $C$ be a set. Then a monoidal single object of $C$ is an element of the function that maps $C$ to $\mathrm{Unit}$.

CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctordefMathlib.CategoryTheory.Bicategory.SingleObj, function or constant

Wording

the end monoidal star functor of C (from the name)

English

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

CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalencedefMathlib.CategoryTheory.Bicategory.SingleObj, function or constant

Wording

the end monoidal star functor equivalence of C (from the name)

English

Let $C$ be a set. Then the end monoidal star functor equivalence of $C$ is an equivalence of $\operatorname{EndMonoidal}$ applied to the star of $C$ and $C$.

CategoryTheory.MonoidalSingleObj.stardefMathlib.CategoryTheory.Bicategory.SingleObj, function or constant

Wording

the star of C (from the name)

English

Let $C$ be a set. Then the star of $C$ is a monoidal single object of $C$ defined as $\operatorname{unit}$.

Mathlib.CategoryTheory.Bicategory.Span.Basic

CategoryTheory.SpanstructureMathlib.CategoryTheory.Bicategory.Span.Basic, type

Wording

span of c and #4 (from the name)

English

Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Let $c$ and $\mathrm{c'}$ be elements of $C$. Then the spans of $c$ and $\mathrm{c'}$ are a basic type.

CategoryTheory.Span.HomstructureMathlib.CategoryTheory.Bicategory.Span.Basic, type

Wording

homomorphism of x3 and x4 (from the name)

English

Let $x_{3}$ and $x_{4}$ be spans of $c$ and $\mathrm{c'}$. Then the homomorphisms of $x_{3}$ and $x_{4}$ are a basic type.

CategoryTheory.Span.Hom.homdefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the homomorphism of self (from the name)

English

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

CategoryTheory.Span.SpanBicatstructureMathlib.CategoryTheory.Bicategory.Span.Basic, type

Wording

no wording

English

Let $C$ be a set. Let $x_{1}$ and $x_{2}$ be morphism properties of $C$. Then the elements of $\operatorname{SpanBicat}$ applied to $C$, $x_{1}$ and $x_{2}$ are a basic type.

CategoryTheory.Span.SpanBicat.apexIsodefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the apex isomorphism of e (from the name)

English

Let $e$ be an isomorphism of $S$ and $\mathrm{S'}$. Then the apex isomorphism of $e$ is an isomorphism of the apex of the span of $S$ and the apex of the span of $\mathrm{S'}$.

CategoryTheory.Span.SpanBicat.associatordefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the associator of x8 and x9 (from the name)

English

Let $x_{7}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $x_{8}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{9}$ be a homomorphism of $x_{5}$ and $x_{6}$. Then the associator of $x_{8}$ and $x_{9}$ is an isomorphism of the composition of the composition of $x_{7}$ and $x_{8}$ and $x_{9}$ and the composition of $x_{7}$ and the composition of $x_{8}$ and $x_{9}$.

CategoryTheory.Span.SpanBicat.compLiftdefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the composition lift of x5 and x6 (from the name)

English

Let $x_{5}$ be a homomorphism of the apex of the span of $S$ and the apex of the span of $x_{3}$. Let $x_{6}$ be a homomorphism of the apex of the span of $S$ and the apex of the span of $x_{4}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{5}$ and $\operatorname{l}$ applied to $x_{3}$ is equal to $\operatorname{l}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Span\_\_SpanBicat\_\_compLift\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{5}$ and $\operatorname{r}$ applied to $x_{3}$ is equal to the composition of $x_{6}$ and $\operatorname{l}$ applied to $x_{4}$ and $\mathrm{CategoryTheory\_\_Span\_\_SpanBicat\_\_compLift\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{6}$ and $\operatorname{r}$ applied to $x_{4}$ is equal to $\operatorname{r}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Span\_\_SpanBicat\_\_compLift\_\_\_auto\_5}$. Then the composition lift of $x_{5}$ and $x_{6}$ is a homomorphism of $S$ and the composition of $x_{3}$ and $x_{4}$.

CategoryTheory.Span.SpanBicat.compLiftApexdefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the composition lift apex of x5 and x6 (from the name)

English

Let $x_{5}$ be a homomorphism of $c$ and the apex of the span of $x_{3}$. Let $x_{6}$ be a homomorphism of $c$ and the apex of the span of $x_{4}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{5}$ and $\operatorname{r}$ applied to $x_{3}$ is equal to the composition of $x_{6}$ and $\operatorname{l}$ applied to $x_{4}$ and $\mathrm{CategoryTheory\_\_Span\_\_SpanBicat\_\_compLiftApex\_\_\_auto\_1}$. Then the composition lift apex of $x_{5}$ and $x_{6}$ is a homomorphism of $c$ and the apex of the span of the composition of $x_{3}$ and $x_{4}$ defined as the lift of $x_{5}$ and $x_{6}$.

CategoryTheory.Span.SpanBicat.compPullbackConedefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the composition pullback cone of x3 and x4 (from the name)

English

Let $x_{3}$ be a homomorphism of $X$ and $Y$. Let $x_{4}$ be a homomorphism of $Y$ and $Z$. Then the composition pullback cone of $x_{3}$ and $x_{4}$ is a pullback cone of $\operatorname{r}$ applied to $x_{3}$ and $\operatorname{l}$ applied to $x_{4}$ defined as $\operatorname{mk}$ applied to the left projection of $x_{3}$ and $x_{4}$, the right projection of $x_{3}$ and $x_{4}$ and $\mathrm{CategoryTheory\_\_Span\_\_SpanBicat\_\_comp\_comm}$ applied to $x_{3}$ and $x_{4}$.

CategoryTheory.Span.SpanBicat.isLimitCompPullbackConedefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

no wording

English

Let $x_{3}$ be a homomorphism of $X$ and $Y$. Let $x_{4}$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{isLimitCompPullbackCone}$ applied to $x_{3}$ and $x_{4}$ is an element of $\operatorname{IsLimit}$ applied to the composition pullback cone of $x_{3}$ and $x_{4}$.

CategoryTheory.Span.SpanBicat.leftUnitordefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the left unitor of x3 (from the name)

English

Let $x_{3}$ be a homomorphism of $c$ and $\mathrm{c'}$. Then the left unitor of $x_{3}$ is an isomorphism of the composition of the identity morphism of $c$ and $x_{3}$ and $x_{3}$.

CategoryTheory.Span.SpanBicat.mkHomdefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the homomorphism of l and r (from the name)

English

Let $l$ be a homomorphism of $\mathrm{apex}$ and $\operatorname{of}$ applied to $X$. Let $r$ be a homomorphism of $\mathrm{apex}$ and $\operatorname{of}$ applied to $Y$. Assume that $x_{1}$ holds for $\mathrm{apex}$, $\operatorname{of}$ applied to $X$ and $l$. Assume that $x_{2}$ holds for $\mathrm{apex}$, $\operatorname{of}$ applied to $Y$ and $r$. Then the homomorphism of $l$ and $r$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\mathrm{apex}$, $l$, $r$, $\mathrm{wl}$ and $\mathrm{wr}$.

CategoryTheory.Span.SpanBicat.mkHom₂defMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the homomorphism of e (from the name)

English

Let $e$ be a homomorphism of the apex of the span of $S$ and the apex of the span of $\mathrm{S'}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of $e$ and $\operatorname{l}$ applied to $\mathrm{S'}$ is equal to $\operatorname{l}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Span\_\_SpanBicat\_\_mkHom\_u2082\_\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of $e$ and $\operatorname{r}$ applied to $\mathrm{S'}$ is equal to $\operatorname{r}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Span\_\_SpanBicat\_\_mkHom\_u2082\_\_\_\_auto\_3}$. Then the homomorphism of $e$ is a homomorphism of $S$ and $\mathrm{S'}$.

CategoryTheory.Span.SpanBicat.mkIso₂defMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the isomorphism of e (from the name)

English

Let $e$ be an isomorphism of the apex of the span of $S$ and the apex of the span of $\mathrm{S'}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $e$ and $\operatorname{l}$ applied to $\mathrm{S'}$ is equal to $\operatorname{l}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Span\_\_SpanBicat\_\_mkIso\_u2082\_\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $e$ and $\operatorname{r}$ applied to $\mathrm{S'}$ is equal to $\operatorname{r}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Span\_\_SpanBicat\_\_mkIso\_u2082\_\_\_\_auto\_3}$. Then the isomorphism of $e$ is an isomorphism of $S$ and $\mathrm{S'}$.

CategoryTheory.Span.SpanBicat.ofdefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

no wording

English

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

CategoryTheory.Span.SpanBicat.rightUnitordefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the right unitor of x3 (from the name)

English

Let $x_{3}$ be a homomorphism of $c$ and $\mathrm{c'}$. Then the right unitor of $x_{3}$ is an isomorphism of the composition of $x_{3}$ and the identity morphism of $\mathrm{c'}$ and $x_{3}$.

CategoryTheory.Span.SpanBicat.πᵣdefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the right projection of x3 and x4 (from the docstring)

English

Let $x_{3}$ be a homomorphism of $X$ and $Y$. Let $x_{4}$ be a homomorphism of $Y$ and $Z$. Then the right projection of $x_{3}$ and $x_{4}$ is a homomorphism of the apex of the span of the composition of $x_{3}$ and $x_{4}$ and the apex of the span of $x_{4}$ defined as the second projection of the pullback of $\operatorname{r}$ applied to $x_{3}$ and $\operatorname{l}$ applied to $x_{4}$.

CategoryTheory.Span.SpanBicat.πₗdefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the left projection of x3 and x4 (from the docstring)

English

Let $x_{3}$ be a homomorphism of $X$ and $Y$. Let $x_{4}$ be a homomorphism of $Y$ and $Z$. Then the left projection of $x_{3}$ and $x_{4}$ is a homomorphism of the apex of the span of the composition of $x_{3}$ and $x_{4}$ and the apex of the span of $x_{3}$ defined as the first projection of the pullback of $\operatorname{r}$ applied to $x_{3}$ and $\operatorname{l}$ applied to $x_{4}$.

CategoryTheory.Span.apexdefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the apex of the span of self (from the docstring)

English

Let $\mathrm{self}$ be a span of $c$ and $\mathrm{c'}$. Then the apex of the span of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Span.compdefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the composition of x3 and x4 (from the name)

English

Let $x_{3}$ be a span of $c$ and $\mathrm{c'}$. Let $x_{4}$ be a span of $\mathrm{c'}$ and $\mathrm{c''}$. Then the composition of $x_{3}$ and $x_{4}$ is a span of $c$ and $\mathrm{c''}$.

CategoryTheory.Span.iddefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the identity of c (from the name)

English

Let $c$ be an element of $C$. Then the identity of $c$ is a span of $c$ and $c$ defined as $\operatorname{mk}$ applied to $c$, the identity morphism of $c$, the identity morphism of $c$, $\mathrm{CategoryTheory\_\_MorphismProperty\_\_ContainsIdentities\_\_id\_mem}$ applied to $c$ and $\mathrm{CategoryTheory\_\_MorphismProperty\_\_ContainsIdentities\_\_id\_mem}$ applied to $c$.

CategoryTheory.Span.ldefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a span of $c$ and $\mathrm{c'}$. Then $\operatorname{l}$ applied to $\mathrm{self}$ is a homomorphism of the apex of the span of $\mathrm{self}$ and $c$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Span.mkIsodefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

the isomorphism of e (from the name)

English

Let $e$ be an isomorphism of the apex of the span of $S$ and the apex of the span of $\mathrm{S'}$ such that $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $e$ and $\operatorname{l}$ applied to $\mathrm{S'}$ is equal to $\operatorname{l}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Span\_\_mkIso\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that the composition of the homomorphism of $e$ and $\operatorname{r}$ applied to $\mathrm{S'}$ is equal to $\operatorname{r}$ applied to $S$ and $\mathrm{CategoryTheory\_\_Span\_\_mkIso\_\_\_auto\_3}$. Then the isomorphism of $e$ is an isomorphism of $S$ and $\mathrm{S'}$.

CategoryTheory.Span.rdefMathlib.CategoryTheory.Bicategory.Span.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a span of $c$ and $\mathrm{c'}$. Then $\operatorname{r}$ applied to $\mathrm{self}$ is a homomorphism of the apex of the span of $\mathrm{self}$ and $\mathrm{c'}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Mathlib.CategoryTheory.Bicategory.Strict.Basic

CategoryTheory.Bicategory.StrictclassMathlib.CategoryTheory.Bicategory.Strict.Basic, predicate

Wording

B is strict (from the name)

English

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

Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

CategoryTheory.Pseudofunctor.isoMapOfCommSqdefMathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor, function or constant

Wording

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

English

Let $F$ be a pseudofunctor of $B$ and $C$. Assume that $\operatorname{CommSq}$ holds for $t$, $l$, $r$ and $b$. Then the isomorphism map of $F$ and $\mathrm{sq}$ is an isomorphism of the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $t$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $r$ and the composition of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $l$ and the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $b$.

Mathlib.CategoryTheory.Bicategory.Yoneda

CategoryTheory.Bicategory.associatorNatIsoLeftCatdefMathlib.CategoryTheory.Bicategory.Yoneda, function or constant

Wording

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

English

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 associator natural isomorphism left category of $g$ and $h$ is an isomorphism of the composition of the action of $\operatorname{postcomposingCat}$ applied to $a$, $b$ and $c$ and $g$ and the action of $\operatorname{postcomposingCat}$ applied to $a$, $c$ and $d$ and $h$ and the action of $\operatorname{postcomposingCat}$ applied to $a$, $b$ and $d$ and the composition of $g$ and $h$.

CategoryTheory.Bicategory.associatorNatIsoMiddleCatdefMathlib.CategoryTheory.Bicategory.Yoneda, function or constant

Wording

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

English

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

CategoryTheory.Bicategory.associatorNatIsoRightCatdefMathlib.CategoryTheory.Bicategory.Yoneda, function or constant

Wording

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

English

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 associator natural isomorphism right category of $g$ and $d$ is an isomorphism of the action of $\operatorname{precomposingCat}$ applied to $a$, $c$ and $d$ and the composition of $f$ and $g$ and the composition of the action of $\operatorname{precomposingCat}$ applied to $b$, $c$ and $d$ and $g$ and the action of $\operatorname{precomposingCat}$ applied to $a$, $b$ and $d$ and $f$.

CategoryTheory.Bicategory.leftUnitorNatIsoCatdefMathlib.CategoryTheory.Bicategory.Yoneda, function or constant

Wording

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

English

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

CategoryTheory.Bicategory.postcomposingCatdefMathlib.CategoryTheory.Bicategory.Yoneda, function or constant

Wording

no wording

English

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

CategoryTheory.Bicategory.postcomposing₂defMathlib.CategoryTheory.Bicategory.Yoneda, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $B$. Then $\mathrm{CategoryTheory\_\_Bicategory\_\_postcomposing\_u2082\_}$ applied to $a$ and $b$ is a functor of the set of homomorphisms of $a$ and $b$ and the set of homomorphisms of the Yoneda of $a$ and the Yoneda of $b$.

CategoryTheory.Bicategory.postcomp₂defMathlib.CategoryTheory.Bicategory.Yoneda, function or constant

Wording

the postcomposition of f (from the name)

English

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

CategoryTheory.Bicategory.precomposingCatdefMathlib.CategoryTheory.Bicategory.Yoneda, function or constant

Wording

no wording

English

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

CategoryTheory.Bicategory.rightUnitorNatIsoCatdefMathlib.CategoryTheory.Bicategory.Yoneda, function or constant

Wording

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

English

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

CategoryTheory.Bicategory.yonedadefMathlib.CategoryTheory.Bicategory.Yoneda, function or constant

Wording

the Yoneda (from the name)

English

The Yoneda is a pseudofunctor of $B$ and the set of pseudofunctors of the set of opposites of $B$ and the set of categories.

CategoryTheory.Bicategory.yoneda₀defMathlib.CategoryTheory.Bicategory.Yoneda, function or constant

Wording

the Yoneda of x1 (from the name)

English

Let $x_{1}$ be an element of $B$. Then the Yoneda of $x_{1}$ is a pseudofunctor of the set of opposites of $B$ and the set of categories.

Mathlib.CategoryTheory.CatCommSq

CategoryTheory.CatCommSqclassMathlib.CategoryTheory.CatCommSq, predicate

Wording

no wording

English

Let $T$ be a functor of $x$ and $x_{1}$. Let $L$ be a functor of $x$ and $x_{2}$. Let $R$ be a functor of $x_{1}$ and $x_{3}$. Let $B$ be a functor of $x_{2}$ and $x_{3}$. Then we can say that $\operatorname{CatCommSq}$ holds for $T$, $L$, $R$ and $B$.

CategoryTheory.CatCommSq.hInvEquivdefMathlib.CategoryTheory.CatCommSq, function or constant

Wording

the inverse equivalence of R and B (from the name)

English

Let $T$ be an equivalence of $x$ and $x_{1}$. Let $L$ be a functor of $x$ and $x_{2}$. Let $R$ be a functor of $x_{1}$ and $x_{3}$. Let $B$ be an equivalence of $x_{2}$ and $x_{3}$. Then the inverse equivalence of $R$ and $B$ is an equivalence from $\operatorname{CatCommSq}$ applied to the functor of $T$, $L$, $R$ and the functor of $B$ to $\operatorname{CatCommSq}$ applied to the inverse of $T$, $R$, $L$ and the inverse of $B$.

CategoryTheory.CatCommSq.isodefMathlib.CategoryTheory.CatCommSq, function or constant

Wording

the isomorphism of R and B (from the name)

English

Let $T$ be a functor of $x$ and $x_{1}$. Let $L$ be a functor of $x$ and $x_{2}$. Let $R$ be a functor of $x_{1}$ and $x_{3}$. Let $B$ be a functor of $x_{2}$ and $x_{3}$. Then the isomorphism of $R$ and $B$ is an isomorphism of the composition of $T$ and $R$ and the composition of $L$ and $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.CatCommSq.vInvEquivdefMathlib.CategoryTheory.CatCommSq, function or constant

Wording

the inverse equivalence of R and B (from the name)

English

Let $T$ be a functor of $x$ and $x_{1}$. Let $L$ be an equivalence of $x$ and $x_{2}$. Let $R$ be an equivalence of $x_{1}$ and $x_{3}$. Let $B$ be a functor of $x_{2}$ and $x_{3}$. Then the inverse equivalence of $R$ and $B$ is an equivalence from $\operatorname{CatCommSq}$ applied to $T$, the functor of $L$, the functor of $R$ and $B$ to $\operatorname{CatCommSq}$ applied to $B$, the inverse of $L$, the inverse of $R$ and $T$.

Mathlib.CategoryTheory.Category.Basic

CategoryTheory.CategoryclassMathlib.CategoryTheory.Category.Basic, predicate

Wording

obj is a category (from the name)

English

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

CategoryTheory.CategoryStructclassMathlib.CategoryTheory.Category.Basic, predicate

Wording

no wording

English

Let $\mathrm{obj}$ be a set. Then we can say that $\operatorname{CategoryStruct}$ holds for $\mathrm{obj}$.

CategoryTheory.CategoryStruct.compdefMathlib.CategoryTheory.Category.Basic, function or constant

Wording

the composition of x and x1 (from the name)

English

Let $x$ be a homomorphism of $X$ and $Y$. Let $x_{1}$ be a homomorphism of $Y$ and $Z$. Then the composition of $x$ and $x_{1}$ is a homomorphism of $X$ and $Z$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $x$ and $x_{1}$.

CategoryTheory.CategoryStruct.iddefMathlib.CategoryTheory.Category.Basic, function or constant

Wording

the identity morphism of X (from the docstring)

English

Let $X$ be an element of $\mathrm{obj}$. Then the identity morphism of $X$ is a homomorphism of $X$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $X$.

CategoryTheory.EpiclassMathlib.CategoryTheory.Category.Basic, predicate

Wording

f is a epimorphism (from the name)

English

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

CategoryTheory.LargeCategorydefMathlib.CategoryTheory.Category.Basic, type

Wording

large category of C (from the name)

English

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

CategoryTheory.MonoclassMathlib.CategoryTheory.Category.Basic, predicate

Wording

f is a monomorphism (from the name)

English

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

CategoryTheory.SmallCategorydefMathlib.CategoryTheory.Category.Basic, type

Wording

small category of C (from the name)

English

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

CategoryTheory.aesop_catdefMathlib.CategoryTheory.Category.Basic, function or constant

Wording

no wording

English

generation took over the time limit

CategoryTheory.aesop_cat?defMathlib.CategoryTheory.Category.Basic, function or constant

Wording

no wording

English

generation took over the time limit

CategoryTheory.aesop_cat_nonterminaldefMathlib.CategoryTheory.Category.Basic, function or constant

Wording

no wording

English

generation took over the time limit

CategoryTheory.cat_dischdefMathlib.CategoryTheory.Category.Basic, function or constant

Wording

no wording

English

generation took over the time limit

CategoryTheory.categoryTheoryDischargerdefMathlib.CategoryTheory.Category.Basic, function or constant

Wording

no wording

English

$\operatorname{TacticM}$ holds for $\mathrm{Unit}$.

CategoryTheory.evalSorryIfSorrydefMathlib.CategoryTheory.Category.Basic, function or constant

Wording

no wording

English

generation took over the time limit

CategoryTheory.rfl_catdefMathlib.CategoryTheory.Category.Basic, function or constant

Wording

no wording

English

generation took over the time limit

CategoryTheory.sorryIfSorrydefMathlib.CategoryTheory.Category.Basic, function or constant

Wording

no wording

English

generation took over the time limit

LibraryNote.category_theory_universesdefMathlib.CategoryTheory.Category.Basic, function or constant

Wording

the category theory universe (from the name)

English

The category theory universe is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

LibraryNote.universe_output_parameters_and_typeclass_cachingdefMathlib.CategoryTheory.Category.Basic, function or constant

Wording

no wording

English

$\mathrm{LibraryNote\_\_universe\_output\_parameters\_and\_typeclass\_caching}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

Mathlib.CategoryTheory.Category.Bipointed

BipointedstructureMathlib.CategoryTheory.Category.Bipointed, type

Wording

no wording

English

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

Bipointed.HomstructureMathlib.CategoryTheory.Category.Bipointed, type

Wording

homomorphism of X and Y (from the name)

English

Let $X$ and $Y$ be elements of $\mathrm{Bipointed}$. Then the homomorphisms of $X$ and $Y$ are a basic type.

Bipointed.Hom.compdefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the composition of f and g (from the name)

English

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

Bipointed.Hom.iddefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the identity morphism of X (from the docstring)

English

Let $X$ be an element of $\mathrm{Bipointed}$. Then the identity morphism of $X$ is a homomorphism of $X$ and $X$.

Bipointed.Hom.toFundefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the homomorphism of self and x (from the name)

English

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

Bipointed.HomSubtypedefMathlib.CategoryTheory.Category.Bipointed, type

Wording

homomorphism subtype of X and Y (from the name)

English

Let $X$ and $Y$ be elements of $\mathrm{Bipointed}$. Then a homomorphism subtype of $X$ and $Y$ is an element of the function that maps $X$ and $Y$ to $\SubtypeSet {f}{\mathrm{and} (\EqtMACRoH {f (\ProdfstMACRoZ {\operatorname{toProd} (X)})}{\ProdfstMACRoZ {\operatorname{toProd} (Y)}}, \EqtMACRoH {f (\ProdsndMACRoAA {\operatorname{toProd} (X)})}{\ProdsndMACRoAA {\operatorname{toProd} (Y)}})}$.

Bipointed.XdefMathlib.CategoryTheory.Category.Bipointed, type

Wording

no wording

English

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

Bipointed.ofdefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

no wording

English

Let $\mathrm{to\_prod}$ be an element of $\mathrm{Prod}$ applied to $X$ and $X$. Then $\operatorname{of}$ applied to $\mathrm{to\_prod}$ is an element of $\mathrm{Bipointed}$ defined as $\operatorname{mk}$ applied to $X$ and $\mathrm{to\_prod}$.

Bipointed.swapdefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the swap (from the name)

English

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

Bipointed.swapEquivdefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the swap equivalence (from the name)

English

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

Bipointed.toProddefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the product of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{Bipointed}$. Then the product of $\mathrm{self}$ is an element of $\mathrm{Prod}$ applied to $\operatorname{X}$ applied to $\mathrm{self}$ and $\operatorname{X}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Prod.BipointeddefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

no wording

English

Let $\mathrm{to\_prod}$ be an element of $\mathrm{Prod}$ applied to $X$ and $X$. Then $\operatorname{Bipointed}$ applied to $\mathrm{to\_prod}$ is an element of $\mathrm{Bipointed}$ defined as $\operatorname{of}$ applied to $\mathrm{to\_prod}$.

bipointedToPointedFstdefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

no wording

English

$\mathrm{bipointedToPointedFst}$ is a functor of $\mathrm{Bipointed}$ and the set of pointeds.

bipointedToPointedSnddefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

no wording

English

$\mathrm{bipointedToPointedSnd}$ is a functor of $\mathrm{Bipointed}$ and the set of pointeds.

pointedToBipointeddefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

no wording

English

$\mathrm{pointedToBipointed}$ is a functor of the set of pointeds and $\mathrm{Bipointed}$.

pointedToBipointedCompBipointedToPointedFstdefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the pointed to bipointed composition bipointed to pointed first component (from the name)

English

The pointed to bipointed composition bipointed to pointed first component is an isomorphism of the composition of $\mathrm{pointedToBipointed}$ and $\mathrm{bipointedToPointedFst}$ and the identity of the set of pointeds.

pointedToBipointedCompBipointedToPointedSnddefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the pointed to bipointed composition bipointed to pointed second component (from the name)

English

The pointed to bipointed composition bipointed to pointed second component is an isomorphism of the composition of $\mathrm{pointedToBipointed}$ and $\mathrm{bipointedToPointedSnd}$ and the identity of the set of pointeds.

pointedToBipointedFstdefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the pointed to bipointed first component (from the name)

English

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

pointedToBipointedFstBipointedToPointedFstAdjunctiondefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the pointed to bipointed first component bipointed to pointed first component adjunction (from the name)

English

The pointed to bipointed first component bipointed to pointed first component adjunction is an adjunction of the pointed to bipointed first component and $\mathrm{bipointedToPointedFst}$.

pointedToBipointedSnddefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the pointed to bipointed second component (from the name)

English

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

pointedToBipointedSndBipointedToPointedSndAdjunctiondefMathlib.CategoryTheory.Category.Bipointed, function or constant

Wording

the pointed to bipointed second component bipointed to pointed second component adjunction (from the name)

English

The pointed to bipointed second component bipointed to pointed second component adjunction is an adjunction of the pointed to bipointed second component and $\mathrm{bipointedToPointedSnd}$.

Mathlib.CategoryTheory.Category.Cat

CategoryTheory.CatdefMathlib.CategoryTheory.Category.Cat, type

Wording

category (from the name)

English

A category is an element of $\operatorname{Bundled}$ applied to the proposition that $\operatorname{Category}$.

CategoryTheory.Cat.HomstructureMathlib.CategoryTheory.Category.Cat, type

Wording

homomorphism of C and D (from the name)

English

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

CategoryTheory.Cat.Hom.equivFunctordefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

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

English

Let $C$ and $D$ be categories. Then the equivalence functor of $C$ and $D$ is an equivalence from the set of homomorphisms of $C$ and $D$ to the set of functors of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $C$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $D$ defined as the inverse of the equivalence category homomorphism of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $C$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $D$.

CategoryTheory.Cat.Hom.isoMkdefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

the isomorphism of e (from the name)

English

Let $e$ be an isomorphism of $F$ and $G$. Then the isomorphism of $e$ is an isomorphism of the category homomorphism of $F$ and the category homomorphism of $G$.

CategoryTheory.Cat.Hom.toFunctordefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

the functor of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $C$ and $D$. Then the functor of $\mathrm{self}$ is a functor of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $C$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $D$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Cat.Hom.toNatIsodefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

the natural isomorphism of e (from the name)

English

Let $e$ be an isomorphism of $F$ and $G$. Then the natural isomorphism of $e$ is an isomorphism of the functor of $F$ and the functor of $G$.

CategoryTheory.Cat.Hom₂structureMathlib.CategoryTheory.Category.Cat, type

Wording

homomorphism of F and G (from the name)

English

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

CategoryTheory.Cat.Hom₂.toNatTransdefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

the natural transformation of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $F$ and $G$. Then the natural transformation of $\mathrm{self}$ is a homomorphism of the functor of $F$ and the functor of $G$ defined as $\mathrm{CategoryTheory\_\_Cat\_\_Hom\_u2082\_\_\_proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Cat.equivOfIsodefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

the equivalence of x (from the name)

English

Let $x$ be an isomorphism of $C$ and $D$. Then the equivalence of $x$ is an equivalence of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $C$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $D$.

CategoryTheory.Cat.isoOfEquivdefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

the isomorphism of e (from the name)

English

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

CategoryTheory.Cat.objectsdefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

the object (from the name)

English

The object is a functor of the set of categories and the set of sets.

CategoryTheory.Cat.ofdefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

no wording

English

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

CategoryTheory.Functor.equivCatHomdefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

the equivalence category homomorphism of C and D (from the name)

English

Let $C$ and $D$ be sets. Then the equivalence category homomorphism of $C$ and $D$ is an equivalence from the set of functors of $C$ and $D$ to the set of homomorphisms of $\operatorname{of}$ applied to $C$ and $\operatorname{of}$ applied to $D$.

CategoryTheory.Functor.toCatHomdefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

the category homomorphism of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the category homomorphism of $F$ is a homomorphism of $\operatorname{of}$ applied to $C$ and $\operatorname{of}$ applied to $D$ defined as $\operatorname{ofFunctor}$ applied to $F$.

CategoryTheory.NatTrans.toCatHom₂defMathlib.CategoryTheory.Category.Cat, function or constant

Wording

the category homomorphism of x2 (from the name)

English

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then the category homomorphism of $x_{2}$ is a homomorphism of the category homomorphism of $F$ and the category homomorphism of $G$ defined as $\mathrm{CategoryTheory\_\_Cat\_\_Hom\_u2082\_\_\_ofNatTrans}$ applied to $x_{2}$.

CategoryTheory.typeToCatdefMathlib.CategoryTheory.Category.Cat, function or constant

Wording

the type to category (from the name)

English

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

Mathlib.CategoryTheory.Category.Cat.Adjunction

CategoryTheory.Cat.connectedComponentsdefMathlib.CategoryTheory.Category.Cat.Adjunction, function or constant

Wording

the connected component (from the name)

English

The connected component is a functor of the set of categories and the set of sets.

CategoryTheory.Cat.connectedComponentsTypeToCatAdjdefMathlib.CategoryTheory.Category.Cat.Adjunction, function or constant

Wording

the connected component type to category adjoint (from the name)

English

The connected component type to category adjoint is an adjunction of the connected component and the type to category.

CategoryTheory.Cat.typeToCatObjectsAdjdefMathlib.CategoryTheory.Category.Cat.Adjunction, function or constant

Wording

the type to category object adjoint (from the name)

English

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

Mathlib.CategoryTheory.Category.Cat.AsSmall

CategoryTheory.Cat.asSmallFunctordefMathlib.CategoryTheory.Category.Cat.AsSmall, function or constant

Wording

no wording

English

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

Mathlib.CategoryTheory.Category.Cat.CartesianClosed

CategoryTheory.Cat.expdefMathlib.CategoryTheory.Category.Cat.CartesianClosed, function or constant

Wording

the exponential of C (from the name)

English

Let $C$ be a set. Then the exponential of $C$ is a functor of the set of categories and the set of categories.

CategoryTheory.curryingIsodefMathlib.CategoryTheory.Category.Cat.CartesianClosed, function or constant

Wording

the currying isomorphism (from the name)

English

The currying isomorphism is an isomorphism of $\operatorname{of}$ applied to the set of functors of $C$ and the set of functors of $D$ and $E$ and $\operatorname{of}$ applied to the set of functors of $\mathrm{Prod}$ applied to $C$ and $D$ and $E$.

CategoryTheory.flippingIsodefMathlib.CategoryTheory.Category.Cat.CartesianClosed, function or constant

Wording

no wording

English

$\operatorname{flippingIso}$ is an isomorphism of $\operatorname{of}$ applied to the set of functors of $C$ and the set of functors of $D$ and $E$ and $\operatorname{of}$ applied to the set of functors of $D$ and the set of functors of $C$ and $E$.

Mathlib.CategoryTheory.Category.Cat.Op

CategoryTheory.Cat.opEquivalencedefMathlib.CategoryTheory.Category.Cat.Op, function or constant

Wording

the equivalence (from the docstring)

English

The equivalence is an equivalence of the set of categories and the set of categories.

CategoryTheory.Cat.opFunctordefMathlib.CategoryTheory.Category.Cat.Op, function or constant

Wording

the opposite functor (from the name)

English

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

CategoryTheory.Cat.opFunctorInvolutivedefMathlib.CategoryTheory.Category.Cat.Op, function or constant

Wording

no wording

English

$\operatorname{opFunctorInvolutive}$ is an isomorphism of the composition of the opposite functor and the opposite functor and the identity of the set of categories.

Mathlib.CategoryTheory.Category.Cat.Terminal

CategoryTheory.Cat.isTerminalDiscretePUnitdefMathlib.CategoryTheory.Category.Cat.Terminal, function or constant

Wording

no wording

English

$\operatorname{isTerminalDiscretePUnit}$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{of}$ applied to $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{isTerminalOfUniqueOfIsDiscrete}$.

CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscretedefMathlib.CategoryTheory.Category.Cat.Terminal, function or constant

Wording

no wording

English

$\operatorname{isTerminalOfUniqueOfIsDiscrete}$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{of}$ applied to $T$.

CategoryTheory.Cat.isoDiscretePUnitOfIsTerminaldefMathlib.CategoryTheory.Category.Cat.Terminal, function or constant

Wording

the isomorphism discrete unit of hT (from the name)

English

Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $\operatorname{of}$ applied to $T$. Then the isomorphism discrete unit of $\mathrm{hT}$ is an isomorphism of $\operatorname{of}$ applied to $T$ and $\operatorname{of}$ applied to $\operatorname{Discrete}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{uniqueUpToIso}$ applied to $\mathrm{hT}$ and $\operatorname{isTerminalDiscretePUnit}$.

Mathlib.CategoryTheory.Category.Factorisation

CategoryTheory.FactorisationstructureMathlib.CategoryTheory.Category.Factorisation, type

Wording

factorisation of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the factorisations of $f$ are a basic type.

CategoryTheory.Factorisation.HomstructureMathlib.CategoryTheory.Category.Factorisation, type

Wording

homomorphism of d and e (from the name)

English

Let $d$ and $e$ be factorisations of $f$. Then the homomorphisms of $d$ and $e$ are a basic type.

CategoryTheory.Factorisation.Hom.hdefMathlib.CategoryTheory.Category.Factorisation, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a homomorphism of $d$ and $e$. Then $\operatorname{h}$ applied to $\mathrm{self}$ is a homomorphism of the midpoint of the factorisation of $d$ and the midpoint of the factorisation of $e$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Factorisation.IsInitial_initialdefMathlib.CategoryTheory.Category.Factorisation, function or constant

Wording

the initial factorisation (from the docstring)

English

The initial factorisation is an element of $\operatorname{IsInitial}$ applied to $\operatorname{initial}$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{initial}$.

CategoryTheory.Factorisation.IsTerminal_terminaldefMathlib.CategoryTheory.Category.Factorisation, function or constant

Wording

the terminal factorisation (from the docstring)

English

The terminal factorisation is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{terminal}$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{terminal}$.

CategoryTheory.Factorisation.forgetdefMathlib.CategoryTheory.Category.Factorisation, function or constant

Wording

no wording

English

$\operatorname{forget}$ is a functor of the set of factorisations of $f$ and $C$.

CategoryTheory.Factorisation.initialdefMathlib.CategoryTheory.Category.Factorisation, function or constant

Wording

no wording

English

$\operatorname{initial}$ is a factorisation of $f$.

CategoryTheory.Factorisation.initialHomdefMathlib.CategoryTheory.Category.Factorisation, function or constant

Wording

the initial homomorphism of d (from the name)

English

Let $d$ be a factorisation of $f$. Then the initial homomorphism of $d$ is a homomorphism of $\operatorname{initial}$ and $d$.

CategoryTheory.Factorisation.middefMathlib.CategoryTheory.Category.Factorisation, function or constant

Wording

the midpoint of the factorisation of self (from the docstring)

English

Let $\mathrm{self}$ be a factorisation of $f$. Then the midpoint of the factorisation of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CategoryTheory.Factorisation.ιdefMathlib.CategoryTheory.Category.Factorisation, function or constant

Wording

the inclusion of self (from the name)

English

Let $\mathrm{self}$ be a factorisation of $f$. Then the inclusion of $\mathrm{self}$ is a homomorphism of $X$ and the midpoint of the factorisation of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CategoryTheory.Factorisation.πdefMathlib.CategoryTheory.Category.Factorisation, function or constant

Wording

the projection of self (from the name)

English

Let $\mathrm{self}$ be a factorisation of $f$. Then the projection of $\mathrm{self}$ is a homomorphism of the midpoint of the factorisation of $\mathrm{self}$ and $Y$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Mathlib.CategoryTheory.Category.GaloisConnection

GaloisConnection.adjunctiondefMathlib.CategoryTheory.Category.GaloisConnection, function or constant

Wording

the adjunction of gc (from the name)

English

Assume that $\mathrm{GaloisConnection}$ holds for $l$ and $u$. Then the adjunction of $\mathrm{gc}$ is an adjunction of the functor of $\mathrm{GaloisConnection\_\_monotone\_l}$ applied to $\mathrm{gc}$ and the functor of $\mathrm{GaloisConnection\_\_monotone\_u}$ applied to $\mathrm{gc}$.

Mathlib.CategoryTheory.Category.Init

mathlib.tactic.category.grindopaqueMathlib.CategoryTheory.Category.Init, function or constant

Wording

no wording

English

$\operatorname{grind}$ is an element of $\operatorname{Option}$ applied to $\mathrm{Bool}$.

mathlib.tactic.category.log_aesopopaqueMathlib.CategoryTheory.Category.Init, function or constant

Wording

no wording

English

$\mathrm{mathlib\_\_tactic\_\_category\_\_log\_aesop}$ is an element of $\operatorname{Option}$ applied to $\mathrm{Bool}$.

mathlib.tactic.category.log_grindopaqueMathlib.CategoryTheory.Category.Init, function or constant

Wording

no wording

English

$\mathrm{mathlib\_\_tactic\_\_category\_\_log\_grind}$ is an element of $\operatorname{Option}$ applied to $\mathrm{Bool}$.

Mathlib.CategoryTheory.Category.KleisliCat

CategoryTheory.KleisliCatdefMathlib.CategoryTheory.Category.KleisliCat, type

Wording

no wording

English

Let $x$ be a function from sets to sets. Then an element of $\operatorname{KleisliCat}$ applied to $x$ is an element of the function that maps $x$ to the set of sets.

CategoryTheory.KleisliCat.mkdefMathlib.CategoryTheory.Category.KleisliCat, function or constant

Wording

no wording

English

Let $m$ be a function from sets to sets. Let $x$ be a set. Then $\operatorname{mk}$ applied to $m$ and $x$ is an element of $\operatorname{KleisliCat}$ applied to $m$ defined as $x$.

Mathlib.CategoryTheory.Category.Pairwise

CategoryTheory.PairwiseinductiveMathlib.CategoryTheory.Category.Pairwise, type

Wording

pairwise of x (from the name)

English

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

CategoryTheory.Pairwise.HominductiveMathlib.CategoryTheory.Category.Pairwise, type

Wording

homomorphism of x1 and x2 (from the name)

English

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

CategoryTheory.Pairwise.Hom.ctorElimTypedefMathlib.CategoryTheory.Category.Pairwise, type

Wording

no wording

English

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $i$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{single}$ applied to $i$, $\operatorname{single}$ applied to $i$ and $\mathrm{CategoryTheory\_\_Pairwise\_\_Hom\_\_id\_single}$ applied to $i$ and $\mathrm{PULift}$ applied to the set of functions from elements $i_{1}$ of $x$ and elements $j$ of $x$ to elements of $\mathrm{motive}$ applied to the pair of $i_{1}$ and $j$, the pair of $i_{1}$ and $j$ and the identity pair of $i_{1}$ and $j$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $2$, $\mathrm{PULift}$ applied to the set of functions from elements $i_{2}$ of $x$ and elements $j_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to the pair of $i_{2}$ and $j_{1}$, $\operatorname{single}$ applied to $i_{2}$ and the left of $i_{2}$ and $j_{1}$ and $\mathrm{PULift}$ applied to the set of functions from elements $i_{3}$ of $x$ and elements $j_{2}$ of $x$ to elements of $\mathrm{motive}$ applied to the pair of $i_{3}$ and $j_{2}$, $\operatorname{single}$ applied to $j_{2}$ and the right of $i_{3}$ and $j_{2}$.

CategoryTheory.Pairwise.Hom.id_pairconstructorMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

the identity pair of i and j (from the name)

English

Let $i$ and $j$ be elements of $x$. Then the identity pair of $i$ and $j$ is a homomorphism of the pair of $i$ and $j$ and the pair of $i$ and $j$.

CategoryTheory.Pairwise.Hom.id_singleconstructorMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Then $\mathrm{CategoryTheory\_\_Pairwise\_\_Hom\_\_id\_single}$ applied to $i$ is a homomorphism of $\operatorname{single}$ applied to $i$ and $\operatorname{single}$ applied to $i$.

CategoryTheory.Pairwise.Hom.leftconstructorMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

the left of i and j (from the name)

English

Let $i$ and $j$ be elements of $x$. Then the left of $i$ and $j$ is a homomorphism of the pair of $i$ and $j$ and $\operatorname{single}$ applied to $i$.

CategoryTheory.Pairwise.Hom.rightconstructorMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

the right of i and j (from the name)

English

Let $i$ and $j$ be elements of $x$. Then the right of $i$ and $j$ is a homomorphism of the pair of $i$ and $j$ and $\operatorname{single}$ applied to $j$.

CategoryTheory.Pairwise.coconedefMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

the cocone of U (from the name)

English

Let $U$ be a function from elements of $x$ to elements of $x_{1}$. Then the cocone of $U$ is a cocone of the diagram of $U$.

CategoryTheory.Pairwise.coconeIsColimitdefMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

no wording

English

Let $U$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{coconeIsColimit}$ applied to $U$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $U$.

CategoryTheory.Pairwise.compdefMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

the composition of x4 and x5 (from the name)

English

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

CategoryTheory.Pairwise.ctorElimTypedefMathlib.CategoryTheory.Category.Pairwise, type

Wording

no wording

English

CategoryTheory.Pairwise.diagramdefMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

the diagram of U (from the name)

English

Let $U$ be a function from elements of $x$ to elements of $x_{1}$. Then the diagram of $U$ is a functor of the set of pairwises of $x$ and $x_{1}$.

CategoryTheory.Pairwise.iddefMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

the identity morphism in o (from the docstring)

English

Let $o$ be a pairwise of $x$. Then the identity morphism in $o$ is a homomorphism of $o$ and $o$.

CategoryTheory.Pairwise.pairconstructorMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

the pair of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be elements of $x$. Then the pair of $x_{1}$ and $x_{2}$ is a pairwise of $x$.

CategoryTheory.Pairwise.pairwiseCasesdefMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

the pairwise case (from the name)

English

The pairwise case is an element of $\operatorname{TacticM}$ applied to $\mathrm{Unit}$.

CategoryTheory.Pairwise.proxyTypedefMathlib.CategoryTheory.Category.Pairwise, type

Wording

no wording

English

Let $x$ be a set. Then an element of $\operatorname{proxyType}$ applied to $x$ is an element of the function that maps $x$ to $\mathrm{Sum}$ applied to $x$ and $\Sigma$ applied to the function that maps $x_{1}$ to $x$.

CategoryTheory.Pairwise.proxyTypeEquivdefMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{proxyTypeEquiv}$ applied to $x$ is an equivalence from $\mathrm{Sum}$ applied to $x$ and $\Sigma$ applied to the function that maps $x_{1}$ to $x$ to the set of pairwises of $x$.

CategoryTheory.Pairwise.singleconstructorMathlib.CategoryTheory.Category.Pairwise, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $x$. Then $\operatorname{single}$ applied to $x_{1}$ is a pairwise of $x$.

Mathlib.CategoryTheory.Category.PartialFun

PartialFundefMathlib.CategoryTheory.Category.PartialFun, type

Wording

partial function (from the name)

English

A partial function is a set.

PartialFun.Iso.mkdefMathlib.CategoryTheory.Category.PartialFun, function or constant

Wording

no wording

English

Let $e$ be an equivalence from $x$ to $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.

PartialFun.ofdefMathlib.CategoryTheory.Category.PartialFun, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{of}$ applied to $x$ is a partial function defined as $\mathrm{id}$ applied to $x$.

partialFunEquivPointeddefMathlib.CategoryTheory.Category.PartialFun, function or constant

Wording

the partial function equivalence pointed (from the name)

English

The partial function equivalence pointed is an equivalence of the set of partial functions and the set of pointeds.

partialFunToPointeddefMathlib.CategoryTheory.Category.PartialFun, function or constant

Wording

the partial function to pointed (from the name)

English

The partial function to pointed is a functor of the set of partial functions and the set of pointeds.

pointedToPartialFundefMathlib.CategoryTheory.Category.PartialFun, function or constant

Wording

the pointed to partial function (from the name)

English

The pointed to partial function is a functor of the set of pointeds and the set of partial functions.

typeToPartialFundefMathlib.CategoryTheory.Category.PartialFun, function or constant

Wording

the type to partial function (from the name)

English

The type to partial function is a functor of the set of sets and the set of partial functions.

typeToPartialFunIsoPartialFunToPointeddefMathlib.CategoryTheory.Category.PartialFun, function or constant

Wording

the type to partial function isomorphism partial function to pointed (from the name)

English

The type to partial function isomorphism partial function to pointed is an isomorphism of the composition of the type to partial function and the partial function to pointed and the type to pointed.

Mathlib.CategoryTheory.Category.Pointed

PointedstructureMathlib.CategoryTheory.Category.Pointed, type

Wording

pointed (from the name)

English

The pointeds are a basic type.

Pointed.HomstructureMathlib.CategoryTheory.Category.Pointed, type

Wording

homomorphism of X and Y (from the name)

English

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

Pointed.Hom.compdefMathlib.CategoryTheory.Category.Pointed, function or constant

Wording

the composition of f and g (from the name)

English

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

Pointed.Hom.iddefMathlib.CategoryTheory.Category.Pointed, function or constant

Wording

the identity morphism of X (from the docstring)

English

Let $X$ be a pointed. Then the identity morphism of $X$ is a homomorphism of $X$ and $X$.

Pointed.Hom.toFundefMathlib.CategoryTheory.Category.Pointed, function or constant

Wording

the homomorphism of self and x (from the name)

English

Pointed.Iso.mkdefMathlib.CategoryTheory.Category.Pointed, function or constant

Wording

no wording

English

Let $e$ be an element of $\EquivMACRoAE {\operatorname{X} (x)}{\operatorname{X} (x_{1})}$ such that $e$ applied to the point of $x$ is equal to the point of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ and $\mathrm{he}$ is an isomorphism of $x$ and $x_{1}$.

Pointed.XdefMathlib.CategoryTheory.Category.Pointed, type

Wording

no wording

English

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

Pointed.ofdefMathlib.CategoryTheory.Category.Pointed, function or constant

Wording

no wording

English

Let $\mathrm{point}$ be an element of $X$. Then $\operatorname{of}$ applied to $\mathrm{point}$ is a pointed defined as $\operatorname{mk}$ applied to $X$ and $\mathrm{point}$.

Pointed.pointdefMathlib.CategoryTheory.Category.Pointed, function or constant

Wording

the point of self (from the name)

English

Let $\mathrm{self}$ be a pointed. Then the point of $\mathrm{self}$ is an element of $\operatorname{X}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Prod.PointeddefMathlib.CategoryTheory.Category.Pointed, function or constant

Wording

the pointed of point (from the name)

English

Let $\mathrm{point}$ be an element of $X$. Then the pointed of $\mathrm{point}$ is a pointed defined as $\operatorname{of}$ applied to $\mathrm{point}$.

typeToPointeddefMathlib.CategoryTheory.Category.Pointed, function or constant

Wording

the type to pointed (from the name)

English

The type to pointed is a functor of the set of sets and the set of pointeds.

typeToPointedForgetAdjunctiondefMathlib.CategoryTheory.Category.Pointed, function or constant

Wording

no wording

English

$\mathrm{typeToPointedForgetAdjunction}$ is an adjunction of the type to pointed and the forgetful functor of the set of pointeds.

Mathlib.CategoryTheory.Category.Preorder

CategoryTheory.Equivalence.toOrderIsodefMathlib.CategoryTheory.Category.Preorder, function or constant

Wording

the order isomorphism of e (from the name)

English

Let $e$ be an equivalence of $X$ and $Y$. Then the order isomorphism of $e$ is an order isomorphism of $X$ and $Y$.

CategoryTheory.Functor.toOrderHomdefMathlib.CategoryTheory.Category.Preorder, function or constant

Wording

the order homomorphism of F (from the name)

English

Let $F$ be a functor of $X$ and $Y$. Then the order homomorphism of $F$ is an order homomorphism of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\operatorname{obj}$ applied to $F$ and $\operatorname{monotone}$ applied to $F$.

CategoryTheory.homOfLEdefMathlib.CategoryTheory.Category.Preorder, function or constant

Wording

the homomorphism of h (from the name)

English

Assume that $x_{1} \leq y$. Then the homomorphism of $h$ is a homomorphism of $x_{1}$ and $y$ defined as $\operatorname{up}$ applied to $\operatorname{up}$ applied to $h$.

CategoryTheory.opHomOfLEdefMathlib.CategoryTheory.Category.Preorder, function or constant

Wording

the opposite homomorphism of h (from the name)

English

Assume that the opposite of $x_{1}$ is less than or equal to the opposite of $y$. Then the opposite homomorphism of $h$ is a homomorphism of $y$ and $x_{1}$ defined as the opposite in the homomorphism of $h$.

CategoryTheory.orderDualEquivalencedefMathlib.CategoryTheory.Category.Preorder, function or constant

Wording

the order dual equivalence of X (from the name)

English

Let $X$ be a set. Then the order dual equivalence of $X$ is an equivalence of the set of order duals of $X$ and the set of opposites of $X$.

LE.le.homdefMathlib.CategoryTheory.Category.Preorder, function or constant

Wording

the homomorphism of h (from the name)

English

Assume that $x_{1} \leq y$. Then the homomorphism of $h$ is a homomorphism of $x_{1}$ and $y$ defined as the homomorphism of $h$.

Monotone.functordefMathlib.CategoryTheory.Category.Preorder, function or constant

Wording

the functor of h (from the name)

English

Assume that $f$ is monotone. Then the functor of $h$ is a functor of $X$ and $Y$.

OrderHom.equivFunctordefMathlib.CategoryTheory.Category.Preorder, function or constant

Wording

the equivalence functor (from the name)

English

The equivalence functor is an equivalence from the set of order homomorphisms of $X$ and $Y$ to the set of functors of $X$ and $Y$.

OrderHom.equivalenceFunctordefMathlib.CategoryTheory.Category.Preorder, function or constant

Wording

the equivalence functor (from the name)

English

The equivalence functor is an equivalence of the set of order homomorphisms of $X$ and $Y$ and the set of functors of $X$ and $Y$.

OrderHom.toFunctordefMathlib.CategoryTheory.Category.Preorder, function or constant

Wording

the functor of f (from the name)

English

Let $f$ be an order homomorphism of $X$ and $Y$. Then the functor of $f$ is a functor of $X$ and $Y$ defined as the functor of $\operatorname{monotone}$ applied to $f$.

OrderIso.equivalencedefMathlib.CategoryTheory.Category.Preorder, function or constant

Wording

the equivalence of e (from the name)

English

Let $e$ be an order isomorphism of $X$ and $Y$. Then the equivalence of $e$ is an equivalence of $X$ and $Y$.

Mathlib.CategoryTheory.Category.Quiv

CategoryTheory.Cat.freedefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the free (from the name)

English

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

CategoryTheory.Cat.freeMapdefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the free map of F (from the name)

English

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

CategoryTheory.Cat.freeMapCompIsodefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

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

English

Let $F$ be a prefunctor of $x$ and $x_{1}$. Let $G$ be a prefunctor of $x_{1}$ and $x_{2}$. Then the free map composition isomorphism of $F$ and $G$ is an isomorphism of the free map of the composition of $F$ and $G$ and the composition of the free map of $F$ and the free map of $G$.

CategoryTheory.Cat.freeMapIdIsodefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the free map identity isomorphism of V (from the name)

English

Let $V$ be a set. Then the free map identity isomorphism of $V$ is an isomorphism of the free map of the identity of $V$ and the identity of the set of paths of $V$.

CategoryTheory.Prefunctor.ofQuivHomdefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the prefunctor of F (from the name)

English

Let $F$ be a homomorphism of $C$ and $D$. Then the prefunctor of $F$ is a prefunctor of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $C$ and $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to $D$ defined as $F$.

CategoryTheory.Prefunctor.toQuivHomdefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

no wording

English

Let $F$ be a prefunctor of $C$ and $D$. Then $\operatorname{toQuivHom}$ applied to $F$ is a homomorphism of $\operatorname{of}$ applied to $C$ and $\operatorname{of}$ applied to $D$ defined as $F$.

CategoryTheory.QuivdefMathlib.CategoryTheory.Category.Quiv, type

Wording

no wording

English

An element of $\operatorname{Quiv}$ is an element of $\operatorname{Bundled}$ applied to the proposition that $\mathrm{Quiver}$.

CategoryTheory.Quiv.adjdefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the adjoint (from the name)

English

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

CategoryTheory.Quiv.equivOfIsodefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the equivalence of e (from the name)

English

Let $e$ be an isomorphism of $V$ and $W$. Then the equivalence of $e$ is an element of $\EquivMACRoAE {\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_} (V)}{\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_} (W)}$.

CategoryTheory.Quiv.forgetdefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

no wording

English

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

CategoryTheory.Quiv.freeMapPathsOfCompPathCompositionIsodefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the free map path of V (from the name)

English

Let $V$ be a set. Then the free map path of $V$ is an isomorphism of the composition of the free map of $\operatorname{of}$ applied to $V$ and the path composition of the set of paths of $V$ and the identity of the set of paths of $V$.

CategoryTheory.Quiv.homEquivOfIsodefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the homomorphism equivalence of e (from the name)

English

Let $e$ be an isomorphism of $V$ and $W$. Then the homomorphism equivalence of $e$ is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of the object of the homomorphism of $e$ and $X$ and the object of the homomorphism of $e$ and $Y$.

CategoryTheory.Quiv.isoOfEquivdefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the isomorphism of e and he (from the name)

English

Let $e$ be an equivalence from $V$ to $W$. Let $\mathrm{he}$ be a function from elements $X$ of $V$ and elements $Y$ of $V$ to equivalences from the set of homomorphisms of $X$ and $Y$ to the set of homomorphisms of $e$ applied to $X$ and $e$ applied to $Y$. Then the isomorphism of $e$ and $X$ is an isomorphism of $\operatorname{of}$ applied to $V$ and $\operatorname{of}$ applied to $W$.

CategoryTheory.Quiv.liftdefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the lift of F (from the name)

English

Let $F$ be a prefunctor of $V$ and $C$. Then the lift of $F$ is a functor of the set of paths of $V$ and $C$.

CategoryTheory.Quiv.ofdefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

no wording

English

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

CategoryTheory.Quiv.pathCompositionNaturalitydefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the path composition naturality of F (from the name)

English

Let $F$ be a functor of $C$ and $D$. Then the path composition naturality of $F$ is an isomorphism of the composition of the free map of the prefunctor between the underlying quivers of $F$ and the path composition of $D$ and the composition of the path composition of $C$ and $F$.

CategoryTheory.Quiv.pathsEquivdefMathlib.CategoryTheory.Category.Quiv, function or constant

Wording

the universal property of the path category (from the docstring)

English

The universal property of the path category is an equivalence from the set of functors of the set of paths of $V$ and $C$ to the set of prefunctors of $V$ and $C$.