Definitions: Mathlib.CategoryTheory, part 24 of 25

the map square of F (from the name)

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

the map square of x2 (from the name)

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

square of C (from the name)

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

homomorphism of x1 and x2 (from the name)

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

the composition of f and g (from the name)

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

the identity of sq (from the docstring)

Let $\mathrm{sq}$ be a square of $C$. Then the identity of $\mathrm{sq}$ is a homomorphism of $\mathrm{sq}$ and $\mathrm{sq}$.

Let $\mathrm{self}$ be a homomorphism of $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_Square\_\_Hom\_\_\_u3c4\_\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2081\_}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2081\_}$ applied to $x_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homomorphism of $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_Square\_\_Hom\_\_\_u3c4\_\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_}$ applied to $x_{2}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homomorphism of $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_Square\_\_Hom\_\_\_u3c4\_\_u2083\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_}$ applied to $x_{2}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homomorphism of $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_Square\_\_Hom\_\_\_u3c4\_\_u2084\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $x_{2}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a square of $C$. Then $\mathrm{CategoryTheory\_\_Square\_\_X\_u2081\_}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a square of $C$. Then $\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a square of $C$. Then $\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a square of $C$. Then $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the equivalence (from the docstring)

The equivalence is an equivalence of the set of squares of $C$ and the set of arrows of the set of arrows of $C$.

the equivalence (from the docstring)

The equivalence is an equivalence of the set of squares of $C$ and the set of arrows of the set of arrows of $C$.

the evaluation (from the name)

The evaluation is a functor of the set of squares of $C$ and $C$.

the evaluation (from the name)

The evaluation is a functor of the set of squares of $C$ and $C$.

the evaluation (from the name)

The evaluation is a functor of the set of squares of $C$ and $C$.

the evaluation (from the name)

The evaluation is a functor of the set of squares of $C$ and $C$.

the flip of sq (from the name)

Let $\mathrm{sq}$ be a square of $C$. Then the flip of $\mathrm{sq}$ is a square of $C$.

the flip equivalence (from the name)

The flip equivalence is an equivalence of the set of squares of $C$ and the set of squares of $C$.

the flip functor (from the name)

The flip functor is a functor of the set of squares of $C$ and the set of squares of $C$.

the functor (from the docstring)

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

the functor (from the docstring)

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

Let $\mathrm{self}$ be a square of $C$. Then $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a square of $C$. Then $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2083\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2081\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a square of $C$. Then $\mathrm{CategoryTheory\_\_Square\_\_f\_u2082\_\_u2084\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a square of $C$. Then $\mathrm{CategoryTheory\_\_Square\_\_f\_u2083\_\_u2084\_}$ applied to $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj7}$ applied to $\mathrm{self}$.

the isomorphism of x5 and x6 (from the name)

Let $x_{3}$ be an isomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2081\_}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2081\_}$ applied to $x_{2}$. Let $x_{4}$ be an isomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_}$ applied to $x_{2}$. Let $x_{5}$ be an isomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_}$ applied to $x_{2}$. Let $x_{6}$ be an isomorphism of $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $x_{2}$. Assume that the composition of $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2082\_}$ applied to $x_{1}$ and the homomorphism of $x_{4}$ is equal to the composition of the homomorphism of $x_{3}$ and $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2082\_}$ applied to $x_{2}$. Assume that the composition of $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2083\_}$ applied to $x_{1}$ and the homomorphism of $x_{5}$ is equal to the composition of the homomorphism of $x_{3}$ and $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2083\_}$ applied to $x_{2}$. Assume that the composition of $\mathrm{CategoryTheory\_\_Square\_\_f\_u2082\_\_u2084\_}$ applied to $x_{1}$ and the homomorphism of $x_{6}$ is equal to the composition of the homomorphism of $x_{4}$ and $\mathrm{CategoryTheory\_\_Square\_\_f\_u2082\_\_u2084\_}$ applied to $x_{2}$. Assume that the composition of $\mathrm{CategoryTheory\_\_Square\_\_f\_u2083\_\_u2084\_}$ applied to $x_{1}$ and the homomorphism of $x_{6}$ is equal to the composition of the homomorphism of $x_{5}$ and $\mathrm{CategoryTheory\_\_Square\_\_f\_u2083\_\_u2084\_}$ applied to $x_{2}$. Then the isomorphism of $x_{5}$ and $x_{6}$ is an isomorphism of $x_{1}$ and $x_{2}$.

the map of sq and F (from the name)

Let $\mathrm{sq}$ be a square of $C$. Let $F$ be a functor of $C$ and $D$. Then the map of $\mathrm{sq}$ and $F$ is a square of $D$.

the functor (from the docstring)

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

the opposite of sq (from the name)

Let $\mathrm{sq}$ be a square of $C$. Then the opposite of $\mathrm{sq}$ is a square of the set of opposites of $C$.

the equivalence (from the docstring)

The equivalence is an equivalence of the set of opposites of the set of squares of $C$ and the set of squares of the set of opposites of $C$.

the functor (from the docstring)

The functor is a functor of the set of opposites of the set of squares of $C$ and the set of squares of the set of opposites of $C$.

the functor (from the docstring)

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

the functor (from the docstring)

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

the opposite of sq (from the name)

Let $\mathrm{sq}$ be a square of the set of opposites of $C$. Then the opposite of $\mathrm{sq}$ is a square of $C$.

the functor (from the docstring)

The functor is a functor of the set of opposites of the set of squares of the set of opposites of $C$ and the set of squares of $C$.

subfunctor of F (from the name)

Let $F$ be a functor of $C$ and the set of sets. Then the subfunctors of $F$ are a basic type.

the homomorphism of h (from the name)

Assume that $G \leq \mathrm{G'}$. Then the homomorphism of $h$ is a homomorphism of the subfunctor as a functor of $G$ and the subfunctor as a functor of $\mathrm{G'}$.

the object of self and U (from the name)

Let $\mathrm{self}$ be a subfunctor of $F$. Let $U$ be an element of $C$. Then the object of $\mathrm{self}$ and $U$ is an element of the power set of the action of $F$ and $U$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $U$.

the subfunctor as a functor of G (from the docstring)

Let $G$ be a subfunctor of $F$. Then the subfunctor as a functor of $G$ is a functor of $C$ and the set of sets.

the inclusion of G (from the docstring)

Let $G$ be a subfunctor of $F$. Then the inclusion of $G$ is a homomorphism of the subfunctor as a functor of $G$ and $F$.

the equalizer of f and g (from the name)

Let $f$ and $g$ be homomorphisms of the subfunctor as a functor of $A$ and $x_{2}$. Then the equalizer of $f$ and $g$ is a subfunctor of $x_{1}$.

the fork of f and g (from the name)

Let $f$ and $g$ be homomorphisms of the subfunctor as a functor of $A$ and $x_{2}$. Then the fork of $f$ and $g$ is a fork of $f$ and $g$ defined as the inclusion of the inclusion of $f$ and $g$ and $\operatorname{condition}$ applied to $f$ and $g$.

Let $f$ and $g$ be homomorphisms of the subfunctor as a functor of $A$ and $x_{2}$. Then $\operatorname{forkIsLimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the fork of $f$ and $g$.

the lift of g and x3 (from the name)

Let $f$ and $g$ be homomorphisms of the subfunctor as a functor of $A$ and $x_{2}$. Let $x_{3}$ be a homomorphism of $G$ and the subfunctor as a functor of $A$ such that the composition of $x_{3}$ and $f$ is equal to the composition of $x_{3}$ and $g$. Then the lift of $g$ and $x_{3}$ is a homomorphism of $G$ and the subfunctor as a functor of the equalizer of $f$ and $g$.

the inclusion of f and g (from the name)

Let $f$ and $g$ be homomorphisms of the subfunctor as a functor of $A$ and $x_{2}$. Then the inclusion of $f$ and $g$ is a homomorphism of the subfunctor as a functor of the equalizer of $f$ and $g$ and the subfunctor as a functor of $A$ defined as the homomorphism of $\mathrm{CategoryTheory\_\_Subfunctor\_\_equalizer\_le}$ applied to $f$ and $g$.

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{PresheafIsFinite}$ holds for $F$, if the top is finite.

Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Let $x_{2}$ be a function from elements $i$ of $x_{1}$ to elements of the action of $F$ and $X$ applied to $i$. Then $\operatorname{PresheafIsGeneratedBy}$ holds for $F$, $i$ and $x_{2}$, if $\operatorname{IsGeneratedBy}$ holds for the top, $i$ and $x_{2}$.

G is finite (from the name)

Let $G$ be a subfunctor of $F$. Then we can say that $G$ is finite.

index of G (from the name)

Let $G$ be a subfunctor of $F$. Then an index of $G$ is an element of the function that maps $G$ to $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Subfunctor\_\_IsFinite\_\_exists\_isGeneratedBy}$.

Let $x_{1}$ be an index of $G$. Then $\operatorname{X}$ applied to $x_{1}$ is an opposite of $C$.

Let $i$ be an index of $G$. Then $\operatorname{x}$ applied to $i$ is an element of the action of $F$ and $\operatorname{X}$ applied to $i$.

Let $G$ be a subfunctor of $F$. Let $x_{2}$ be a function from elements $i$ of $x_{1}$ to elements of the action of $F$ and $X$ applied to $i$. Then $\operatorname{IsGeneratedBy}$ holds for $G$, $i$ and $x_{2}$, if the supremum of the function that maps $i$ to the subfunctor of $i$ applied to $i$ is equal to $G$.

Let $G$ be a subfunctor of $F$. Let $p$ be a homomorphism of $\mathrm{F'}$ and $F$. Then $\operatorname{fromPreimage}$ applied to $G$ and $p$ is a homomorphism of the subfunctor as a functor of the preimage of $G$ and $p$ and the subfunctor as a functor of $G$.

the image of G and f (from the docstring)

Let $G$ be a subfunctor of $F$. Let $f$ be a homomorphism of $F$ and $\mathrm{F'}$. Then the image of $G$ and $f$ is a subfunctor of $\mathrm{F'}$.

the lift of f and hf (from the name)

Let $f$ be a homomorphism of $\mathrm{F'}$ and $F$ such that the range of $f$ is less than or equal to $G$. Then the lift of $f$ and $\mathrm{hf}$ is a homomorphism of $\mathrm{F'}$ and the subfunctor as a functor of $G$.

the preimage of G and p (from the docstring)

Let $G$ be a subfunctor of $F$. Let $p$ be a homomorphism of $\mathrm{F'}$ and $F$. Then the preimage of $G$ and $p$ is a subfunctor of $\mathrm{F'}$.

the range of p (from the docstring)

Let $p$ be a homomorphism of $\mathrm{F'}$ and $F$. Then the range of $p$ is a subfunctor of $F$.

the range of p (from the name)

Let $p$ be a homomorphism of $\mathrm{F'}$ and $F$. Then the range of $p$ is a homomorphism of $\mathrm{F'}$ and the subfunctor as a functor of the range of $p$.

the subfunctor of x1 (from the name)

Let $x_{1}$ be an element of the action of $F$ and $X$. Then the subfunctor of $x_{1}$ is a subfunctor of $F$.

the family of G and s (from the name)

Let $G$ be a subfunctor of $F$. Let $s$ be an element of the action of $F$ and $U$. Then the family of $G$ and $s$ is a family of element of the subfunctor as a functor of $G$ and the arrow of the sieve of $G$ and $s$ defined as the function that maps $x_{1}$, $i$ and $\mathrm{hi}$ to $\operatorname{hom}$ applied to the map of $F$ and the opposite in $i$ and $s$.

the sieve of G and s (from the name)

Let $G$ be a subfunctor of $F$. Let $s$ be an element of the action of $F$ and $U$. Then the sieve of $G$ and $s$ is a sieve of the opposite of $U$.

submonoid functor of M (from the name)

Let $M$ be a functor of $C$ and the set of monoid categories. Then the submonoid functors of $M$ are a basic type.

the preimage of p and #2 (from the name)

Let $p$ be a homomorphism of $M$ and $\mathrm{M'}$. Let $\mathrm{S'}$ be a submonoid functor of $\mathrm{M'}$. Then the preimage of $p$ and $\mathrm{S'}$ is a submonoid functor of $M$.

the image of p and S (from the name)

Let $p$ be a homomorphism of $M$ and $\mathrm{M'}$. Let $S$ be a submonoid functor of $M$. Then the image of $p$ and $S$ is a submonoid functor of $\mathrm{M'}$.

the lift of p and hp (from the name)

Let $p$ be a homomorphism of $M$ and $\mathrm{M'}$. Let $\mathrm{S'}$ be a submonoid functor of $\mathrm{M'}$ such that the image of $p$ and the top is less than or equal to $\mathrm{S'}$. Then the lift of $p$ and $\mathrm{S'}$ is a homomorphism of $M$ and the functor of $\mathrm{S'}$.

the object of self and U (from the name)

Let $\mathrm{self}$ be a submonoid functor of $M$. Let $U$ be an element of $C$. Then the object of $\mathrm{self}$ and $U$ is a submonoid of the set of carriers of the action of $M$ and $U$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $U$.

the functor of S (from the name)

Let $S$ be a submonoid functor of $M$. Then the functor of $S$ is a functor of $C$ and the set of monoid categories.

the subfunctor of S (from the name)

Let $S$ be a submonoid functor of $M$. Then the subfunctor of $S$ is a subfunctor of the composition of $M$ and the forgetful functor of the set of monoid categories defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ to the carrier of $\operatorname{toSubsemigroup}$ applied to the object of $S$ and $x_{1}$ and the function that maps $x_{2}$ and $x_{3}$ to $\operatorname{map}$ applied to $S$.

the inclusion of S (from the docstring)

Let $S$ be a submonoid functor of $M$. Then the inclusion of $S$ is a homomorphism of the functor of $S$ and $M$.

Let $F$ be a functor of $C$ and the set of sets. Then $\operatorname{equivalenceMonoOver}$ applied to $F$ is an equivalence of the set of subfunctors of $F$ and $\operatorname{MonoOver}$ applied to $F$.

the order isomorphism of F (from the docstring)

Let $F$ be a functor of $C$ and the set of sets. Then the order isomorphism of $F$ is an order isomorphism of the set of subfunctors of $F$ and the set of subobjects of $F$.

X is a Artinian object (from the name)

Let $X$ be an element of $C$. Then $X$ is an Artinian object, if $\operatorname{Is}$ holds for $\operatorname{isArtinianObject}$ and $X$.

There is an object property of $C$. Proof. Let $X$ be arbitrary. By X. By CategoryTheory__Subobject. By WellFoundedLT.

the simple subobject of h2 (from the name)

Assume that $X$ is not a zero. Then the simple subobject of $h_{2}$ is an element of $C$ defined as the action of $\operatorname{underlying}$ and $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_exists\_simple\_subobject}$ applied to $h_{2}$.

the monomorphism from the arbitrary simple subobject of h2 (from the docstring)

Assume that $X$ is not a zero. Then the monomorphism from the arbitrary simple subobject of $h_{2}$ is a homomorphism of the simple subobject of $h_{2}$ and $X$ defined as the arrow of $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_exists\_simple\_subobject}$ applied to $h_{2}$.

subobject of X (from the name)

Let $X$ be an element of $C$. Then a subobject of $X$ is an element of the function that maps $X$ to the set of thin skeletons of $\operatorname{MonoOver}$ applied to $X$.

the arrow of Y (from the name)

