Definitions: Mathlib.CategoryTheory, part 22 of 25

descent data as coalgebra of F and f (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of adjoints of the set of categories. Let $f$ be a function from elements $i$ of $x_{1}$ to homomorphisms of $X$ applied to $i$ and $S$. Then the descent data as coalgebra of $F$ and $i$ are a basic type.

homomorphism of x2 and x3 (from the name)

Let $x_{2}$ and $x_{3}$ be descent data as coalgebra of $F$ and $f$. Then the homomorphisms of $x_{2}$ and $x_{3}$ are a basic type.

the homomorphism of self and i (from the name)

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

the coalgebra equivalence of F and f (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of adjoints of the set of categories. Let $x_{1}$ be a set. Let $f$ be a homomorphism of $X$ and $S$. Then the coalgebra equivalence of $F$ and $f$ is an equivalence of the set of descent data as coalgebra of $F$ and the function that maps $x_{3}$ to $f$ and the set of coalgebras of the comonad of the adjunction of the adjoint of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $f$.

the homomorphism of x2 and x3 (from the name)

Let $\mathrm{self}$ be a descent data as coalgebra of $F$ and $f$. Let $x_{2}$ and $x_{3}$ be elements of $x_{1}$. Then the homomorphism of $x_{2}$ and $x_{3}$ is a homomorphism of the object of $\mathrm{self}$ and $x_{2}$ and the action of the functor of $\operatorname{l}$ applied to the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $f$ applied to $x_{2}$ and the action of the functor of $\operatorname{r}$ applied to the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $f$ applied to $x_{3}$ and the object of $\mathrm{self}$ and $x_{3}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

the isomorphism of e and i (from the name)

Let $e$ be a function from elements $i$ of $x_{1}$ to isomorphisms of the object of $x_{2}$ and $i$ and the object of $x_{3}$ and $i$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{4}$ and $x_{5}$ of $x_{1}$, the composition of the homomorphism of $x_{4}$ and $x_{5}$ and the map of the functor of $\operatorname{l}$ applied to the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $f$ applied to $x_{4}$ and the map of the functor of $\operatorname{r}$ applied to the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $f$ applied to $x_{5}$ and the homomorphism of $e$ applied to $x_{5}$ is equal to the composition of the homomorphism of $e$ applied to $x_{4}$ and the homomorphism of $x_{4}$ and $x_{5}$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentDataAsCoalgebra\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $i$ and $e$ is an isomorphism of $x_{2}$ and $x_{3}$.

the object of self and i (from the name)

Let $\mathrm{self}$ be a descent data as coalgebra of $F$ and $f$. Let $i$ be an element of $x_{1}$. Then the object of $\mathrm{self}$ and $i$ is an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $X$ applied to $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

the descent data as coalgebra of F and f (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of adjoints of the set of categories. Let $f$ be a function from elements $i$ of $x_{1}$ to homomorphisms of $X$ applied to $i$ and $S$. Then the descent data as coalgebra of $F$ and $i$ is a functor of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$ and the set of descent data as coalgebra of $F$ and $f$.

the descent data as coalgebra composition coalgebra equivalence functor isomorphism of x1 and f (from the name)

Let $x_{1}$ be a set. Let $f$ be a homomorphism of $X$ and $S$. Then the descent data as coalgebra composition coalgebra equivalence functor isomorphism of $x_{1}$ and $f$ is an isomorphism of the composition of the descent data as coalgebra of $F$ and the function that maps $x_{3}$ to $f$ and the functor of the coalgebra equivalence of $F$ and $f$ and the comparison of the adjunction of the adjoint of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $f$ defined as the identity of the composition of the descent data as coalgebra of $F$ and the function that maps $x_{3}$ to $f$ and the functor of the coalgebra equivalence of $F$ and $f$.

descent data of sq and i (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $\mathrm{sq}$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ to chosen pullbacks of $f$ applied to $i$ and $f$ applied to $j$. Let $x_{2}$ be a function from elements $x_{3}$ of $x_{1}$ and elements $x_{4}$ of $x_{1}$ and elements $x_{5}$ of $x_{1}$ to chosen pullbacks of $\mathrm{sq}$ applied to $x_{4}$ and $x_{5}$ and $\mathrm{sq}$ applied to $x_{3}$ and $x_{5}$. Then the descent data of $i$ and $j$ are a basic type.

homomorphism of x3 and x4 (from the name)

Let $x_{3}$ and $x_{4}$ be descent data of $\mathrm{sq}$ and $x_{2}$. Then the homomorphisms of $x_{3}$ and $x_{4}$ are a basic type.

the homomorphism of self and i (from the name)

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

the descent data of D (from the name)

Let $D$ be a descent data of $\mathrm{sq}$ and $x_{2}$. Then the descent data of $D$ is a descent data of $F$ and $f$.

the descent data equivalence of sq and i (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $\mathrm{sq}$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ to chosen pullbacks of $f$ applied to $i$ and $f$ applied to $j$. Let $x_{2}$ be a function from elements $x_{3}$ of $x_{1}$ and elements $x_{4}$ of $x_{1}$ and elements $x_{5}$ of $x_{1}$ to chosen pullbacks of $\mathrm{sq}$ applied to $x_{4}$ and $x_{5}$ and $\mathrm{sq}$ applied to $x_{3}$ and $x_{5}$. Then the descent data equivalence of $i$ and $j$ is an equivalence of the set of descent data of $\mathrm{sq}$ and $x_{2}$ and the set of descent data of $F$ and $f$.

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $\mathrm{sq}$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ to chosen pullbacks of $f$ applied to $i$ and $f$ applied to $j$. Let $x_{2}$ be a function from elements $x_{3}$ of $x_{1}$ and elements $x_{4}$ of $x_{1}$ and elements $x_{5}$ of $x_{1}$ to chosen pullbacks of $\mathrm{sq}$ applied to $x_{4}$ and $x_{5}$ and $\mathrm{sq}$ applied to $x_{3}$ and $x_{5}$. Then $\operatorname{fromDescentDataFunctor}$ applied to $F$, $i$, $j$, $\mathrm{sq}$, $x_{3}$, $x_{4}$, $x_{5}$ and $x_{2}$ is a functor of the set of descent data of $F$ and $f$ and the set of descent data of $\mathrm{sq}$ and $x_{2}$.

the homomorphism of i and j (from the name)

Let $\mathrm{self}$ be a descent data of $\mathrm{sq}$ and $x_{2}$. Let $i$ and $j$ be elements of $x_{1}$. Then the homomorphism of $i$ and $j$ is a homomorphism of the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2081\_}$ applied to $\mathrm{sq}$ applied to $i$ and $j$ and the object of $\mathrm{self}$ and $i$ and the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2082\_}$ applied to $\mathrm{sq}$ applied to $i$ and $j$ and the object of $\mathrm{self}$ and $j$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $i$ and $j$.

the isomorphism of e and i (from the name)

Let $e$ be a function from elements $i$ of $x_{1}$ to isomorphisms of the object of $x_{3}$ and $i$ and the object of $x_{4}$ and $i$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $x_{5}$ and $x_{6}$ of $x_{1}$, the composition of the map of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2081\_}$ applied to $\mathrm{sq}$ applied to $x_{5}$ and $x_{6}$ and the homomorphism of $e$ applied to $x_{5}$ and the homomorphism of $x_{5}$ and $x_{6}$ is equal to the composition of the homomorphism of $x_{5}$ and $x_{6}$ and the map of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2082\_}$ applied to $\mathrm{sq}$ applied to $x_{5}$ and $x_{6}$ and the homomorphism of $e$ applied to $x_{6}$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData'\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $i$ and $e$ is an isomorphism of $x_{3}$ and $x_{4}$.

the object of self and i (from the name)

Let $\mathrm{self}$ be a descent data of $\mathrm{sq}$ and $x_{2}$. Let $i$ be an element of $x_{1}$. Then the object of $\mathrm{self}$ and $i$ is an element of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $X$ applied to $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

the descent data of i and j (from the name)

Let $\mathrm{sq}$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ to chosen pullbacks of $f$ applied to $i$ and $f$ applied to $j$. Let $x_{2}$ be a function from elements $x_{3}$ of $x_{1}$ and elements $x_{4}$ of $x_{1}$ and elements $x_{5}$ of $x_{1}$ to chosen pullbacks of $\mathrm{sq}$ applied to $x_{4}$ and $x_{5}$ and $\mathrm{sq}$ applied to $x_{3}$ and $x_{5}$. Let $D$ be a descent data of $F$ and $f$. Then the descent data of $j$ and $\mathrm{sq}$ is a descent data of $\mathrm{sq}$ and $x_{2}$.

Let $\mathrm{hom}$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ to homomorphisms of the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2081\_}$ applied to $\mathrm{sq}$ applied to $i$ and $j$ and $\mathrm{obj}$ applied to $i$ and the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $\mathrm{CategoryTheory\_\_Limits\_\_ChosenPullback\_\_p\_u2082\_}$ applied to $\mathrm{sq}$ applied to $i$ and $j$ and $\mathrm{obj'}$ applied to $j$. Let $q$ be a homomorphism of $Y$ and $S$. Let $x_{4}$ be a homomorphism of $Y$ and $X$ applied to $x_{2}$. Let $x_{5}$ be a homomorphism of $Y$ and $X$ applied to $x_{3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{4}$ and $f$ applied to $x_{2}$ is equal to $q$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData'\_\_pullHom'\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $x_{5}$ and $f$ applied to $x_{3}$ is equal to $q$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData'\_\_pullHom'\_\_\_auto\_3}$. Then $\operatorname{pullHom'}$ applied to $i$, $j$, $\mathrm{hom}$, $q$, $x_{4}$, $x_{5}$, $h$ and $h_{1}$ is a homomorphism of the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{4}$ and $\mathrm{obj}$ applied to $x_{2}$ and the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{5}$ and $\mathrm{obj'}$ applied to $x_{3}$.

the descent data functor of sq and i (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $\mathrm{sq}$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ to chosen pullbacks of $f$ applied to $i$ and $f$ applied to $j$. Let $x_{2}$ be a function from elements $x_{3}$ of $x_{1}$ and elements $x_{4}$ of $x_{1}$ and elements $x_{5}$ of $x_{1}$ to chosen pullbacks of $\mathrm{sq}$ applied to $x_{4}$ and $x_{5}$ and $\mathrm{sq}$ applied to $x_{3}$ and $x_{5}$. Then the descent data functor of $i$ and $j$ is a functor of the set of descent data of $\mathrm{sq}$ and $x_{2}$ and the set of descent data of $F$ and $f$.

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $J$ be a Grothendieck topology of $C$. Then we can say that $\operatorname{IsPrestack}$ holds for $F$ and $J$.

Let $x_{7}$ be a homomorphism of the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{5}$ and $x_{3}$ and the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{6}$ and $x_{4}$. Let $g$ be a homomorphism of $\mathrm{Y'}$ and $Y$. Let $x_{8}$ be a homomorphism of $\mathrm{Y'}$ and $x_{1}$. Let $x_{9}$ be a homomorphism of $\mathrm{Y'}$ and $x_{2}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $g$ and $x_{5}$ is equal to $x_{8}$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_LocallyDiscreteOpToCat\_\_pullHom\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that the composition of $g$ and $x_{6}$ is equal to $x_{9}$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_LocallyDiscreteOpToCat\_\_pullHom\_\_\_auto\_3}$. Then $\operatorname{pullHom}$ applied to $x_{7}$, $g$, $x_{8}$, $x_{9}$, $h$ and $h_{1}$ is a homomorphism of the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{8}$ and $x_{3}$ and the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $x_{9}$ and $x_{4}$.

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $M$ and $N$ be elements of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$. Let $q$ be a homomorphism of $\mathrm{S'}$ and $S$. Then $\operatorname{overMapCompPresheafHomIso}$ applied to $F$, $M$, $N$ and $q$ is an isomorphism of the composition of the opposite of the map of $q$ and the presheaf homomorphism of $M$ and $N$ and the presheaf homomorphism of the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $q$ and $M$ and the action of the functor of the map of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{toLoc}$ applied to the opposite in $q$ and $N$.

the presheaf homomorphism of M and N (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $M$ and $N$ be elements of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$. Then the presheaf homomorphism of $M$ and $N$ is a functor of the set of opposites of $\operatorname{Over}$ applied to $S$ and the set of sets.

the presheaf homomorphism object homomorphism equivalence of F (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Then the presheaf homomorphism object homomorphism equivalence of $F$ is an equivalence from the set of homomorphisms of $M$ and $N$ to the action of the presheaf homomorphism of $M$ and $N$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to the identity morphism of $S$ defined as the homomorphism congruence of the application of the inverse of the natural isomorphism of the map identity of $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$ and $M$ and the application of the inverse of the natural isomorphism of the map identity of $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$ and $N$.

the sheaf homomorphism of M and N (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $J$ be a Grothendieck topology of $C$. Let $M$ and $N$ be elements of $\mathrm{CategoryTheory\_\_Bundled\_\_\_u3b1\_}$ applied to the object of $\operatorname{toPrefunctor}$ applied to $\operatorname{toPrelaxFunctorStruct}$ applied to $\operatorname{toPrelaxFunctor}$ applied to $F$ and $\operatorname{mk}$ applied to $\operatorname{op}$ applied to $S$. Then the sheaf homomorphism of $M$ and $N$ is a sheaf of $\operatorname{over}$ applied to $J$ and $S$ and the set of sets defined as $\operatorname{mk}$ applied to the presheaf homomorphism of $M$ and $N$ and $\operatorname{isSheaf}$ applied to $J$, $M$ and $N$.

F is a stack with respect to J (from the name)

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Let $J$ be a Grothendieck topology of $C$. Then we can say that $F$ is a stack with respect to $J$.

Let $F$ be a pseudofunctor of $\operatorname{LocallyDiscrete}$ applied to the set of opposites of $C$ and the set of categories. Assume that for all elements $j$ of $x_{2}$, the composition of $\mathrm{p'}$ applied to $j$ and $f$ applied to $x_{3}$ applied to $j$ is equal to $\mathrm{f'}$ applied to $j$. Assume that the sieve of $\mathrm{X'}$ and $\mathrm{f'}$ is an element of $J$ applied to $S$. Then $\operatorname{fullyFaithfulPullFunctor}$ applied to $F$, $w$ and $\mathrm{hf'}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{pullFunctor}$ applied to $F$ and $\mathrm{CategoryTheory\_\_Pseudofunctor\_\_DescentData\_\_faithful\_pullFunctor\_\_\_proof\_2}$ applied to $w$.

Let $S$ be a presieve of $X$. Then $\operatorname{EffectiveEpimorphic}$ holds for $S$, if $\operatorname{EffectiveEpimorphic}$ holds for $\operatorname{generate}$ applied to $S$.

Let $S$ be a sieve of $X$. Then $\operatorname{EffectiveEpimorphic}$ holds for $S$, if $\mathrm{Nonempty}$ holds for $\operatorname{IsColimit}$ applied to the cocone of the arrow of $S$.

Let $X$ be a function from elements of $x_{1}$ to elements of $C$. Let $x_{2}$ be a function from elements $a$ of $x_{1}$ to homomorphisms of $X$ applied to $a$ and $B$. Then $\operatorname{generateFamily}$ applied to $X$, $a$ and $x_{2}$ is a sieve of $B$.

Let $f$ be a homomorphism of $Y$ and $X$. Then $\operatorname{generateSingleton}$ applied to $f$ is a sieve of $X$.

the functorial locally surjective injective factorization of J and data (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then there is a morphism property of the set of sheaves of $J$ and $A$. Proof. Let $J$ be arbitrary. Let $A$ be arbitrary. Let $x_{4}$ be arbitrary. Let $x_{5}$ be arbitrary. Let $f$ be arbitrary. By f. By CategoryTheory__Sheaf__IsLocallyInjective.

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then there is a morphism property of the set of sheaves of $J$ and $A$. Proof. Let $J$ be arbitrary. Let $A$ be arbitrary. Let $x_{4}$ be arbitrary. Let $x_{5}$ be arbitrary. Let $f$ be arbitrary. By f. By CategoryTheory__Sheaf__IsLocallySurjective.

first object of P and R (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $R$ be a presieve of $X$. Then a first object of $P$ and $R$ is an element of the function that maps $P$ and $R$ to the product object of the function that maps $f$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{fst}$ applied to $f$.

first object of P and X (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $X$ be a function from elements of $I$ to elements of $C$. Then a first object of $P$ and $X$ is an element of the function that maps $P$ and $X$ to the product object of the function that maps $i$ to the action of $P$ and $\operatorname{op}$ applied to $X$ applied to $i$.

second object of X and x1 (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $X$ be a function from elements of $I$ to elements of $C$. Let $x_{1}$ be a function from elements $i$ of $I$ to homomorphisms of $X$ applied to $i$ and $B$. Then a second object of $X$ and $i$ is an element of the function that maps $P$, $X$, $x_{1}$ and $x_{1}$ to the product object of the function that maps $\mathrm{ij}$ to the action of $P$ and $\operatorname{op}$ applied to the pullback of $i$ applied to $\ProdfstMACRoZ {\mathrm{ij}}$ and $i$ applied to $\ProdsndMACRoAA {\mathrm{ij}}$.

the first map of X and x1 (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $X$ be a function from elements of $I$ to elements of $C$. Let $x_{1}$ be a function from elements $i$ of $I$ to homomorphisms of $X$ applied to $i$ and $B$. Then the first map of $X$ and $i$ is a homomorphism of the set of first objects of $P$ and $X$ and the set of second objects of $X$ and $x_{1}$ defined as the function that maps $x_{1}$ to the lift of the function that maps $x_{2}$ to the composition of the projection of the function that maps $i$ to the action of $P$ and $\operatorname{op}$ applied to $X$ applied to $i$ and $\ProdfstMACRoZ {x_{2}}$ and the map of $P$ and the opposite in the first projection of the pullback of $i$ applied to $\ProdfstMACRoZ {x_{2}}$ and $i$ applied to $\ProdsndMACRoAA {x_{2}}$.

the fork map of X and x1 (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $X$ be a function from elements of $I$ to elements of $C$. Let $x_{1}$ be a function from elements $i$ of $I$ to homomorphisms of $X$ applied to $i$ and $B$. Then the fork map of $X$ and $i$ is a homomorphism of the action of $P$ and $\operatorname{op}$ applied to $B$ and the set of first objects of $P$ and $X$ defined as the function that maps $x_{1}$ to the lift of the function that maps $i$ to the map of $P$ and the opposite in $i$ applied to $i$.

the second map of X and x1 (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $X$ be a function from elements of $I$ to elements of $C$. Let $x_{1}$ be a function from elements $i$ of $I$ to homomorphisms of $X$ applied to $i$ and $B$. Then the second map of $X$ and $i$ is a homomorphism of the set of first objects of $P$ and $X$ and the set of second objects of $X$ and $x_{1}$ defined as the function that maps $x_{1}$ to the lift of the function that maps $x_{2}$ to the composition of the projection of the function that maps $i$ to the action of $P$ and $\operatorname{op}$ applied to $X$ applied to $i$ and $\ProdsndMACRoAA {x_{2}}$ and the map of $P$ and the opposite in the second projection of the pullback of $i$ applied to $\ProdfstMACRoZ {x_{2}}$ and $i$ applied to $\ProdsndMACRoAA {x_{2}}$.

second object of P and R (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $R$ be a presieve of $X$. Then a second object of $P$ and $R$ is an element of the function that maps $P$ and $R$ to the product object of the function that maps $\mathrm{fg}$ to the action of $P$ and $\operatorname{op}$ applied to the pullback of $\operatorname{snd}$ applied to $\ProdfstMACRoZ {\mathrm{fg}}$ and $\operatorname{snd}$ applied to $\ProdsndMACRoAA {\mathrm{fg}}$.

the map of P and R (from the docstring)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $R$ be a presieve of $X$. Then the map of $P$ and $R$ is a homomorphism of the set of first objects of $P$ and $R$ and the set of second objects of $P$ and $R$ defined as the lift of the function that maps $\mathrm{fg}$ to the composition of the projection of the function that maps $f$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{fst}$ applied to $f$ and $\ProdfstMACRoZ {\mathrm{fg}}$ and the map of $P$ and the opposite in the first projection of the pullback of $\operatorname{snd}$ applied to $\ProdfstMACRoZ {\mathrm{fg}}$ and $\operatorname{snd}$ applied to $\ProdsndMACRoAA {\mathrm{fg}}$.

the map of P and R (from the docstring)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $R$ be a presieve of $X$. Then the map of $P$ and $R$ is a homomorphism of the set of first objects of $P$ and $R$ and the set of second objects of $P$ and $R$ defined as the lift of the function that maps $\mathrm{fg}$ to the composition of the projection of the function that maps $f$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{fst}$ applied to $f$ and $\ProdsndMACRoAA {\mathrm{fg}}$ and the map of $P$ and the opposite in the second projection of the pullback of $\operatorname{snd}$ applied to $\ProdfstMACRoZ {\mathrm{fg}}$ and $\operatorname{snd}$ applied to $\ProdsndMACRoAA {\mathrm{fg}}$.

second object of P and S (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $S$ be a sieve of $X$. Then a second object of $P$ and $S$ is an element of the function that maps $P$ and $S$ to the product object of the function that maps $f$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{fst}$ applied to $\operatorname{snd}$ applied to $f$.

the first map of P and S (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $S$ be a sieve of $X$. Then the first map of $P$ and $S$ is a homomorphism of the set of first objects of $P$ and the arrow of $S$ and the set of second objects of $P$ and $S$ defined as the lift of the function that maps $\mathrm{fg}$ to the projection of the function that maps $f$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{fst}$ applied to $f$ and $\operatorname{mk}$ applied to $\operatorname{fst}$ applied to $\operatorname{snd}$ applied to $\mathrm{fg}$ and the composition of $\operatorname{fst}$ applied to $\operatorname{snd}$ applied to $\operatorname{snd}$ applied to $\mathrm{fg}$ and $\operatorname{snd}$ applied to $\operatorname{snd}$ applied to $\operatorname{snd}$ applied to $\mathrm{fg}$.

the second map of P and S (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $S$ be a sieve of $X$. Then the second map of $P$ and $S$ is a homomorphism of the set of first objects of $P$ and the arrow of $S$ and the set of second objects of $P$ and $S$ defined as the lift of the function that maps $\mathrm{fg}$ to the composition of the projection of the function that maps $f$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{fst}$ applied to $f$ and $\operatorname{mk}$ applied to $\operatorname{fst}$ applied to $\mathrm{fg}$ and $\operatorname{snd}$ applied to $\operatorname{snd}$ applied to $\operatorname{snd}$ applied to $\mathrm{fg}$ and the map of $P$ and the opposite in $\operatorname{fst}$ applied to $\operatorname{snd}$ applied to $\operatorname{snd}$ applied to $\mathrm{fg}$.

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $R$ be a presieve of $X$. Then $\operatorname{firstObjEqFamily}$ applied to $P$ and $R$ is an isomorphism of the set of first objects of $P$ and $R$ and the set of families of element of $P$ and $R$.

the fork map of P and R (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $R$ be a presieve of $X$. Then the fork map of $P$ and $R$ is a homomorphism of the action of $P$ and $\operatorname{op}$ applied to $X$ and the set of first objects of $P$ and $R$ defined as the lift of the function that maps $f$ to the map of $P$ and the opposite in $\operatorname{snd}$ applied to $f$.

the sheaf congruence of K and e (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $e$ be an equivalence of $C$ and $D$. Let $A$ be a set. Then the sheaf congruence of $K$ and $e$ is an equivalence of the set of sheaves of $J$ and $A$ and the set of sheaves of $K$ and $A$.

the counit isomorphism of K and e (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $e$ be an equivalence of $C$ and $D$. Let $A$ be a set. Then the counit isomorphism of $K$ and $e$ is an isomorphism of the composition of the inverse of $K$ and $e$ and the functor of $K$ and $e$ and the identity of the set of sheaves of $K$ and $A$.

the functor of K and e (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $e$ be an equivalence of $C$ and $D$. Let $A$ be a set. Then the functor of $K$ and $e$ is a functor of the set of sheaves of $J$ and $A$ and the set of sheaves of $K$ and $A$.

the inverse of K and e (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $e$ be an equivalence of $C$ and $D$. Let $A$ be a set. Then the inverse of $K$ and $e$ is a functor of the set of sheaves of $K$ and $A$ and the set of sheaves of $J$ and $A$.

the unit isomorphism of K and e (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $e$ be an equivalence of $C$ and $D$. Let $A$ be a set. Then the unit isomorphism of $K$ and $e$ is an isomorphism of the identity of the set of sheaves of $J$ and $A$ and the composition of the functor of $K$ and $e$ and the inverse of $K$ and $e$.

the transport and sheafification of K and e (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $e$ be an equivalence of $C$ and $D$. Let $A$ be a set. Then the transport and sheafification of $K$ and $e$ is a functor of the set of functors of the set of opposites of $C$ and $A$ and the set of sheaves of $J$ and $A$ defined as the composition of the functor of the left congruence of the opposite of $e$ and the composition of the presheaf to sheaf of $K$ and $A$ and the inverse of the sheaf congruence of $K$ and $e$.

the transport sheafification adjunction of K and e (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $K$ be a Grothendieck topology of $D$. Let $e$ be an equivalence of $C$ and $D$. Let $A$ be a set. Then the transport sheafification adjunction of $K$ and $e$ is an adjunction of the transport and sheafification of $K$ and $e$ and the sheaf to presheaf of $J$ and $A$ defined as the adjunction of the composition of the composition of the adjunction of the left congruence of the opposite of $e$ and the sheafification adjunction of $K$ and $A$ and the adjunction of the inverse of the sheaf congruence of $K$ and $e$ and $\operatorname{transportIsoSheafToPresheaf}$ applied to $J$, $K$, $e$ and $A$.

the small sheafification adjunction of J and A (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the small sheafification adjunction of $J$ and $A$ is an adjunction of the small sheafification of $J$ and $A$ and the sheaf to presheaf of $J$ and $A$ defined as the transport sheafification adjunction of the induced topology of the inverse of the equivalence small model of $C$ and $J$ and the equivalence small model of $C$.

the small sheafification of J and A (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the small sheafification of $J$ and $A$ is a functor of the set of functors of the set of opposites of $C$ and $A$ and the set of sheaves of $J$ and $A$ defined as the transport and sheafification of the induced topology of the inverse of the equivalence small model of $C$ and $J$ and the equivalence small model of $C$.

Let $C$ be a set. Then $\operatorname{finite}$ applied to $C$ is a precoverage of $C$ defined as $\operatorname{mk}$ applied to the function that maps $X$ to $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $\operatorname{uncurry}$ applied to $s$ is finite.

Let $C$ be a set. Then $\operatorname{finite}$ applied to $C$ is a pretopology of $C$.

J has global sections functors (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then $J$ has global sections functors, if the constant sheaf of $J$ and $A$ is a left adjoint.

the cone of F (from the docstring)

Let $F$ be a sheaf of $J$ and $A$. Then the cone of $F$ is a cone of the object of $F$ defined as $\operatorname{mk}$ applied to the action of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ and $F$ and $\operatorname{symm}$ applied to the homomorphism equivalence and the identity morphism of the action of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ and $F$.

Let $F$ be a sheaf of $J$ and $A$. Then $\mathrm{CategoryTheory\_\_Sheaf\_\_isLimitCone\_u393\_}$ applied to $F$ is an element of $\operatorname{IsLimit}$ applied to the cone of $F$.

the natural transformation restriction of J and U (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Let $U$ be an opposite of $C$. Then the natural transformation restriction of $J$ and $U$ is a homomorphism of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ and the action of the sheaf section of $J$ and $A$ and $U$ defined as $\operatorname{mk}$ applied to the function that maps $F$ to the restriction of $F$ and $U$ and the function that maps $x_{2}$, $x_{3}$ and $f$ to $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_Res\_naturality}$ applied to $f$ and $U$.

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ is a functor of the set of sheaves of $J$ and $A$ and $A$ defined as the right adjoint of the constant sheaf of $J$ and $A$.

the homomorphism equivalence (from the name)

The homomorphism equivalence is an equivalence from the set of homomorphisms of the action of the constant of the set of opposites of $C$ and $X$ and the object of $F$ to the set of homomorphisms of $X$ and the action of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ and $F$ defined as the composition of the inverse of the homomorphism equivalence of the action of the constant of the set of opposites of $C$ and $X$ and $F$ and the homomorphism equivalence of $X$ and $F$.

the natural isomorphism Coyoneda of J and X (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $X$ be a set. Then the natural isomorphism Coyoneda of $J$ and $X$ is an isomorphism of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and the set of sets and the action of the Coyoneda and $\operatorname{op}$ applied to the action of the constant sheaf of $J$ and the set of sets and $X$.

the natural isomorphism limit of J and A (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the natural isomorphism limit of $J$ and $A$ is an isomorphism of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ and the composition of the sheaf to presheaf of $J$ and $A$ and the limit defined as $\operatorname{rightAdjointUniq}$ applied to the constant sheaf functor of $J$ and $A$ and the composition of the constant functor and limit functor and the sheafification adjunction of $J$ and $A$.

the natural isomorphism section functor of J (from the name)

Let $J$ be a Grothendieck topology of $C$. Then the natural isomorphism section functor of $J$ is an isomorphism of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and the set of sets and the composition of the sheaf to presheaf of $J$ and the set of sets and the section functor of the set of opposites of $C$.

the natural isomorphism sheaf section of J and hT (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then the natural isomorphism sheaf section of $J$ and $\mathrm{hT}$ is an isomorphism of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ and the action of the sheaf section of $J$ and $A$ and $\operatorname{op}$ applied to $T$ defined as $\operatorname{rightAdjointUniq}$ applied to the constant sheaf functor of $J$ and $A$ and the constant sheaf adjoint of $J$ and $\mathrm{hT}$.

the object equivalence homomorphism of J and F (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $F$ be a sheaf of $J$ and the set of sets. Let $X$ be a set. Then the object equivalence homomorphism of $J$ and $F$ is an equivalence from the action of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and the set of sets and $F$ to the set of homomorphisms of the action of the constant sheaf of $J$ and the set of sets and $X$ and $F$ defined as the composition of the composition of the inverse of $\operatorname{funUnique}$ applied to $X$ and the action of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and the set of sets and $F$ and the inverse of the homomorphism equivalence and the inverse of the homomorphism equivalence of $X$ and $F$.

the object equivalence section of J and F (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $F$ be a sheaf of $J$ and the set of sets. Then the object equivalence section of $J$ and $F$ is an equivalence from the action of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and the set of sets and $F$ to the set of elements of the section of the object of $F$ defined as the composition of the composition of the composition of the inverse of $\operatorname{funUnique}$ applied to $\mathrm{PUnit}$ and the action of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and the set of sets and $F$ and the inverse of the homomorphism equivalence and the inverse of the homomorphism equivalence and the inverse of the section equivalence homomorphism of the object of $F$ and $\mathrm{PUnit}$.

the restriction of F and U (from the name)

Let $F$ be a sheaf of $J$ and $A$. Let $U$ be an opposite of $C$. Then the restriction of $F$ and $U$ is a homomorphism of the action of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ and $F$ and the action of the object of $F$ and $U$ defined as the component of the projection of the cone of $F$ and $U$.

the constant sheaf functor of J and A (from the docstring)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the constant sheaf functor of $J$ and $A$ is an adjunction of the constant sheaf of $J$ and $A$ and $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ defined as the adjunction of the constant sheaf of $J$ and $A$.

Grothendieck topology of C (from the name)

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

cover of J and X (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $X$ be an element of $C$. Then a cover of $J$ and $X$ is an element of the function that maps $J$ and $X$ to $\SubtypeSet {S}{(\MembershipmemMACRoT {J (X)}{S})}$.

relation of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{Arrow}$ applied to $S$. Then the relations of $x_{1}$ and $x_{2}$ are a basic type.

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

the base of r (from the name)

Let $r$ be a relation of $x_{1}$ and $x_{2}$. Then the base of $r$ is a relation of the base of $x_{1}$ and the base of $x_{2}$.

Let $\mathrm{self}$ be a relation of $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2081\_}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{Z}$ applied to $\mathrm{self}$ and $\operatorname{Y}$ applied to $x_{1}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a relation of $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2082\_}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{Z}$ applied to $\mathrm{self}$ and $\operatorname{Y}$ applied to $x_{2}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the map of r and f (from the name)

Let $r$ be a relation of $x_{1}$ and $x_{2}$. Let $f$ be a homomorphism of $S$ and $T$. Then the map of $r$ and $f$ is a relation of the map of $x_{1}$ and $f$ and the map of $x_{2}$ and $f$ defined as $\operatorname{mk}$ applied to $\operatorname{Z}$ applied to $r$, $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2081\_}$ applied to $r$, $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2082\_}$ applied to $r$ and $\operatorname{w}$ applied to $r$.

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

the base of I (from the name)

Let $I$ be an element of $\operatorname{Arrow}$ applied to the pullback of $S$ and $f$. Then the base of $I$ is an element of $\operatorname{Arrow}$ applied to $S$.

Let $\mathrm{self}$ be an element of $\operatorname{Arrow}$ applied to $S$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is a homomorphism of $\operatorname{Y}$ applied to $\mathrm{self}$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $I$ be an element of $\operatorname{Arrow}$ applied to $\operatorname{bind}$ applied to $S$ and $T$. Then $\operatorname{fromMiddle}$ applied to $I$ is an element of $\operatorname{Arrow}$ applied to $S$ defined as $\operatorname{mk}$ applied to the middle of $I$, $\operatorname{fromMiddleHom}$ applied to $I$ and $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_from\_middle\_condition}$ applied to $I$.

Let $I$ be an element of $\operatorname{Arrow}$ applied to $\operatorname{bind}$ applied to $S$ and $T$. Then $\operatorname{fromMiddleHom}$ applied to $I$ is a homomorphism of the middle of $I$ and $X$.

the map of I and f (from the name)

Let $I$ be an element of $\operatorname{Arrow}$ applied to $S$. Let $f$ be a homomorphism of $S$ and $T$. Then the map of $I$ and $f$ is an element of $\operatorname{Arrow}$ applied to $T$.

the middle of I (from the name)

Let $I$ be an element of $\operatorname{Arrow}$ applied to $\operatorname{bind}$ applied to $S$ and $T$. Then the middle of $I$ is an element of $C$.

the precomposition of I and g (from the name)

Let $I$ be an element of $\operatorname{Arrow}$ applied to $S$. Let $g$ be a homomorphism of $Z$ and $\operatorname{Y}$ applied to $I$. Then the precomposition of $I$ and $g$ is an element of $\operatorname{Arrow}$ applied to $S$.

the precomposition relation of I and g (from the name)

Let $I$ be an element of $\operatorname{Arrow}$ applied to $S$. Let $g$ be a homomorphism of $Z$ and $\operatorname{Y}$ applied to $I$. Then the precomposition relation of $I$ and $g$ is a relation of the precomposition of $I$ and $g$ and $I$.

the middle of I (from the name)

Let $I$ be an element of $\operatorname{Arrow}$ applied to $\operatorname{bind}$ applied to $S$ and $T$. Then the middle of $I$ is an element of $\operatorname{Arrow}$ applied to $T$ applied to $\operatorname{fromMiddle}$ applied to $I$ defined as $\operatorname{mk}$ applied to $\operatorname{Y}$ applied to $I$, the middle homomorphism of $I$ and $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_to\_middle\_condition}$ applied to $I$.

the middle homomorphism of I (from the name)

Let $I$ be an element of $\operatorname{Arrow}$ applied to $\operatorname{bind}$ applied to $S$ and $T$. Then the middle homomorphism of $I$ is a homomorphism of $\operatorname{Y}$ applied to $I$ and the middle of $I$.

the first arrow of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{Relation}$ applied to $S$. Then the first arrow of $\mathrm{self}$ is an element of $\operatorname{Arrow}$ applied to $S$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $r$ be a relation of $\mathrm{fst}$ and $\mathrm{snd}$. Then $\operatorname{mk'}$ applied to $r$ is an element of $\operatorname{Relation}$ applied to $S$ defined as $\operatorname{mk}$ applied to $r$.

Let $\mathrm{self}$ be an element of $\operatorname{Relation}$ applied to $S$. Then $\operatorname{r}$ applied to $\mathrm{self}$ is a relation of the first arrow of $\mathrm{self}$ and the second arrow of $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

the second arrow of self (from the docstring)

Let $\mathrm{self}$ be an element of $\operatorname{Relation}$ applied to $S$. Then the second arrow of $\mathrm{self}$ is an element of $\operatorname{Arrow}$ applied to $S$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $S$ be a cover of $J$ and $X$. Let $T$ be a function from elements $I$ of $\operatorname{Arrow}$ applied to $S$ to covers of $J$ and $\operatorname{Y}$ applied to $I$. Then $\operatorname{bind}$ applied to $S$, $I$ and $T$ is a cover of $J$ and $X$ defined as the function that maps $T$ to $\operatorname{bind}$ applied to the arrow of $S$, the function that maps $Y$, $f$ and $\mathrm{hf}$ to $I$ applied to $\operatorname{mk}$ applied to $Y$, $f$ and $\mathrm{hf}$ and $T$.

Let $S$ be a cover of $J$ and $X$. Let $T$ be a function from elements $I$ of $\operatorname{Arrow}$ applied to $S$ to covers of $J$ and $\operatorname{Y}$ applied to $I$. Then $\operatorname{bindToBase}$ applied to $S$, $I$ and $T$ is a homomorphism of $\operatorname{bind}$ applied to $S$ and $T$ and $S$.

the index of S and P (from the name)

Let $S$ be a cover of $J$ and $X$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Then the index of $S$ and $P$ is a multicospan index of the shape of $S$ and $D$ defined as $\operatorname{mk}$ applied to the function that maps $I$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{Y}$ applied to $I$, the function that maps $I_{1}$ to the action of $P$ and $\operatorname{op}$ applied to $\operatorname{Z}$ applied to $\operatorname{r}$ applied to $I_{1}$, the function that maps $I_{2}$ to the map of $P$ and the opposite in $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2081\_}$ applied to $\operatorname{r}$ applied to $I_{2}$ and the function that maps $I_{3}$ to the map of $P$ and the opposite in $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2082\_}$ applied to $\operatorname{r}$ applied to $I_{3}$.

the multifork of S and P (from the name)

Let $S$ be a cover of $J$ and $X$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Then the multifork of $S$ and $P$ is a multifork of the index of $S$ and $P$.

the pullback of S and f (from the name)

Let $S$ be a cover of $J$ and $X$. Let $f$ be a homomorphism of $Y$ and $X$. Then the pullback of $S$ and $f$ is a cover of $J$ and $Y$ defined as the pullback of $f$ and $S$.

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

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

the pullback identity of S (from the name)

Let $S$ be a cover of $J$ and $X$. Then the pullback identity of $S$ is an isomorphism of the pullback of $S$ and the identity morphism of $X$ and $S$.

the shape of S (from the name)

Let $S$ be a cover of $J$ and $X$. Then the shape of $S$ is a shape defined as $\operatorname{mk}$ applied to $\operatorname{Arrow}$ applied to $S$, $\operatorname{Relation}$ applied to $S$, the function that maps $I$ to the first arrow of $I$ and the function that maps $I_{1}$ to the second arrow of $I_{1}$.

the multiequalizer of S and P (from the name)

Let $S$ be a cover of $J$ and $X$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Then the multiequalizer of $S$ and $P$ is a homomorphism of the action of $P$ and $\operatorname{op}$ applied to $X$ and the multiequalizer of the index of $S$ and $P$.

Let $J$ be a Grothendieck topology of $C$. Let $S$ be a sieve of $X$. Let $f$ be a homomorphism of $Y$ and $X$. Then $\operatorname{Covers}$ holds for $J$, $S$ and $f$, if the pullback of $f$ and $S$ is an element of $J$ applied to $Y$.

Let $C$ be a set. Then $\operatorname{RightOreCondition}$ holds for $C$, if for all elements $X$, $Y$ and $Z$ of $C$, for all homomorphisms $\mathrm{yx}$ of $Y$ and $X$, for all homomorphisms $\mathrm{zx}$ of $Z$ and $X$, there exists an element $W$ of $C$, such that there exists a homomorphism $\mathrm{wy}$ of $W$ and $Y$, such that there exists a homomorphism $\mathrm{wz}$ of $W$ and $Z$, such that the composition of $\mathrm{wy}$ and $\mathrm{yx}$ is equal to the composition of $\mathrm{wz}$ and $\mathrm{zx}$.

Assume that $\operatorname{RightOreCondition}$ holds for $C$. Then $\operatorname{atomic}$ applied to $\mathrm{hro}$ is a Grothendieck topology of $C$.

the copy of J and s (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $s$ be a function from elements $X_{1}$ of $C$ to elements of the power set of the set of sieves of $X_{1}$ such that $\operatorname{sieves}$ applied to $J$ is equal to $s$. Then the copy of $J$ and $X_{1}$ is a Grothendieck topology of $C$.

the dense Grothendieck topology (from the docstring)

The dense Grothendieck topology is a Grothendieck topology of $C$.

Let $C$ be a set. Then $\operatorname{discrete}$ applied to $C$ is a Grothendieck topology of $C$.

the pullback of J and f (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $f$ be a homomorphism of $Y$ and $X$. Then the pullback of $J$ and $f$ is a functor of the set of covers of $J$ and $X$ and the set of covers of $J$ and $Y$.

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

Let $J$ be a Grothendieck topology of $C$. 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 $J$ and the composition of $f$ and $g$ and the composition of the pullback of $J$ and $g$ and the pullback of $J$ and $f$.

the pullback identity of J and X (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $X$ be an element of $C$. Then the pullback identity of $J$ and $X$ is an isomorphism of the pullback of $J$ and the identity morphism of $X$ and the identity of the set of covers of $J$ and $X$.

the sieve of self and X (from the name)

Let $\mathrm{self}$ be a Grothendieck topology of $C$. Let $X$ be an element of $C$. Then the sieve of $\mathrm{self}$ and $X$ is an element of the power set of the set of sieves of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $X$.

Let $C$ be a set. Then $\operatorname{trivial}$ applied to $C$ is a Grothendieck topology of $C$.

one hypercover of J and S (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $S$ be an element of $C$. Then an one hypercover of $J$ and $S$ is an element of the function that maps $J$ and $S$ to the set of quotients of the homotopic relation of $J$ and $S$.

the cylinder of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $E$ and $F$. Then the cylinder of $f$ and $g$ is an one hypercover of $J$ and $S$.

the homotopic relation of J and S (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $S$ be an element of $C$. Then the homotopic relation of $J$ and $S$ is a homomorphism relation of the set of one hypercovers of $J$ and $S$ defined as the function that maps $x_{1}$, $x_{2}$, $f$ and $g$ to $\mathrm{Nonempty}$ applied to the set of homotopies of $f$ and $g$.

the one hypercover of J and S (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $S$ be an element of $C$. Then the one hypercover of $J$ and $S$ is a functor of the set of one hypercovers of $J$ and $S$ and the set of one hypercovers of $J$ and $S$ defined as the functor of the homotopic relation of $J$ and $S$.

homotopy of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $E$ and $F$. Then the homotopies of $f$ and $g$ are a basic type.

Let $\mathrm{self}$ be a homotopy of $f$ and $g$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$. Then $\operatorname{H}$ applied to $\mathrm{self}$ and $i$ is an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $F$, $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_}$ applied to $\operatorname{toHom}$ applied to $f$ and $i$ and $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_}$ applied to $\operatorname{toHom}$ applied to $g$ and $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

Let $\mathrm{self}$ be a homotopy of $f$ and $g$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$. Then $\operatorname{a}$ applied to $\mathrm{self}$ and $i$ is a homomorphism of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $i$ and $\operatorname{Y}$ applied to $F$ and $\operatorname{H}$ applied to $\mathrm{self}$ and $i$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $i$.

Let $f$ be a homomorphism of $E$ and $F$. Let $g$ be a homomorphism of $F$ and $E$. Let $\mathrm{hgf}$ be a homotopy of the composition of $g$ and $f$ and the identity refinement of $F$. Let $\mathrm{hE}$ be an element of $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $E$ and $G$. Then $\operatorname{isLimitMultifork}$ applied to $f$, $g$, $\mathrm{hgf}$ and $\mathrm{hE}$ is an element of $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $F$ and $G$.

Let $f$ be a homomorphism of $E$ and $F$. Let $g$ be a homomorphism of $F$ and $E$. Let $\mathrm{hfg}$ be a homotopy of the composition of $f$ and $g$ and the identity refinement of $E$. Let $\mathrm{hgf}$ be a homotopy of the composition of $g$ and $f$ and the identity refinement of $F$. Then $\operatorname{isLimitMultiforkEquiv}$ applied to $f$, $g$, $\mathrm{hfg}$ and $\mathrm{hgf}$ is an equivalence from $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $E$ and $G$ to $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $F$ and $G$.

the cylinder of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $E$ and $F$. Then the cylinder of $f$ and $g$ is an one hypercover of $S$.

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

Let $f$ and $g$ be homomorphisms of $E$ and $F$. Then the cylinder homomorphism of $f$ and $g$ is a homomorphism of the cylinder of $f$ and $g$ and $E$.

the cylinder homotopy of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $E$ and $F$. Then the cylinder homotopy of $f$ and $g$ is a homotopy of the composition of the cylinder homomorphism of $f$ and $g$ and $f$ and the composition of the cylinder homomorphism of $f$ and $g$ and $g$.

the cylinder of g and k (from the name)

Let $f$ and $g$ be homomorphisms of $E$ and $F$. Let $k$ be an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $F$, $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_}$ applied to $\operatorname{toHom}$ applied to $f$ and $i$ and $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_}$ applied to $\operatorname{toHom}$ applied to $g$ and $i$. Then the cylinder of $g$ and $k$ is an element of $C$.

Let $f$ and $g$ be homomorphisms of $E$ and $F$. Let $k$ be an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $F$, $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_}$ applied to $\operatorname{toHom}$ applied to $f$ and $i$ and $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_}$ applied to $\operatorname{toHom}$ applied to $g$ and $i$. Then $\operatorname{cylinderf}$ applied to $f$, $g$ and $k$ is a homomorphism of the cylinder of $g$ and $k$ and $S$.

Let $J$ be a Grothendieck topology of $C$. Then $\operatorname{IsGeneratedByOneHypercovers}$ holds for $J$, if the top is a generating.

one hypercover family of J (from the name)

Let $J$ be a Grothendieck topology of $C$. Then an one hypercover family of $J$ is an element of the function that maps $J$ to the set of functions from elements $X$ of $C$ and one hypercovers of $J$ and $X$ to propositions.

H is a generating (from the name)

Let $H$ be an one hypercover family of $J$. Then we can say that $H$ is a generating.

the one hypercover of S (from the name)

Let $S$ be a cover of $J$ and $X$. Then the one hypercover of $S$ is an one hypercover of $J$ and $X$.

the one hypercover of S (from the name)

Let $S$ be a cover of $J$ and $X$. Then the one hypercover of $S$ is an one hypercover of $X$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{Arrow}$ applied to $S$, the function that maps $f$ to $\operatorname{Y}$ applied to $f$ and the function that maps $f_{1}$ to $\operatorname{f}$ applied to $f_{1}$, the function that maps $x_{1}$ and $x_{2}$ to the set of relations of $x_{1}$ and $x_{2}$, the function that maps $x_{3}$, $x_{4}$ and $r$ to $\operatorname{Z}$ applied to $r$, the function that maps $x_{5}$, $x_{6}$ and $r_{1}$ to $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2081\_}$ applied to $r_{1}$, the function that maps $x_{7}$, $x_{8}$ and $r_{2}$ to $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_Cover\_\_Arrow\_\_Relation\_\_g\_u2082\_}$ applied to $r_{2}$ and the function that maps $x_{9}$, $x_{10}$ and $r_{3}$ to $\operatorname{w}$ applied to $r_{3}$.

one hypercover of J and S (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $S$ be an element of $C$. Then the one hypercovers of $J$ and $S$ are a basic type.

homomorphism of E and F (from the name)

Let $E$ and $F$ be one hypercovers of $J$ and $S$. Then a homomorphism of $E$ and $F$ is an element of the function that maps $E$ and $F$ to the set of homomorphisms of $\operatorname{toPreOneHypercover}$ applied to $E$ and $\operatorname{toPreOneHypercover}$ applied to $F$.

the intersection of E and F (from the name)

Let $E$ and $F$ be one hypercovers of $J$ and $S$. Then the intersection of $E$ and $F$ is an one hypercover of $J$ and $S$.

Let $E$ be an one hypercover of $J$ and $S$. Let $F$ be a sheaf of $J$ and $A$. Then $\operatorname{isLimitMultifork}$ applied to $E$ and $F$ is an element of $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $\operatorname{toPreOneHypercover}$ applied to $E$ and the object of $F$.

the isomorphism of f (from the name)

Let $f$ be an isomorphism of $\operatorname{toPreOneHypercover}$ applied to $E$ and $\operatorname{toPreOneHypercover}$ applied to $F$. Then the isomorphism of $f$ is an isomorphism of $E$ and $F$.

Let $E$ be an one hypercover of $S$ such that the sieve of $\operatorname{toPreZeroHypercover}$ applied to $E$ is an element of $J$ applied to $S$ and for all elements $x_{1}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$, for all elements $x_{2}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$, the sieve of $E$ is an element of $J$ applied to the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $x_{1}$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $x_{2}$. Then $\operatorname{mk'}$ applied to $E$, $h_{1}$ and $h_{2}$ is an one hypercover of $J$ and $S$.

the zero hypercover of E (from the name)

Let $E$ be an one hypercover of $J$ and $S$. Then the zero hypercover of $E$ is a zero hypercover of the induced coverage by a Grothendieck topology as a precoverage of $J$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\operatorname{toPreOneHypercover}$ applied to $E$ and $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_OneHypercover\_\_mem\_u2080\_}$ applied to $E$.

Let $J$ be a Grothendieck topology of $C$. Let $S$ be an element of $C$. Then $\operatorname{trivial}$ applied to $J$ and $S$ is an one hypercover of $J$ and $S$.

one hypercover of S (from the name)

Let $S$ be an element of $C$. Then the one hypercovers of $S$ are a basic type.

homomorphism of E and F (from the name)

Let $E$ and $F$ be one hypercovers of $S$. Then the homomorphisms of $E$ and $F$ are a basic type.

the composition of f and g (from the name)

Let $f$ be a homomorphism of $E$ and $F$. Let $g$ be a homomorphism of $F$ and $G$. Then the composition of $f$ and $g$ is a homomorphism of $E$ and $G$.

Let $\mathrm{self}$ be a homomorphism of $E$ and $F$. Let $k$ be an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $E$, $i$ and $j$. Then $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_Hom\_\_h\_u2081\_}$ applied to $\mathrm{self}$ and $k$ is a homomorphism of $\operatorname{Y}$ applied to $E$ and $k$ and $\operatorname{Y}$ applied to $F$ and $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_Hom\_\_s\_u2081\_}$ applied to $\mathrm{self}$ and $k$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $k$.

the identity refinement of E (from the docstring)

Let $E$ be an one hypercover of $S$. Then the identity refinement of $E$ is a homomorphism of $E$ and $E$.

the map multicospan of f (from the name)

Let $f$ be a homomorphism of $E$ and $F$. Then the map multicospan of $f$ is a functor of the set of walking multicospans of the multicospan shape of $E$ and the set of walking multicospans of the multicospan shape of $F$.

the map multifork of hc and d (from the name)

Let $f$ be a homomorphism of $E$ and $F$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $d$ be a multifork of the diagram of the multifork attached to a presheaf of $F$ and $P$. Then the map multifork of $\mathrm{hc}$ and $d$ is a homomorphism of $\operatorname{pt}$ applied to $d$ and $\operatorname{pt}$ applied to $c$.

Let $\mathrm{self}$ be a homomorphism of $E$ and $F$. Let $k$ be an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $E$, $i$ and $j$. Then $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_Hom\_\_s\_u2081\_}$ applied to $\mathrm{self}$ and $k$ is an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $F$, $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_}$ applied to $\operatorname{toHom}$ applied to $\mathrm{self}$ and $i$ and $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_}$ applied to $\operatorname{toHom}$ applied to $\mathrm{self}$ and $j$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $k$.

Let $f$ be a homomorphism of $E$ and $F$. Let $k$ be an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_'}$ applied to $E$. Then $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_Hom\_\_s\_u2081\_'}$ applied to $f$ and $k$ is an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_'}$ applied to $F$ defined as $\operatorname{mk}$ applied to $\ProdmkMACRoU {\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_} (\operatorname{toHom} (f), \ProdfstMACRoZ {\operatorname{fst} (k)})}{\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_} (\operatorname{toHom} (f), \ProdsndMACRoAA {\operatorname{fst} (k)})}$ and $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_Hom\_\_s\_u2081\_}$ applied to $f$ and $\operatorname{snd}$ applied to $k$.

Let $\mathrm{self}$ be an one hypercover of $S$. Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{self}$. Then an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$ is an element of the function that maps $\mathrm{self}$, $x_{1}$ and $x_{2}$ to $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

Let $E$ be an one hypercover of $S$. Then an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_'}$ applied to $E$ is an element of the function that maps $E$ to $\Sigma$ applied to the function that maps $i$ to $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $E$, $\ProdfstMACRoZ {i}$ and $\ProdsndMACRoAA {i}$.

Let $\mathrm{self}$ be an one hypercover of $S$. Let $j$ be an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$. Then $\operatorname{Y}$ applied to $\mathrm{self}$ and $j$ is an element of $C$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $j$.

Let $E$ be an one hypercover of $S$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_'}$ applied to $E$. Then $\operatorname{Y'}$ applied to $E$ and $i$ is an element of $C$ defined as $\operatorname{Y}$ applied to $E$ and $\operatorname{snd}$ applied to $i$.

the congruence index one of #1 and #2 (from the name)

Assume that $\EqtMACRoH {i}{\mathrm{i'}}$. Assume that $\EqtMACRoH {j}{\mathrm{j'}}$. Then the congruence index one of $\mathrm{hii'}$ and $\mathrm{hjj'}$ is an element of $\EquivMACRoAE {\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_} (E , i , j)}{\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_} (E , \mathrm{i'} , \mathrm{j'})}$.

the congruence index one of #3 (from the name)

Assume that $\EqtMACRoH {i}{\mathrm{i'}}$. Assume that $\EqtMACRoH {j}{\mathrm{j'}}$. Let $k$ be an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $E$, $i$ and $j$. Then the congruence index one of $k$ is an isomorphism of $\operatorname{Y}$ applied to $E$ and $\operatorname{congrIndexOneOfEq}$ applied to $\mathrm{hii'}$, $\mathrm{hjj'}$ and $k$ and $\operatorname{Y}$ applied to $E$ and $k$.

the equivalence multicospan of f (from the name)

Let $f$ be an isomorphism of $E$ and $F$. Then the equivalence multicospan of $f$ is an equivalence of the set of walking multicospans of the multicospan shape of $E$ and the set of walking multicospans of the multicospan shape of $F$.

the fork of hd and F (from the name)

Let $E$ be an one hypercover of $S$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{hd}$ be an element of $\operatorname{IsColimit}$ applied to $d$. Let $F$ be a functor of the set of opposites of $C$ and $A$. Then the fork of $\mathrm{hd}$ and $F$ is a fork of the map of $F$ and the opposite in $\operatorname{desc}$ applied to $\mathrm{hd}$ and the function that maps $x_{2}$ to the composition of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2081\_}$ applied to $E$ and $\operatorname{snd}$ applied to $x_{2}$ and the injection of $c$ and $\ProdfstMACRoZ {\operatorname{fst} (x_{2})}$ and the map of $F$ and the opposite in $\operatorname{desc}$ applied to $\mathrm{hd}$ and the function that maps $x_{3}$ to the composition of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2082\_}$ applied to $E$ and $\operatorname{snd}$ applied to $x_{3}$ and the injection of $c$ and $\ProdsndMACRoAA {\operatorname{fst} (x_{3})}$.

the intersection of E and F (from the name)

Let $E$ and $F$ be one hypercovers of $S$. Then the intersection of $E$ and $F$ is an one hypercover of $S$.

the intersection first component of E and F (from the name)

Let $E$ and $F$ be one hypercovers of $S$. Then the intersection first component of $E$ and $F$ is a homomorphism of the intersection of $E$ and $F$ and $E$.

the intersection lift of f and g (from the name)

Let $f$ be a homomorphism of $G$ and $E$. Let $g$ be a homomorphism of $G$ and $F$. Then the intersection lift of $f$ and $g$ is a homomorphism of $G$ and the intersection of $E$ and $F$.

the intersection second component of E and F (from the name)

Let $E$ and $F$ be one hypercovers of $S$. Then the intersection second component of $E$ and $F$ is a homomorphism of the intersection of $E$ and $F$ and $F$.

Let $f$ be an isomorphism of $E$ and $F$. Let $G$ be a functor of the set of opposites of $C$ and $A$. Then $\operatorname{isLimitEquivOfIso}$ applied to $f$ and $G$ is an equivalence from $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $E$ and $G$ to $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $F$ and $G$.

Let $E$ be an one hypercover of $S$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{hd}$ be an element of $\operatorname{IsColimit}$ applied to $d$. Let $F$ be a functor of the set of opposites of $C$ and $A$. Then $\operatorname{isLimitMultiforkEquivIsLimitFork}$ applied to $E$, $\mathrm{hc}$, $\mathrm{hd}$ and $F$ is an equivalence from $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $E$ and $F$ to $\operatorname{IsLimit}$ applied to the fork of $\mathrm{hd}$ and $F$.

Let $E$ be an one hypercover of $S$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{hd}$ be an element of $\operatorname{IsColimit}$ applied to $d$. Let $F$ be a functor of the set of opposites of $C$ and $A$. Then $\operatorname{isLimitSigmaOfIsColimitEquiv}$ applied to $E$, $\mathrm{hc}$, $\mathrm{hd}$ and $F$ is an equivalence from $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of the sigma of $\mathrm{hc}$ and $\mathrm{hd}$ and $F$ to $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $E$ and $F$.

the isomorphism of i5 and x3 (from the name)

Let $x_{1}$ be an element of $\EquivMACRoAE {\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_} (\operatorname{toPreZeroHypercover} (E))}{\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_} (\operatorname{toPreZeroHypercover} (F))}$. Let $x_{2}$ be a function from elements $i_{5}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ to isomorphisms of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $i_{5}$ and $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $F$ and $x_{1}$ applied to $i_{5}$. Let $x_{3}$ be a function from elements $i_{4}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and elements $j_{3}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ to elements of $\EquivMACRoAE {\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_} (E , i_{4} , j_{3})}{\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_} (F , x_{1} (i_{4}), x_{1} (j_{3}))}$. Let $x_{4}$ be a function from elements $i_{3}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and elements $j_{2}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and elements $k_{2}$ of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $E$, $i_{3}$ and $j_{2}$ to isomorphisms of $\operatorname{Y}$ applied to $E$ and $k_{2}$ and $\operatorname{Y}$ applied to $F$ and $x_{3}$ applied to $i_{3}$, $j_{2}$ and $k_{2}$. Assume that $\mathrm{autoParam}$ holds for the proposition that for all elements $i_{2}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$, the composition of the homomorphism of $x_{2}$ applied to $i_{2}$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $F$ and $x_{1}$ applied to $i_{2}$ is equal to $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $i_{2}$ and $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_isoMk\_\_\_auto\_1}$. Assume that $\mathrm{autoParam}$ holds for the proposition that for all elements $i_{1}$ and $j_{1}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$, for all elements $k_{1}$ of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $E$, $i_{1}$ and $j_{1}$, the composition of the homomorphism of $x_{4}$ applied to $i_{1}$, $j_{1}$ and $k_{1}$ and $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2081\_}$ applied to $F$ and $x_{3}$ applied to $i_{1}$, $j_{1}$ and $k_{1}$ is equal to the composition of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2081\_}$ applied to $E$ and $k_{1}$ and the homomorphism of $x_{2}$ applied to $i_{1}$ and $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_isoMk\_\_\_auto\_3}$. Assume that $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ and $j$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$, for all elements $k$ of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $E$, $i$ and $j$, the composition of the homomorphism of $x_{4}$ applied to $i$, $j$ and $k$ and $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2082\_}$ applied to $F$ and $x_{3}$ applied to $i$, $j$ and $k$ is equal to the composition of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2082\_}$ applied to $E$ and $k$ and the homomorphism of $x_{2}$ applied to $j$ and $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_isoMk\_\_\_auto\_5}$. Then the isomorphism of $x_{2}$ and $i_{4}$ is an isomorphism of $E$ and $F$.

the diagram of the multifork attached to a presheaf of E and F (from the docstring)

Let $E$ be an one hypercover of $S$. Let $F$ be a functor of the set of opposites of $C$ and $A$. Then the diagram of the multifork attached to a presheaf of $E$ and $F$ is a multicospan index of the multicospan shape of $E$ and $A$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to the action of $F$ and $\operatorname{op}$ applied to $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $i$, the function that maps $j$ to the action of $F$ and $\operatorname{op}$ applied to $\operatorname{Y}$ applied to $E$ and $\operatorname{snd}$ applied to $j$, the function that maps $j_{1}$ to the map of $F$ and the opposite in $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2081\_}$ applied to $E$ and $\operatorname{snd}$ applied to $j_{1}$ and the function that maps $j_{2}$ to the map of $F$ and the opposite in $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2082\_}$ applied to $E$ and $\operatorname{snd}$ applied to $j_{2}$.

the multicospan shape of E (from the name)

Let $E$ be an one hypercover of $S$. Then the multicospan shape of $E$ is a shape defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$, $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_'}$ applied to $E$, the function that maps $j$ to $\ProdfstMACRoZ {\operatorname{fst} (j)}$ and the function that maps $j_{1}$ to $\ProdsndMACRoAA {\operatorname{fst} (j_{1})}$.

the multifork attached to a presheaf of E and F (from the docstring)

Let $E$ be an one hypercover of $S$. Let $F$ be a functor of the set of opposites of $C$ and $A$. Then the multifork attached to a presheaf of $E$ and $F$ is a multifork of the diagram of the multifork attached to a presheaf of $E$ and $F$.

the one to zero (from the name)

The one to zero is a functor of the set of one hypercovers of $S$ and the set of zero hypercovers of $S$.

Let $\mathrm{self}$ be an one hypercover of $S$. Let $j$ be an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2081\_}$ applied to $\mathrm{self}$ and $j$ is a homomorphism of $\operatorname{Y}$ applied to $\mathrm{self}$ and $j$ and $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{self}$ and $x_{1}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $j$.

Let $\mathrm{self}$ be an one hypercover of $S$. Let $j$ be an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$. Then $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2082\_}$ applied to $\mathrm{self}$ and $j$ is a homomorphism of $\operatorname{Y}$ applied to $\mathrm{self}$ and $j$ and $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\mathrm{self}$ and $x_{2}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$ and $j$.

the sieve of x3 and x4 (from the name)

Let $E$ be an one hypercover of $S$. Let $x_{3}$ be a homomorphism of $W$ and $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $x_{1}$. Let $x_{4}$ be a homomorphism of $W$ and $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $x_{2}$. Then the sieve of $x_{3}$ and $x_{4}$ is a sieve of $W$.

the sieve of E (from the docstring)

Let $E$ be an one hypercover of $S$. Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$. Then the sieve of $E$ is a sieve of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $x_{1}$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $x_{2}$ defined as the sieve of $\operatorname{Y}$ applied to $E$ and the function that maps $j$ to the pullback of $E$ and $j$.

the sigma of hc and hd (from the name)

Let $E$ be an one hypercover of $S$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Let $\mathrm{hd}$ be an element of $\operatorname{IsColimit}$ applied to $d$. Then the sigma of $\mathrm{hc}$ and $\mathrm{hd}$ is an one hypercover of $S$.

the pullback of E and j (from the name)

Let $E$ be an one hypercover of $S$. Let $j$ be an element of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $E$, $x_{1}$ and $x_{2}$. Then the pullback of $E$ and $j$ is a homomorphism of $\operatorname{Y}$ applied to $E$ and $j$ and the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $x_{1}$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $x_{2}$ defined as the lift of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2081\_}$ applied to $E$ and $j$ and $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2082\_}$ applied to $E$ and $j$.