Let $Y$ be a subobject of $X$. Then the arrow of $Y$ is a homomorphism of the action of $\operatorname{underlying}$ and $Y$ and $X$ defined as the homomorphism of the object of the action of the representative and $Y$.

Let $X$ be an element of $C$. Then $\operatorname{equivMonoOver}$ applied to $X$ is an equivalence of the set of subobjects of $X$ and $\operatorname{MonoOver}$ applied to $X$ defined as the equivalence of $\operatorname{MonoOver}$ applied to $X$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{exists}$ applied to $f$ is a functor of the set of subobjects of $X$ and the set of subobjects of $Y$ defined as $\operatorname{lower}$ applied to $\operatorname{exists}$ applied to $f$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{existsCompRepresentativeIso}$ applied to $f$ is an isomorphism of the composition of $\operatorname{exists}$ applied to $f$ and the representative and the composition of the representative and $\operatorname{exists}$ applied to $f$ defined as the lower composition representative isomorphism of $\operatorname{exists}$ applied to $f$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $x_{1}$ be a subobject of $X$. Then $\operatorname{existsIsoImage}$ applied to $f$ and $x_{1}$ is an isomorphism of the action of $\operatorname{underlying}$ and the action of $\operatorname{exists}$ applied to $f$ and $x_{1}$ and the categorical image of the composition of the arrow of $x_{1}$ and $f$ defined as the map isomorphism of the composition of $\operatorname{forget}$ applied to $Y$ and $\operatorname{forget}$ applied to $Y$ and the application of $\operatorname{existsCompRepresentativeIso}$ applied to $f$ and $x_{1}$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{existsPullbackAdj}$ applied to $f$ is an adjunction of $\operatorname{exists}$ applied to $f$ and the pullback of $f$ defined as the lower adjunction of $\operatorname{existsPullbackAdj}$ applied to $f$.

the image factorisation of f and x1 (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $x_{1}$ be a subobject of $X$. Then the image factorisation of $f$ and $x_{1}$ is an image factorisation of the composition of the arrow of $x_{1}$ and $f$.

the isomorphism of X and Y (from the name)

Let $X$ and $Y$ be subobjects of $B$ such that $\EqtMACRoH {X}{Y}$. Then the isomorphism of $X$ and $Y$ is an isomorphism of the action of $\operatorname{underlying}$ and $X$ and the action of $\operatorname{underlying}$ and $Y$.

the isomorphism of X and f (from the name)

Let $X$ be a subobject of $B$. Let $f$ be a homomorphism of $A$ and $B$ such that $\EqtMACRoH {X}{\operatorname{mk} (f)}$. Then the isomorphism of $X$ and $f$ is an isomorphism of the action of $\operatorname{underlying}$ and $X$ and $A$.

the isomorphism of f and X (from the name)

Let $f$ be a homomorphism of $A$ and $B$. Let $X$ be a subobject of $B$ such that $\EqtMACRoH {\operatorname{mk} (f)}{X}$. Then the isomorphism of $f$ and $X$ is an isomorphism of $A$ and the action of $\operatorname{underlying}$ and $X$.

the isomorphism of f and g (from the name)

Let $f$ be a homomorphism of $x_{1}$ and $B$. Let $g$ be a homomorphism of $x_{2}$ and $B$ such that $\EqtMACRoH {\operatorname{mk} (f)}{\operatorname{mk} (g)}$. Then the isomorphism of $f$ and $g$ is an isomorphism of $x_{1}$ and $x_{2}$.

the lift of F and f1 (from the name)

Let $F$ be a function from elements $A_{1}$ of $C$ and homomorphisms $f_{1}$ of $A_{1}$ and $X$ and elements of $\mathrm{Proof}$ applied to the proposition that $f_{1}$ is a monomorphism to elements of $x_{1}$ such that for all elements $A$ and $B$ of $C$, for all homomorphisms $f$ of $A$ and $X$, for all homomorphisms $g$ of $B$ and $X$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to the proposition that $f$ is a monomorphism, for all elements $h_{2}$ of $\mathrm{Proof}$ applied to the proposition that $g$ is a monomorphism, for all isomorphisms $i$ of $A$ and $B$, if the composition of the homomorphism of $i$ and $g$ is equal to $f$, then $\EqtMACRoH {F (A , f , h_{1})}{F (B , g , h_{2})}$. Let $x_{2}$ be a subobject of $X$. Then the lift of $A_{1}$ and $F$ is an element of $x_{1}$.

Let $F$ be a functor of $\operatorname{MonoOver}$ applied to $X$ and $\operatorname{MonoOver}$ applied to $Y$. Then $\operatorname{lower}$ applied to $F$ is a functor of the set of subobjects of $X$ and the set of subobjects of $Y$ defined as the map of $F$.

the lower adjunction of h (from the name)

Let $h$ be an adjunction of $L$ and $R$. Then the lower adjunction of $h$ is an adjunction of $\operatorname{lower}$ applied to $L$ and $\operatorname{lower}$ applied to $R$ defined as the lower adjunction of $L$ and $h$.

the lower composition representative isomorphism of F (from the name)

Let $F$ be a functor of $\operatorname{MonoOver}$ applied to $Y$ and $\operatorname{MonoOver}$ applied to $X$. Then the lower composition representative isomorphism of $F$ is an isomorphism of the composition of $\operatorname{lower}$ applied to $F$ and the representative and the composition of the representative and $F$ defined as the map composition from thin skeleton isomorphism of $F$.

the lower equivalence of e (from the name)

Let $e$ be an equivalence of $\operatorname{MonoOver}$ applied to $A$ and $\operatorname{MonoOver}$ applied to $B$. Then the lower equivalence of $e$ is an equivalence of the set of subobjects of $A$ and the set of subobjects of $B$.

Let $F$ be a functor of $\operatorname{MonoOver}$ applied to $X$ and the set of functors of $\operatorname{MonoOver}$ applied to $Y$ and $\operatorname{MonoOver}$ applied to $Z$. Then $\mathrm{CategoryTheory\_\_Subobject\_\_lower\_u2082\_}$ applied to $F$ is a functor of the set of subobjects of $X$ and the set of functors of the set of subobjects of $Y$ and the set of subobjects of $Z$ defined as the map of $F$.

the map of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $f$ is a functor of the set of subobjects of $X$ and the set of subobjects of $Y$ defined as $\operatorname{lower}$ applied to the map of $f$.

the map isomorphism of e (from the name)

Let $e$ be an isomorphism of $A$ and $B$. Then the map isomorphism of $e$ is an equivalence of the set of subobjects of $A$ and the set of subobjects of $B$ defined as the lower equivalence of the map isomorphism of $e$.

the map isomorphism to order isomorphism of e (from the name)

Let $e$ be an isomorphism of $X$ and $Y$. Then the map isomorphism to order isomorphism of $e$ is an order isomorphism of the set of subobjects of $X$ and the set of subobjects of $Y$.

the left adjoint of f (from the docstring)

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

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

the subobject of X and Y (from the name)

Let $X$ and $Y$ be subobjects of $B$ such that $X \leq Y$. Then the subobject of $X$ and $Y$ is a homomorphism of the action of $\operatorname{underlying}$ and $X$ and the action of $\operatorname{underlying}$ and $Y$ defined as the map of $\operatorname{underlying}$ and the homomorphism of $h$.

the subobject of X and f (from the name)

Let $X$ be a subobject of $B$. Let $f$ be a homomorphism of $A$ and $B$ such that $X \leq \operatorname{mk} (f)$. Then the subobject of $X$ and $f$ is a homomorphism of the action of $\operatorname{underlying}$ and $X$ and $A$ defined as the composition of the subobject of $X$ and $\operatorname{mk}$ applied to $f$ and the homomorphism of the underlying isomorphism of $f$.

the subobject of f and X (from the name)

Let $f$ be a homomorphism of $A$ and $B$. Let $X$ be a subobject of $B$ such that $\operatorname{mk} (f)\leq X$. Then the subobject of $f$ and $X$ is a homomorphism of $A$ and the action of $\operatorname{underlying}$ and $X$ defined as the composition of the inverse of the underlying isomorphism of $f$ and the subobject of $\operatorname{mk}$ applied to $f$ and $X$.

the subobject of f and g (from the name)

Let $f$ be a homomorphism of $x_{1}$ and $B$. Let $g$ be a homomorphism of $x_{2}$ and $B$ such that $\operatorname{mk} (f)\leq \operatorname{mk} (g)$. Then the subobject of $f$ and $g$ is a homomorphism of $x_{1}$ and $x_{2}$ defined as the composition of the inverse of the underlying isomorphism of $f$ and the composition of the subobject of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $g$ and the homomorphism of the underlying isomorphism of $g$.

the pullback of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback of $f$ is a functor of the set of subobjects of $Y$ and the set of subobjects of $X$ defined as $\operatorname{lower}$ applied to the pullback of $f$.

the pullback projection of f and y (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $y$ be a subobject of $Y$. Then the pullback projection of $f$ and $y$ is a homomorphism of the action of $\operatorname{underlying}$ and the action of the pullback of $f$ and $y$ and the action of $\operatorname{underlying}$ and $y$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Subobject\_\_isPullback\_aux}$ applied to $f$ and $y$.

the representative (from the name)

The representative is a functor of the set of subobjects of $X$ and $\operatorname{MonoOver}$ applied to $X$ defined as the functor of $\operatorname{equivMonoOver}$ applied to $X$.

the representative isomorphism of A (from the name)

Let $A$ be an element of $\operatorname{MonoOver}$ applied to $X$. Then the representative isomorphism of $A$ is an isomorphism of the action of the representative and the action of the functor of $\operatorname{MonoOver}$ applied to $X$ and $A$ and $A$ defined as the application of the counit isomorphism of $\operatorname{equivMonoOver}$ applied to $X$ and $A$.

$\operatorname{underlying}$ is a functor of the set of subobjects of $X$ and $C$ defined as the composition of the representative and the composition of $\operatorname{forget}$ applied to $X$ and $\operatorname{forget}$ applied to $X$.

the underlying isomorphism of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the underlying isomorphism of $f$ is an isomorphism of the action of $\operatorname{underlying}$ and $\operatorname{mk}$ applied to $f$ and $X$ defined as the map isomorphism of the composition of $\operatorname{forget}$ applied to $Y$ and $\operatorname{forget}$ applied to $Y$ and the representative isomorphism of $\operatorname{mk}$ applied to $f$.

C has subobject classifiers (from the name)

Let $C$ be a set. Then we can say that $C$ has subobject classifiers.

the truth of C (from the name)

Let $C$ be a set. Then the truth of $C$ is a homomorphism of $\mathrm{CategoryTheory\_\_HasSubobjectClassifier\_\_\_u3a9\_\_u2080\_}$ applied to $C$ and $\mathrm{CategoryTheory\_\_HasSubobjectClassifier\_\_\_u3a9\_}$ applied to $C$ defined as the truth morphism of the subobject classifier of $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_HasSubobjectClassifier\_\_exists\_classifier}$.

$\operatorname{truthIsRegularMono}$ is a regular monomorphism of the truth of $C$ defined as the regular monomorphism of the truth of $C$.

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_HasSubobjectClassifier\_\_\_u3a9\_}$ applied to $C$ is an element of $C$ defined as $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_}$ applied to $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_HasSubobjectClassifier\_\_exists\_classifier}$.

Let $C$ be a set. Then $\mathrm{CategoryTheory\_\_HasSubobjectClassifier\_\_\_u3a9\_\_u2080\_}$ applied to $C$ is an element of $C$ defined as $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_\_u2080\_}$ applied to $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_HasSubobjectClassifier\_\_exists\_classifier}$.

Let $m$ be a homomorphism of $U$ and $X$. Then $\mathrm{CategoryTheory\_\_HasSubobjectClassifier\_\_\_u3c7\_}$ applied to $m$ is a homomorphism of $X$ and $\mathrm{CategoryTheory\_\_HasSubobjectClassifier\_\_\_u3a9\_}$ applied to $C$ defined as $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3c7\_}$ applied to $\operatorname{some}$ applied to $\mathrm{CategoryTheory\_\_HasSubobjectClassifier\_\_exists\_classifier}$ and $m$.

classifier of C (from the name)

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

the homomorphism of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be classifiers of $C$. Then the homomorphism of $x_{1}$ and $x_{2}$ is a homomorphism of $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_}$ applied to $x_{2}$ defined as $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3c7\_}$ applied to $x_{2}$ and the truth morphism of the subobject classifier of $x_{1}$.

$\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_isTerminal\_u3a9\_\_u2080\_}$ is an element of $\operatorname{IsTerminal}$ applied to $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_\_u2080\_}$ applied to $c$ defined as $\operatorname{ofUnique}$ applied to $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_\_u2080\_}$ applied to $c$.

Let $x_{1}$ and $x_{2}$ be elements of $C$. Let $t$ be an element of $\operatorname{IsTerminal}$ applied to $x_{1}$. Let $\mathrm{truth}$ be a homomorphism of $x_{1}$ and $x_{2}$. Let $x_{3}$ be a function from elements $U_{2}$ of $C$ and elements $X_{2}$ of $C$ and homomorphisms $m_{2}$ of $U_{2}$ and $X_{2}$ and elements of $\mathrm{Proof}$ applied to the proposition that $m_{2}$ is a monomorphism to homomorphisms of $X_{2}$ and $x_{2}$ such that for all elements $U_{1}$ of $C$, for all elements $X_{1}$ of $C$, for all homomorphisms $m_{1}$ of $U_{1}$ and $X_{1}$, for all elements $h_{2}$ of $\mathrm{Proof}$ applied to the proposition that $m_{1}$ is a monomorphism, $\operatorname{IsPullback}$ holds for $m_{1}$, $\operatorname{from}$ applied to $t$ and $U_{1}$, $x_{3}$ applied to $U_{1}$, $X_{1}$, $m_{1}$ and $h_{2}$ and $\mathrm{truth}$ and for all elements $U$ of $C$, for all elements $X$ of $C$, for all homomorphisms $m$ of $U$ and $X$, for all elements $h$ of $\mathrm{Proof}$ applied to the proposition that $m$ is a monomorphism, for all homomorphisms $x_{4}$ of $X$ and $x_{2}$, if $\operatorname{IsPullback}$ holds for $m$, $\operatorname{from}$ applied to $t$ and $U$, $x_{4}$ and $\mathrm{truth}$, then $\EqtMACRoH {x_{4}}{x_{3} (U , X , m , h)}$. Then $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_mkOfTerminal\_u3a9\_\_u2080\_}$ applied to $x_{1}$, $t$, $x_{2}$, $\mathrm{truth}$, $U_{2}$, $X_{2}$, $m_{2}$, $x_{3}$, $\mathrm{isPullback}$ and $\mathrm{uniq}$ is a classifier of $C$.

the classifier of x2 and e (from the name)

Let $x_{2}$ be a classifier of $C$. Let $e$ be an equivalence of $C$ and $D$. Then the classifier of $x_{2}$ and $e$ is a classifier of $D$.

the classifier of C1 and t (from the name)

Let $x_{1}$ be a classifier of $C$. Let $x_{4}$ be an isomorphism of $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_}$ applied to $x_{1}$ and $x_{3}$. Let $x_{5}$ be an isomorphism of $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_\_u2080\_}$ applied to $x_{1}$ and $x_{2}$. Let $\mathrm{from'}$ be a function from elements $C_{1}$ of $C$ to homomorphisms of $C_{1}$ and $x_{2}$. Let $t$ be a homomorphism of $x_{2}$ and $x_{3}$ such that $\mathrm{autoParam}$ holds for the proposition that $t$ is equal to the composition of the inverse of $x_{5}$ and the composition of the truth morphism of the subobject classifier of $x_{1}$ and the homomorphism of $x_{4}$ and $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_ofIso\_\_\_auto\_1}$. Then the classifier of $C_{1}$ and $\mathrm{from'}$ is a classifier of $C$.

Let $x_{1}$ be a classifier of $C$. Then $\operatorname{representableBy}$ applied to $x_{1}$ is an element of $\operatorname{RepresentableBy}$ applied to the presheaf of $C$ and $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_}$ applied to $x_{1}$.

the truth morphism of the subobject classifier of self (from the docstring)

Let $\mathrm{self}$ be a classifier of $C$. Then the truth morphism of the subobject classifier of $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_\_u2080\_}$ applied to $\mathrm{self}$ and $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the subobject of x1 (from the docstring)

Let $x_{1}$ be a classifier of $C$. Then the subobject of $x_{1}$ is a subobject of $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to the truth morphism of the subobject classifier of $x_{1}$.

Let $x_{1}$ and $x_{2}$ be classifiers of $C$. Then $\operatorname{uniqueUpToIso}$ applied to $x_{1}$ and $x_{2}$ is an isomorphism of $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_}$ applied to $x_{1}$ and $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_}$ applied to $x_{2}$.

Let $\mathrm{self}$ be a classifier of $C$. Then $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a classifier of $C$. Then $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_\_u2080\_}$ applied to $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a classifier of $C$. Let $m$ be a homomorphism of $U$ and $X$. Then $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3c7\_}$ applied to $\mathrm{self}$ and $m$ is a homomorphism of $X$ and $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$ and $m$.

Let $\mathrm{self}$ be a classifier of $C$. Let $U$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3c7\_\_u2080\_}$ applied to $\mathrm{self}$ and $U$ is a homomorphism of $U$ and $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_\_u3a9\_\_u2080\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$ and $U$.

Let $x_{1}$ be an element of $C$. Then an element of $\operatorname{SubobjectRepresentableBy}$ applied to $x_{1}$ is an element of the function that maps $x_{1}$ to $\operatorname{RepresentableBy}$ applied to the presheaf of $C$ and $x_{1}$.

the classifier of h1 (from the name)

Let $h_{1}$ be an element of $\operatorname{SubobjectRepresentableBy}$ applied to $x_{1}$. Then the classifier of $h_{1}$ is a classifier of $C$.

Let $h_{1}$ be an element of $\operatorname{SubobjectRepresentableBy}$ applied to $x_{1}$. Then $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_isTerminal\_u3a9\_\_u2080\_}$ applied to $h_{1}$ is an element of $\operatorname{IsTerminal}$ applied to the action of $\operatorname{underlying}$ and $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_\_u3a9\_\_u2080\_}$ applied to $h_{1}$.

the isomorphism of h1 and m (from the name)

Let $h_{1}$ be an element of $\operatorname{SubobjectRepresentableBy}$ applied to $x_{1}$. Let $m$ be a homomorphism of $U$ and $X$. Then the isomorphism of $h_{1}$ and $m$ is an isomorphism of $\operatorname{mk}$ applied to $m$ and the action of the representative and the action of the pullback of $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_\_u3c7\_}$ applied to $h_{1}$ and $m$ and $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_\_u3a9\_\_u2080\_}$ applied to $h_{1}$.

the isomorphism of h1 (from the name)

Let $h_{1}$ be an element of $\operatorname{SubobjectRepresentableBy}$ applied to $x_{1}$. Then the isomorphism of $h_{1}$ is an isomorphism of the action of $\operatorname{underlying}$ and $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_\_u3a9\_\_u2080\_}$ applied to $h_{1}$ and $\operatorname{terminal}$ applied to $C$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_isTerminal\_u3a9\_\_u2080\_}$ applied to $h_{1}$ and $\operatorname{isLimit}$ applied to $\operatorname{empty}$ applied to $C$.

Let $h_{1}$ be an element of $\operatorname{SubobjectRepresentableBy}$ applied to $x_{1}$. Then $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_\_u3a9\_\_u2080\_}$ applied to $h_{1}$ is a subobject of $x_{1}$ defined as $\operatorname{homEquiv}$ applied to $h_{1}$ and the identity morphism of $x_{1}$.

the projection of h1 and m (from the name)

Let $h_{1}$ be an element of $\operatorname{SubobjectRepresentableBy}$ applied to $x_{1}$. Let $m$ be a homomorphism of $U$ and $X$. Then the projection of $h_{1}$ and $m$ is a homomorphism of $U$ and the action of $\operatorname{underlying}$ and $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_\_u3a9\_\_u2080\_}$ applied to $h_{1}$ defined as the composition of the left of the homomorphism of the homomorphism of the isomorphism of $h_{1}$ and $m$ and the pullback projection of $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_\_u3c7\_}$ applied to $h_{1}$ and $m$ and $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_\_u3a9\_\_u2080\_}$ applied to $h_{1}$.

Let $h_{1}$ be an element of $\operatorname{SubobjectRepresentableBy}$ applied to $x_{1}$. Let $m$ be a homomorphism of $U$ and $X$. Then $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_\_u3c7\_}$ applied to $h_{1}$ and $m$ is a homomorphism of $X$ and $x_{1}$ defined as $\operatorname{symm}$ applied to the homomorphism equivalence of $h_{1}$ and $\operatorname{mk}$ applied to $m$.

Let $h_{1}$ be an element of $\operatorname{SubobjectRepresentableBy}$ applied to $x_{1}$. Let $U$ be an element of $C$. Then $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_\_u3c7\_\_u2080\_}$ applied to $h_{1}$ and $U$ is a homomorphism of $U$ and the action of $\operatorname{underlying}$ and $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_\_u3a9\_\_u2080\_}$ applied to $h_{1}$ defined as $\operatorname{from}$ applied to $\mathrm{CategoryTheory\_\_SubobjectRepresentableBy\_\_isTerminal\_u3a9\_\_u2080\_}$ applied to $h_{1}$ and $U$.

the lift quotient of P and hq (from the name)

Let $P$ be a subobject of $\operatorname{op}$ applied to the left object of $A$ such that the composition of the map of $S$ and the opposite of the arrow of $P$ and $q$ is equal to the homomorphism of $A$. Then the lift quotient of $P$ and $\mathrm{hq}$ is a subobject of $\operatorname{op}$ applied to $A$ defined as $\operatorname{mk}$ applied to the opposite in the homomorphism of the opposite of the arrow of $P$ and $\mathrm{hq}$.

the project quotient of x2 (from the name)

Let $x_{2}$ be a subobject of $\operatorname{op}$ applied to $A$. Then the project quotient of $x_{2}$ is a subobject of $\operatorname{op}$ applied to the left object of $A$.

the quotient equivalence of A (from the name)

Let $A$ be a costructured arrow of $S$ and $T$. Then the quotient equivalence of $A$ is an order isomorphism of the set of subobjects of $\operatorname{op}$ applied to $A$ and $\SubtypeSet {P}{\mathrm{exists} (\operatorname{Hom} (\operatorname{obj} (S , \operatorname{unop} (\operatorname{obj} (\operatorname{underlying} , P))), T), \lambda q . \EqtMACRoH {\operatorname{comp} (\operatorname{map} (S , \operatorname{unop} (\operatorname{arrow} (P))), q)}{\operatorname{hom} (A)})}$.

the lift subobject of P and hq (from the name)

Let $P$ be a subobject of the right object of $A$ such that the composition of $q$ and the map of $T$ and the arrow of $P$ is equal to the homomorphism of $A$. Then the lift subobject of $P$ and $\mathrm{hq}$ is a subobject of $A$ defined as $\operatorname{mk}$ applied to the homomorphism of the arrow of $P$ and $\mathrm{hq}$.

the project subobject of x2 (from the name)

Let $x_{2}$ be a subobject of $A$. Then the project subobject of $x_{2}$ is a subobject of the right object of $A$.

the subobject equivalence of A (from the name)

Let $A$ be a structured arrow of $S$ and $T$. Then the subobject equivalence of $A$ is an order isomorphism of the set of subobjects of $A$ and $\SubtypeSet {P}{\mathrm{exists} (\operatorname{Hom} (S , \operatorname{obj} (T , \operatorname{obj} (\operatorname{underlying} , P))), \lambda q . \EqtMACRoH {\operatorname{comp} (q , \operatorname{map} (T , \operatorname{arrow} (P)))}{\operatorname{hom} (A)})}$.

Let $P$ be an element of $\operatorname{MonoOver}$ applied to $Y$. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{Factors}$ holds for $P$ and $f$, if there exists a homomorphism $g$ of $X$ and the left of the object of $P$, such that the composition of $g$ and the arrow of $P$ is equal to $f$.

Let $P$ be an element of $\operatorname{MonoOver}$ applied to $Y$. Let $f$ be a homomorphism of $X$ and $Y$ such that $\operatorname{Factors}$ holds for $P$ and $f$. Then $\operatorname{factorThru}$ applied to $P$, $f$ and $h$ is a homomorphism of $X$ and the left of the object of $P$ defined as $\operatorname{choose}$ applied to $h$.

Let $P$ be a subobject of $Y$. Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $\operatorname{Factors}$ holds for $P$ and $f$.

Let $P$ be a subobject of $Y$. Let $f$ be a homomorphism of $X$ and $Y$ such that $\operatorname{Factors}$ holds for $P$ and $f$. Then $\operatorname{factorThru}$ applied to $P$, $f$ and $h$ is a homomorphism of $X$ and the action of $\operatorname{underlying}$ and $P$.

the homomorphism of h (from the name)

Assume that $\operatorname{Factors}$ holds for $Q$ and the arrow of $P$. Then the homomorphism of $h$ is a homomorphism of $P$ and $Q$ defined as the homomorphism of $\mathrm{CategoryTheory\_\_Subobject\_\_le\_of\_factors}$ applied to $h$.

the bottom coercion isomorphism zero (from the name)

The bottom coercion isomorphism zero is an isomorphism of the left of the object of the bottom and $0$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{initialIsInitial}$ and $\operatorname{zeroIsInitial}$.

Let $f$ be an element of $\operatorname{MonoOver}$ applied to $X$. Then $\operatorname{botLE}$ applied to $f$ is a homomorphism of the bottom and $f$.

the infimum (from the name)

The infimum is a functor of $\operatorname{MonoOver}$ applied to $A$ and the set of functors of $\operatorname{MonoOver}$ applied to $A$ and $\operatorname{MonoOver}$ applied to $A$.

Let $f$ and $g$ be elements of $\operatorname{MonoOver}$ applied to $A$. Then $\operatorname{infLELeft}$ applied to $f$ and $g$ is a homomorphism of the action of the action of the infimum and $f$ and $g$ and $f$.

Let $f$ and $g$ be elements of $\operatorname{MonoOver}$ applied to $A$. Then $\operatorname{infLERight}$ applied to $f$ and $g$ is a homomorphism of the action of the action of the infimum and $f$ and $g$ and $g$.

Let $f$, $g$ and $h_{1}$ be elements of $\operatorname{MonoOver}$ applied to $A$. Let $x_{1}$ be a homomorphism of $h_{1}$ and $f$. Let $x_{2}$ be a homomorphism of $h_{1}$ and $g$. Then $\operatorname{leInf}$ applied to $f$, $g$, $h_{1}$, $x_{1}$ and $x_{2}$ is a homomorphism of $h_{1}$ and the action of the action of the infimum and $f$ and $g$.

Let $f$ and $g$ be elements of $\operatorname{MonoOver}$ applied to $A$. Then $\operatorname{leSupLeft}$ applied to $f$ and $g$ is a homomorphism of $f$ and the action of the action of the supremum and $f$ and $g$.

Let $f$ and $g$ be elements of $\operatorname{MonoOver}$ applied to $A$. Then $\operatorname{leSupRight}$ applied to $f$ and $g$ is a homomorphism of $g$ and the action of the action of the supremum and $f$ and $g$.

the morphism to the top object in f (from the docstring)

Let $f$ be an element of $\operatorname{MonoOver}$ applied to $X$. Then the morphism to the top object in $f$ is a homomorphism of $f$ and the top.

the map bottom of f (from the name)

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

the map top of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map top of $f$ is an isomorphism of the action of the map of $f$ and the top and $\operatorname{mk}$ applied to $f$.

the pullback of f (from the docstring)

Let $f$ be a homomorphism of $A$ and $B$. Then the pullback of $f$ is an isomorphism of the action of the pullback of $f$ and $\operatorname{mk}$ applied to $f$ and the top defined as the isomorphism of the morphism to the top object in the action of the pullback of $f$ and $\operatorname{mk}$ applied to $f$ and $\operatorname{topLEPullbackSelf}$ applied to $f$.

the pullback of the top object in f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback of the top object in $f$ is an isomorphism of the action of the pullback of $f$ and the top and the top.

the supremum (from the name)

The supremum is a functor of $\operatorname{MonoOver}$ applied to $A$ and the set of functors of $\operatorname{MonoOver}$ applied to $A$ and $\operatorname{MonoOver}$ applied to $A$ defined as the object level part of the currying functor of the composition of the product of $\operatorname{forget}$ applied to $A$ and $\operatorname{forget}$ applied to $A$ and the composition of the action of $\operatorname{uncurry}$ and the coproduct and the image.

Let $f$, $g$ and $h_{2}$ be elements of $\operatorname{MonoOver}$ applied to $A$. Let $x_{1}$ be a homomorphism of $f$ and $h_{2}$. Let $x_{2}$ be a homomorphism of $g$ and $h_{2}$. Then $\operatorname{supLe}$ applied to $f$, $g$, $h_{2}$, $x_{1}$ and $x_{2}$ is a homomorphism of the action of the action of the supremum and $f$ and $g$ and $h_{2}$.

Let $f$ be a homomorphism of $A$ and $B$. Then $\operatorname{topLEPullbackSelf}$ applied to $f$ is a homomorphism of the top and the action of the pullback of $f$ and $\operatorname{mk}$ applied to $f$.

$\operatorname{botCoeIsoInitial}$ is an isomorphism of the action of $\operatorname{underlying}$ and the bottom and $\operatorname{initial}$ applied to $C$ defined as the underlying isomorphism of $\operatorname{to}$ applied to $B$.

the bottom coercion isomorphism zero (from the name)

The bottom coercion isomorphism zero is an isomorphism of the action of $\operatorname{underlying}$ and the bottom and $0$ defined as the composition of $\operatorname{botCoeIsoInitial}$ and $\operatorname{uniqueUpToIso}$ applied to $\operatorname{initialIsInitial}$ and $\operatorname{zeroIsInitial}$.

the functor of C (from the name)

Let $C$ be a set. Then the functor of $C$ is a functor of the set of opposites of $C$ and the set of sets.

the infimum (from the name)

The infimum is a functor of the set of subobjects of $A$ and the set of functors of the set of subobjects of $A$ and the set of subobjects of $A$ defined as the map of the infimum.

the infimum of s (from the name)

Let $s$ be an element of the power set of the set of subobjects of $A$. Then the infimum of $s$ is a subobject of $A$ defined as $\operatorname{mk}$ applied to the wide pullback inclusion of $s$.

the supremum of s (from the name)

Let $s$ be an element of the power set of the set of subobjects of $A$. Then the supremum of $s$ is a subobject of $A$ defined as $\operatorname{mk}$ applied to the inclusion of the image of $\operatorname{smallCoproductDesc}$ applied to $s$.