Let $S$ be an element of $C$. Then $\operatorname{trivial}$ applied to $S$ is an one hypercover of $S$.

Let $E$ be a zero hypercover of $X$. Let $F$ be a function from elements $i$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$ and elements $j$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$ to zero hypercovers of the pullback of $\operatorname{f}$ applied to $E$ and $i$ and $\operatorname{f}$ applied to $E$ and $j$. Then $\operatorname{refineOneHypercover}$ applied to $E$, $i$, $j$ and $F$ is an one hypercover of $X$.

the one hypercover of E (from the name)

Let $E$ be a zero hypercover of $S$. Then the one hypercover of $E$ is an one hypercover of $S$.

the one hypercover of E (from the name)

Let $E$ be a zero hypercover of $J$ and $S$. Then the one hypercover of $E$ is an one hypercover of $\operatorname{toGrothendieck}$ applied to $J$ and $S$.

relation of i and j (from the name)

Let $E$ be a zero hypercover of $S$. Let $i$ and $j$ be elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$. Then the relations of $i$ and $j$ are a basic type.

the first projection of self (from the docstring)

Let $\mathrm{self}$ be a relation of $i$ and $j$. Then the first projection of $\mathrm{self}$ is a homomorphism of the object of $\mathrm{self}$ and $\operatorname{X}$ applied to $E$ and $i$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the object of self (from the docstring)

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