Let $s$ be an element of the power set of the set of subobjects of $A$. Then $\operatorname{smallCoproductDesc}$ applied to $s$ is a homomorphism of the sigma object of the function that maps $j$ to the action of $\operatorname{underlying}$ and $\operatorname{symm}$ applied to the equivalence shrink of the set of subobjects of $A$ and $j$ and $A$ defined as $\operatorname{desc}$ applied to the function that maps $j$ to the arrow of $\operatorname{symm}$ applied to the equivalence shrink of the set of subobjects of $A$ and $j$.

the subobject lattice of Y (from the docstring)

Let $Y$ be a subobject of $X$. Then the subobject lattice of $Y$ is an order isomorphism of the set of subobjects of the action of $\operatorname{underlying}$ and $Y$ and the set of elements of $\operatorname{Iic}$ applied to $Y$.

the supremum (from the name)

The supremum is a functor of the set of subobjects of $A$ and the set of functors of the set of subobjects of $A$ and the set of subobjects of $A$ defined as the map of the supremum.

Let $f$ and $g$ be subobjects of $A$. Then $\operatorname{supIsImage}$ applied to $f$ and $g$ is an element of $\operatorname{IsImage}$ applied to the supremum monomorphism factorisation of $f$ and $g$.

the supremum isomorphism image of f and g (from the name)

Let $f$ and $g$ be subobjects of $A$. Then the supremum isomorphism image of $f$ and $g$ is an isomorphism of the action of $\operatorname{underlying}$ and $\MaxmaxMACRoAF {f}{g}$ and the categorical image of $\operatorname{desc}$ applied to the arrow of $f$ and the arrow of $g$ defined as the isomorphism extension of $\operatorname{supIsImage}$ applied to $f$ and $g$ and $\operatorname{isImage}$ applied to $\operatorname{desc}$ applied to the arrow of $f$ and the arrow of $g$.

the supremum monomorphism factorisation of f and g (from the name)

Let $f$ and $g$ be subobjects of $A$. Then the supremum monomorphism factorisation of $f$ and $g$ is a monomorphism factorisation of $\operatorname{desc}$ applied to the arrow of $f$ and the arrow of $g$.

the wide cospan of s (from the name)

Let $s$ be an element of the power set of the set of subobjects of $A$. Then the wide cospan of $s$ is a functor of the set of wide pullback shapes of the set of elements of the image of $\operatorname{coe}$ applied to the equivalence shrink of the set of subobjects of $A$ and $s$ and $C$ defined as the wide cospan of the function that maps $j$ to the action of $\operatorname{underlying}$ and $\operatorname{symm}$ applied to the equivalence shrink of the set of subobjects of $A$ and $j$ and the function that maps $j_{1}$ to the arrow of $\operatorname{symm}$ applied to the equivalence shrink of the set of subobjects of $A$ and $j_{1}$.

the wide pullback of s (from the name)

Let $s$ be an element of the power set of the set of subobjects of $A$. Then the wide pullback of $s$ is an element of $C$ defined as the limit of the wide cospan of $s$.

the wide pullback inclusion of s (from the name)

Let $s$ be an element of the power set of the set of subobjects of $A$. Then the wide pullback inclusion of $s$ is a homomorphism of the wide pullback of $s$ and $A$ defined as the projection from the limit object to a value of the functor of the wide cospan of $s$ and $\operatorname{none}$.

the cokernel order homomorphism of X (from the name)

Let $X$ be an element of $C$. Then the cokernel order homomorphism of $X$ is an order homomorphism of the set of subobjects of $X$ and the set of order duals of the set of subobjects of $\operatorname{op}$ applied to $X$.

the equalizer subobject of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the equalizer subobject of $f$ and $g$ is a subobject of $X$ defined as $\operatorname{mk}$ applied to the inclusion of $f$ and $g$.

the equalizer subobject isomorphism of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the equalizer subobject isomorphism of $f$ and $g$ is an isomorphism of the action of $\operatorname{underlying}$ and the equalizer subobject of $f$ and $g$ and the equalizer of $f$ and $g$ defined as the underlying isomorphism of the inclusion of $f$ and $g$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{factorThruImageSubobject}$ applied to $f$ is a homomorphism of $X$ and the action of $\operatorname{underlying}$ and the image of $f$ defined as the composition of the map from the source to the image of $f$ and the inverse of the image subobject isomorphism of $f$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $h_{1}$ be a homomorphism of $W$ and $X$ such that the composition of $h_{1}$ and $f$ is equal to $0$. Then $\operatorname{factorThruKernelSubobject}$ applied to $f$, $h_{1}$ and $w$ is a homomorphism of $W$ and the action of $\operatorname{underlying}$ and the kernel of $f$ defined as $\operatorname{factorThru}$ applied to the kernel of $f$, $h_{1}$ and $\mathrm{CategoryTheory\_\_Limits\_\_kernelSubobject\_factors}$ applied to $f$, $h_{1}$ and $w$.

the image of f (from the docstring)

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