the second projection of self (from the docstring)

Let $\mathrm{self}$ be a relation of $i$ and $j$. Then the second projection of $\mathrm{self}$ is a homomorphism of the object of $\mathrm{self}$ and $\operatorname{X}$ applied to $E$ and $j$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $E$ be a zero hypercover of $S$. Then $\operatorname{fromSaturateOfHasPullbacks}$ applied to $E$ is a homomorphism of $\operatorname{saturate}$ applied to $E$ and the one hypercover of $E$.

Let $E$ be a zero hypercover of $S$. Then $\operatorname{fromSaturateToSaturateHomotopy}$ applied to $E$ is a homotopy of the composition of $\operatorname{fromSaturateOfHasPullbacks}$ applied to $E$ and $\operatorname{toSaturateOfHasPullbacks}$ applied to $E$ and the identity refinement of $\operatorname{saturate}$ applied to $E$.

Let $E$ be a zero hypercover of $S$. Let $F$ be a functor of the set of opposites of $C$ and $A$. Then $\operatorname{isLimitSaturateEquivOfHasPullbacks}$ applied to $E$ and $F$ is an equivalence from $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $\operatorname{saturate}$ applied to $E$ and $F$ to $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of the one hypercover of $E$ and $F$.

Let $E$ be a zero hypercover of $S$. Then $\operatorname{saturate}$ applied to $E$ is an one hypercover of $S$ defined as $\operatorname{mk}$ applied to $E$, the set of elements of $\operatorname{Relation}$, the function that maps $x_{1}$, $x_{2}$ and $r$ to the object of $r$, the function that maps $x_{3}$, $x_{4}$ and $r_{1}$ to the first projection of $r_{1}$, the function that maps $x_{5}$, $x_{6}$ and $r_{2}$ to the second projection of $r_{2}$ and the function that maps $x_{7}$, $x_{8}$ and $r_{3}$ to $\operatorname{w}$ applied to $r_{3}$.