the image subobject composition isomorphism of f and h2 (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $h_{2}$ be a homomorphism of $Y$ and $\mathrm{Y'}$. Then the image subobject composition isomorphism of $f$ and $h_{2}$ is an isomorphism of the action of $\operatorname{underlying}$ and the image of the composition of $f$ and $h_{2}$ and the action of $\operatorname{underlying}$ and the image of $f$ defined as the composition of the image subobject isomorphism of the composition of $f$ and $h_{2}$ and the composition of the inverse of the composition isomorphism of $f$ and $h_{2}$ and the inverse of the image subobject isomorphism of $f$.

the image subobject isomorphism of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the image subobject isomorphism of $f$ is an isomorphism of the action of $\operatorname{underlying}$ and the image of $f$ and the categorical image of $f$ defined as the underlying isomorphism of the inclusion of the image of $f$.

the image subobject map of sq (from the name)

Let $\mathrm{sq}$ be a homomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $g$. Then the image subobject map of $\mathrm{sq}$ is a homomorphism of the action of $\operatorname{underlying}$ and the image of $f$ and the action of $\operatorname{underlying}$ and the image of $g$ defined as the composition of the homomorphism of the image subobject isomorphism of $f$ and the composition of the map of $\mathrm{sq}$ and the inverse of the image subobject isomorphism of $g$.

the kernel order homomorphism of X (from the name)

Let $X$ be an element of $C$. Then the kernel order homomorphism of $X$ is an order homomorphism of the set of order duals of the set of subobjects of $\operatorname{op}$ applied to $X$ and the set of subobjects of $X$.

the kernel of f (from the docstring)

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

the kernel subobject isomorphism of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the kernel subobject isomorphism of $f$ is an isomorphism of the action of $\operatorname{underlying}$ and the kernel of $f$ and the kernel of $f$ defined as the underlying isomorphism of the inclusion of $f$.

the kernel subobject isomorphism composition of f and g (from the name)

Let $f$ be a homomorphism of $\mathrm{X'}$ and $X$. Let $g$ be a homomorphism of $X$ and $Y$. Then the kernel subobject isomorphism composition of $f$ and $g$ is an isomorphism of the action of $\operatorname{underlying}$ and the kernel of the composition of $f$ and $g$ and the action of $\operatorname{underlying}$ and the kernel of $g$ defined as the composition of the kernel subobject isomorphism of the composition of $f$ and $g$ and the composition of $\operatorname{kernelIsIsoComp}$ applied to $f$ and $g$ and the inverse of the kernel subobject isomorphism of $g$.

the kernel subobject map of sq (from the name)

Let $\mathrm{sq}$ be a homomorphism of $\operatorname{mk}$ applied to $f$ and $\operatorname{mk}$ applied to $\mathrm{f'}$. Then the kernel subobject map of $\mathrm{sq}$ is a homomorphism of the action of $\operatorname{underlying}$ and the kernel of $f$ and the action of $\operatorname{underlying}$ and the kernel of $\mathrm{f'}$.

Let $X$ be an element of $C$. Then an element of $\operatorname{MonoOver}$ applied to $X$ is an element of the function that maps $X$ to the set of full subcategories of $\operatorname{isMono}$ applied to $X$.

the arrow of f (from the name)

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

the cocone of F (from the name)

Let $F$ be a functor of $J$ and $\operatorname{MonoOver}$ applied to $Y$. Then the cocone of $F$ is a cocone of $F$.

the congruence of X and e (from the name)

Let $X$ be an element of $C$. Let $e$ be an equivalence of $C$ and $D$. Then the congruence of $X$ and $e$ is an equivalence of $\operatorname{MonoOver}$ applied to $X$ and $\operatorname{MonoOver}$ applied to the action of the functor of $e$ and $X$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{exists}$ applied to $f$ is a functor of $\operatorname{MonoOver}$ applied to $X$ and $\operatorname{MonoOver}$ applied to $Y$ defined as the composition of $\operatorname{forget}$ applied to $X$ and the composition of the map of $f$ and the image.

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{existsComp}$ applied to $f$ and $g$ is an isomorphism of $\operatorname{exists}$ applied to the composition of $f$ and $g$ and the composition of $\operatorname{exists}$ applied to $f$ and $\operatorname{exists}$ applied to $g$ defined as the inverse of $\operatorname{symm}$ applied to the conjugate isomorphism equivalence of $\operatorname{existsPullbackAdj}$ applied to the composition of $f$ and $g$ and the composition of $\operatorname{existsPullbackAdj}$ applied to $f$ and $\operatorname{existsPullbackAdj}$ applied to $g$ and the pullback composition of $f$ and $g$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{existsIsoMap}$ applied to $f$ is an isomorphism of $\operatorname{exists}$ applied to $f$ and the map of $f$.

Let $p$ be a homomorphism of $X$ and $Y$. Let $f$ be an element of $\operatorname{MonoOver}$ applied to $X$. Let $e$ be a homomorphism of the left of the object of $f$ and $Z$. Let $m$ be a homomorphism of $Z$ and $Y$ such that the composition of $e$ and $m$ is equal to the composition of the arrow of $f$ and $p$. Then $\operatorname{existsObjIso}$ applied to $p$, $f$, $e$, $m$ and $\mathrm{fac}$ is an isomorphism of the action of $\operatorname{exists}$ applied to $p$ and $f$ and $\operatorname{mk}$ applied to $m$ defined as the image object isomorphism of $e$ and $m$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{existsPullbackAdj}$ applied to $f$ is an adjunction of $\operatorname{exists}$ applied to $f$ and the pullback of $f$ defined as $\operatorname{restrictFullyFaithful}$ applied to the composition of the map pullback adjoint of $f$ and $\operatorname{imageForgetAdj}$, $\operatorname{fullyFaithfulForget}$ applied to $X$, the identity functor of $\operatorname{MonoOver}$ applied to $Y$, the identity of the composition of $\operatorname{forget}$ applied to $X$ and the composition of the map of $f$ and the image and the identity of the composition of the identity of $\operatorname{MonoOver}$ applied to $Y$ and the composition of $\operatorname{forget}$ applied to $Y$ and the pullback of $f$.

Let $X$ be an element of $C$. Then $\operatorname{forget}$ applied to $X$ is a functor of $\operatorname{MonoOver}$ applied to $X$ and $\operatorname{Over}$ applied to $X$ defined as the inclusion of $\operatorname{isMono}$ applied to $X$.

$\operatorname{forgetImage}$ is an isomorphism of the composition of $\operatorname{forget}$ applied to $X$ and the image and the identity of $\operatorname{MonoOver}$ applied to $X$ defined as $\operatorname{asIso}$ applied to the counit of $\operatorname{imageForgetAdj}$.

Let $X$ be an element of $C$. Then $\operatorname{fullyFaithfulForget}$ applied to $X$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{forget}$ applied to $X$ defined as the inclusion of $\operatorname{isMono}$ applied to $X$.

the homomorphism of h and w (from the name)

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

the image (from the name)

The image is a functor of $\operatorname{Over}$ applied to $X$ and $\operatorname{MonoOver}$ applied to $X$.

$\operatorname{imageForgetAdj}$ is an adjunction of the image and $\operatorname{forget}$ applied to $X$.

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

the image object isomorphism of e and m (from the name)

Let $f$ be an element of $\operatorname{Over}$ applied to $X$. Let $e$ be a homomorphism of the left of $f$ and $Z$. Let $m$ be a homomorphism of $Z$ and $X$ such that the composition of $e$ and $m$ is equal to the homomorphism of $f$. Then the image object isomorphism of $e$ and $m$ is an isomorphism of the action of the image and $f$ and $\operatorname{mk}$ applied to $m$.

the cocone of F (from the docstring)

Let $F$ be a functor of $J$ and $\operatorname{MonoOver}$ applied to $Y$. Then the cocone of $F$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $F$.

the isomorphism of h and w (from the name)

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

the lift of F and h (from the name)

Let $F$ be a functor of $\operatorname{Over}$ applied to $Y$ and $\operatorname{Over}$ applied to $X$ such that for all elements $f$ of $\operatorname{MonoOver}$ applied to $Y$, the homomorphism of the action of $F$ and the action of $\operatorname{forget}$ applied to $Y$ and $f$ is a monomorphism. Then the lift of $F$ and $h$ is a functor of $\operatorname{MonoOver}$ applied to $Y$ and $\operatorname{MonoOver}$ applied to $X$ defined as the lift of $\operatorname{isMono}$ applied to $X$ and the composition of $\operatorname{forget}$ applied to $Y$ and $F$.

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

Let $F$ be a functor of $\operatorname{Over}$ applied to $X$ and $\operatorname{Over}$ applied to $Y$. Let $G$ be a functor of $\operatorname{Over}$ applied to $Y$ and $\operatorname{Over}$ applied to $Z$. Assume that for all elements $f_{2}$ of $\operatorname{MonoOver}$ applied to $X$, the homomorphism of the action of $F$ and the action of $\operatorname{forget}$ applied to $X$ and $f_{2}$ is a monomorphism. Assume that for all elements $f_{1}$ of $\operatorname{MonoOver}$ applied to $Y$, the homomorphism of the action of $G$ and the action of $\operatorname{forget}$ applied to $Y$ and $f_{1}$ is a monomorphism. Then the lift composition of $F$ and $G$ is an isomorphism of the composition of the lift of $F$ and $h$ and the lift of $G$ and $h_{1}$ and the lift of the composition of $F$ and $G$ and the function that maps $f$ to $h_{1}$ applied to $\operatorname{mk}$ applied to the action of $F$ and the action of $\operatorname{forget}$ applied to $X$ and $f$ and $h$ applied to $f$ defined as $\operatorname{fullyFaithfulCancelRight}$ applied to $\operatorname{forget}$ applied to $Z$ and the identity of the composition of the composition of the lift of $F$ and $h$ and the lift of $G$ and $h_{1}$ and $\operatorname{forget}$ applied to $Z$.

the lift identity (from the name)

The lift identity is an isomorphism of the lift of the identity of $\operatorname{Over}$ applied to $X$ and the function that maps $f$ to $\operatorname{property}$ applied to $f$ and the identity of $\operatorname{MonoOver}$ applied to $X$.

the lift isomorphism of i (from the name)

Assume that for all elements $f_{1}$ of $\operatorname{MonoOver}$ applied to $Y$, the homomorphism of the action of $x_{2}$ and the action of $\operatorname{forget}$ applied to $Y$ and $f_{1}$ is a monomorphism. Assume that for all elements $f$ of $\operatorname{MonoOver}$ applied to $Y$, the homomorphism of the action of $x_{3}$ and the action of $\operatorname{forget}$ applied to $Y$ and $f$ is a monomorphism. Let $i$ be an isomorphism of $x_{2}$ and $x_{3}$. Then the lift isomorphism of $i$ is an isomorphism of the lift of $x_{2}$ and $h$ and the lift of $x_{3}$ and $h_{1}$ defined as $\operatorname{fullyFaithfulCancelRight}$ applied to $\operatorname{forget}$ applied to $X$ and the left isomorphism whisker of $\operatorname{forget}$ applied to $Y$ and $i$.

Let $F$ be a functor of $J$ and $\operatorname{MonoOver}$ applied to $Y$. Let $c$ be a cocone of $F$. Then $\operatorname{liftStructOfHasStrongEpiMonoFactorisation}$ applied to $F$ and $c$ is an element of $\operatorname{LiftStruct}$ applied to $\operatorname{commSqOfHasStrongEpiMonoFactorisation}$ applied to $F$ and $c$.

the map of f (from the name)

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

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

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

the map identity of X (from the name)

Let $X$ be an element of $C$. Then the map identity of $X$ is an isomorphism of the map of the identity morphism of $X$ and the identity of $\operatorname{MonoOver}$ applied to $X$.

the map isomorphism of e (from the name)

Let $e$ be an isomorphism of $A$ and $B$. Then the map isomorphism of $e$ is an equivalence of $\operatorname{MonoOver}$ applied to $A$ and $\operatorname{MonoOver}$ applied to $B$.

the map pullback adjoint of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map pullback adjoint of $f$ is an adjunction of the map of $f$ and the pullback of $f$ defined as $\operatorname{restrictFullyFaithful}$ applied to the map pullback adjoint of $f$, $\operatorname{fullyFaithfulForget}$ applied to $X$, $\operatorname{fullyFaithfulForget}$ applied to $Y$, the identity of the composition of $\operatorname{forget}$ applied to $X$ and the map of $f$ and the identity of the composition of $\operatorname{forget}$ applied to $Y$ and the pullback of $f$.

Let $f$ be a homomorphism of $A$ and $X$. Then $\operatorname{mk}$ applied to $f$ is an element of $\operatorname{MonoOver}$ applied to $X$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $f$ and $\mathrm{hf}$.

the arrow isomorphism of f (from the name)

Let $f$ be an element of $\operatorname{MonoOver}$ applied to $X$. Then the arrow isomorphism of $f$ is an isomorphism of $\operatorname{mk}$ applied to the arrow of $f$ and $f$.

the pullback of f (from the name)

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

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

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

the pullback identity (from the name)

The pullback identity is an isomorphism of the pullback of the identity morphism of $X$ and the identity of $\operatorname{MonoOver}$ applied to $X$.

the pullback map self of f (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback map self of $f$ is an isomorphism of the composition of the map of $f$ and the pullback of $f$ and the identity of $\operatorname{MonoOver}$ applied to $X$ defined as the inverse of $\operatorname{asIso}$ applied to the unit of the map pullback adjoint of $f$.

the pullback object isomorphism of T and h1 (from the name)

Let $f$ be a homomorphism of $Y$ and $X$. Let $S$ be an element of $\operatorname{MonoOver}$ applied to $X$. Let $T$ be an element of $\operatorname{MonoOver}$ applied to $Y$. Let $\mathrm{f'}$ be a homomorphism of the left of the object of $T$ and the left of the object of $S$ such that $\operatorname{IsPullback}$ holds for $\mathrm{f'}$, the arrow of $T$, the arrow of $S$ and $f$. Then the pullback object isomorphism of $T$ and $\mathrm{f'}$ is an isomorphism of the action of the pullback of $f$ and $S$ and $T$.

the slice of h and h1 (from the name)

Assume that for all elements $g_{1}$ of $\operatorname{MonoOver}$ applied to $f$, the homomorphism of the action of the functor of the iterated slice equivalence of $f$ and the action of $\operatorname{forget}$ applied to $f$ and $g_{1}$ is a monomorphism. Assume that for all elements $g$ of $\operatorname{MonoOver}$ applied to the left of $f$, the homomorphism of the action of the inverse of the iterated slice equivalence of $f$ and the action of $\operatorname{forget}$ applied to the left of $f$ and $g$ is a monomorphism. Then the slice of $h$ and $h_{1}$ is an equivalence of $\operatorname{MonoOver}$ applied to $f$ and $\operatorname{MonoOver}$ applied to the left of $f$.

Let $F$ be a functor of $J$ and $\operatorname{MonoOver}$ applied to $Y$. Then $\operatorname{strongEpiMonoFactorisationSigmaDesc}$ applied to $F$ is a strong epimorphism monomorphism factorisation of $\operatorname{desc}$ applied to the function that maps $i$ to the arrow of the action of $F$ and $i$.

Let $X$ be an element of $C$. Then there is an object property of $\operatorname{Over}$ applied to $X$. Proof. Let $X$ be arbitrary. Let $f$ be arbitrary. By f. By CategoryTheory__Over__hom. By CategoryTheory__Mono.

X is a Noetherian object (from the name)

Let $X$ be an element of $C$. Then $X$ is a Noetherian object, if $\operatorname{Is}$ holds for $\operatorname{isNoetherianObject}$ and $X$.

There is an object property of $C$. Proof. Let $X$ be arbitrary. By X. By CategoryTheory__Subobject. By WellFoundedGT.

the presheaf of C (from the name)

Let $C$ be a set. Then the presheaf of $C$ is a functor of the set of opposites of $C$ and the set of sets.

the monomorphism over equivalence set of x (from the name)

Let $x$ be a set. Then the monomorphism over equivalence set of $x$ is an equivalence of $\operatorname{MonoOver}$ applied to $x$ and $\wp x$.

the subobject equivalence set of x (from the name)

Let $x$ be a set. Then the subobject equivalence set of $x$ is an order isomorphism of the set of subobjects of $x$ and $\wp x$ defined as the thin skeleton order isomorphism of the monomorphism over equivalence set of $x$.

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

A is subterminal (from the name)

Let $A$ be an element of $C$. Then $A$ is subterminal, if for all elements $Z$ of $C$, for all homomorphisms $f$ and $g$ of $Z$ and $A$, $\EqtMACRoH {f}{g}$.

the isomorphism diagonal of hA (from the name)

Assume that $A$ is subterminal. Then the isomorphism diagonal of $\mathrm{hA}$ is an isomorphism of the product of $A$ and $A$ and $A$ defined as the inverse of $\operatorname{asIso}$ applied to the diagonal of $A$.

Let $C$ be a set. Then an element of $\operatorname{Subterminals}$ applied to $C$ is an element of the function that maps $C$ to the set of full subcategories of the function that maps $A$ to the proposition that $A$ is subterminal.

the inclusion of the subterminal objects into the original category of C (from the docstring)

Let $C$ be a set. Then the inclusion of the subterminal objects into the original category of $C$ is a functor of $\operatorname{Subterminals}$ applied to $C$ and $C$ defined as the inclusion of the function that maps $A$ to the proposition that $A$ is subterminal.

the subterminal equivalence monomorphism over terminal of C (from the name)

Let $C$ be a set. Then the subterminal equivalence monomorphism over terminal of $C$ is an equivalence of $\operatorname{Subterminals}$ applied to $C$ and $\operatorname{MonoOver}$ applied to $\operatorname{terminal}$ applied to $C$.

the associativity of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the associativity of $D$ and $E$ is an equivalence of $\mathrm{Sum}$ applied to $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and $\mathrm{Sum}$ applied to $C$ and $\mathrm{Sum}$ applied to $D$ and $E$.

the associator of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the associator of $D$ and $E$ is a functor of $\mathrm{Sum}$ applied to $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and $\mathrm{Sum}$ applied to $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ defined as the sum of the sum of the left injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the composition of the left injection of $D$ and $E$ and the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the composition of the right injection of $D$ and $E$ and the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$.

the left injection composition associator of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the left injection composition associator of $D$ and $E$ is an isomorphism of the composition of the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the associator of $D$ and $E$ and the sum of the left injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the composition of the left injection of $D$ and $E$ and the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ defined as the sum of the sum of the left injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the composition of the left injection of $D$ and $E$ and the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the composition of the right injection of $D$ and $E$ and the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$.

the left injection composition left injection composition associator of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the left injection composition left injection composition associator of $D$ and $E$ is an isomorphism of the composition of the left injection of $C$ and $D$ and the composition of the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the associator of $D$ and $E$ and the left injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ defined as the composition of the left isomorphism whisker of the left injection of $C$ and $D$ and the left injection composition associator of $D$ and $E$ and the sum of the left injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the composition of the left injection of $D$ and $E$ and the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$.

the left injection composition right injection composition inverse associator of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the left injection composition right injection composition inverse associator of $D$ and $E$ is an isomorphism of the composition of the left injection of $D$ and $E$ and the composition of the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the inverse associator of $D$ and $E$ and the composition of the right injection of $C$ and $D$ and the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ defined as the composition of the left isomorphism whisker of the left injection of $D$ and $E$ and the right injection composition inverse associator of $D$ and $E$ and the sum of the composition of the right injection of $C$ and $D$ and the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the right injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$.

the left injection composition inverse associator of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the left injection composition inverse associator of $D$ and $E$ is an isomorphism of the composition of the left injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the inverse associator of $D$ and $E$ and the composition of the left injection of $C$ and $D$ and the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ defined as the sum of the composition of the left injection of $C$ and $D$ and the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the sum of the composition of the right injection of $C$ and $D$ and the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the right injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$.

the right injection composition associator of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the right injection composition associator of $D$ and $E$ is an isomorphism of the composition of the right injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the associator of $D$ and $E$ and the composition of the right injection of $D$ and $E$ and the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ defined as the sum of the sum of the left injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the composition of the left injection of $D$ and $E$ and the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the composition of the right injection of $D$ and $E$ and the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$.

the right injection composition left injection composition associator of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the right injection composition left injection composition associator of $D$ and $E$ is an isomorphism of the composition of the right injection of $C$ and $D$ and the composition of the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the associator of $D$ and $E$ and the composition of the left injection of $D$ and $E$ and the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ defined as the composition of the left isomorphism whisker of the right injection of $C$ and $D$ and the left injection composition associator of $D$ and $E$ and the sum of the left injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the composition of the left injection of $D$ and $E$ and the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$.

the right injection composition right injection composition inverse associator of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the right injection composition right injection composition inverse associator of $D$ and $E$ is an isomorphism of the composition of the right injection of $D$ and $E$ and the composition of the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the inverse associator of $D$ and $E$ and the right injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ defined as the composition of the left isomorphism whisker of the right injection of $D$ and $E$ and the right injection composition inverse associator of $D$ and $E$ and the sum of the composition of the right injection of $C$ and $D$ and the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the right injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$.

the right injection composition inverse associator of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the right injection composition inverse associator of $D$ and $E$ is an isomorphism of the composition of the right injection of $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and the inverse associator of $D$ and $E$ and the sum of the composition of the right injection of $C$ and $D$ and the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the right injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ defined as the sum of the composition of the left injection of $C$ and $D$ and the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the sum of the composition of the right injection of $C$ and $D$ and the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the right injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$.

the inverse associator of D and E (from the name)

Let $C$, $D$ and $E$ be sets. Then the inverse associator of $D$ and $E$ is a functor of $\mathrm{Sum}$ applied to $C$ and $\mathrm{Sum}$ applied to $D$ and $E$ and $\mathrm{Sum}$ applied to $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ defined as the sum of the composition of the left injection of $C$ and $D$ and the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the sum of the composition of the right injection of $C$ and $D$ and the left injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$ and the right injection of $\mathrm{Sum}$ applied to $C$ and $D$ and $E$.

the sum of F and G (from the docstring)

Let $F$ be a functor of $A$ and $C$. Let $G$ be a functor of $B$ and $C$. Then the sum of $F$ and $G$ is an isomorphism of the composition of the left injection of $A$ and $B$ and the sum of $F$ and $G$ and $F$.

the sum of F and G (from the docstring)

Let $F$ be a functor of $A$ and $C$. Let $G$ be a functor of $B$ and $C$. Then the sum of $F$ and $G$ is an isomorphism of the composition of the right injection of $A$ and $B$ and the sum of $F$ and $G$ and $G$.

the isomorphism sum of F (from the name)

Let $F$ be a functor of $\mathrm{Sum}$ applied to $A$ and $B$ and $C$. Then the isomorphism sum of $F$ is an isomorphism of $F$ and the sum of the composition of the left injection of $A$ and $B$ and $F$ and the composition of the right injection of $A$ and $B$ and $F$ defined as the sum isomorphism extension of the inverse of the sum of the composition of the left injection of $A$ and $B$ and $F$ and the composition of the right injection of $A$ and $B$ and $F$ and the inverse of the sum of the composition of the left injection of $A$ and $B$ and $F$ and the composition of the right injection of $A$ and $B$ and $F$.

the sum of F and G (from the name)

Let $F$ be a functor of $A$ and $B$. Let $G$ be a functor of $C$ and $D$. Then the sum of $F$ and $G$ is a functor of $\mathrm{Sum}$ applied to $A$ and $C$ and $\mathrm{Sum}$ applied to $B$ and $D$ defined as the sum of the composition of $F$ and the left injection of $B$ and $D$ and the composition of $G$ and the right injection of $B$ and $D$.

the sum of F and G (from the name)

Let $F$ be a functor of $A$ and $C$. Let $G$ be a functor of $B$ and $C$. Then the sum of $F$ and $G$ is a functor of $\mathrm{Sum}$ applied to $A$ and $B$ and $C$.

the sum isomorphism extension of x3 and x4 (from the name)

Let $x_{3}$ be an isomorphism of the composition of the left injection of $A$ and $B$ and $F$ and the composition of the left injection of $A$ and $B$ and $G$. Let $x_{4}$ be an isomorphism of the composition of the right injection of $A$ and $B$ and $F$ and the composition of the right injection of $A$ and $B$ and $G$. Then the sum isomorphism extension of $x_{3}$ and $x_{4}$ is an isomorphism of $F$ and $G$.

the sum of x4 and x5 (from the name)

Let $x_{4}$ be a homomorphism of $F$ and $G$. Let $x_{5}$ be a homomorphism of $H$ and $I$. Then the sum of $x_{4}$ and $x_{5}$ is a homomorphism of the sum of $F$ and $H$ and the sum of $G$ and $I$.

the sum of x3 and x4 (from the name)

Let $x_{3}$ be a homomorphism of $F$ and $G$. Let $x_{4}$ be a homomorphism of $H$ and $I$. Then the sum of $x_{3}$ and $x_{4}$ is a homomorphism of the sum of $F$ and $H$ and the sum of $G$ and $I$.

the equivalence of C and D (from the name)

Let $C$ and $D$ be sets. Then the equivalence of $C$ and $D$ is an equivalence of $\mathrm{Sum}$ applied to $C$ and $D$ and $\mathrm{Sum}$ applied to $D$ and $C$.

the symmetry of C and D (from the name)

Let $C$ and $D$ be sets. Then the symmetry of $C$ and $D$ is an isomorphism of the composition of the swap of $C$ and $D$ and the swap of $D$ and $C$ and the identity of $\mathrm{Sum}$ applied to $C$ and $D$ defined as the inverse of the unit isomorphism of the equivalence of $C$ and $D$.

the homomorphism induction of x4 and y2 (from the name)

Let $\mathrm{inl}$ be a function from elements $x_{4}$ of $C$ and elements $y_{2}$ of $C$ and homomorphisms $f_{2}$ of $x_{4}$ and $y_{2}$ to elements of $P$ applied to the action of the left injection of $C$ and $D$ and $x_{4}$, the action of the left injection of $C$ and $D$ and $y_{2}$ and the map of the left injection of $C$ and $D$ and $f_{2}$. Let $\mathrm{inr}$ be a function from elements $x_{3}$ of $D$ and elements $y_{1}$ of $D$ and homomorphisms $f_{1}$ of $x_{3}$ and $y_{1}$ to elements of $P$ applied to the action of the right injection of $C$ and $D$ and $x_{3}$, the action of the right injection of $C$ and $D$ and $y_{1}$ and the map of the right injection of $C$ and $D$ and $f_{1}$. Let $f$ be a homomorphism of $x_{2}$ and $y$. Then the homomorphism induction of $y_{2}$ and $f_{2}$ is an element of $P$ applied to $x_{2}$, $y$ and $f$.

the left injection of C and D (from the name)

Let $C$ and $D$ be sets. Then the left injection of $C$ and $D$ is a functor of $C$ and $\mathrm{Sum}$ applied to $C$ and $D$.

the right injection of C and D (from the name)

Let $C$ and $D$ be sets. Then the right injection of $C$ and $D$ is a functor of $D$ and $\mathrm{Sum}$ applied to $C$ and $D$.

the swap of C and D (from the name)

Let $C$ and $D$ be sets. Then the swap of $C$ and $D$ is a functor of $\mathrm{Sum}$ applied to $C$ and $D$ and $\mathrm{Sum}$ applied to $D$ and $C$ defined as the sum of the right injection of $D$ and $C$ and the left injection of $D$ and $C$.

the swap composition left injection of C and D (from the name)

Let $C$ and $D$ be sets. Then the swap composition left injection of $C$ and $D$ is an isomorphism of the composition of the left injection of $C$ and $D$ and the swap of $C$ and $D$ and the right injection of $D$ and $C$ defined as the sum of the right injection of $D$ and $C$ and the left injection of $D$ and $C$.

the swap composition right injection of C and D (from the name)

Let $C$ and $D$ be sets. Then the swap composition right injection of $C$ and $D$ is an isomorphism of the composition of the right injection of $C$ and $D$ and the swap of $C$ and $D$ and the left injection of $D$ and $C$ defined as the sum of the right injection of $D$ and $C$ and the left injection of $D$ and $C$.

the equivalence functor equivalence functor isomorphism (from the name)

The equivalence functor equivalence functor isomorphism is an isomorphism of the functor of the composition of the left congruence of the equivalence of $A$ and $\mathrm{A'}$ and the functor equivalence of $A$ and $B$ and the functor of the composition of the functor equivalence of $\mathrm{A'}$ and $B$ and the braiding of the set of functors of $A$ and $B$ and the set of functors of $\mathrm{A'}$ and $B$.

the equivalence of T (from the docstring)

Let $T$ be a set. Then the equivalence of $T$ is an isomorphism of the functor of the composition of the left congruence of the associativity of $\mathrm{A'}$ and $T$ and the composition of the functor equivalence of $\mathrm{Sum}$ applied to $\mathrm{A'}$ and $T$ and $B$ and the product of the identity and the functor equivalence of $T$ and $B$ and the functor of the composition of the composition of the functor equivalence of $T$ and $B$ and the product of the functor equivalence of $\mathrm{A'}$ and $B$ and the identity and the associativity of the set of functors of $\mathrm{A'}$ and $B$ and the set of functors of $T$ and $B$.

the functor equivalence of B and #3 (from the name)

Let $A$, $\mathrm{A'}$ and $B$ be sets. Then the functor equivalence of $\mathrm{A'}$ and $B$ is an equivalence of the set of functors of $\mathrm{Sum}$ applied to $A$ and $\mathrm{A'}$ and $B$ and $\mathrm{Prod}$ applied to the set of functors of $A$ and $B$ and the set of functors of $\mathrm{A'}$ and $B$.

the functor equivalence functor composition first component isomorphism (from the name)

The functor equivalence functor composition first component isomorphism is an isomorphism of the composition of the functor of the functor equivalence of $\mathrm{A'}$ and $B$ and the first component of the set of functors of $A$ and $B$ and the set of functors of $\mathrm{A'}$ and $B$ and the action of the left whiskering of $\mathrm{Sum}$ applied to $A$ and $\mathrm{A'}$ and $B$ and the left injection of $A$ and $\mathrm{A'}$.

the functor equivalence functor composition second component isomorphism (from the name)

The functor equivalence functor composition second component isomorphism is an isomorphism of the composition of the functor of the functor equivalence of $\mathrm{A'}$ and $B$ and the second component of the set of functors of $A$ and $B$ and the set of functors of $\mathrm{A'}$ and $B$ and the action of the left whiskering of $\mathrm{Sum}$ applied to $A$ and $\mathrm{A'}$ and $B$ and the right injection of $A$ and $\mathrm{A'}$.

the functor equivalence inverse composition whiskering left left injection isomorphism (from the name)

The functor equivalence inverse composition whiskering left left injection isomorphism is an isomorphism of the composition of the inverse of the functor equivalence of $\mathrm{A'}$ and $B$ and the action of the left whiskering of $\mathrm{Sum}$ applied to $A$ and $\mathrm{A'}$ and $B$ and the left injection of $A$ and $\mathrm{A'}$ and the first component of the set of functors of $A$ and $B$ and the set of functors of $\mathrm{A'}$ and $B$.

the functor equivalence inverse composition whiskering left right injection isomorphism (from the name)

The functor equivalence inverse composition whiskering left right injection isomorphism is an isomorphism of the composition of the inverse of the functor equivalence of $\mathrm{A'}$ and $B$ and the action of the left whiskering of $\mathrm{Sum}$ applied to $A$ and $\mathrm{A'}$ and $B$ and the right injection of $A$ and $\mathrm{A'}$ and the second component of the set of functors of $A$ and $B$ and the set of functors of $\mathrm{A'}$ and $B$.

the natural isomorphism of x3 and x4 (from the name)

Let $x_{3}$ be an isomorphism of the composition of the left injection of $A$ and $\mathrm{A'}$ and $F$ and the composition of the left injection of $A$ and $\mathrm{A'}$ and $G$. Let $x_{4}$ be an isomorphism of the composition of the right injection of $A$ and $\mathrm{A'}$ and $F$ and the composition of the right injection of $A$ and $\mathrm{A'}$ and $G$. Then the natural isomorphism of $x_{3}$ and $x_{4}$ is an isomorphism of $F$ and $G$.

the natural transformation of x3 and x4 (from the name)

Let $x_{3}$ be a homomorphism of the composition of the left injection of $A$ and $\mathrm{A'}$ and $F$ and the composition of the left injection of $A$ and $\mathrm{A'}$ and $G$. Let $x_{4}$ be a homomorphism of the composition of the right injection of $A$ and $\mathrm{A'}$ and $F$ and the composition of the right injection of $A$ and $\mathrm{A'}$ and $G$. Then the natural transformation of $x_{3}$ and $x_{4}$ is a homomorphism of $F$ and $G$ defined as the composition of the component of the unit of the functor equivalence of $\mathrm{A'}$ and $B$ and $F$ and the composition of the map of the inverse of the functor equivalence of $\mathrm{A'}$ and $B$ and $\ProdmkMACRoU {x_{3}}{x_{4}}$ and the component of the inverse of the unit of the functor equivalence of $\mathrm{A'}$ and $B$ and $G$.

the isomorphism of f and g (from the name)

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

the classifier of C (from the name)

Let $C$ be a set. Then the classifier of $C$ is a classifier of the set of functors of the set of opposites of $C$ and the set of sets defined as $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_mkOfTerminal\_u3a9\_\_u2080\_}$ applied to the action of the constant of the set of opposites of $C$ and $\mathrm{PUnit}$, $\operatorname{isTerminalConst}$ applied to the set of opposites of $C$ and $\operatorname{isTerminalPUnit}$, the sieve of $C$, the truth of $C$, the function that maps $x_{1}$, $x_{2}$, $x_{3}$ and $h$ to $\mathrm{CategoryTheory\_\_Presheaf\_\_\_u3c7\_}$ applied to $x_{3}$, the function that maps $x_{4}$ and $x_{5}$ to $\operatorname{truth}$ and the function that maps $x_{6}$, $x_{7}$, $x_{8}$ and $h_{1}$ to $\mathrm{CategoryTheory\_\_Presheaf\_\_\_u3c7\_\_unique}$ applied to $x_{8}$.

the truth of C (from the name)

Let $C$ be a set. Then the truth of $C$ is a homomorphism of the action of the constant of the set of opposites of $C$ and $\mathrm{PUnit}$ and the sieve of $C$.

Let $m$ be a homomorphism of $F$ and $G$. Then $\mathrm{CategoryTheory\_\_Presheaf\_\_\_u3c7\_}$ applied to $m$ is a homomorphism of $G$ and the sieve of $C$.

the classifier of J (from the name)

Let $J$ be a Grothendieck topology of $C$. Then the classifier of $J$ is a classifier of the set of sheaves of $J$ and the set of sets defined as $\mathrm{CategoryTheory\_\_Subobject\_\_Classifier\_\_mkOfTerminal\_u3a9\_\_u2080\_}$ applied to $\operatorname{terminal}$ applied to $J$ and $\operatorname{isTerminalPUnit}$, the constant sheaf of $J$ and $\operatorname{isTerminalPUnit}$, $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u3a9\_}$ applied to $J$, the truth of $J$, the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u3c7\_}$, the function that maps $x_{3}$ and $x_{4}$ to $\operatorname{truth}$ and the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u3c7\_\_unique}$.

the truth of J (from the name)

Let $J$ be a Grothendieck topology of $C$. Then the truth of $J$ is a homomorphism of $\operatorname{terminal}$ applied to $J$ and $\operatorname{isTerminalPUnit}$ and $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u3a9\_}$ applied to $J$.

Let $J$ be a Grothendieck topology of $C$. Then $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u3a9\_}$ applied to $J$ is a sheaf of $J$ and the set of sets.

Let $m$ be a homomorphism of $F$ and $G$. Then $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u3c7\_}$ applied to $m$ is a homomorphism of $G$ and $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u3a9\_}$ applied to $J$.

adj is triangulated (from the name)

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

E is triangulated (from the name)

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

triangle of C (from the name)

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

the functor homomorphism of x4 and x5 (from the name)

Let $A$ and $B$ be functors of $J$ and the set of triangles of $C$. Let $x_{3}$ be a homomorphism of the composition of $A$ and the first projection and the composition of $B$ and the first projection. Let $x_{4}$ be a homomorphism of the composition of $A$ and the second projection and the composition of $B$ and the second projection. Let $x_{5}$ be a homomorphism of the composition of $A$ and the third projection and the composition of $B$ and the third projection. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the left whisker of $A$ and the projection to projection and $x_{4}$ is equal to the composition of $x_{3}$ and the left whisker of $B$ and the projection to projection and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_Triangle\_\_functorHomMk\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the left whisker of $A$ and the projection to projection and $x_{5}$ is equal to the composition of $x_{4}$ and the left whisker of $B$ and the projection to projection and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_Triangle\_\_functorHomMk\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the left whisker of $A$ and the projection to projection and the right whisker of $x_{3}$ and the shift functor of $C$ and $1$ is equal to the composition of $x_{5}$ and the left whisker of $B$ and the projection to projection and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_Triangle\_\_functorHomMk\_\_\_auto\_5}$. Then the functor homomorphism of $x_{4}$ and $x_{5}$ is a homomorphism of $A$ and $B$.

the functor homomorphism of x16 and x17 (from the name)

Let $x_{15}$ be a homomorphism of $x_{3}$ and $x_{9}$. Let $x_{16}$ be a homomorphism of $x_{4}$ and $x_{10}$. Let $x_{17}$ be a homomorphism of $x_{5}$ and $x_{11}$. Assume that the composition of $x_{6}$ and $x_{16}$ is equal to the composition of $x_{15}$ and $x_{12}$. Assume that the composition of $x_{7}$ and $x_{17}$ is equal to the composition of $x_{16}$ and $x_{13}$. Assume that the composition of $x_{8}$ and the right whisker of $x_{15}$ and the shift functor of $C$ and $1$ is equal to the composition of $x_{17}$ and $x_{14}$. Then the functor homomorphism of $x_{16}$ and $x_{17}$ is a homomorphism of the functor of $x_{7}$ and $x_{8}$ and the functor of $x_{13}$ and $x_{14}$ defined as the functor homomorphism of $x_{16}$ and $x_{17}$.

the functor isomorphism of x4 and x5 (from the name)

Let $A$ and $B$ be functors of $J$ and the set of triangles of $C$. Let $x_{3}$ be an isomorphism of the composition of $A$ and the first projection and the composition of $B$ and the first projection. Let $x_{4}$ be an isomorphism of the composition of $A$ and the second projection and the composition of $B$ and the second projection. Let $x_{5}$ be an isomorphism of the composition of $A$ and the third projection and the composition of $B$ and the third projection. Assume that the composition of the left whisker of $A$ and the projection to projection and the homomorphism of $x_{4}$ is equal to the composition of the homomorphism of $x_{3}$ and the left whisker of $B$ and the projection to projection. Assume that the composition of the left whisker of $A$ and the projection to projection and the homomorphism of $x_{5}$ is equal to the composition of the homomorphism of $x_{4}$ and the left whisker of $B$ and the projection to projection. Assume that the composition of the left whisker of $A$ and the projection to projection and the right whisker of the homomorphism of $x_{3}$ and the shift functor of $C$ and $1$ is equal to the composition of the homomorphism of $x_{5}$ and the left whisker of $B$ and the projection to projection. Then the functor isomorphism of $x_{4}$ and $x_{5}$ is an isomorphism of $A$ and $B$.

the functor isomorphism of x16 and x17 (from the name)

Let $x_{15}$ be an isomorphism of $x_{3}$ and $x_{9}$. Let $x_{16}$ be an isomorphism of $x_{4}$ and $x_{10}$. Let $x_{17}$ be an isomorphism of $x_{5}$ and $x_{11}$. Assume that the composition of $x_{6}$ and the homomorphism of $x_{16}$ is equal to the composition of the homomorphism of $x_{15}$ and $x_{12}$. Assume that the composition of $x_{7}$ and the homomorphism of $x_{17}$ is equal to the composition of the homomorphism of $x_{16}$ and $x_{13}$. Assume that the composition of $x_{8}$ and the right whisker of the homomorphism of $x_{15}$ and the shift functor of $C$ and $1$ is equal to the composition of the homomorphism of $x_{17}$ and $x_{14}$. Then the functor isomorphism of $x_{16}$ and $x_{17}$ is an isomorphism of the functor of $x_{7}$ and $x_{8}$ and the functor of $x_{13}$ and $x_{14}$ defined as the functor isomorphism of $x_{16}$ and $x_{17}$.

the functor of x7 and x8 (from the name)

Let $x_{6}$ be a homomorphism of $x_{3}$ and $x_{4}$. Let $x_{7}$ be a homomorphism of $x_{4}$ and $x_{5}$. Let $x_{8}$ be a homomorphism of $x_{5}$ and the composition of $x_{3}$ and the shift functor of $C$ and $1$. Then the functor of $x_{7}$ and $x_{8}$ is a functor of $J$ and the set of triangles of $C$.