Let $E$ be a zero hypercover of $S$. Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then $\operatorname{sectionsSaturateEquiv}$ applied to $E$ and $F$ is an equivalence from the set of sections of the diagram of the multifork attached to a presheaf of $\operatorname{saturate}$ applied to $E$ and $F$ to $\SubtypeSet {x_{1}}{\operatorname{Compatible} (F , \operatorname{f} (E), x_{1})}$.

the one hypercover homotopy of E (from the name)

Let $E$ be a zero hypercover of $S$. Then the one hypercover homotopy of $E$ is a homotopy of the identity refinement of the one hypercover of $E$ and the identity refinement of the one hypercover of $E$.

Let $E$ be a zero hypercover of $S$. Then $\operatorname{toSaturateOfHasPullbacks}$ applied to $E$ is a homomorphism of the one hypercover of $E$ and $\operatorname{saturate}$ applied to $E$.

Let $E$ be an one hypercover of $X$. Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then we can say that $\operatorname{IsStronglySeparatedFor}$ holds for $E$ and $F$.

Let $E$ be an one hypercover of $X$. Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then we can say that $\operatorname{IsStronglySheafFor}$ holds for $E$ and $F$.

Assume that $\operatorname{IsStronglySheafFor}$ holds for $E$ and $F$. Let $x_{1}$ be a function from elements $i_{1}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ to elements of the action of $F$ and $\operatorname{op}$ applied to $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $i_{1}$ such that for all elements $i$ and $j$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$, for all elements $k$ of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $E$, $i$ and $j$, $\operatorname{hom}$ applied to the map of $F$ and the opposite in $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2081\_}$ applied to $E$ and $k$ and $x_{1}$ applied to $i$ is equal to $\operatorname{hom}$ applied to the map of $F$ and the opposite in $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2082\_}$ applied to $E$ and $k$ and $x_{1}$ applied to $j$. Then $\operatorname{amalgamate}$ applied to $h$, $i_{1}$, $x_{1}$ and $\mathrm{hc}$ is an element of the action of $F$ and $\operatorname{op}$ applied to $X$.

Assume that $\operatorname{IsStronglySheafFor}$ holds for $E$ and $F$. Then $\operatorname{isLimitMultifork}$ applied to $h$ is an element of $\operatorname{IsLimit}$ applied to the multifork attached to a presheaf of $E$ and $F$.

the section equivalence of E and F (from the name)