the homomorphism of x3 and x4 (from the name)

Let $A$ and $B$ be triangles of $C$. Let $x_{2}$ be a homomorphism of the first object of $A$ and the first object of $B$. Let $x_{3}$ be a homomorphism of the second object of $A$ and the second object of $B$. Let $x_{4}$ be a homomorphism of the third object of $A$ and the third object of $B$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the first morphism of $A$ and $x_{3}$ is equal to the composition of $x_{2}$ and the first morphism of $B$ and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_Triangle\_\_homMk\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the second morphism of $A$ and $x_{4}$ is equal to the composition of $x_{3}$ and the second morphism of $B$ and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_Triangle\_\_homMk\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the third morphism of $A$ and the map of the shift functor of $C$ and $1$ and $x_{2}$ is equal to the composition of $x_{4}$ and the third morphism of $B$ and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_Triangle\_\_homMk\_\_\_auto\_5}$. Then the homomorphism of $x_{3}$ and $x_{4}$ is a homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to $x_{2}$, $x_{3}$, $x_{4}$, $h$, $h_{1}$ and $h_{2}$.

the isomorphism of x3 and x4 (from the name)

Let $A$ and $B$ be triangles of $C$. Let $x_{2}$ be an isomorphism of the first object of $A$ and the first object of $B$. Let $x_{3}$ be an isomorphism of the second object of $A$ and the second object of $B$. Let $x_{4}$ be an isomorphism of the third object of $A$ and the third object of $B$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the first morphism of $A$ and the homomorphism of $x_{3}$ is equal to the composition of the homomorphism of $x_{2}$ and the first morphism of $B$ and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_Triangle\_\_isoMk\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the second morphism of $A$ and the homomorphism of $x_{4}$ is equal to the composition of the homomorphism of $x_{3}$ and the second morphism of $B$ and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_Triangle\_\_isoMk\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of the third morphism of $A$ and the map of the shift functor of $C$ and $1$ and the homomorphism of $x_{2}$ is equal to the composition of the homomorphism of $x_{4}$ and the third morphism of $B$ and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_Triangle\_\_isoMk\_\_\_auto\_5}$. Then the isomorphism of $x_{3}$ and $x_{4}$ is an isomorphism of $A$ and $B$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $h$ be a homomorphism of $Z$ and the action of the shift functor of $C$ and $1$ and $X$. Then $\operatorname{mk}$ applied to $f$, $g$ and $h$ is a triangle of $C$ defined as $\operatorname{mk'}$ applied to $X$, $Y$, $Z$, $f$, $g$ and $h$.

the first morphism of self (from the docstring)

Let $\mathrm{self}$ be a triangle of $C$. Then the first morphism of $\mathrm{self}$ is a homomorphism of the first object of $\mathrm{self}$ and the second object of $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the second morphism of self (from the docstring)

Let $\mathrm{self}$ be a triangle of $C$. Then the second morphism of $\mathrm{self}$ is a homomorphism of the second object of $\mathrm{self}$ and the third object of $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

the third morphism of self (from the docstring)

Let $\mathrm{self}$ be a triangle of $C$. Then the third morphism of $\mathrm{self}$ is a homomorphism of the third object of $\mathrm{self}$ and the action of the shift functor of $C$ and $1$ and the first object of $\mathrm{self}$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

the first object of self (from the docstring)

Let $\mathrm{self}$ be a triangle of $C$. Then the first object of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the second object of self (from the docstring)

Let $\mathrm{self}$ be a triangle of $C$. Then the second object of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the third object of self (from the docstring)

Let $\mathrm{self}$ be a triangle of $C$. Then the third object of $\mathrm{self}$ is an element of $C$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the first projection (from the docstring)

The first projection is a functor of the set of triangles of $C$ and $C$.

the projection to projection (from the name)

The projection to projection is a homomorphism of the first projection and the second projection.

the second projection (from the docstring)

The second projection is a functor of the set of triangles of $C$ and $C$.

the projection to projection (from the name)

The projection to projection is a homomorphism of the second projection and the third projection.

the third projection (from the docstring)

The third projection is a functor of the set of triangles of $C$ and $C$.

the projection to projection (from the name)

The projection to projection is a homomorphism of the third projection and the composition of the first projection and the shift functor of $C$ and $1$.

triangle morphism of x2 and x3 (from the name)

Let $x_{2}$ and $x_{3}$ be triangles of $C$. Then the triangle morphisms of $x_{2}$ and $x_{3}$ are a basic type.

the composition of f and g (from the name)

Let $f$ be a triangle morphism of $x_{2}$ and $x_{3}$. Let $g$ be a triangle morphism of $x_{3}$ and $x_{4}$. Then the composition of $f$ and $g$ is a triangle morphism of $x_{2}$ and $x_{4}$.

the homomorphism of self (from the name)

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

the homomorphism of self (from the name)

Let $\mathrm{self}$ be a triangle morphism of $x_{2}$ and $x_{3}$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of the second object of $x_{2}$ and the second object of $x_{3}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the homomorphism of self (from the name)

Let $\mathrm{self}$ be a triangle morphism of $x_{2}$ and $x_{3}$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of the third object of $x_{2}$ and the third object of $x_{3}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the obvious triangle of x2 and x3 (from the docstring)

Let $x_{2}$ and $x_{3}$ be elements of $C$. Then the obvious triangle of $x_{2}$ and $x_{3}$ is a triangle of $C$ defined as $\operatorname{mk}$ applied to the left injection, the projection onto the second summand and $0$.

the obvious triangle of x2 and x3 (from the docstring)

Let $x_{2}$ and $x_{3}$ be elements of $C$. Then the obvious triangle of $x_{2}$ and $x_{3}$ is a triangle of $C$ defined as $\operatorname{mk}$ applied to the lift of the identity morphism of $x_{2}$ and $0$, the projection map to the second component of the product and $0$.

the binary product triangle isomorphism binary biproduct triangle of x2 and x3 (from the name)

Let $x_{2}$ and $x_{3}$ be elements of $C$. Then the binary product triangle isomorphism binary biproduct triangle of $x_{2}$ and $x_{3}$ is an isomorphism of the obvious triangle of $x_{2}$ and $x_{3}$ and the obvious triangle of $x_{2}$ and $x_{3}$.

the contractible triangle of X (from the name)

Let $X$ be an element of $C$. Then the contractible triangle of $X$ is a triangle of $C$ defined as $\operatorname{mk}$ applied to the identity morphism of $X$, $0$ and $0$.

the functor of C (from the docstring)

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

the product of T (from the docstring)

Let $T$ be a function from elements of $J$ to triangles of $C$. Then the product of $T$ is a triangle of $C$ defined as $\operatorname{mk}$ applied to the map of the function that maps $j$ to the first morphism of $T$ applied to $j$, the map of the function that maps $j_{1}$ to the second morphism of $T$ applied to $j_{1}$ and the composition of the map of the function that maps $j_{2}$ to the third morphism of $T$ applied to $j_{2}$ and the inverse of the product comparison of the shift functor of $C$ and $1$ and the function that maps $j_{3}$ to the first object of $T$ applied to $j_{3}$.

Let $T$ be a function from elements of $J$ to triangles of $C$. Then $\operatorname{fan}$ applied to $T$ is an element of $\operatorname{Fan}$ applied to $T$ defined as $\operatorname{mk}$ applied to the product of $T$ and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_productTriangle\_\_\_u3c0\_}$ applied to $T$.

Let $T$ be a function from elements of $J$ to triangles of $C$. Then $\operatorname{isLimitFan}$ applied to $T$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{fan}$ applied to $T$.

the lift of T and x2 (from the name)

Let $T$ be a function from elements of $J$ to triangles of $C$. Let $x_{2}$ be a function from elements $j$ of $J$ to homomorphisms of $\mathrm{T'}$ and $T$ applied to $j$. Then the lift of $T$ and $j$ is a homomorphism of $\mathrm{T'}$ and the product of $T$.

the projection of T and j (from the name)

Let $T$ be a function from elements of $J$ to triangles of $C$. Let $j$ be an element of $J$. Then the projection of $T$ and $j$ is a homomorphism of the product of $T$ and $T$ applied to $j$.

the identity triangle morphism of T (from the docstring)

Let $T$ be a triangle of $C$. Then the identity triangle morphism of $T$ is a triangle morphism of $T$ and $T$.

F is triangulated (from the name)

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

the map triangle of F (from the name)

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

the map triangle commutative shift isomorphism of F and n (from the name)

Let $F$ be a functor of $C$ and $D$. Let $n$ be an integer. Then the map triangle commutative shift isomorphism of $F$ and $n$ is an isomorphism of the composition of the shift functor of $C$ and $n$ and the map triangle of $F$ and the composition of the map triangle of $F$ and the shift functor of $D$ and $n$.

the canonical isomorphism of F and G (from the docstring)

Let $F$ be a functor of $C$ and $D$. Let $G$ be a functor of $D$ and $E$. Then the canonical isomorphism of $F$ and $G$ is an isomorphism of the map triangle of the composition of $F$ and $G$ and the composition of the map triangle of $F$ and the map triangle of $G$.

the canonical isomorphism of C (from the docstring)

Let $C$ be a set. Then the canonical isomorphism of $C$ is an isomorphism of the map triangle of the identity of $C$ and the identity of the set of triangles of $C$.

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{mapTriangleInvRotateIso}$ applied to $F$ is an isomorphism of the composition of the map triangle of $F$ and $\operatorname{invRotate}$ applied to $D$ and the composition of $\operatorname{invRotate}$ applied to $C$ and the map triangle of $F$.

the map triangle isomorphism of e (from the name)

Let $e$ be an isomorphism of $x_{4}$ and $x_{5}$. Then the map triangle isomorphism of $e$ is an isomorphism of the map triangle of $x_{4}$ and the map triangle of $x_{5}$.

Let $F$ be a functor of $C$ and $D$. Then $\operatorname{mapTriangleRotateIso}$ applied to $F$ is an isomorphism of the composition of the map triangle of $F$ and $\operatorname{rotate}$ applied to $D$ and the composition of $\operatorname{rotate}$ applied to $C$ and the map triangle of $F$.

the map of h7 and F (from the name)

Let $h_{7}$ be an octahedron of $h_{5}$ and $h_{6}$. Let $F$ be a functor of $C$ and $D$. Then the map of $h_{7}$ and $F$ is an octahedron of $\mathrm{CategoryTheory\_\_Functor\_\_map\_distinguished}$ applied to $F$, $\operatorname{mk}$ applied to $x_{15}$, $x_{19}$ and $x_{20}$ and $h_{5}$ and $\mathrm{CategoryTheory\_\_Functor\_\_map\_distinguished}$ applied to $F$, $\operatorname{mk}$ applied to $x_{16}$, $x_{21}$ and $x_{22}$ and $h_{6}$.

P is a classical triangulated generator (from the name)

Let $P$ be an object property of $C$. Then $P$ is a classical triangulated generator, if $\operatorname{triangEnvelope}$ applied to $P$ is equal to the top.

P is a strong triangulated generator (from the name)

Let $P$ be an object property of $C$. Then $P$ is a strong triangulated generator, if there exists a natural number $n$, such that $\operatorname{triangEnvelopeIter}$ applied to $P$ and $n$ is equal to the top.

Let $P$ be an object property of $C$. Then there is an object property of $C$. Proof. Let $P$ be arbitrary. Let $n$ be arbitrary. By P. By n. By CategoryTheory__ObjectProperty__triangEnvelopeIter. By iSup.

Let $P$ be an object property of $C$. Let $n$ be a natural number. Then there is an object property of $C$. Proof. Let $P$ be arbitrary. Let $n$ be arbitrary. By P. By Int. By CategoryTheory__ObjectProperty__shiftClosure. By CategoryTheory__ObjectProperty__binaryProductsClosure. By CategoryTheory__ObjectProperty__retractClosure. By n. By CategoryTheory__ObjectProperty__extensionProductIter. By CategoryTheory__ObjectProperty__retractClosure.

F is a homological functor (from the docstring)

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

the kernel of F (from the docstring)

Let $F$ be a functor of $C$ and $A$. Then the kernel of $F$ is an object property of $C$ defined as the function that maps $X$ to the proposition that for all integers $n$, the action of $F$ and the action of the shift functor of $C$ and $n$ and $X$ is a zero.

the homology sequence composable arrow of x4 and x5 (from the name)

Let $F$ be a functor of $C$ and $A$. Let $T$ be a triangle of $C$. Let $x_{4}$ and $x_{5}$ be integers such that $x_{4} + 1 = x_{5}$. Then the homology sequence composable arrow of $x_{4}$ and $x_{5}$ is a composable arrow of $A$ and $5$ defined as $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2085\_}$ applied to the map of the shift of $F$ and $x_{4}$ and the first morphism of $T$, the map of the shift of $F$ and $x_{4}$ and the second morphism of $T$, the homology sequence of $x_{4}$ and $x_{5}$, the map of the shift of $F$ and $x_{5}$ and the first morphism of $T$ and the map of the shift of $F$ and $x_{5}$ and the second morphism of $T$.

the homology sequence of x4 and x5 (from the name)

Let $F$ be a functor of $C$ and $A$. Let $T$ be a triangle of $C$. Let $x_{4}$ and $x_{5}$ be integers such that $x_{4} + 1 = x_{5}$. Then the homology sequence of $x_{4}$ and $x_{5}$ is a homomorphism of the action of the shift of $F$ and $x_{4}$ and the third object of $T$ and the action of the shift of $F$ and $x_{5}$ and the first object of $T$.

Let $A$ and $B$ be object properties of $C$. Then we can say that $\operatorname{IsVerdierLeftLocalizing}$ holds for $A$ and $B$.

Let $A$ and $B$ be object properties of $C$. Let $e$ be an isomorphism of the composition of $x_{8}$ and $F$ and the composition of the inclusion of $A$ and $x_{9}$. Then $\operatorname{fullyFaithful}$ applied to $A$, $B$ and $e$ is an element of $\operatorname{FullyFaithful}$ applied to $F$ defined as $\operatorname{ofIso}$ applied to $\operatorname{ofFullyFaithful}$ applied to the localized functor of $x_{8}$ and $x_{9}$ and the lift natural isomorphism of $F$ and the inverse of $e$.

Let $A$ and $B$ be object properties of $C$. Then we can say that $\operatorname{IsVerdierRightLocalizing}$ holds for $A$ and $B$.

Let $A$ and $B$ be object properties of $C$. Let $e$ be an isomorphism of the composition of $x_{8}$ and $F$ and the composition of the inclusion of $A$ and $x_{9}$. Then $\operatorname{fullyFaithful}$ applied to $A$, $B$ and $e$ is an element of $\operatorname{FullyFaithful}$ applied to $F$ defined as $\operatorname{ofIso}$ applied to $\operatorname{ofFullyFaithful}$ applied to the localized functor of $x_{8}$ and $x_{9}$ and the lift natural isomorphism of $F$ and the inverse of $e$.

the triangulated localizer morphism of A and B (from the name)

Let $A$ and $B$ be object properties of $C$. Then the triangulated localizer morphism of $A$ and $B$ is a localizer morphism of the trace of the inverse image of $B$ and the inclusion of $A$ and the trace of $B$.

the opposite shift functor equivalence of C and n (from the name)

Let $C$ be a set. Let $n$ be an integer. Then the opposite shift functor equivalence of $C$ and $n$ is an equivalence of the set of opposites of $C$ and the set of opposites of $C$.