Let $E$ be a zero hypercover of $S$. Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the section equivalence of $E$ and $F$ is an equivalence from the set of sections of the diagram of the multifork attached to a presheaf of the one hypercover of $E$ and $F$ to $\SubtypeSet {x_{1}}{\operatorname{Compatible} (F , \operatorname{f} (E), x_{1})}$.

the glue morphism of E and f (from the name)

Let $E$ be an one hypercover of $J$ and $S$. Let $f$ be a function from elements $i_{1}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\operatorname{toPreOneHypercover}$ applied to $E$ to homomorphisms of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\operatorname{toPreOneHypercover}$ applied to $E$ and $i_{1}$ and $T$ such that for all elements $i$ and $j$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $\operatorname{toPreOneHypercover}$ applied to $E$, for all elements $k$ of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_I\_u2081\_}$ applied to $\operatorname{toPreOneHypercover}$ applied to $E$, $i$ and $j$, the composition of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2081\_}$ applied to $\operatorname{toPreOneHypercover}$ applied to $E$ and $k$ and $f$ applied to $i$ is equal to the composition of $\mathrm{CategoryTheory\_\_PreOneHypercover\_\_p\_u2082\_}$ applied to $\operatorname{toPreOneHypercover}$ applied to $E$ and $k$ and $f$ applied to $j$. Then the glue morphism of $E$ and $i_{1}$ is a homomorphism of $S$ and $T$.

the glue morphism of x1 and f (from the name)

Let $x_{1}$ be a zero hypercover of $J$ and $S$. Let $f$ be a function from elements $i_{1}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ to homomorphisms of $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $i_{1}$ and $T$ such that for all elements $i$ and $j$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$, the composition of the first projection of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $i$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $j$ and $f$ applied to $i$ is equal to the composition of the second projection of the pullback of $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $i$ and $\operatorname{f}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $x_{1}$ and $j$ and $f$ applied to $j$. Then the glue morphism of $x_{1}$ and $i_{1}$ is a homomorphism of $S$ and $T$ defined as the function that maps $\mathrm{hf}$ to the glue morphism of the one hypercover of $x_{1}$ and $i_{1}$.

zero hypercover of S (from the name)

Let $S$ be an element of $C$. Then the zero hypercovers of $S$ are a basic type.

E has pullbacks (from the name)

Let $E$ be a zero hypercover of $S$. Then $E$ has pullbacks, if for all elements $x_{1}$ and $x_{2}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$, $\operatorname{HasPullback}$ holds for $\operatorname{f}$ applied to $E$ and $x_{1}$ and $\operatorname{f}$ applied to $E$ and $x_{2}$.

homomorphism of E and F (from the name)

Let $E$ and $F$ be zero hypercovers of $S$. Then the homomorphisms of $E$ and $F$ are a basic type.

the composition of f and g (from the name)

Let $f$ be a homomorphism of $E$ and $F$. Let $g$ be a homomorphism of $F$ and $G$. Then the composition of $f$ and $g$ is a homomorphism of $E$ and $G$.

Let $\mathrm{self}$ be a homomorphism of $E$ and $F$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$. Then $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_h\_u2080\_}$ applied to $\mathrm{self}$ and $i$ is a homomorphism of $\operatorname{X}$ applied to $E$ and $i$ and $\operatorname{X}$ applied to $F$ and $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_}$ applied to $\mathrm{self}$ and $i$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $i$.

the identity refinement of E (from the docstring)

Let $E$ be a zero hypercover of $S$. Then the identity refinement of $E$ is a homomorphism of $E$ and $E$.

Let $\mathrm{self}$ be a homomorphism of $E$ and $F$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$. Then $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_Hom\_\_s\_u2080\_}$ applied to $\mathrm{self}$ and $i$ is an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

Let $\mathrm{self}$ be a zero hypercover of $S$. Then an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a zero hypercover of $S$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\mathrm{self}$. Then $\operatorname{X}$ applied to $\mathrm{self}$ and $i$ is an element of $C$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $i$.

the sum of E and f (from the name)

Let $E$ be a zero hypercover of $S$. Let $f$ be a homomorphism of $T$ and $S$. Then the sum of $E$ and $f$ is a zero hypercover of $S$ defined as the reindexing of the sum of $E$ and the singleton of $f$ and the option equivalence sum unit of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$.

Let $E$ be a zero hypercover of $T$. Let $F$ be a function from elements $i$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$ to zero hypercovers of $\operatorname{X}$ applied to $E$ and $i$. Then $\operatorname{bind}$ applied to $E$, $i$ and $F$ is a zero hypercover of $T$ defined as the function that maps $F$ to $\operatorname{mk}$ applied to $\Sigma$ applied to the function that maps $i$ to $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $i$ applied to $i$, the function that maps $\mathrm{ij}$ to $\operatorname{X}$ applied to $i$ applied to $\operatorname{fst}$ applied to $\mathrm{ij}$ and $\operatorname{snd}$ applied to $\mathrm{ij}$, the function that maps $\mathrm{ij1}$ to the composition of $\operatorname{f}$ applied to $i$ applied to $\operatorname{fst}$ applied to $\mathrm{ij1}$ and $\operatorname{snd}$ applied to $\mathrm{ij1}$ and $\operatorname{f}$ applied to $E$ and $\operatorname{fst}$ applied to $\mathrm{ij1}$ and $F$.

Let $S$ be an element of $C$. Then $\operatorname{empty}$ applied to $S$ is a zero hypercover of $S$ defined as $\operatorname{mk}$ applied to $\mathrm{PEmpty}$, $\operatorname{elim}$ and the function that maps $i$ to $\operatorname{elim}$ applied to $i$.

the equivalence of e (from the name)

Let $e$ be an isomorphism of $E$ and $F$. Then the equivalence of $e$ is an element of $\EquivMACRoAE {\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_} (E)}{\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_} (F)}$.

Let $\mathrm{self}$ be a zero hypercover of $S$. Let $i$ be an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\mathrm{self}$. Then $\operatorname{f}$ applied to $\mathrm{self}$ and $i$ is a homomorphism of $\operatorname{X}$ applied to $\mathrm{self}$ and $i$ and $S$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $i$.

Let $E$ be a zero hypercover of $S$. Then $\operatorname{fromShrink}$ applied to $E$ is a homomorphism of the shrink of $E$ and $E$.

the intersection of E and F (from the name)

Let $E$ and $F$ be zero hypercovers of $T$. Then the intersection of $E$ and $F$ is a zero hypercover of $T$ defined as the reindexing of $\operatorname{bind}$ applied to $E$ and the function that maps $i$ to the pullback of $\operatorname{f}$ applied to $E$ and $i$ and $F$ and the inverse of the sigma equivalence product of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$ and $\operatorname{proj0}$ applied to $F$.

the intersection first component of E and F (from the name)

Let $E$ and $F$ be zero hypercovers of $S$. Then the intersection first component of $E$ and $F$ is a homomorphism of the intersection of $E$ and $F$ and $E$.

the intersection lift of f and g (from the name)

Let $f$ be a homomorphism of $G$ and $E$. Let $g$ be a homomorphism of $G$ and $F$. Then the intersection lift of $f$ and $g$ is a homomorphism of $G$ and the intersection of $E$ and $F$.

the intersection second component of E and F (from the name)

Let $E$ and $F$ be zero hypercovers of $S$. Then the intersection second component of $E$ and $F$ is a homomorphism of the intersection of $E$ and $F$ and $F$.

the isomorphism of x1 and x2 (from the name)

Let $x_{1}$ be an element of $\EquivMACRoAE {\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_} (E)}{\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_} (F)}$. Let $x_{2}$ be a function from elements $i_{1}$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$ to isomorphisms of $\operatorname{X}$ applied to $E$ and $i_{1}$ and $\operatorname{X}$ applied to $F$ and $x_{1}$ applied to $i_{1}$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $i$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$, the composition of the homomorphism of $x_{2}$ applied to $i$ and $\operatorname{f}$ applied to $F$ and $x_{1}$ applied to $i$ is equal to $\operatorname{f}$ applied to $E$ and $i$ and $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_isoMk\_\_\_auto\_1}$. Then the isomorphism of $x_{1}$ and $i_{1}$ is an isomorphism of $E$ and $F$.

the map of F and E (from the name)

Let $F$ be a functor of $C$ and $D$. Let $E$ be a zero hypercover of $S$. Then the map of $F$ and $E$ is a zero hypercover of the action of $F$ and $S$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$, the function that maps $i$ to the action of $F$ and $\operatorname{X}$ applied to $E$ and $i$ and the function that maps $i_{1}$ to the map of $F$ and $\operatorname{f}$ applied to $E$ and $i_{1}$.

the presieve of E (from the docstring)

Let $E$ be a zero hypercover of $S$. Then the presieve of $E$ is a presieve of $S$ defined as the presieve of $\operatorname{X}$ applied to $E$ and $\operatorname{f}$ applied to $E$.

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

Let $E$ be a zero hypercover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cover of $f$ and $g$ is a zero hypercover of the pullback of $f$ and $g$.

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

Let $E$ be a zero hypercover of $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cover of $f$ and $g$ is an isomorphism of the pullback cover of $f$ and $g$ and the pullback of the first projection of the pullback of $f$ and $g$ and $E$.

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

Let $E$ be a zero hypercover of $Y$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cover of $f$ and $g$ is a zero hypercover of the pullback of $f$ and $g$.

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

Let $E$ be a zero hypercover of $Y$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cover of $f$ and $g$ is an isomorphism of the pullback cover of $f$ and $g$ and the pullback of the second projection of the pullback of $f$ and $g$ and $E$.

the pullback isomorphism of f and E (from the name)

Let $f$ be a homomorphism of $S$ and $T$. Let $E$ be a zero hypercover of $T$. Then the pullback isomorphism of $f$ and $E$ is an isomorphism of the pullback of $f$ and $E$ and the pullback of $f$ and $E$.

the pullback of f and E (from the name)

Let $f$ be a homomorphism of $S$ and $T$. Let $E$ be a zero hypercover of $T$. Then the pullback of $f$ and $E$ is a zero hypercover of $S$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$, the function that maps $i$ to the pullback of $f$ and $\operatorname{f}$ applied to $E$ and $i$ and the function that maps $x_{1}$ to the first projection of the pullback of $f$ and $\operatorname{f}$ applied to $E$ and $x_{1}$.

the pullback of f and E (from the name)

Let $f$ be a homomorphism of $S$ and $T$. Let $E$ be a zero hypercover of $T$. Then the pullback of $f$ and $E$ is a zero hypercover of $S$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$, the function that maps $i$ to the pullback of $\operatorname{f}$ applied to $E$ and $i$ and $f$ and the function that maps $x_{1}$ to the second projection of the pullback of $\operatorname{f}$ applied to $E$ and $x_{1}$ and $f$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $E$ be a zero hypercover of $X$. Then $\operatorname{pushforward}$ applied to $f$ and $E$ is a zero hypercover of $Y$ defined as $\operatorname{mk}$ applied to $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$, $\operatorname{X}$ applied to $E$ and the function that maps $i$ to the composition of $\operatorname{f}$ applied to $E$ and $i$ and $f$.

Let $f$ be a homomorphism of $X$ and $Y$. Let $E$ be a zero hypercover of $X$. Then $\operatorname{pushforwardIsoBind}$ applied to $f$ and $E$ is an isomorphism of $\operatorname{pushforward}$ applied to $f$ and $E$ and $\operatorname{bind}$ applied to the singleton of $f$ and the function that maps $x_{1}$ to $E$.

the reindexing of E and e (from the name)

Let $E$ be a zero hypercover of $T$. Let $e$ be an element of $\EquivMACRoAE {x_{1}}{\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_} (E)}$. Then the reindexing of $E$ and $e$ is a zero hypercover of $T$ defined as $\operatorname{restrictIndex}$ applied to $E$ and $\operatorname{coe}$ applied to $e$.

Let $E$ be a zero hypercover of $T$. Let $f$ be a function from elements of $x_{1}$ to elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$. Then $\operatorname{restrictIndex}$ applied to $E$ and $f$ is a zero hypercover of $T$ defined as $\operatorname{mk}$ applied to $x_{1}$, $\operatorname{comp}$ applied to $\operatorname{X}$ applied to $E$ and $f$ and the function that maps $i$ to $\operatorname{f}$ applied to $E$ and $f$ applied to $i$.

Let $E$ be a zero hypercover of $S$. Let $f$ be a function from elements of $x_{1}$ to elements of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $E$. Then $\operatorname{restrictIndexHom}$ applied to $E$ and $f$ is a homomorphism of $\operatorname{restrictIndex}$ applied to $E$ and $f$ and $E$.

the shrink of E (from the name)

Let $E$ be a zero hypercover of $S$. Then the shrink of $E$ is a zero hypercover of $S$ defined as the zero hypercover of the presieve of $E$.

the sieve of E (from the docstring)

Let $E$ be a zero hypercover of $S$. Then the sieve of $E$ is a sieve of $S$ defined as the sieve of $\operatorname{X}$ applied to $E$ and $\operatorname{f}$ applied to $E$.

the sigma of E and hc (from the name)

Let $E$ be a zero hypercover of $S$. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the sigma of $E$ and $\mathrm{hc}$ is a zero hypercover of $S$ defined as $\operatorname{mk}$ applied to $\mathrm{PUnit}$, the function that maps $x_{1}$ to $\operatorname{pt}$ applied to $c$ and the function that maps $x_{2}$ to $\operatorname{desc}$ applied to $\mathrm{hc}$ and $\operatorname{f}$ applied to $E$.

the singleton of f (from the name)

Let $f$ be a homomorphism of $S$ and $T$. Then the singleton of $f$ is a zero hypercover of $T$ defined as $\operatorname{mk}$ applied to $\mathrm{PUnit}$, the function that maps $x_{1}$ to $S$ and the function that maps $x_{2}$ to $f$.

the sum of E and F (from the name)

Let $E$ and $F$ be zero hypercovers of $X$. Then the sum of $E$ and $F$ is a zero hypercover of $X$.

the left inclusion into the disjoint union of E and F (from the docstring)

Let $E$ and $F$ be zero hypercovers of $S$. Then the left inclusion into the disjoint union of $E$ and $F$ is a homomorphism of $E$ and the sum of $E$ and $F$.

the right inclusion into the disjoint union of E and F (from the docstring)

Let $E$ and $F$ be zero hypercovers of $S$. Then the right inclusion into the disjoint union of $E$ and $F$ is a homomorphism of $F$ and the sum of $E$ and $F$.

the sum lift of f and g (from the name)

Let $f$ be a homomorphism of $E$ and $G$. Let $g$ be a homomorphism of $F$ and $G$. Then the sum lift of $f$ and $g$ is a homomorphism of the sum of $E$ and $F$ and $G$.

the shrink of E (from the name)

Let $E$ be a zero hypercover of $S$. Then the shrink of $E$ is a homomorphism of $E$ and the shrink of $E$.

Let $J$ be a precoverage of $C$. Then we can say that $\operatorname{RespectsIso}$ holds for $J$.

J is small (from the name)

Let $J$ be a precoverage of $C$. Then we can say that $J$ is small.

zero hypercover of J and S (from the name)

Let $J$ be a precoverage of $C$. Let $S$ be an element of $C$. Then the zero hypercovers of $J$ and $S$ are a basic type.

homomorphism of E and F (from the name)

Let $J$ be a precoverage of $C$. Let $E$ and $F$ be zero hypercovers of $J$ and $S$. Then a homomorphism of $E$ and $F$ is an element of the function that maps $J$, $E$ and $F$ to the set of homomorphisms of $\operatorname{toPreZeroHypercover}$ applied to $E$ and $\operatorname{toPreZeroHypercover}$ applied to $F$.

E is small (from the name)

Let $E$ be a zero hypercover of $J$ and $S$. Then we can say that $E$ is small.

index of E (from the name)

Let $E$ be a zero hypercover of $J$ and $S$. Then an index of $E$ is an element of the function that maps $E$ to $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Precoverage\_\_ZeroHypercover\_\_Small\_\_exists\_restrictIndex\_mem}$ applied to $E$.

the index restriction function of E and x1 (from the docstring)

Let $E$ be a zero hypercover of $J$ and $S$. Let $x_{1}$ be an index of $E$. Then the index restriction function of $E$ and $x_{1}$ is an element of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$.

the sum of E and f (from the name)

Let $E$ be a zero hypercover of $J$ and $S$. Let $f$ be a homomorphism of $T$ and $S$ such that the maximum of the presieve of $\operatorname{toPreZeroHypercover}$ applied to $E$ and the singleton presieve of $f$ is an element of the covering of $J$ and $S$. Then the sum of $E$ and $f$ is a zero hypercover of $J$ and $S$.

Let $E$ be a zero hypercover of $J$ and $T$. Let $F$ be a function from elements $i$ of $\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ to zero hypercovers of $J$ and $\operatorname{X}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $i$. Then $\operatorname{bind}$ applied to $E$, $i$ and $F$ is a zero hypercover of $J$ and $T$.

the intersection of E and F (from the name)

Let $E$ and $F$ be zero hypercovers of $J$ and $T$. Then the intersection of $E$ and $F$ is a zero hypercover of $J$ and $T$.

the isomorphism of e (from the name)

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

the map of F and E (from the name)

Let $F$ be a functor of $C$ and $D$. Let $E$ be a zero hypercover of $J$ and $S$. Assume that $J$ is less than or equal to the preimage of $F$ and $K$. Then the map of $F$ and $E$ is a zero hypercover of $K$ and the action of $F$ and $S$.

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

Let $E$ be a zero hypercover of $J$ and $X$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cover of $f$ and $g$ is a zero hypercover of $J$ and the pullback of $f$ and $g$.

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

Let $E$ be a zero hypercover of $J$ and $Y$. Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cover of $f$ and $g$ is a zero hypercover of $J$ and the pullback of $f$ and $g$.

the pullback of f and E (from the name)

Let $f$ be a homomorphism of $S$ and $T$. Let $E$ be a zero hypercover of $J$ and $T$. Then the pullback of $f$ and $E$ is a zero hypercover of $J$ and $S$.

the pullback of f and E (from the name)

Let $f$ be a homomorphism of $S$ and $T$. Let $E$ be a zero hypercover of $J$ and $T$. Then the pullback of $f$ and $E$ is a zero hypercover of $J$ and $S$.

Let $f$ be a homomorphism of $X$ and $Y$ such that the singleton presieve of $f$ is an element of the covering of $J$ and $Y$. Let $E$ be a zero hypercover of $J$ and $X$. Then $\operatorname{pushforward}$ applied to $f$, $\mathrm{hf}$ and $E$ is a zero hypercover of $J$ and $Y$.

the reindexing of E and e (from the name)

Let $E$ be a zero hypercover of $J$ and $T$. Let $e$ be an element of $\EquivMACRoAE {x_{1}}{\mathrm{CategoryTheory\_\_PreZeroHypercover\_\_I\_u2080\_} (\operatorname{toPreZeroHypercover} (E))}$. Then the reindexing of $E$ and $e$ is a zero hypercover of $J$ and $T$.

Let $E$ be a zero hypercover of $J$ and $S$. Then $\operatorname{restrictIndexOfSmall}$ applied to $E$ is a zero hypercover of $J$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{restrictIndex}$ applied to $\operatorname{toPreZeroHypercover}$ applied to $E$ and $\operatorname{restrictFun}$ applied to $E$ and $\mathrm{CategoryTheory\_\_Precoverage\_\_ZeroHypercover\_\_Small\_\_mem\_u2080\_}$ applied to $E$.

the singleton of f and hf (from the name)

Let $f$ be a homomorphism of $S$ and $T$ such that the singleton presieve of $f$ is an element of the covering of $J$ and $T$. Then the singleton of $f$ and $\mathrm{hf}$ is a zero hypercover of $J$ and $T$.

the sum of E and F (from the name)

Let $E$ and $F$ be zero hypercovers of $J$ and $S$. Then the sum of $E$ and $F$ is a zero hypercover of $J$ and $S$.

the weaken of E and h (from the name)

Let $E$ be a zero hypercover of $K$ and $X$. Assume that $K \leq L$. Then the weaken of $E$ and $h$ is a zero hypercover of $L$ and $X$.

the zero hypercover of R (from the name)

Let $R$ be a presieve of $S$. Then the zero hypercover of $R$ is a zero hypercover of $S$ defined as $\operatorname{mk}$ applied to the set of elements of $\operatorname{uncurry}$ applied to $R$, the function that maps $i$ to $\operatorname{fst}$ applied to $i$ and the function that maps $i_{1}$ to $\operatorname{snd}$ applied to $i_{1}$.

zero hypercover family of C (from the name)

Let $C$ be a set. Then the zero hypercover families of $C$ are a basic type.

the precoverage of P (from the name)

Let $P$ be a zero hypercover family of $C$. Then the precoverage of $P$ is a precoverage of $C$ defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ to $\operatorname{ofPred}$ applied to the function that maps $R$ to $\operatorname{presieve}$ applied to $P$ and $R$.

Let $P$ be a zero hypercover family of $C$. Let $x_{1}$ be a presieve of $X$. Then we can say that $\operatorname{presieve}$ holds for $P$ and $x_{1}$.

the property of self (from the name)

Let $\mathrm{self}$ be a zero hypercover family of $C$. Then the property of $\mathrm{self}$ is an object property of the set of zero hypercovers of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the equivalence zero hypercover family of C (from the name)

Let $C$ be a set. Then the equivalence zero hypercover family of $C$ is an equivalence from the set of precoverages of $C$ to the set of zero hypercover families of $C$.

the zero hypercover family of K (from the name)

Let $K$ be a precoverage of $C$. Then the zero hypercover family of $K$ is a zero hypercover family of $C$.

the induced topology of F and K (from the name)

Let $F$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Then the induced topology of $F$ and $K$ is a Grothendieck topology of $C$ defined as $\operatorname{finestTopology}$ applied to the range of the function that maps $G$ to the composition of the opposite of $F$ and the object of $G$.

the restricted topology of F and K (from the name)

Let $F$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Then the restricted topology of $F$ and $K$ is a Grothendieck topology of $C$ defined as $\operatorname{toGrothendieck}$ applied to the preimage of $F$ and the induced coverage by a Grothendieck topology as a precoverage of $K$.

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $x_{1}$ be a function from elements $i_{1}$ of $I$ to homomorphisms of $X$ applied to $i_{1}$ and $B$. Let $x_{2}$ be a function from elements $i$ of $I$ to elements of the action of $P$ and $\operatorname{op}$ applied to $X$ applied to $i$. Then $\operatorname{Compatible}$ holds for $P$, $i_{1}$, $x_{1}$, $i$ and $x_{2}$, if for all elements $i$ and $j$ of $I$, for all elements $Z$ of $C$, for all homomorphisms $\mathrm{gi}$ of $Z$ and $X$ applied to $i$, for all homomorphisms $\mathrm{gj}$ of $Z$ and $X$ applied to $j$, if the composition of $\mathrm{gi}$ and $i_{1}$ applied to $i$ is equal to the composition of $\mathrm{gj}$ and $i_{1}$ applied to $j$, then $\operatorname{hom}$ applied to the map of $P$ and the opposite in $\mathrm{gi}$ and $x_{1}$ applied to $i$ is equal to $\operatorname{hom}$ applied to the map of $P$ and the opposite in $\mathrm{gj}$ and $x_{1}$ applied to $j$.

the family of hx (from the name)

Assume that $\operatorname{Compatible}$ holds for $P$, $x_{1}$ and $x_{2}$. Then the family of $\mathrm{hx}$ is a family of element of $P$ and the presieve of $X$ and $x_{1}$ defined as $\operatorname{choose}$ applied to $\mathrm{CategoryTheory\_\_Presieve\_\_Arrows\_\_Compatible\_\_exists\_familyOfElements}$ applied to $\mathrm{hx}$.

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $x_{1}$ be a function from elements $i_{1}$ of $I$ to homomorphisms of $X$ applied to $i_{1}$ and $B$. Let $x_{2}$ be a function from elements $i$ of $I$ to elements of the action of $P$ and $\operatorname{op}$ applied to $X$ applied to $i$. Then $\operatorname{PullbackCompatible}$ holds for $P$, $i_{1}$, $x_{1}$, $i$ and $x_{2}$, if for all elements $i$ and $j$ of $I$, $\operatorname{hom}$ applied to the map of $P$ and the opposite in the first projection of the pullback of $i_{1}$ applied to $i$ and $i_{1}$ applied to $j$ and $x_{1}$ applied to $i$ is equal to $\operatorname{hom}$ applied to the map of $P$ and the opposite in the second projection of the pullback of $i_{1}$ applied to $i$ and $i_{1}$ applied to $j$ and $x_{1}$ applied to $j$.

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $x_{1}$ be a function from elements $i$ of $I$ to homomorphisms of $X$ applied to $i$ and $B$. Let $s$ be an element of the action of $P$ and $\operatorname{op}$ applied to $B$. Then $\operatorname{toCompatible}$ applied to $P$, $i$, $x_{1}$ and $s$ is an element of $\SubtypeSet {x_{2}}{\operatorname{Compatible} (P , x_{1} , x_{2})}$ defined as the function that maps $i$ to $\operatorname{hom}$ applied to the map of $P$ and the opposite in $i$ applied to $s$ and $x_{1}$.

family of element of P and R (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $R$ be a presieve of $X$. Then a family of element of $P$ and $R$ is an element of the function that maps $P$ and $R$ to the set of functions from elements $Y$ of $C$ and homomorphisms $f$ of $Y$ and $X$ and elements of $\mathrm{Proof}$ applied to $R$ applied to $Y$ and $f$ to elements of the action of $P$ and $\operatorname{op}$ applied to $Y$.

x1 is compatible (from the name)

Let $x_{1}$ be a family of element of $P$ and $R$. Then $x_{1}$ is compatible, if for all elements $x_{2}$, $x_{3}$ and $Z$ of $C$, for all homomorphisms $x_{4}$ of $Z$ and $x_{2}$, for all homomorphisms $x_{5}$ of $Z$ and $x_{3}$, for all homomorphisms $x_{6}$ of $x_{2}$ and $X$, for all homomorphisms $x_{7}$ of $x_{3}$ and $X$, for all elements $h$ of $\mathrm{Proof}$ applied to $R$ applied to $x_{2}$ and $x_{6}$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $R$ applied to $x_{3}$ and $x_{7}$, if the composition of $x_{4}$ and $x_{6}$ is equal to the composition of $x_{5}$ and $x_{7}$, then $\operatorname{hom}$ applied to the map of $P$ and the opposite in $x_{4}$ and $x_{1}$ applied to $x_{2}$, $x_{6}$ and $h$ is equal to $\operatorname{hom}$ applied to the map of $P$ and the opposite in $x_{5}$ and $x_{1}$ applied to $x_{3}$, $x_{7}$ and $h_{1}$.

Let $x_{1}$ be a family of element of $P$ and $R$. Let $t$ be an element of the action of $P$ and $\operatorname{op}$ applied to $X$. Then $\operatorname{IsAmalgamation}$ holds for $x_{1}$ and $t$, if for all elements $Y$ of $C$, for all homomorphisms $f$ of $Y$ and $X$, for all elements $h$ of $\mathrm{Proof}$ applied to $R$ applied to $Y$ and $f$, $\operatorname{hom}$ applied to the map of $P$ and the opposite in $f$ and $t$ is equal to $x_{1}$ applied to $Y$, $f$ and $h$.

Let $x_{1}$ be a family of element of $P$ and $R$. Then $\operatorname{PullbackCompatible}$ holds for $x_{1}$, if for all elements $x_{2}$ and $x_{3}$ of $C$, for all homomorphisms $x_{4}$ of $x_{2}$ and $X$, for all homomorphisms $x_{5}$ of $x_{3}$ and $X$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $R$ applied to $x_{2}$ and $x_{4}$, for all elements $h_{2}$ of $\mathrm{Proof}$ applied to $R$ applied to $x_{3}$ and $x_{5}$, $\operatorname{hom}$ applied to the map of $P$ and the opposite in the first projection of the pullback of $x_{4}$ and $x_{5}$ and $x_{1}$ applied to $x_{2}$, $x_{4}$ and $h_{1}$ is equal to $\operatorname{hom}$ applied to the map of $P$ and the opposite in the second projection of the pullback of $x_{4}$ and $x_{5}$ and $x_{1}$ applied to $x_{3}$, $x_{5}$ and $h_{2}$.

Let $x_{1}$ be a family of element of $P$ and the arrow of $S$. Then $\operatorname{SieveCompatible}$ holds for $x_{1}$, if for all elements $Y$ and $Z$ of $C$, for all homomorphisms $f$ of $Y$ and $X$, for all homomorphisms $g$ of $Z$ and $Y$, for all elements $\mathrm{hf}$ of $\mathrm{Proof}$ applied to the arrow of $S$, $x_{1}$ applied to $Z$, the composition of $g$ and $f$ and $\mathrm{CategoryTheory\_\_Sieve\_\_downward\_closed}$ applied to $S$, $\mathrm{hf}$ and $g$ is equal to $\operatorname{hom}$ applied to the map of $P$ and the opposite in $g$ and $x_{1}$ applied to $Y$, $f$ and $\mathrm{hf}$.

the functor pullback of F and x2 (from the name)

Let $F$ be a functor of $D$ and $C$. Let $x_{2}$ be a family of element of $P$ and $T$. Then the functor pullback of $F$ and $x_{2}$ is a family of element of the composition of the opposite of $F$ and $P$ and the functor pullback of $F$ and $T$ defined as the function that maps $x_{3}$, $f$ and $\mathrm{hf}$ to $x_{2}$ applied to the action of $F$ and the opposite of $\operatorname{op}$ applied to $x_{3}$, the map of $F$ and $f$ and $\mathrm{hf}$.

Let $F$ be a functor of $D$ and $C$. Let $x_{2}$ be a family of element of the composition of the opposite of $F$ and $P$ and $T$. Then there is a family of element of $P$ and $\operatorname{functorPushforward}$ applied to $F$ and $T$.

the map of p and x1 (from the name)

Let $p$ be a family of element of $P$ and $R$. Let $x_{1}$ be a homomorphism of $P$ and $Q$. Then the map of $p$ and $x_{1}$ is a family of element of $Q$ and $R$ defined as the function that maps $x_{2}$, $f$ and $\mathrm{hf}$ to $\operatorname{hom}$ applied to the component of $x_{1}$ and $\operatorname{op}$ applied to $x_{2}$ and $p$ applied to $x_{2}$, $f$ and $\mathrm{hf}$.

the pullback of f and x1 (from the name)

Let $f$ be a homomorphism of $Y$ and $X$. Let $x_{1}$ be a family of element of $P$ and the arrow of $S$. Then the pullback of $f$ and $x_{1}$ is a family of element of $P$ and the arrow of the pullback of $f$ and $S$ defined as the function that maps $x_{2}$, $g$ and $\mathrm{hg}$ to $x_{1}$ applied to $x_{2}$, the composition of $g$ and $f$ and $\mathrm{hg}$.

Assume that $x_{1} \leq x_{2}$. Let $x_{3}$ be a family of element of $P$ and $x_{2}$. Then there is a family of element of $P$ and $x_{1}$. Proof. Let $h$ be arbitrary. Let $x_{3}$ be arbitrary. Let $x_{4}$ be arbitrary. Let $f$ be arbitrary. Let $\mathrm{hf}$ be arbitrary. By x4. By f. By x4. By f. By hf. By h. By x3.

Let $x_{1}$ be a family of element of $P$ and $R$. Then there is a family of element of $P$ and the arrow of $\operatorname{generate}$ applied to $R$.

the singleton equivalence of P and f (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $f$ be a homomorphism of $X$ and $Y$. Then the singleton equivalence of $P$ and $f$ is an equivalence from the set of families of element of $P$ and the singleton presieve of $f$ to the action of $P$ and $\operatorname{op}$ applied to $X$.

P is separated (from the docstring)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $R$ be a presieve of $X$. Then $P$ is separated, if for all families of element $x_{1}$ of $P$ and $R$, for all elements $x_{2}$ and $x_{3}$ of the action of $P$ and $\operatorname{op}$ applied to $X$, if $\operatorname{IsAmalgamation}$ holds for $x_{1}$ and $x_{2}$, then if $\operatorname{IsAmalgamation}$ holds for $x_{1}$ and $x_{3}$, then $\EqtMACRoH {x_{2}}{x_{3}}$.

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $R$ be a presieve of $X$. Then $\operatorname{IsSheafFor}$ holds for $P$ and $R$, if for all families of element $x_{1}$ of $P$ and $R$, if $x_{1}$ is compatible, then $\mathrm{ExistsUnique}$ holds for the function that maps $t$ to $\operatorname{IsAmalgamation}$ applied to $x_{1}$ and $t$.

Assume that $\operatorname{IsSheafFor}$ holds for $P$ and $R$. Let $x_{1}$ be a compatible family of element of $P$ and $R$. Then $\operatorname{amalgamate}$ applied to $t$, $x_{1}$ and $\mathrm{hx}$ is an element of the action of $P$ and $\operatorname{op}$ applied to $X$.

Assume that $\operatorname{IsSheafFor}$ holds for $P$ and the arrow of $S$. Let $f$ be a homomorphism of the functor of $S$ and $P$. Then $\operatorname{extend}$ applied to $h$ and $f$ is a homomorphism of the action of the Yoneda and $X$ and $P$.

P is a Yoneda sheaf condition with respect to S (from the name)

Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $S$ be a sieve of $X$. Then $P$ is a Yoneda sheaf condition with respect to $S$, if for all homomorphisms $f$ of the functor of $S$ and $P$, $\mathrm{ExistsUnique}$ holds for the function that maps $g$ to the proposition that the composition of the functor inclusion of $S$ and $g$ is equal to $f$.

$\operatorname{compatibleEquivGenerateSieveCompatible}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{\operatorname{Compatible} (x_{1})})}{(\SubtypeSet {x_{2}}{\operatorname{Compatible} (x_{2})})}$.

the shrink functor homomorphism equivalence (from the name)

The shrink functor homomorphism equivalence is an element of $\EquivMACRoAE {\operatorname{Hom} (\operatorname{toFunctor} (\operatorname{shrinkFunctor} (S)), F)}{(\SubtypeSet {x_{1}}{\operatorname{Compatible} (x_{1})})}$.

the jointly surjective precoverage (from the name)