the opposite shift functor equivalence inverse homomorphism equivalence (from the name)

The opposite shift functor equivalence inverse homomorphism equivalence is an equivalence from the set of homomorphisms of $\operatorname{op}$ applied to the action of the shift functor of $C$ and $n$ and the opposite of $X$ and $Y$ to the set of homomorphisms of $X$ and the action of the shift functor of the set of opposites of $C$ and $n$ and $Y$ defined as the homomorphism equivalence of $X$ and $Y$.

the shift functor opposite isomorphism of n and m (from the name)

Let $C$ be a set. Let $n$ and $m$ be integers such that $n + m = 0$. Then the shift functor opposite isomorphism of $n$ and $m$ is an isomorphism of the shift functor of the set of opposites of $C$ and $n$ and the opposite of the shift functor of $C$ and $m$.

the map triangle opposite composition triangle opposite equivalence functor of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the map triangle opposite composition triangle opposite equivalence functor of $F$ is an isomorphism of the composition of the opposite of the map triangle of $F$ and the functor of the triangle opposite equivalence of $D$ and the composition of the functor of the triangle opposite equivalence of $C$ and the map triangle of the opposite of $F$.

the map triangle opposite composition triangle opposite equivalence functor application of F and T (from the name)

Let $F$ be a functor of $C$ and $D$. Let $T$ be a triangle of $C$. Then the map triangle opposite composition triangle opposite equivalence functor application of $F$ and $T$ is an isomorphism of the action of the functor of the triangle opposite equivalence of $D$ and $\operatorname{op}$ applied to the action of the map triangle of $F$ and $T$ and the action of the map triangle of the opposite of $F$ and the action of the functor of the triangle opposite equivalence of $C$ and $\operatorname{op}$ applied to $T$.

the opposite map triangle composition triangle opposite equivalence inverse of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the opposite map triangle composition triangle opposite equivalence inverse of $F$ is an isomorphism of the composition of the map triangle of the opposite of $F$ and the inverse of the triangle opposite equivalence of $D$ and the composition of the inverse of the triangle opposite equivalence of $C$ and the opposite of the map triangle of $F$ defined as the isomorphism of the inverse of the triangle opposite equivalence of $D$ and the opposite of the map triangle of $F$.

the isomorphism of C and n (from the name)

Let $C$ be a set. Let $n$ be an integer. Then the isomorphism of $C$ and $n$ is an isomorphism of the composition of the shift functor of $C$ and $n$ and the functor of $C$ and the composition of the functor of $C$ and the shift functor of the set of opposites of the set of opposites of $C$ and $n$.

the isomorphism of C and n (from the name)

Let $C$ be a set. Let $n$ be an integer. Then the isomorphism of $C$ and $n$ is an isomorphism of the composition of the shift functor of the set of opposites of the set of opposites of $C$ and $n$ and the opposite opposite of $C$ and the composition of the opposite opposite of $C$ and the shift functor of $C$ and $n$.

the contractible triangle isomorphism of X (from the name)

Let $X$ be an opposite of $C$. Then the contractible triangle isomorphism of $X$ is an isomorphism of the contractible triangle of $X$ and the action of the functor of the triangle opposite equivalence of $C$ and $\operatorname{op}$ applied to $\operatorname{invRotate}$ applied to the contractible triangle of the opposite of $X$.

the distinguished triangle of C (from the name)

Let $C$ be a set. Then the distinguished triangle of $C$ is an element of the power set of the set of triangles of the set of opposites of $C$ defined as $\operatorname{ofPred}$ applied to the function that maps $T$ to the proposition that the opposite of the action of the inverse of the triangle opposite equivalence of $C$ and $T$ is an element of the distinguished triangle.

Let $T$ be a triangle of the set of opposites of $C$. Then $\operatorname{rotateTriangleOpEquivalenceInverseObjRotateUnopIso}$ applied to $T$ is an isomorphism of $\operatorname{rotate}$ applied to the opposite of the action of the inverse of the triangle opposite equivalence of $C$ and $\operatorname{rotate}$ applied to $T$ and the opposite of the action of the inverse of the triangle opposite equivalence of $C$ and $T$.

the counit isomorphism of the equivalence of C (from the docstring)

Let $C$ be a set. Then the counit isomorphism of the equivalence of $C$ is an isomorphism of the composition of the inverse of $C$ and the functor of $C$ and the identity of the set of triangles of the set of opposites of $C$.

the functor of C (from the name)

Let $C$ be a set. Then the functor of $C$ is a functor of the set of opposites of the set of triangles of $C$ and the set of triangles of the set of opposites of $C$.

the inverse of C (from the name)

Let $C$ be a set. Then the inverse of $C$ is a functor of the set of triangles of the set of opposites of $C$ and the set of opposites of the set of triangles of $C$.

the unit isomorphism of the equivalence of C (from the docstring)

Let $C$ be a set. Then the unit isomorphism of the equivalence of $C$ is an isomorphism of the identity of the set of opposites of the set of triangles of $C$ and the composition of the functor of $C$ and the inverse of $C$.

the triangle opposite equivalence of C (from the name)

Let $C$ be a set. Then the triangle opposite equivalence of $C$ is an equivalence of the set of opposites of the set of triangles of $C$ and the set of triangles of the set of opposites of $C$.

C is pretriangulated (from the name)

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

the binary biproduct data of inr and fst (from the name)

Let $T$ be a triangle of $C$ such that $T$ is an element of the distinguished triangle and the third morphism of $T$ is equal to $0$. Let $\mathrm{inr}$ be a homomorphism of the third object of $T$ and the second object of $T$ such that the composition of $\mathrm{inr}$ and the second morphism of $T$ is equal to the identity morphism of the third object of $T$. Let $\mathrm{fst}$ be a homomorphism of the second object of $T$ and the first object of $T$ such that the sum of the composition of $\mathrm{fst}$ and the first morphism of $T$ and the composition of the second morphism of $T$ and $\mathrm{inr}$ is equal to the identity morphism of the second object of $T$. Then the binary biproduct data of $\mathrm{inr}$ and $\mathrm{fst}$ is a binary biproduct data of the first object of $T$ and the third object of $T$.

the complete distinguished triangle morphism of a and b (from the name)

Let $x_{3}$ and $x_{4}$ be triangles of $C$ such that $x_{3}$ is an element of the distinguished triangle and $x_{4}$ is an element of the distinguished triangle. Let $a$ be a homomorphism of the first object of $x_{3}$ and the first object of $x_{4}$. Let $b$ be a homomorphism of the second object of $x_{3}$ and the second object of $x_{4}$ such that the composition of the first morphism of $x_{3}$ and $b$ is equal to the composition of $a$ and the first morphism of $x_{4}$. Then the complete distinguished triangle morphism of $a$ and $b$ is a homomorphism of $x_{3}$ and $x_{4}$.

the distinguished triangle (from the name)

The distinguished triangle is an element of the power set of the set of triangles of $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the isomorphism triangle of x5 and x6 (from the name)

Let $x_{3}$ and $x_{4}$ be triangles of $C$ such that $x_{3}$ is an element of the distinguished triangle and $x_{4}$ is an element of the distinguished triangle. Let $x_{5}$ be an isomorphism of the first object of $x_{3}$ and the first object of $x_{4}$. Let $x_{6}$ be an isomorphism of the second object of $x_{3}$ and the second object of $x_{4}$ such that the composition of the first morphism of $x_{3}$ and the homomorphism of $x_{6}$ is equal to the composition of the homomorphism of $x_{5}$ and the first morphism of $x_{4}$. Then the isomorphism triangle of $x_{5}$ and $x_{6}$ is an isomorphism of $x_{3}$ and $x_{4}$.

the isomorphism triangle of x5 and x6 (from the name)

Let $x_{3}$ and $x_{4}$ be triangles of $C$ such that $x_{3}$ is an element of the distinguished triangle and $x_{4}$ is an element of the distinguished triangle. Let $x_{5}$ be an isomorphism of the first object of $x_{3}$ and the first object of $x_{4}$. Let $x_{6}$ be an isomorphism of the third object of $x_{3}$ and the third object of $x_{4}$ such that the composition of the third morphism of $x_{3}$ and the map of the shift functor of $C$ and $1$ and the homomorphism of $x_{5}$ is equal to the composition of the homomorphism of $x_{6}$ and the third morphism of $x_{4}$. Then the isomorphism triangle of $x_{5}$ and $x_{6}$ is an isomorphism of $x_{3}$ and $x_{4}$.

the short complex of T and hT (from the docstring)

Let $T$ be a triangle of $C$ such that $T$ is an element of the distinguished triangle. Then the short complex of $T$ and $\mathrm{hT}$ is a short complex of $C$ defined as $\operatorname{mk}$ applied to the first morphism of $T$, the second morphism of $T$ and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_comp\_distTriang\_mor\_zero\_u2081\_\_u2082\_}$ applied to $T$ and $\mathrm{hT}$.

the short complex of e and hT (from the name)

Let $e$ be an isomorphism of $T$ and $\mathrm{T'}$. Assume that $T$ is an element of the distinguished triangle. Then the short complex of $e$ and $\mathrm{hT}$ is an isomorphism of the short complex of $T$ and $\mathrm{hT}$ and the short complex of $\mathrm{T'}$ and $\mathrm{CategoryTheory\_\_Pretriangulated\_\_isomorphic\_distinguished}$ applied to $T$, $\mathrm{hT}$, $\mathrm{T'}$ and the inverse of $e$.

Let $T$ be a triangle of $C$. Then $\operatorname{invRotate}$ applied to $T$ is a triangle of $C$ defined as $\operatorname{mk}$ applied to $\operatorname{neg}$ applied to the composition of the map of the shift functor of $C$ and $\operatorname{neg}$ applied to $1$ and the third morphism of $T$ and the component of the inverse of the unit isomorphism of the shift equivalence of $C$ and $1$ and the first object of $T$, the first morphism of $T$ and the composition of the second morphism of $T$ and the component of the inverse of the counit isomorphism of the shift equivalence of $C$ and $1$ and $\operatorname{proj2}$ applied to $T$.

Let $T$ be a triangle of $C$. Then $\operatorname{rotate}$ applied to $T$ is a triangle of $C$ defined as $\operatorname{mk}$ applied to the second morphism of $T$, the third morphism of $T$ and $\operatorname{neg}$ applied to the map of the shift functor of $C$ and $1$ and the first morphism of $T$.

$\operatorname{invRotCompRot}$ is an isomorphism of the composition of $\operatorname{invRotate}$ applied to $C$ and $\operatorname{rotate}$ applied to $C$ and the identity of the set of triangles of $C$.

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

$\operatorname{rotCompInvRot}$ is an isomorphism of the identity of the set of triangles of $C$ and the composition of $\operatorname{rotate}$ applied to $C$ and $\operatorname{invRotate}$ applied to $C$.

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

the triangle rotation of C (from the name)

Let $C$ be a set. Then the triangle rotation of $C$ is an equivalence of the set of triangles of $C$ and the set of triangles of $C$.

the map triangulated spectral object of F and x9 (from the name)

Let $F$ be a functor of $C$ and $D$. Let $x_{9}$ be a set. Then the map triangulated spectral object of $F$ and $x_{9}$ is a functor of the set of spectral objects of $C$ and $x_{9}$ and the set of spectral objects of $D$ and $x_{9}$.

spectral object of C and x (from the name)

Let $C$ and $x$ be sets. Then the spectral objects of $C$ and $x$ are a basic type.

homomorphism of X and Y (from the name)

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

the homomorphism of self (from the name)

Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of $\mathrm{CategoryTheory\_\_Triangulated\_\_SpectralObject\_\_\_u3c9\_\_u2081\_}$ applied to $X$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_SpectralObject\_\_\_u3c9\_\_u2081\_}$ applied to $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the map homological functor of X and F (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $F$ be a functor of $C$ and $A$. Then the map homological functor of $X$ and $F$ is a spectral object of $A$ and $x$.

the map homological functor functor of F and x7 (from the name)

Let $F$ be a functor of $C$ and $A$. Let $x_{7}$ be a set. Then the map homological functor functor of $F$ and $x_{7}$ is a functor of the set of spectral objects of $C$ and $x_{7}$ and the set of spectral objects of $A$ and $x_{7}$.

the map triangle of X and x6 (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $x_{6}$ be a homomorphism of $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $f$ and $g$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $\mathrm{f'}$ and $\mathrm{g'}$. Then the map triangle of $X$ and $x_{6}$ is a homomorphism of the triangle of $f$ and $g$ and the triangle of $\mathrm{f'}$ and $\mathrm{g'}$.

the image of X and F (from the docstring)

Let $X$ be a spectral object of $C$ and $x$. Let $F$ be a functor of $C$ and $D$. Then the image of $X$ and $F$ is a spectral object of $D$ and $x$.

the precomposition of X and F (from the docstring)

Let $X$ be a spectral object of $C$ and $x$. Let $F$ be a functor of $x_{6}$ and $x$. Then the precomposition of $X$ and $F$ is a spectral object of $C$ and $x_{6}$.

the triangle of f and g (from the name)

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Then the triangle of $f$ and $g$ is a triangle of $C$.

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

Let $x_{6}$ be a homomorphism of $X$ and $Y$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Then the triangle map of $f$ and $g$ is a homomorphism of the triangle of $f$ and $g$ and the triangle of $f$ and $g$.

Let $X$ be a spectral object of $C$ and $x$. Let $f$ be a homomorphism of $i$ and $j$. Let $g$ be a homomorphism of $j$ and $k$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_SpectralObject\_\_\_u3b4\_}$ applied to $X$, $f$ and $g$ is a homomorphism of the action of $\mathrm{CategoryTheory\_\_Triangulated\_\_SpectralObject\_\_\_u3c9\_\_u2081\_}$ applied to $X$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $g$ and the action of the shift functor of $C$ and $1$ and the action of $\mathrm{CategoryTheory\_\_Triangulated\_\_SpectralObject\_\_\_u3c9\_\_u2081\_}$ applied to $X$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2081\_}$ applied to $f$ defined as the component of $\mathrm{CategoryTheory\_\_Triangulated\_\_SpectralObject\_\_\_u3b4\_'}$ applied to $X$ and $\mathrm{CategoryTheory\_\_ComposableArrows\_\_mk\_u2082\_}$ applied to $f$ and $g$.

Let $\mathrm{self}$ be a spectral object of $C$ and $x$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_SpectralObject\_\_\_u3b4\_'}$ applied to $\mathrm{self}$ is a homomorphism of the composition of the functor arrow of $2$ and $2$ and $\mathrm{CategoryTheory\_\_Triangulated\_\_SpectralObject\_\_\_u3c9\_\_u2081\_}$ applied to $\mathrm{self}$ and the composition of the functor arrow of $1$ and $2$ and the composition of $\mathrm{CategoryTheory\_\_Triangulated\_\_SpectralObject\_\_\_u3c9\_\_u2081\_}$ applied to $\mathrm{self}$ and the shift functor of $C$ and $1$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a spectral object of $C$ and $x$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_SpectralObject\_\_\_u3c9\_\_u2081\_}$ applied to $\mathrm{self}$ is a functor of the set of composable arrows of $x$ and $1$ and $C$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $X$ be a spectral object of $C$ and $x$. Then $\mathrm{CategoryTheory\_\_Triangulated\_\_SpectralObject\_\_\_u3c9\_\_u2082\_}$ applied to $X$ is a functor of the set of composable arrows of $x$ and $2$ and the set of triangles of $C$.