the plus plus functor isomorphism sheafification of J and D (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Then the plus plus functor isomorphism sheafification of $J$ and $D$ is an isomorphism of the sheafification of $J$ and $D$ and the sheafification of $J$ and $D$ defined as the right isomorphism whisker of the plus plus sheaf isomorphism presheaf to sheaf of $J$ and $D$ and the sheaf to presheaf of $J$ and $D$.

the plus plus isomorphism sheafification of J and P (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Let $P$ be a functor of the set of opposites of $C$ and $D$. Then the plus plus isomorphism sheafification of $J$ and $P$ is an isomorphism of the sheafification of $J$ and $P$ and the sheafification of $J$ and $P$ defined as the map isomorphism of the sheaf to presheaf of $J$ and $D$ and the application of the plus plus sheaf isomorphism presheaf to sheaf of $J$ and $D$ and $P$.

the plus plus sheaf isomorphism presheaf to sheaf of J and D (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Then the plus plus sheaf isomorphism presheaf to sheaf of $J$ and $D$ is an isomorphism of the plus plus sheaf of $J$ and $D$ and the presheaf to sheaf of $J$ and $D$ defined as $\operatorname{leftAdjointUniq}$ applied to the plus plus adjunction of $J$ and $D$ and the sheafification adjunction of $J$ and $D$.

Let $E$ be a cocone of the composition of $F$ and the sheaf to presheaf of $J$ and $D$. Let $\mathrm{hE}$ be an element of $\operatorname{IsColimit}$ applied to $E$. Then $\operatorname{isColimitSheafifyCocone}$ applied to $E$ and $\mathrm{hE}$ is an element of $\operatorname{IsColimit}$ applied to the sheafification cocone of $E$ defined as $\operatorname{symm}$ applied to the precomposition homomorphism equivalence of the left isomorphism whisker of $F$ and the inverse of $\operatorname{asIso}$ applied to the counit of the sheafification adjunction of $J$ and $D$ and the map cocone of the presheaf to sheaf of $J$ and $D$ and $E$ and $\operatorname{isColimitOfPreserves}$ applied to the presheaf to sheaf of $J$ and $D$ and $\mathrm{hE}$.

Let $F$ be a functor of $K$ and the set of sheaves of $J$ and $D$. Let $E$ be a cone of the composition of $F$ and the sheaf to presheaf of $J$ and $D$. Let $\mathrm{hE}$ be an element of $\operatorname{IsLimit}$ applied to $E$. Let $X$ be an element of $C$. Let $W$ be a cover of $J$ and $X$. Then $\operatorname{isLimitMultiforkOfIsLimit}$ applied to $F$, $E$, $\mathrm{hE}$, $X$ and $W$ is an element of $\operatorname{IsLimit}$ applied to the multifork of $W$ and $\operatorname{pt}$ applied to $E$.

the sheafification cocone of E (from the name)

Let $E$ be a cocone of the composition of $F$ and the sheaf to presheaf of $J$ and $D$. Then the sheafification cocone of $E$ is a cocone of $F$ defined as the action of the precomposition of the homomorphism of the left isomorphism whisker of $F$ and the inverse of $\operatorname{asIso}$ applied to the counit of the sheafification adjunction of $J$ and $D$ and the map cocone of the presheaf to sheaf of $J$ and $D$ and $E$.

Let $J$ be a Grothendieck topology of $C$. Then we can say that $\operatorname{IsLocalSite}$ holds for $J$.

the coconstant sheaf of J and A (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the coconstant sheaf of $J$ and $A$ is a functor of $A$ and the set of sheaves of $J$ and $A$ defined as the skyscraper sheaf functor of the point of $J$.

the coconstant sheaf natural isomorphism identity of J and A (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the coconstant sheaf natural isomorphism identity of $J$ and $A$ is an isomorphism of the composition of the coconstant sheaf of $J$ and $A$ and $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ and the identity of $A$.

the adjoint triple of J and A (from the docstring)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the adjoint triple of $J$ and $A$ is a triple of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ and the coconstant sheaf of $J$ and $A$ defined as $\operatorname{mk}$ applied to the constant sheaf functor of $J$ and $A$ and the coconstant sheaf adjoint of $J$ and $A$.

the fully faithful coconstant sheaf of J and A (from the name)

the fully faithful constant sheaf of J and A (from the name)

the point of J (from the name)

Let $J$ be a Grothendieck topology of $C$. Then the point of $J$ is a point of $J$.

the fibre of J and P (from the docstring)

Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then the fibre of $J$ and $P$ is an isomorphism of the action of the presheaf fiber of the point of $J$ and $P$ and the action of $P$ and $\operatorname{op}$ applied to $\operatorname{terminal}$ applied to $C$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the action of the action of the left whiskering of the set of opposites of $C$ and $A$ and the opposite of the projection of the fiber of the point of $J$ and $P$ and the colimit of the opposite of the set of elements of the action of the shrink Coyoneda and $\operatorname{op}$ applied to $\operatorname{terminal}$ applied to $C$ and $\operatorname{isInitialOfCorepresentableBy}$ applied to $\operatorname{shrinkCoyonedaCorepresentableBy}$ applied to $\operatorname{op}$ applied to $\operatorname{terminal}$ applied to $C$ and the action of the action of the left whiskering of the set of opposites of $C$ and $A$ and the opposite of the projection of the fiber of the point of $J$ and $P$.

the point presheaf fiber natural isomorphism of J and A (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the point presheaf fiber natural isomorphism of $J$ and $A$ is an isomorphism of the presheaf fiber of the point of $J$ and the action of the evaluation of the set of opposites of $C$ and $A$ and $\operatorname{op}$ applied to $\operatorname{terminal}$ applied to $C$ defined as the natural isomorphism of $\operatorname{pointPresheafFiberIso}$ applied to $J$ and the function that maps $x_{2}$, $x_{3}$ and $F$ to $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_IsLocalSite\_\_pointPresheafFiberIso\_naturality}$ applied to $J$ and $F$.

the point sheaf fiber isomorphism of J and A (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the point sheaf fiber isomorphism of $J$ and $A$ is an isomorphism of the sheaf fiber of the point of $J$ and $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ defined as the composition of the left isomorphism whisker of the sheaf to presheaf of $J$ and $A$ and the point presheaf fiber natural isomorphism of $J$ and $A$ and the inverse of the natural isomorphism sheaf section of $J$ and $\operatorname{terminalIsTerminal}$.

the coconstant sheaf adjoint of J and A (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then the coconstant sheaf adjoint of $J$ and $A$ is an adjunction of $\mathrm{CategoryTheory\_\_Sheaf\_\_\_u393\_}$ applied to $J$ and $A$ and the coconstant sheaf of $J$ and $A$ defined as the adjunction of the skyscraper sheaf adjunction of the point of $J$ and the point sheaf fiber isomorphism of $J$ and $A$.

Let $J$ be a Grothendieck topology of $C$. Then there is a morphism property of the set of functors of the set of opposites of $C$ and $A$. Proof. Let $J$ be arbitrary. By J. By CategoryTheory__Presheaf__IsSheaf. By CategoryTheory__ObjectProperty__isLocal.

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Then we can say that $\operatorname{WEqualsLocallyBijective}$ holds for $J$ and $A$.

Let $G$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Then we can say that $\operatorname{IsLocallyFaithful}$ holds for $G$ and $K$.

Let $G$ be a functor of $C$ and $D$. Let $K$ be a Grothendieck topology of $D$. Then we can say that $\operatorname{IsLocallyFull}$ holds for $G$ and $K$.

the image sieve of G and f (from the name)

Let $G$ be a functor of $C$ and $D$. Let $f$ be a homomorphism of the action of $G$ and $U$ and the action of $G$ and $V$. Then the image sieve of $G$ and $f$ is a sieve of $U$.

the equalizer of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be homomorphisms of $U$ and $V$. Then the equalizer of $x_{1}$ and $x_{2}$ is a sieve of $U$.

x6 is locally injective with respect to J (from the name)

the equalizer sieve of x4 and y (from the name)

Let $x_{4}$ and $y$ be types of the action of $F$ and $X$. Then the equalizer sieve of $x_{4}$ and $y$ is a sieve of the opposite of $X$.

x6 is locally injective (from the name)

f is locally surjective to J (from the name)

the image sieve of f and s (from the name)

Let $f$ be a homomorphism of $F$ and $G$. Let $s$ be a type of the action of $G$ and $\operatorname{op}$ applied to $U$. Then the image sieve of $f$ and $s$ is a sieve of $U$.

the local preimage of s and g (from the name)

Let $f$ be a homomorphism of $F$ and $G$. Let $s$ be a type of the action of $G$ and $U$. Let $g$ be a homomorphism of $V$ and the opposite of $U$. Assume that $\operatorname{arrows}$ holds for the image sieve of $f$ and $s$. Then the local preimage of $s$ and $g$ is a type of the action of $F$ and $\operatorname{op}$ applied to $V$ defined as $\operatorname{choose}$ applied to $\mathrm{hg}$.

the sheafification isomorphism image presheaf of J and F (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $F$ be a functor of the set of opposites of $C$ and the set of sets. Then the sheafification isomorphism image presheaf of $J$ and $F$ is an isomorphism of the sheafification of $J$ and $F$ and the subfunctor as a functor of the sheafification of $J$ and the range of the sheafification of $J$ and $F$.

the local preimage of x1 and #2 (from the name)

Let $x_{1}$ be a homomorphism of $R$ and $\mathrm{R'}$. Let $\mathrm{r'}$ be an element of the action of $\mathrm{R'}$ and $X$. Then the local preimage of $x_{1}$ and $\mathrm{r'}$ is a family of element of $R$ and the arrow of the image sieve of $x_{1}$ and $\mathrm{r'}$ defined as the function that maps $x_{2}$, $f$ and $\mathrm{hf}$ to the local preimage of $\mathrm{r'}$ and $f$.

x6 is locally surjective (from the name)

Let $J$ be a Grothendieck topology of $C$. Then the elements of $\operatorname{MayerVietorisSquare}$ applied to $J$ are a basic type.

Let $S$ be an element of $\operatorname{MayerVietorisSquare}$ applied to $J$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then $\operatorname{SheafCondition}$ holds for $S$ and $P$, if the map of the opposite of $\operatorname{toSquare}$ applied to $S$ and $P$ is a pullback.

the glue of u and v (from the name)

Assume that $\operatorname{SheafCondition}$ holds for $S$ and $P$. Let $u$ be an element of the action of $P$ and $\operatorname{op}$ applied to $\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_}$ applied to $\operatorname{toSquare}$ applied to $S$. Let $v$ be an element of the action of $P$ and $\operatorname{op}$ applied to $\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_}$ applied to $\operatorname{toSquare}$ applied to $S$ such that $\operatorname{hom}$ applied to the map of $P$ and the opposite in $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2082\_}$ applied to $\operatorname{toSquare}$ applied to $S$ and $u$ is equal to $\operatorname{hom}$ applied to the map of $P$ and the opposite in $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2083\_}$ applied to $\operatorname{toSquare}$ applied to $S$ and $v$. Then the glue of $u$ and $v$ is an element of the action of $P$ and $\operatorname{op}$ applied to $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $\operatorname{toSquare}$ applied to $S$ defined as $\operatorname{symm}$ applied to the equivalence pullback object of $\operatorname{isLimit}$ applied to $h_{1}$ and $\ProdmkMACRoU {u}{v}$.

Let $\mathrm{sq}$ be a square of $C$ such that for all sheaves $F$ of $J$ and the set of sets, the map of the opposite of $\mathrm{sq}$ and the object of $F$ is a pullback. Then $\operatorname{mk'}$ applied to $\mathrm{sq}$ and $H$ is an element of $\operatorname{MayerVietorisSquare}$ applied to $J$.

Let $\mathrm{sq}$ be a square of $C$ such that $\mathrm{sq}$ is a pullback and the sieve of $\mathrm{CategoryTheory\_\_Square\_\_f\_u2082\_\_u2084\_}$ applied to $\mathrm{sq}$ and $\mathrm{CategoryTheory\_\_Square\_\_f\_u2083\_\_u2084\_}$ applied to $\mathrm{sq}$ is an element of $J$ applied to $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $\mathrm{sq}$. Then $\mathrm{CategoryTheory\_\_GrothendieckTopology\_\_MayerVietorisSquare\_\_mk\_of\_isPullback}$ applied to $\mathrm{sq}$, $h_{3}$ and $h_{4}$ is an element of $\operatorname{MayerVietorisSquare}$ applied to $J$.

the short complex of S (from the name)

Let $S$ be an element of $\operatorname{MayerVietorisSquare}$ applied to $J$. Then the short complex of $S$ is a short complex of the set of sheaves of $J$ and the set of additive commutative group categories.

the pullback object of P and x1 (from the name)

Let $S$ be an element of $\operatorname{MayerVietorisSquare}$ applied to $J$. Let $P$ be a functor of the set of opposites of $C$ and the set of sets. Let $x_{1}$ be an element of the action of $P$ and $\operatorname{op}$ applied to $\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_}$ applied to $\operatorname{toSquare}$ applied to $S$. Then the pullback object of $P$ and $x_{1}$ is a pullback object of the map of $P$ and the opposite in $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2082\_}$ applied to $\operatorname{toSquare}$ applied to $S$ and the map of $P$ and the opposite in $\mathrm{CategoryTheory\_\_Square\_\_f\_u2081\_\_u2083\_}$ applied to $\operatorname{toSquare}$ applied to $S$ defined as the pullback object of the pullback cone attached to a commutative square of the map of the opposite of $\operatorname{toSquare}$ applied to $S$ and $P$ and $x_{1}$.

the functor enriched homomorphism Coyoneda object equivalence of G and X (from the name)

Let $M$ be an element of $A$. Let $F$ and $G$ be functors of the set of opposites of $C$ and $A$. Let $X$ be an element of $C$. Then the functor enriched homomorphism Coyoneda object equivalence of $G$ and $X$ is an equivalence from the action of the composition of the functor enriched homomorphism of $F$ and $G$ and the action of the Coyoneda and $\operatorname{op}$ applied to $M$ and $\operatorname{op}$ applied to $X$ to the action of the presheaf homomorphism of the tensor object of $F$ and the action of the constant of the set of opposites of $C$ and $M$ and $G$ and $\operatorname{op}$ applied to $X$.

the coverage of P (from the name)

Let $P$ be a morphism property of $C$. Then the coverage of $P$ is a coverage of $C$.

the Grothendieck topology of P (from the name)

Let $P$ be a morphism property of $C$. Then the Grothendieck topology of $P$ is a Grothendieck topology of $C$ defined as $\operatorname{toGrothendieck}$ applied to the coverage of $P$.

the precoverage of P (from the name)

Let $P$ be a morphism property of $C$. Then the precoverage of $P$ is a precoverage of $C$ defined as $\operatorname{mk}$ applied to the function that maps $X$ to $\operatorname{ofPred}$ applied to the function that maps $S$ to the proposition that for all elements $Y$ of $C$, for all homomorphisms $f$ of $Y$ and $X$, if $S$ holds for $Y$ and $f$, then $P$ holds for $Y$, $X$ and $f$.

the pretopology of P (from the name)

Let $P$ be a morphism property of $C$. Then the pretopology of $P$ is a pretopology of $C$ defined as the pretopology of $C$ and the precoverage of $P$.

the morphism property of K (from the name)

Let $K$ be a precoverage of $C$. Then the morphism property of $K$ is a morphism property of $C$ defined as the function that maps $x_{1}$, $Y$ and $f$ to the proposition that there exists a presieve $R$ of $Y$, such that $R$ is an element of the covering of $K$ and $Y$ and $R$ holds for $x_{1}$ and $f$.

Let $G$ be a functor of the set of opposites of $C$ and the set of group categories. Let $U$ be a function from elements of $I$ to elements of $C$. Then an element of $\operatorname{H1}$ applied to $G$ and $U$ is an element of the function that maps $G$ and $U$ to $\mathrm{Quot}$ applied to $\operatorname{IsCohomologous}$.

one cochain of G and U (from the name)

Let $G$ be a functor of the set of opposites of $C$ and the set of group categories. Let $U$ be a function from elements of $I$ to elements of $C$. Then the one cochains of $G$ and $U$ are a basic type.

Let $\mathrm{self}$ be an one cochain of $G$ and $U$. Let $i$ and $j$ be elements of $I$. Let $a$ be a homomorphism of $T$ and $U$ applied to $i$. Let $b$ be a homomorphism of $T$ and $U$ applied to $j$. Then $\operatorname{ev}$ applied to $\mathrm{self}$, $i$, $j$, $a$ and $b$ is a carrier of the action of $G$ and $\operatorname{op}$ applied to $T$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $i$, $j$, $a$ and $b$.

one cocycle of G and U (from the name)

Let $G$ be a functor of the set of opposites of $C$ and the set of group categories. Let $U$ be a function from elements of $I$ to elements of $C$. Then the one cocycles of $G$ and $U$ are a basic type.

Let $x_{1}$ and $x_{2}$ be one cocycles of $G$ and $U$. Then $\operatorname{IsCohomologous}$ holds for $x_{1}$ and $x_{2}$, if there exists a zero cochain $x_{3}$ of $G$ and $U$, such that $\operatorname{OneCohomologyRelation}$ holds for $\operatorname{toOneCochain}$ applied to $x_{1}$, $\operatorname{toOneCochain}$ applied to $x_{2}$ and $x_{3}$.

the cohomology class of x1 (from the docstring)

Let $x_{1}$ be an one cocycle of $G$ and $U$. Then the cohomology class of $x_{1}$ is an element of $\operatorname{H1}$ applied to $G$ and $U$ defined as $\operatorname{mk}$ applied to $\operatorname{IsCohomologous}$ and $x_{1}$.

Let $x_{1}$ and $x_{2}$ be one cochains of $G$ and $U$. Let $x_{3}$ be a zero cochain of $G$ and $U$. Then $\operatorname{OneCohomologyRelation}$ holds for $x_{1}$, $x_{2}$ and $x_{3}$, if for all elements $i$ and $j$ of $I$, for all elements $T$ of $C$, for all homomorphisms $a$ of $T$ and $U$ applied to $i$, for all homomorphisms $b$ of $T$ and $U$ applied to $j$, the product of $\operatorname{hom}$ applied to the map of $G$ and the opposite in $a$ and $x_{3}$ applied to $i$ and $\operatorname{ev}$ applied to $x_{1}$, $i$, $j$, $a$ and $b$ is equal to the product of $\operatorname{ev}$ applied to $x_{2}$, $i$, $j$, $a$ and $b$ and $\operatorname{hom}$ applied to the map of $G$ and the opposite in $b$ and $x_{3}$ applied to $j$.

zero cochain of G and U (from the name)

Let $G$ be a functor of the set of opposites of $C$ and the set of group categories. Let $U$ be a function from elements of $I$ to elements of $C$. Then a zero cochain of $G$ and $U$ is an element of the function that maps $G$ and $U$ to the set of functions from elements $i$ of $I$ to carriers of the action of $G$ and $\operatorname{op}$ applied to $U$ applied to $i$.

Let $J$ be a Grothendieck topology of $C$. Let $X$ be an element of $C$. Then $\operatorname{over}$ applied to $J$ and $X$ is a Grothendieck topology of $\operatorname{Over}$ applied to $X$.

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{overMapPullback}$ applied to $J$, $A$ and $f$ is a functor of the set of sheaves of $\operatorname{over}$ applied to $J$ and $Y$ and $A$ and the set of sheaves of $\operatorname{over}$ applied to $J$ and $X$ and $A$ defined as $\operatorname{sheafPushforwardContinuous}$ applied to the map of $f$, $A$, $\operatorname{over}$ applied to $J$ and $X$ and $\operatorname{over}$ applied to $J$ and $Y$.

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{overMapPullbackComp}$ applied to $J$, $A$, $f$ and $g$ is an isomorphism of the composition of $\operatorname{overMapPullback}$ applied to $J$, $A$ and $g$ and $\operatorname{overMapPullback}$ applied to $J$, $A$ and $f$ and $\operatorname{overMapPullback}$ applied to $J$, $A$ and the composition of $f$ and $g$ defined as the sheaf pushforward continuous composition of $\operatorname{over}$ applied to $J$ and $Y$ and $\operatorname{over}$ applied to $J$ and $Z$.

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Assume that $\EqtMACRoH {f}{g}$. Then $\operatorname{overMapPullbackCongr}$ applied to $J$, $A$ and $h$ is an isomorphism of $\operatorname{overMapPullback}$ applied to $J$, $A$ and $f$ and $\operatorname{overMapPullback}$ applied to $J$, $A$ and $g$ defined as the sheaf pushforward continuous isomorphism of $\operatorname{over}$ applied to $J$ and $X$ and $\operatorname{over}$ applied to $J$ and $Y$.

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Let $X$ be an element of $C$. Then $\operatorname{overMapPullbackId}$ applied to $J$, $A$ and $X$ is an isomorphism of $\operatorname{overMapPullback}$ applied to $J$, $A$ and the identity morphism of $X$ and the identity of the set of sheaves of $\operatorname{over}$ applied to $J$ and $X$ and $A$ defined as the sheaf pushforward continuous identity of the map identity of $X$ and $\operatorname{over}$ applied to $J$ and $X$.

Let $J$ be a Grothendieck topology of $C$. Let $A$ be a set. Let $X$ be an element of $C$. Then $\operatorname{overPullback}$ applied to $J$, $A$ and $X$ is a functor of the set of sheaves of $J$ and $A$ and the set of sheaves of $\operatorname{over}$ applied to $J$ and $X$ and $A$ defined as $\operatorname{sheafPushforwardContinuous}$ applied to $\operatorname{forget}$ applied to $X$, $A$, $\operatorname{over}$ applied to $J$ and $X$ and $J$.

Let $X$ be an element of $C$. Let $J$ be a precoverage of $C$. Then $\operatorname{over}$ applied to $X$ and $J$ is a precoverage of $\operatorname{Over}$ applied to $X$ defined as the preimage of $\operatorname{forget}$ applied to $X$ and $J$.

the equivalence of Y (from the docstring)

Let $Y$ be an element of $\operatorname{Over}$ applied to $X$. Then the equivalence of $Y$ is an order isomorphism of the set of presieves of $Y$ and the set of presieves of the left of $Y$.

Let $F$ be a sheaf of $J$ and $A$. Let $X$ be an element of $C$. Then $\operatorname{over}$ applied to $F$ and $X$ is a sheaf of $\operatorname{over}$ applied to $J$ and $X$ and $A$ defined as the action of $\operatorname{overPullback}$ applied to $J$, $A$ and $X$ and $F$.

Let $F$ be a sheaf of $J$ and $A$. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{pushforwardOverMapIso}$ applied to $F$ and $f$ is an isomorphism of the action of $\operatorname{sheafPushforwardContinuous}$ applied to the map of $f$, $A$, $\operatorname{over}$ applied to $J$ and $X$ and $\operatorname{over}$ applied to $J$ and $Y$ and $\operatorname{over}$ applied to $F$ and $Y$ and $\operatorname{over}$ applied to $F$ and $X$.

Let $F$ be a sheaf of $J$ and $A$. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{toPushforwardOverPullback}$ applied to $F$ and $f$ is a homomorphism of $\operatorname{over}$ applied to $F$ and $Y$ and the action of $\operatorname{sheafPushforwardContinuous}$ applied to the pullback of $f$, $A$, $\operatorname{over}$ applied to $J$ and $Y$ and $\operatorname{over}$ applied to $J$ and $X$ and $\operatorname{over}$ applied to $F$ and $X$.

the equivalence of Y (from the docstring)

Let $Y$ be an element of $\operatorname{Over}$ applied to $X$. Then the equivalence of $Y$ is an order isomorphism of the set of sieves of $Y$ and the set of sieves of the left of $Y$.

the diagram of P and X (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Let $X$ be an element of $C$. Then the diagram of $P$ and $X$ is a functor of the set of opposites of the set of covers of $J$ and $X$ and $D$.

the diagram functor of J and X (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Let $X$ be an element of $C$. Then the diagram functor of $J$ and $X$ is a functor of the set of functors of the set of opposites of $C$ and $D$ and the set of functors of the set of opposites of the set of covers of $J$ and $X$ and $D$.

the diagram natural transformation of x2 and X (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $x_{2}$ be a homomorphism of $P$ and $Q$. Let $X$ be an element of $C$. Then the diagram natural transformation of $x_{2}$ and $X$ is a homomorphism of the diagram of $P$ and $X$ and the diagram of $Q$ and $X$.

the diagram pullback of P and f (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Let $f$ be a homomorphism of $X$ and $Y$. Then the diagram pullback of $P$ and $f$ is a homomorphism of the diagram of $P$ and $Y$ and the composition of the opposite of the pullback of $J$ and $f$ and the diagram of $P$ and $X$.

the isomorphism to plus of J and P (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $D$ such that $\operatorname{IsSheaf}$ holds for $J$ and $P$. Then the isomorphism to plus of $J$ and $P$ is an isomorphism of $P$ and the plus object of $J$ and $P$ defined as $\operatorname{asIso}$ applied to the plus of $J$ and $P$.

the plus functor of J and D (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Then the plus functor of $J$ and $D$ is a functor of the set of functors of the set of opposites of $C$ and $D$ and the set of functors of the set of opposites of $C$ and $D$.

the plus lift of J and x2 (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $x_{2}$ be a homomorphism of $P$ and $Q$. Assume that $\operatorname{IsSheaf}$ holds for $J$ and $Q$. Then the plus lift of $J$ and $x_{2}$ is a homomorphism of the plus object of $J$ and $P$ and $Q$ defined as the composition of $\operatorname{plusMap}$ applied to $J$ and $x_{2}$ and the inverse of the isomorphism to plus of $J$ and $Q$.

the plus object of J and P (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Then the plus object of $J$ and $P$ is a functor of the set of opposites of $C$ and $D$.

the plus of J and P (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $P$ be a functor of the set of opposites of $C$ and $D$. Then the plus of $J$ and $P$ is a homomorphism of $P$ and the plus object of $J$ and $P$.

the plus natural transformation of J and D (from the name)

Let $J$ be a Grothendieck topology of $C$. Let $D$ be a set. Then the plus natural transformation of $J$ and $D$ is a homomorphism of the identity of the set of functors of the set of opposites of $C$ and $D$ and the plus functor of $J$ and $D$.

point of J (from the name)

Let $J$ be a Grothendieck topology of $C$. Then the points of $J$ are a basic type.

the fiber of self (from the name)

Let $\mathrm{self}$ be a point of $J$. Then the fiber of $\mathrm{self}$ is a functor of $C$ and the set of sets defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the cocone of x1 and P (from the docstring)

Let $x_{1}$ be a point of $J$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then the cocone of $x_{1}$ and $P$ is an element of $\operatorname{IsColimit}$ applied to the presheaf fiber cocone of $x_{1}$ and $P$ defined as $\operatorname{isColimit}$ applied to the composition of the opposite of the projection of the fiber of $x_{1}$ and $P$.

Let $x_{1}$ be a point of $J$. Let $T$ be an element of $C$. Let $\mathrm{hT}$ be an element of $\operatorname{IsTerminal}$ applied to $T$. Then $\operatorname{isTerminalFiberObj}$ applied to $x_{1}$, $T$ and $\mathrm{hT}$ is an element of $\operatorname{IsTerminal}$ applied to the action of the fiber of $x_{1}$ and $T$ defined as $\operatorname{isTerminalObj}$ applied to the fiber of $x_{1}$, $T$ and $\mathrm{hT}$.

the presheaf fiber of x1 (from the name)

Let $x_{1}$ be a point of $J$. Then the presheaf fiber of $x_{1}$ is a functor of the set of functors of the set of opposites of $C$ and $A$ and $A$ defined as the composition of the action of the left whiskering of the set of opposites of $C$ and $A$ and the opposite of the projection of the fiber of $x_{1}$ and the colimit.

the presheaf fiber cocone of x1 and P (from the name)

Let $x_{1}$ be a point of $J$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then the presheaf fiber cocone of $x_{1}$ and $P$ is a cocone of the composition of the opposite of the projection of the fiber of $x_{1}$ and $P$.

the presheaf fiber composition isomorphism of x1 and F (from the name)

Let $x_{1}$ be a point of $J$. Let $F$ be a functor of $A$ and $B$. Then the presheaf fiber composition isomorphism of $x_{1}$ and $F$ is an isomorphism of the composition of the action of the right whiskering of $A$ and $B$ and $F$ and the presheaf fiber of $x_{1}$ and the composition of the presheaf fiber of $x_{1}$ and $F$ defined as the left isomorphism whisker of the action of the left whiskering of the set of opposites of $C$ and $A$ and the opposite of the projection of the fiber of $x_{1}$ and the inverse of $\operatorname{preservesColimitNatIso}$ applied to $F$.

Let $x_{1}$ be a point of $J$. Let $x_{3}$ be a function from elements $X_{2}$ of $C$ and elements of the action of the fiber of $x_{1}$ and $X_{2}$ to homomorphisms of the action of $P$ and $\operatorname{op}$ applied to $X_{2}$ and $T$ such that $\mathrm{autoParam}$ holds for the proposition that for all elements $X$ and $Y$ of $C$, for all homomorphisms $f$ of $X$ and $Y$, for all elements $x_{4}$ of the action of the fiber of $x_{1}$ and $X$, the composition of the map of $P$ and the opposite in $f$ and $x_{3}$ applied to $X$ and $x_{4}$ is equal to $x_{3}$ applied to $Y$ and $\operatorname{hom}$ applied to the map of the fiber of $x_{1}$ and $f$ and $x_{4}$ and $\mathrm{\_private\_\_Mathlib\_\_CategoryTheory\_\_Sites\_\_Point\_\_Basic\_\_0\_\_\_auto\_48}$. Then $\operatorname{presheafFiberDesc}$ applied to $x_{1}$, $X_{2}$, $x_{3}$ and $h_{1}$ is a homomorphism of the action of the presheaf fiber of $x_{1}$ and $P$ and $T$.

the sheaf fiber of x1 (from the name)

Let $x_{1}$ be a point of $J$. Then the sheaf fiber of $x_{1}$ is a functor of the set of sheaves of $J$ and $A$ and $A$ defined as the composition of the sheaf to presheaf of $J$ and $A$ and the presheaf fiber of $x_{1}$.

the sheaf fiber composition isomorphism of x1 and F (from the name)

Let $x_{1}$ be a point of $J$. Let $F$ be a functor of $A$ and $B$. Then the sheaf fiber composition isomorphism of $x_{1}$ and $F$ is an isomorphism of the composition of $\operatorname{sheafCompose}$ applied to $J$ and $F$ and the sheaf fiber of $x_{1}$ and the composition of the sheaf fiber of $x_{1}$ and $F$ defined as the composition of the left isomorphism whisker of the sheaf to presheaf of $J$ and $A$ and the presheaf fiber composition isomorphism of $x_{1}$ and $F$ and the inverse of the associator of the presheaf fiber of $x_{1}$ and $F$.

the sheaf to presheaf composition presheaf fiber isomorphism of x1 (from the name)

Let $x_{1}$ be a point of $J$. Then the sheaf to presheaf composition presheaf fiber isomorphism of $x_{1}$ is an isomorphism of the composition of the sheaf to presheaf of $J$ and $A$ and the presheaf fiber of $x_{1}$ and the sheaf fiber of $x_{1}$ defined as the identity of the composition of the sheaf to presheaf of $J$ and $A$ and the presheaf fiber of $x_{1}$.

the isomorphism of x1 (from the docstring)

Let $x_{1}$ be a point of $J$. Then the isomorphism of $x_{1}$ is an isomorphism of the composition of the Yoneda embedding and the presheaf fiber of $x_{1}$ and the fiber of $x_{1}$ defined as the shrink Yoneda composition whiskering left object projection composition colimit isomorphism of the fiber of $x_{1}$.

the presheaf fiber of x3 and P (from the name)

Let $x_{1}$ be a point of $J$. Let $X$ be an element of $C$. Let $x_{3}$ be an element of the action of the fiber of $x_{1}$ and $X$. Let $P$ be a functor of the set of opposites of $C$ and $A$. Then the presheaf fiber of $x_{3}$ and $P$ is a homomorphism of the action of $P$ and $\operatorname{op}$ applied to $X$ and the action of the presheaf fiber of $x_{1}$ and $P$ defined as the inclusion of the composition of the opposite of the projection of the fiber of $x_{1}$ and $P$ and $\operatorname{op}$ applied to the element of $X$ and $x_{3}$.

the presheaf fiber natural transformation of X and x3 (from the name)

Let $x_{1}$ be a point of $J$. Let $X$ be an element of $C$. Let $x_{3}$ be an element of the action of the fiber of $x_{1}$ and $X$. Then the presheaf fiber natural transformation of $X$ and $x_{3}$ is a homomorphism of the action of the evaluation of the set of opposites of $C$ and $A$ and $\operatorname{op}$ applied to $X$ and the presheaf fiber of $x_{1}$.

homomorphism of x1 and x2 (from the name)

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

the homomorphism of self (from the name)

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

the presheaf fiber of f (from the name)

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the presheaf fiber of $f$ is a homomorphism of the presheaf fiber of $x_{3}$ and the presheaf fiber of $x_{2}$.

the sheaf fiber of f (from the name)

Let $f$ be a homomorphism of $x_{2}$ and $x_{3}$. Then the sheaf fiber of $f$ is a homomorphism of the sheaf fiber of $x_{3}$ and the sheaf fiber of $x_{2}$ defined as the left whisker of the sheaf to presheaf of $J$ and $A$ and the presheaf fiber of $f$.

the preimage of x2 and F (from the name)

Let $x_{2}$ be a point of $K$. Let $F$ be a functor of $C$ and $D$ such that $\operatorname{CoverPreserving}$ holds for $J$, $K$ and $F$. Then the preimage of $x_{2}$ and $F$ is a point of $J$.

the sheaf fiber preimage isomorphism of x2 and F (from the name)

Let $x_{2}$ be a point of $K$. Let $F$ be a functor of $C$ and $D$ such that $\operatorname{CoverPreserving}$ holds for $J$, $K$ and $F$. Let $A$ be a set. Then the sheaf fiber preimage isomorphism of $x_{2}$ and $F$ is an isomorphism of the sheaf fiber of the preimage of $x_{2}$ and $F$ and the composition of the sheaf pullback of $J$ and $K$ and the sheaf fiber of $x_{2}$ defined as $\operatorname{symm}$ applied to the conjugate isomorphism equivalence of the composition of $\operatorname{sheafAdjunctionContinuous}$ applied to $F$, $A$, $J$ and $K$ and the skyscraper sheaf adjunction of $x_{2}$ and the skyscraper sheaf adjunction of the preimage of $x_{2}$ and $F$ and $\operatorname{skyscraperSheafFunctorCompSheafPushforwardContinuous}$ applied to $x_{2}$, $F$, $\mathrm{hF}$ and $A$.

Let $x_{2}$ be a point of $K$. Let $F$ be a functor of $C$ and $D$ such that $\operatorname{CoverPreserving}$ holds for $J$, $K$ and $F$. Let $A$ be a set. Then $\operatorname{skyscraperSheafFunctorCompSheafPushforwardContinuous}$ applied to $x_{2}$, $F$, $\mathrm{hF}$ and $A$ is an isomorphism of the composition of the skyscraper sheaf functor of $x_{2}$ and $\operatorname{sheafPushforwardContinuous}$ applied to $F$, $A$, $J$ and $K$ and the skyscraper sheaf functor of the preimage of $x_{2}$ and $F$ defined as the identity of the composition of the skyscraper sheaf functor of $x_{2}$ and $\operatorname{sheafPushforwardContinuous}$ applied to $F$, $A$, $J$ and $K$.

J has enough points (from the name)

Let $J$ be a Grothendieck topology of $C$. Then we can say that $J$ has enough points.

Let $P$ be an object property of the set of points of $J$. Then we can say that $\operatorname{IsConservativeFamilyOfPoints}$ holds for $P$.