Definitions: Mathlib.Condensed

Let $C$ be a set. Then an element of $\mathrm{Condensed}$ applied to $C$ is an element of the function that maps $C$ to the set of sheaves of the coherent topology of $\mathrm{CompHaus}$ and $C$.

condensed set (from the name)

A condensed set is an element of $\mathrm{Condensed}$ applied to the set of sets.

Let $C$ be a set. Then $\operatorname{discrete}$ applied to $C$ is a functor of $C$ and $\mathrm{Condensed}$ applied to $C$ defined as the constant sheaf of the coherent topology of $\mathrm{CompHaus}$ and $C$.

the discrete underlying adjoint of C (from the name)

Let $C$ be a set. Then the discrete underlying adjoint of $C$ is an adjunction of $\operatorname{discrete}$ applied to $C$ and the underlying object of $C$ defined as the constant sheaf adjoint of the coherent topology of $\mathrm{CompHaus}$ and $\operatorname{isTerminalPUnit}$.

the underlying object of C (from the docstring)

Let $C$ be a set. Then the underlying object of $C$ is a functor of $\mathrm{Condensed}$ applied to $C$ and $C$ defined as the action of the sheaf section of the coherent topology of $\mathrm{CompHaus}$ and $C$ and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\mathrm{PUnit}$.

$\operatorname{discrete}$ is a functor of the set of sets and $\mathrm{LightCondensed}$ applied to the set of sets defined as $\operatorname{discrete}$ applied to the set of sets.

the discrete underlying adjoint (from the name)

The discrete underlying adjoint is an adjunction of $\operatorname{discrete}$ and $\operatorname{underlying}$ defined as the discrete underlying adjoint of the set of sets.

$\operatorname{underlying}$ is a functor of $\mathrm{LightCondensed}$ applied to the set of sets and the set of sets defined as the underlying object of the set of sets.

Let $C$ be a set. Then $\operatorname{discrete}$ applied to $C$ is a functor of $C$ and $\mathrm{LightCondensed}$ applied to $C$ defined as the constant sheaf of the coherent topology of $\mathrm{LightProfinite}$ and $C$.

the discrete underlying adjoint of C (from the name)

Let $C$ be a set. Then the discrete underlying adjoint of $C$ is an adjunction of $\operatorname{discrete}$ applied to $C$ and the underlying object of $C$ defined as the constant sheaf adjoint of the coherent topology of $\mathrm{LightProfinite}$ and $\operatorname{isTerminalPUnit}$.

the underlying object of C (from the docstring)

Let $C$ be a set. Then the underlying object of $C$ is a functor of $\mathrm{LightCondensed}$ applied to $C$ and $C$ defined as the action of the sheaf section of the coherent topology of $\mathrm{LightProfinite}$ and $C$ and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\mathrm{PUnit}$.

X is discrete (from the docstring)

Let $X$ be an element of $\mathrm{Condensed}$ applied to $C$. Then $X$ is discrete, if the coherent topology of $\mathrm{CompHaus}$ is constant.

the adjunction (from the name)

The adjunction is an adjunction of the functor and the underlying object of the set of sets.

the adjunction (from the name)

The adjunction is an adjunction of the functor and the underlying object of the set of sets.

X is discrete (from the docstring)

Let $X$ be an element of $\mathrm{LightCondensed}$ applied to $C$. Then $X$ is discrete, if the coherent topology of $\mathrm{LightProfinite}$ is constant.

the finite Yoneda of F (from the name)

Let $F$ be a functor of the set of opposites of $\mathrm{Profinite}$ and the set of sets. Then the finite Yoneda of $F$ is a functor of the set of opposites of the set of finite type categories and the set of sets.

the finite type category as cofan of X (from the name)

Let $X$ be an element of $\mathrm{Profinite}$. Then the finite type category as cofan of $X$ is a cofan of the function that maps $x$ to $\operatorname{of}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{mk}$ applied to $X$ and the function that maps $x$ to the concrete category of the constant map of the set of carriers of the underlying topological space of $\operatorname{of}$ applied to $\mathrm{PUnit}$ and $x$.

Let $X$ be an element of $\mathrm{Profinite}$. Then $\operatorname{fintypeCatAsCofanIsColimit}$ applied to $X$ is an element of $\operatorname{IsColimit}$ applied to the finite type category as cofan of $X$.

the isomorphism finite Yoneda of F (from the name)

Let $F$ be a functor of the set of opposites of $\mathrm{Profinite}$ and the set of sets. Then the isomorphism finite Yoneda of $F$ is an isomorphism of the composition of the opposite of $\operatorname{toProfinite}$ and $F$ and the finite Yoneda of $F$.

Let $X$ be a set. Then $\operatorname{lanCondensedSet}$ applied to $X$ is a condensed set defined as the action of the functor of the equivalence of the set of sets and $\operatorname{lanSheafProfinite}$ applied to $X$.

Let $F$ be a functor of the set of opposites of $\mathrm{Profinite}$ and the set of sets. Then $\operatorname{lanPresheaf}$ applied to $F$ is a functor of the set of opposites of $\mathrm{Profinite}$ and the set of sets defined as the pointwise left Kan extension of the opposite of $\operatorname{toProfinite}$ and the composition of the opposite of $\operatorname{toProfinite}$ and $F$.

Let $i$ be an isomorphism of the composition of the opposite of $\operatorname{toProfinite}$ and $F$ and the composition of the opposite of $\operatorname{toProfinite}$ and $G$. Then $\operatorname{lanPresheafExt}$ applied to $i$ is an isomorphism of $\operatorname{lanPresheaf}$ applied to $F$ and $\operatorname{lanPresheaf}$ applied to $G$ defined as $\operatorname{leftKanExtensionUniqueOfIso}$ applied to the pointwise left Kan extension of the opposite of $\operatorname{toProfinite}$ and the composition of the opposite of $\operatorname{toProfinite}$ and $F$, the pointwise left Kan extension unit of the opposite of $\operatorname{toProfinite}$ and the composition of the opposite of $\operatorname{toProfinite}$ and $F$, $i$, $\operatorname{lanPresheaf}$ applied to $G$ and the pointwise left Kan extension unit of the opposite of $\operatorname{toProfinite}$ and the composition of the opposite of $\operatorname{toProfinite}$ and $G$.

Let $\mathrm{hF}$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of $F$ and the opposite of $\operatorname{asLimitCone}$ applied to $S$. Then $\operatorname{lanPresheafIso}$ applied to $\mathrm{hF}$ is an isomorphism of the action of $\operatorname{lanPresheaf}$ applied to $F$ and $\operatorname{op}$ applied to $S$ and the action of $F$ and $\operatorname{op}$ applied to $S$ defined as the composition of the inverse of the colimit isomorphism of the functor opposite of $\operatorname{asLimitCone}$ applied to $S$ and the composition of the projection of the opposite of $\operatorname{toProfinite}$ and $\operatorname{op}$ applied to $S$ and the composition of the opposite of $\operatorname{toProfinite}$ and $F$ and $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the composition of the opposite of the diagram of $S$ and $F$ and $\mathrm{hF}$.

Let $\mathrm{hF}$ be a function from elements $S$ of $\mathrm{Profinite}$ to elements of $\operatorname{IsColimit}$ applied to the map cocone of $F$ and the opposite of $\operatorname{asLimitCone}$ applied to $S$. Then $\operatorname{lanPresheafNatIso}$ applied to $S$ and $\mathrm{hF}$ is an isomorphism of $\operatorname{lanPresheaf}$ applied to $F$ and $F$.

Let $X$ be a set. Then $\operatorname{lanSheafProfinite}$ applied to $X$ is a sheaf of the coherent topology of $\mathrm{Profinite}$ and the set of sets.

the locally constant isomorphism finite Yoneda of F (from the name)

the locally constant presheaf of X (from the name)

the finite Yoneda of F (from the name)

Let $F$ be a functor of the set of opposites of $\mathrm{LightProfinite}$ and the set of sets. Then the finite Yoneda of $F$ is a functor of the set of opposites of the set of finite type categories and the set of sets.

the finite type category as cofan of X (from the name)

Let $X$ be an element of $\mathrm{LightProfinite}$. Then the finite type category as cofan of $X$ is a cofan of the function that maps $x$ to $\operatorname{of}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{mk}$ applied to $X$ and the function that maps $x$ to the concrete category of the constant map of the set of carriers of the underlying topological space of $\operatorname{of}$ applied to $\mathrm{PUnit}$ and $x$.

Let $X$ be an element of $\mathrm{LightProfinite}$. Then $\operatorname{fintypeCatAsCofanIsColimit}$ applied to $X$ is an element of $\operatorname{IsColimit}$ applied to the finite type category as cofan of $X$.

the isomorphism finite Yoneda of F (from the name)

Let $F$ be a functor of the set of opposites of $\mathrm{LightProfinite}$ and the set of sets. Then the isomorphism finite Yoneda of $F$ is an isomorphism of the composition of the opposite of $\operatorname{toLightProfinite}$ and $F$ and the finite Yoneda of $F$.

Let $X$ be a set. Then $\operatorname{lanLightCondSet}$ applied to $X$ is a light conditional set.

Let $F$ be a functor of the set of opposites of $\mathrm{LightProfinite}$ and the set of sets. Then $\operatorname{lanPresheaf}$ applied to $F$ is a functor of the set of opposites of $\mathrm{LightProfinite}$ and the set of sets defined as the pointwise left Kan extension of the opposite of $\operatorname{toLightProfinite}$ and the composition of the opposite of $\operatorname{toLightProfinite}$ and $F$.

Let $i$ be an isomorphism of the composition of the opposite of $\operatorname{toLightProfinite}$ and $F$ and the composition of the opposite of $\operatorname{toLightProfinite}$ and $G$. Then $\operatorname{lanPresheafExt}$ applied to $i$ is an isomorphism of $\operatorname{lanPresheaf}$ applied to $F$ and $\operatorname{lanPresheaf}$ applied to $G$ defined as $\operatorname{leftKanExtensionUniqueOfIso}$ applied to the pointwise left Kan extension of the opposite of $\operatorname{toLightProfinite}$ and the composition of the opposite of $\operatorname{toLightProfinite}$ and $F$, the pointwise left Kan extension unit of the opposite of $\operatorname{toLightProfinite}$ and the composition of the opposite of $\operatorname{toLightProfinite}$ and $F$, $i$, $\operatorname{lanPresheaf}$ applied to $G$ and the pointwise left Kan extension unit of the opposite of $\operatorname{toLightProfinite}$ and the composition of the opposite of $\operatorname{toLightProfinite}$ and $G$.

Let $\mathrm{hF}$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of $F$ and the cocone right opposite of $\operatorname{asLimitCone}$ applied to $S$. Then $\operatorname{lanPresheafIso}$ applied to $\mathrm{hF}$ is an isomorphism of the action of $\operatorname{lanPresheaf}$ applied to $F$ and $\operatorname{op}$ applied to $S$ and the action of $F$ and $\operatorname{op}$ applied to $S$ defined as the composition of the inverse of the colimit isomorphism of the functor opposite of $\operatorname{asLimitCone}$ applied to $S$ and the composition of the projection of the opposite of $\operatorname{toLightProfinite}$ and $\operatorname{op}$ applied to $S$ and the composition of the opposite of $\operatorname{toLightProfinite}$ and $F$ and $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the composition of the right opposite of the diagram of $S$ and $F$ and $\mathrm{hF}$.

Let $\mathrm{hF}$ be a function from elements $S$ of $\mathrm{LightProfinite}$ to elements of $\operatorname{IsColimit}$ applied to the map cocone of $F$ and the cocone right opposite of $\operatorname{asLimitCone}$ applied to $S$. Then $\operatorname{lanPresheafNatIso}$ applied to $S$ and $\mathrm{hF}$ is an isomorphism of $\operatorname{lanPresheaf}$ applied to $F$ and $F$.

the locally constant isomorphism finite Yoneda of F (from the name)

the locally constant presheaf of X (from the name)

the adjunction of P and hs (from the name)

Let $P$ be a function from topological categories to propositions such that for all elements $X$ and $Y$ of $\mathrm{CompHausLike}$ applied to $P$, for all homomorphisms $f$ of $X$ and $Y$, if $f$ is an effective epimorphism, then $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then the adjunction of $P$ and $\mathrm{hs}$ is an adjunction of the functor of $P$ and $\mathrm{hs}$ and the action of the sheaf section of the coherent topology of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $P$ and $\mathrm{PUnit}$.

the component homomorphism of g and a (from the name)

Let $f$ be an element of $\mathrm{LocallyConstant}$ applied to the set of carriers of the underlying topological space of $S$ and the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $P$ and $\mathrm{PUnit}$. Let $g$ be a homomorphism of $T$ and $S$. Let $a$ be a fiber of $\operatorname{coe}$ applied to the preimage of the homomorphism of the homomorphism of $g$ and $f$. Then the component homomorphism of $g$ and $a$ is a homomorphism of the fiber of the preimage of the homomorphism of the homomorphism of $g$ and $f$ and $a$ and the fiber of $f$ and $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{hom}$ applied to $g$ and the preimage of $\operatorname{coe}$ applied to the preimage of the homomorphism of the homomorphism of $g$ and $f$ and $a$.

the counit of P and hs (from the docstring)

Let $P$ be a function from topological categories to propositions such that for all elements $X$ and $Y$ of $\mathrm{CompHausLike}$ applied to $P$, for all homomorphisms $f$ of $X$ and $Y$, if $f$ is an effective epimorphism, then $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then the counit of $P$ and $\mathrm{hs}$ is a homomorphism of the composition of the action of the sheaf section of the coherent topology of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $P$ and $\mathrm{PUnit}$ and the functor of $P$ and $\mathrm{hs}$ and the identity of the set of sheaves of the coherent topology of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets.

the counit of Y (from the docstring)

Let $Y$ be a functor of the set of opposites of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets. Then the counit of $Y$ is a homomorphism of the action of $\operatorname{functorToPresheaves}$ and the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $P$ and $\mathrm{PUnit}$ and $Y$.

the counit of S and Y (from the docstring)

Let $S$ be an element of $\mathrm{CompHausLike}$ applied to $P$. Let $Y$ be a functor of the set of opposites of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets. Then the counit of $S$ and $Y$ is a homomorphism of $\mathrm{LocallyConstant}$ applied to the set of carriers of the underlying topological space of $S$ and the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $P$ and $\mathrm{PUnit}$ and the action of $Y$ and $\operatorname{op}$ applied to $S$ defined as the type category of the function that maps $r$ to $\operatorname{hom}$ applied to the composition of the inverse of the comparison map from the value of $Y$ and the function that maps $a_{2}$ to the set of carriers of the underlying topological space of the fiber of $r$ and $a_{2}$ and the inverse of the map isomorphism of $Y$ and the opposite isomorphism of the sigma isomorphism of $r$ and $\operatorname{counitAppAppImage}$ applied to $r$.

the projection of the counit of f and a (from the docstring)

Let $f$ be an element of $\mathrm{LocallyConstant}$ applied to the set of carriers of the underlying topological space of $S$ and the action of $Y$ and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $P$ and $\mathrm{PUnit}$. Let $a$ be a fiber of $\operatorname{coe}$ applied to $f$. Then the projection of the counit of $f$ and $a$ is an element of the action of $Y$ and $\operatorname{op}$ applied to the fiber of $f$ and $a$ defined as $\operatorname{hom}$ applied to the map of $Y$ and the opposite in $\operatorname{from}$ applied to $\operatorname{isTerminalPUnit}$ and the fiber of $f$ and $a$ and the image of $\operatorname{coe}$ applied to $f$ and $a$.

the fiber of r and a (from the name)

Let $r$ be an element of $\mathrm{LocallyConstant}$ applied to the set of carriers of the underlying topological space of $Q$ and $Z$. Let $a$ be a fiber of $\operatorname{coe}$ applied to $r$. Then the fiber of $r$ and $a$ is an element of $\mathrm{CompHausLike}$ applied to $P$ defined as $\operatorname{of}$ applied to $P$ and the set of elements of $a$.

the functor of P and hs (from the name)

Let $P$ be a function from topological categories to propositions such that for all elements $X$ and $Y$ of $\mathrm{CompHausLike}$ applied to $P$, for all homomorphisms $f$ of $X$ and $Y$, if $f$ is an effective epimorphism, then $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then the functor of $P$ and $\mathrm{hs}$ is a functor of the set of sets and the set of sheaves of the coherent topology of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets.

the functor isomorphism of P and hs (from the name)

Let $P$ be a function from topological categories to propositions such that for all elements $X$ and $Y$ of $\mathrm{CompHausLike}$ applied to $P$, for all homomorphisms $f$ of $X$ and $Y$, if $f$ is an effective epimorphism, then $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then the functor isomorphism of $P$ and $\mathrm{hs}$ is an isomorphism of the functor of $P$ and $\mathrm{hs}$ and the composition of the discrete topology and $\mathrm{topCatToSheafCompHausLike}$ applied to $P$ and $\mathrm{hs}$.

$\operatorname{functorToPresheaves}$ is a functor of the set of sets and the set of functors of the set of opposites of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets.

Let $P$ be a function from topological categories to propositions such that for all elements $X_{1}$ and $Y$ of $\mathrm{CompHausLike}$ applied to $P$, for all homomorphisms $f$ of $X_{1}$ and $Y$, if $f$ is an effective epimorphism, then $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Let $X$ be a set. Then $\operatorname{functorToPresheavesIso}$ applied to $P$, $\mathrm{hs}$ and $X$ is an isomorphism of the action of $\operatorname{functorToPresheaves}$ and $X$ and the object of $\operatorname{toSheafCompHausLike}$ applied to $P$, the action of the discrete topology and $X$ and $\mathrm{hs}$.

the locally constant isomorphism continuous map of Y and X (from the name)

the sigma inclusion of r and a (from the name)

Let $r$ be an element of $\mathrm{LocallyConstant}$ applied to the set of carriers of the underlying topological space of $Q$ and $Z$. Let $a$ be a fiber of $\operatorname{coe}$ applied to $r$. Then the sigma inclusion of $r$ and $a$ is a homomorphism of the fiber of $r$ and $a$ and $Q$ defined as $\operatorname{ofHom}$ applied to $P$ and the sigma inclusion of $\operatorname{coe}$ applied to $r$ and $a$.

the sigma isomorphism of r (from the name)

Let $r$ be an element of $\mathrm{LocallyConstant}$ applied to the set of carriers of the underlying topological space of $Q$ and $Z$. Then the sigma isomorphism of $r$ is an isomorphism of the coproduct in $\operatorname{fiber}$ applied to $r$ and $Q$.

the unit of the adjunction of P and hs (from the docstring)

Let $P$ be a function from topological categories to propositions such that for all elements $X$ and $Y$ of $\mathrm{CompHausLike}$ applied to $P$, for all homomorphisms $f$ of $X$ and $Y$, if $f$ is an effective epimorphism, then $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then the unit of the adjunction of $P$ and $\mathrm{hs}$ is a homomorphism of the identity of the set of sets and the composition of the functor of $P$ and $\mathrm{hs}$ and the action of the sheaf section of the coherent topology of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $P$ and $\mathrm{PUnit}$.

the unit of the adjunction of P and hs (from the docstring)

Let $P$ be a function from topological categories to propositions such that for all elements $X$ and $Y$ of $\mathrm{CompHausLike}$ applied to $P$, for all homomorphisms $f$ of $X$ and $Y$, if $f$ is an effective epimorphism, then $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then the unit of the adjunction of $P$ and $\mathrm{hs}$ is an isomorphism of the identity of the set of sets and the composition of the functor of $P$ and $\mathrm{hs}$ and the action of the sheaf section of the coherent topology of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $P$ and $\mathrm{PUnit}$.

the functor (from the name)

The functor is a functor of the set of sets and the set of condensed sets.

$\operatorname{functorFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the functor.

the isomorphism (from the name)

The isomorphism is an isomorphism of the functor and $\operatorname{discrete}$ applied to the set of sets.

the functor (from the name)

The functor is a functor of the set of sets and the set of light conditional sets.

$\operatorname{functorFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the functor.

the isomorphism (from the name)

The isomorphism is an isomorphism of the functor and $\operatorname{discrete}$ applied to the set of sets.

the functor of R and hs (from the name)

Let $R$ be a set. Assume that for all elements $X$ and $Y$ of $\mathrm{CompHausLike}$ applied to $P$, for all homomorphisms $f$ of $X$ and $Y$, if $f$ is an effective epimorphism, then $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then the functor of $R$ and $\mathrm{hs}$ is a functor of the set of module categories of $R$ and the set of sheaves of the coherent topology of $\mathrm{CompHausLike}$ applied to $P$ and the set of module categories of $R$.

Let $R$ be a set. Then $\operatorname{functorToPresheaves}$ applied to $R$ is a functor of the set of module categories of $R$ and the set of functors of the set of opposites of $\mathrm{CompHausLike}$ applied to $P$ and the set of module categories of $R$.

the adjunction of R (from the name)

Let $R$ be a set. Then the adjunction of $R$ is an adjunction of the functor of $R$ and the underlying object of the set of module categories of $R$ defined as the adjunction of the discrete underlying adjoint of the set of module categories of $R$ and the inverse of $\operatorname{functorIsoDiscrete}$ applied to $R$.

the fully faithful functor of R (from the name)

the functor of R (from the name)

Let $R$ be a set. Then the functor of $R$ is a functor of the set of module categories of $R$ and $\mathrm{CondensedMod}$ applied to $R$.

Let $R$ be a set. Then $\operatorname{functorIsoDiscrete}$ applied to $R$ is an isomorphism of the functor of $R$ and $\operatorname{discrete}$ applied to the set of module categories of $R$.

Let $R$ be a set. Then $\operatorname{functorToPresheaves}$ applied to $R$ is a functor of the set of module categories of $R$ and the set of functors of the set of opposites of $\mathrm{CompHaus}$ and the set of module categories of $R$ defined as $\operatorname{functorToPresheaves}$ applied to $R$.

the adjunction of R (from the name)

Let $R$ be a set. Then the adjunction of $R$ is an adjunction of the functor of $R$ and the underlying object of the set of module categories of $R$ defined as the adjunction of the discrete underlying adjoint of the set of module categories of $R$ and the inverse of $\operatorname{functorIsoDiscrete}$ applied to $R$.

the fully faithful functor of R (from the name)

the functor of R (from the name)

Let $R$ be a set. Then the functor of $R$ is a functor of the set of module categories of $R$ and $\mathrm{LightCondMod}$ applied to $R$.

Let $R$ be a set. Then $\operatorname{functorIsoDiscrete}$ applied to $R$ is an isomorphism of the functor of $R$ and $\operatorname{discrete}$ applied to the set of module categories of $R$.

Let $R$ be a set. Then $\operatorname{functorToPresheaves}$ applied to $R$ is a functor of the set of module categories of $R$ and the set of functors of the set of opposites of $\mathrm{LightProfinite}$ and the set of module categories of $R$ defined as $\operatorname{functorToPresheaves}$ applied to $R$.

the equivalence of A (from the name)

Let $A$ be a set. Then the equivalence of $A$ is an equivalence of the set of sheaves of the coherent topology of $\mathrm{Profinite}$ and $A$ and $\mathrm{Condensed}$ applied to $A$ defined as the equivalence of $\mathrm{profiniteToCompHaus}$ and $A$.

the equivalence of A (from the name)

Let $A$ be a set. Then the equivalence of $A$ is an equivalence of the set of sheaves of the coherent topology of $\mathrm{Stonean}$ and $A$ and $\mathrm{Condensed}$ applied to $A$ defined as the equivalence of $\operatorname{toCompHaus}$ and $A$.

the equivalence of A (from the name)

Let $A$ be a set. Then the equivalence of $A$ is an equivalence of the set of sheaves of the coherent topology of $\mathrm{Stonean}$ and $A$ and the set of sheaves of the coherent topology of $\mathrm{Profinite}$ and $A$ defined as the equivalence of $\operatorname{toProfinite}$ and $A$.

Let $X$ be an element of $\mathrm{Profinite}$. Then $\operatorname{stoneanToProfiniteEffectivePresentation}$ applied to $X$ is an effective presentation of $\operatorname{toProfinite}$ and $X$.

Let $F$ be a functor of the set of opposites of $\mathrm{CompHaus}$ and $A$ such that $F$ is an equalizer condition. Then $\operatorname{ofSheafCompHaus}$ applied to $F$ and $\mathrm{hF}$ is an element of $\mathrm{Condensed}$ applied to $A$.

Let $F$ be a functor of the set of opposites of $\mathrm{CompHaus}$ and $A$ such that the composition of $F$ and the forgetful functor of $A$ is an equalizer condition. Then $\operatorname{ofSheafForgetCompHaus}$ applied to $F$ and $\mathrm{hF}$ is an element of $\mathrm{Condensed}$ applied to $A$.

Let $F$ be a functor of the set of opposites of $\mathrm{Profinite}$ and $A$ such that the composition of $F$ and the forgetful functor of $A$ is an equalizer condition. Then $\operatorname{ofSheafForgetProfinite}$ applied to $F$ and $\mathrm{hF}$ is an element of $\mathrm{Condensed}$ applied to $A$.

Let $F$ be a functor of the set of opposites of $\mathrm{Stonean}$ and $A$. Then $\operatorname{ofSheafForgetStonean}$ applied to $F$ is an element of $\mathrm{Condensed}$ applied to $A$.

Let $F$ be a functor of the set of opposites of $\mathrm{Profinite}$ and $A$ such that $F$ is an equalizer condition. Then $\operatorname{ofSheafProfinite}$ applied to $F$ and $\mathrm{hF}$ is an element of $\mathrm{Condensed}$ applied to $A$.

Let $F$ be a functor of the set of opposites of $\mathrm{Stonean}$ and $A$. Then $\operatorname{ofSheafStonean}$ applied to $F$ is an element of $\mathrm{Condensed}$ applied to $A$.

Let $R$ be a set. Let $F$ be a functor of the set of opposites of $\mathrm{CompHaus}$ and the set of module categories of $R$ such that $F$ is an equalizer condition. Then $\operatorname{ofSheafCompHaus}$ applied to $R$, $F$ and $\mathrm{hF}$ is an element of $\mathrm{CondensedMod}$ applied to $R$ defined as $\operatorname{ofSheafCompHaus}$ applied to $F$ and $\mathrm{hF}$.

Let $R$ be a set. Let $F$ be a functor of the set of opposites of $\mathrm{Profinite}$ and the set of module categories of $R$ such that $F$ is an equalizer condition. Then $\operatorname{ofSheafProfinite}$ applied to $R$, $F$ and $\mathrm{hF}$ is an element of $\mathrm{CondensedMod}$ applied to $R$ defined as $\operatorname{ofSheafProfinite}$ applied to $F$ and $\mathrm{hF}$.

Let $R$ be a set. Let $F$ be a functor of the set of opposites of $\mathrm{Stonean}$ and the set of module categories of $R$. Then $\operatorname{ofSheafStonean}$ applied to $R$ and $F$ is an element of $\mathrm{CondensedMod}$ applied to $R$ defined as $\operatorname{ofSheafStonean}$ applied to $F$.

the condensed set of F and hF (from the name)

Let $F$ be a functor of the set of opposites of $\mathrm{CompHaus}$ and the set of sets such that $F$ is an equalizer condition. Then the condensed set of $F$ and $\mathrm{hF}$ is a condensed set defined as $\operatorname{ofSheafCompHaus}$ applied to $F$ and $\mathrm{hF}$.

the condensed set of F and hF (from the name)

Let $F$ be a functor of the set of opposites of $\mathrm{Profinite}$ and the set of sets such that $F$ is an equalizer condition. Then the condensed set of $F$ and $\mathrm{hF}$ is a condensed set defined as $\operatorname{ofSheafProfinite}$ applied to $F$ and $\mathrm{hF}$.

the condensed set of F (from the name)

Let $F$ be a functor of the set of opposites of $\mathrm{Stonean}$ and the set of sets. Then the condensed set of $F$ is a condensed set defined as $\operatorname{ofSheafStonean}$ applied to $F$.

Let $S$ be an element of $\mathrm{CompHaus}$. Then $\operatorname{toCondensed}$ applied to $S$ is a condensed set defined as the action of $\mathrm{compHausToCondensed}$ and $S$.

the lift (from the name)

The lift is a functor of $\mathrm{Condensed}$ applied to the set of sets and the set of condensed sets defined as $\operatorname{sheafCompose}$ applied to the coherent topology of $\mathrm{CompHaus}$ and the functor embedding.

Let $S$ be an element of $\mathrm{Profinite}$. Then $\operatorname{toCondensed}$ applied to $S$ is a condensed set defined as the action of $\mathrm{profiniteToCondensed}$ and $S$.

Let $S$ be an element of $\mathrm{Stonean}$. Then $\operatorname{toCondensed}$ applied to $S$ is a condensed set defined as the action of $\mathrm{stoneanToCondensed}$ and $S$.

$\mathrm{compHausToCondensed}$ is a functor of $\mathrm{CompHaus}$ and the set of condensed sets defined as the composition of $\mathrm{compHausToCondensed'}$ and the lift.

$\mathrm{compHausToCondensed'}$ is a functor of $\mathrm{CompHaus}$ and $\mathrm{Condensed}$ applied to the set of sets defined as the Yoneda of the coherent topology of $\mathrm{CompHaus}$.

$\mathrm{profiniteToCondensed}$ is a functor of $\mathrm{Profinite}$ and the set of condensed sets defined as the composition of $\mathrm{profiniteToCompHaus}$ and $\mathrm{compHausToCondensed}$.

$\mathrm{stoneanToCondensed}$ is a functor of $\mathrm{Stonean}$ and the set of condensed sets defined as the composition of $\operatorname{toCompHaus}$ and $\mathrm{compHausToCondensed}$.

light conditional set (from the name)

A light conditional set is an element of $\mathrm{LightCondensed}$ applied to the set of sets.

Let $C$ be a set. Then an element of $\mathrm{LightCondensed}$ applied to $C$ is an element of the function that maps $C$ to the set of sheaves of the coherent topology of $\mathrm{LightProfinite}$ and $C$.

the light conditional abelian group of F and hF (from the name)

Let $F$ be a functor of the set of opposites of $\mathrm{LightProfinite}$ and the set of module categories of $\Integer$ such that $F$ is an equalizer condition. Then the light conditional abelian group of $F$ and $\mathrm{hF}$ is a light conditional abelian group defined as $\operatorname{ofSheafLightProfinite}$ applied to $\Integer$, $F$ and $\mathrm{hF}$.

Let $R$ be a set. Let $F$ be a functor of the set of opposites of $\mathrm{LightProfinite}$ and the set of module categories of $R$ such that $F$ is an equalizer condition. Then $\operatorname{ofSheafLightProfinite}$ applied to $R$, $F$ and $\mathrm{hF}$ is an element of $\mathrm{LightCondMod}$ applied to $R$ defined as $\operatorname{ofSheafLightProfinite}$ applied to $F$ and $\mathrm{hF}$.

the light conditional set of F and hF (from the name)

Let $F$ be a functor of the set of opposites of $\mathrm{LightProfinite}$ and the set of sets such that $F$ is an equalizer condition. Then the light conditional set of $F$ and $\mathrm{hF}$ is a light conditional set defined as $\operatorname{ofSheafLightProfinite}$ applied to $F$ and $\mathrm{hF}$.

Let $F$ be a functor of the set of opposites of $\mathrm{LightProfinite}$ and $A$ such that the composition of $F$ and the forgetful functor of $A$ is an equalizer condition. Then $\operatorname{ofSheafForgetLightProfinite}$ applied to $F$ and $\mathrm{hF}$ is an element of $\mathrm{LightCondensed}$ applied to $A$.

Let $F$ be a functor of the set of opposites of $\mathrm{LightProfinite}$ and $A$ such that $F$ is an equalizer condition. Then $\operatorname{ofSheafLightProfinite}$ applied to $F$ and $\mathrm{hF}$ is an element of $\mathrm{LightCondensed}$ applied to $A$.

Let $S$ be an element of $\mathrm{LightProfinite}$. Then $\operatorname{toCondensed}$ applied to $S$ is a light conditional set defined as the action of the light profinite to light conditional set and $S$.

the light profinite to light conditional set (from the name)

The light profinite to light conditional set is a functor of $\mathrm{LightProfinite}$ and the set of light conditional sets defined as the Yoneda of the coherent topology of $\mathrm{LightProfinite}$.

$\mathrm{lightProfiniteToLightCondSetFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the light profinite to light conditional set defined as $\operatorname{yonedaFullyFaithful}$ applied to the coherent topology of $\mathrm{LightProfinite}$.

the light profinite to light conditional set isomorphism topological category to light conditional set (from the name)

The light profinite to light conditional set isomorphism topological category to light conditional set is an isomorphism of the light profinite to light conditional set and the composition of the topological category and the topological category to light conditional set.

Let $R$ be a set. Let $A$ and $B$ be elements of $\mathrm{LightCondMod}$ applied to $R$. Let $S$ be an element of $\mathrm{LightProfinite}$. Then $\operatorname{ihomPoints}$ applied to $R$, $A$, $B$ and $S$ is an equivalence from the set of carriers of the action of the object of the action of $\operatorname{ihom}$ applied to $A$ and $B$ and $\operatorname{op}$ applied to $S$ to the set of homomorphisms of the tensor object of $A$ and the action of the free of $R$ and $\operatorname{toCondensed}$ applied to $S$ and $B$ defined as the composition of the inverse of the composition of the homomorphism equivalence of the action of the Yoneda of the coherent topology of $\mathrm{LightProfinite}$ and $S$ and the action of $\operatorname{ihom}$ applied to $A$ and $B$ and the Yoneda equivalence of the coherent topology of $\mathrm{LightProfinite}$ and the inverse of the homomorphism equivalence of the action of the free of $R$ and the action of the Yoneda of the coherent topology of $\mathrm{LightProfinite}$ and $S$ and $B$.

light conditional abelian group (from the name)

A light conditional abelian group is an element of $\mathrm{LightCondMod}$ applied to $\Integer$.

Let $R$ be a set. Then an element of $\mathrm{LightCondMod}$ applied to $R$ is an element of the function that maps $R$ to $\mathrm{LightCondensed}$ applied to the set of module categories of $R$.

Let $R$ be a set. Then $\operatorname{forget}$ applied to $R$ is a functor of $\mathrm{LightCondMod}$ applied to $R$ and the set of light conditional sets defined as $\operatorname{sheafCompose}$ applied to the coherent topology of $\mathrm{LightProfinite}$ and the forgetful functor of the set of module categories of $R$.

the free of R (from the name)

Let $R$ be a set. Then the free of $R$ is a functor of the set of light conditional sets and $\mathrm{LightCondMod}$ applied to $R$ defined as $\operatorname{composeAndSheafify}$ applied to the coherent topology of $\mathrm{LightProfinite}$ and the free functor of $R$.

Let $R$ be a set. Then $\operatorname{freeForgetAdjunction}$ applied to $R$ is an adjunction of the free of $R$ and $\operatorname{forget}$ applied to $R$ defined as the adjunction of the coherent topology of $\mathrm{LightProfinite}$ and the adjoint of $R$.

the equivalence small of C (from the name)

Let $C$ be a set. Then the equivalence small of $C$ is an equivalence of $\mathrm{LightCondensed}$ applied to $C$ and the set of sheaves of the induced topology of the inverse of the equivalence small model of $\mathrm{LightProfinite}$ and the coherent topology of $\mathrm{LightProfinite}$ and $C$ defined as the sheaf congruence of the induced topology of the inverse of the equivalence small model of $\mathrm{LightProfinite}$ and the coherent topology of $\mathrm{LightProfinite}$ and the equivalence small model of $\mathrm{LightProfinite}$.

the equivalence small free isomorphism of R (from the name)

Let $R$ be a set. Then the equivalence small free isomorphism of $R$ is an isomorphism of the composition of the inverse of the equivalence small of the set of sets and the composition of the free of $R$ and the functor of the equivalence small of the set of module categories of $R$ and $\operatorname{composeAndSheafify}$ applied to the induced topology of the inverse of the equivalence small model of $\mathrm{LightProfinite}$ and the coherent topology of $\mathrm{LightProfinite}$ and the free functor of $R$.

the equivalence small sheafification isomorphism (from the name)

The equivalence small sheafification isomorphism is an isomorphism of the composition of the inverse of the left congruence of the opposite of the equivalence small model of $\mathrm{LightProfinite}$ and the composition of the presheaf to sheaf of the coherent topology of $\mathrm{LightProfinite}$ and $C$ and the functor of the equivalence small of $C$ and the presheaf to sheaf of the induced topology of the inverse of the equivalence small model of $\mathrm{LightProfinite}$ and the coherent topology of $\mathrm{LightProfinite}$ and $C$.

$\operatorname{fullyFaithfulSequentialToLightCondSet}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{sequentialToLightCondSet}$ defined as $\operatorname{fullyFaithfulROfIsIsoCounit}$ applied to the adjunction.

$\operatorname{lightCondSetToSequential}$ is a functor of the set of light conditional sets and $\mathrm{Sequential}$.

the adjunction (from the docstring)

The adjunction is an adjunction of $\operatorname{lightCondSetToSequential}$ and $\operatorname{sequentialToLightCondSet}$ defined as $\operatorname{restrictFullyFaithful}$ applied to the adjunction, the identity functor of the set of light conditional sets, $\operatorname{fullyFaithfulSequentialToTop}$, the identity of the composition of the identity of the set of light conditional sets and the light conditional set to topological category and the identity of the composition of $\operatorname{sequentialToTop}$ and the topological category to light conditional set.

the counit of the adjunction of X (from the docstring)

Let $X$ be an element of $\mathrm{Sequential}$. Then the counit of the adjunction of $X$ is an isomorphism of the action of $\operatorname{lightCondSetToSequential}$ and the action of $\operatorname{sequentialToLightCondSet}$ and $X$ and $X$ defined as the isomorphism of the counit of the adjunction of the underlying topological space of $X$.

the counit of the adjunction of X (from the docstring)

Let $X$ be a topological category. Then the counit of the adjunction of $X$ is a homeomorphism of the set of carriers of the topological category of the light conditional set of $X$ and the set of carriers of $X$.

$\operatorname{sequentialToLightCondSet}$ is a functor of $\mathrm{Sequential}$ and the set of light conditional sets defined as the composition of $\operatorname{sequentialToTop}$ and the topological category to light conditional set.

the topological category of X (from the name)

Let $X$ be a light conditional set. Then the topological category of $X$ is a topological category defined as $\operatorname{of}$ applied to the action of the object of $X$ and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\mathrm{PUnit}$.

the map part of the functor of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map part of the functor of $f$ is a homomorphism of the topological category of $X$ and the topological category of $Y$.

the adjunction (from the docstring)

The adjunction is an adjunction of the light conditional set to topological category and the topological category to light conditional set.

the counit of the adjunction of X (from the docstring)

Let $X$ be a topological category. Then the counit of the adjunction of $X$ is a homomorphism of the topological category of the light conditional set of $X$ and $X$.

the counit of the adjunction of X (from the docstring)

Let $X$ be a topological category. Then the counit of the adjunction of $X$ is an equivalence from the set of carriers of the topological category of the light conditional set of $X$ to the set of carriers of $X$.

the unit of the adjunction of X (from the docstring)

Let $X$ be a light conditional set. Then the unit of the adjunction of $X$ is a homomorphism of $X$ and the light conditional set of the topological category of $X$.

the light conditional set to topological category (from the name)

The light conditional set to topological category is a functor of the set of light conditional sets and the set of topological categories.

the light conditional set of X (from the name)

Let $X$ be a topological category. Then the light conditional set of $X$ is a light conditional set.

the topological category to light conditional set (from the name)

The topological category to light conditional set is a functor of the set of topological categories and the set of light conditional sets.

$\operatorname{abForget}$ is a functor of the set of condensed abelian groups and the set of condensed sets defined as $\operatorname{forget}$ applied to $\mathrm{ULift}$ applied to $\Integer$.

Let $R$ be a set. Then $\operatorname{forget}$ applied to $R$ is a functor of $\mathrm{CondensedMod}$ applied to $R$ and the set of condensed sets defined as $\operatorname{sheafCompose}$ applied to the coherent topology of $\mathrm{CompHaus}$ and the forgetful functor of the set of module categories of $R$.

the free of R (from the name)

Let $R$ be a set. Then the free of $R$ is a functor of the set of condensed sets and $\mathrm{CondensedMod}$ applied to $R$ defined as $\operatorname{composeAndSheafify}$ applied to the coherent topology of $\mathrm{CompHaus}$ and the free functor of $R$.

the free condensed abelian group (from the docstring)

The free condensed abelian group is a functor of the set of condensed sets and the set of condensed abelian groups defined as the free of $\mathrm{ULift}$ applied to $\Integer$.

Let $R$ be a set. Then $\operatorname{freeForgetAdjunction}$ applied to $R$ is an adjunction of the free of $R$ and $\operatorname{forget}$ applied to $R$ defined as the adjunction of the coherent topology of $\mathrm{CompHaus}$ and the adjoint of $R$.

the set abelian group adjunction (from the name)

The set abelian group adjunction is an adjunction of the free condensed abelian group and $\operatorname{abForget}$ defined as $\operatorname{freeForgetAdjunction}$ applied to $\mathrm{ULift}$ applied to $\Integer$.

condensed abelian group (from the name)

A condensed abelian group is an element of $\mathrm{CondensedMod}$ applied to $\mathrm{ULift}$ applied to $\Integer$.

Let $R$ be a set. Then an element of $\mathrm{CondensedMod}$ applied to $R$ is an element of the function that maps $R$ to $\mathrm{Condensed}$ applied to the set of module categories of $R$.

the finite free of R (from the name)

Let $R$ be a set. Then the finite free of $R$ is a functor of the set of finite type categories and $\mathrm{CondensedMod}$ applied to $R$ defined as the composition of $\operatorname{toProfinite}$ and the composition of $\mathrm{profiniteToCondensed}$ and the free of $R$.

the profinite free of R (from the name)

Let $R$ be a set. Then the profinite free of $R$ is a functor of $\mathrm{Profinite}$ and $\mathrm{CondensedMod}$ applied to $R$ defined as the composition of $\mathrm{profiniteToCondensed}$ and the free of $R$.

Let $R$ be a set. Then $\operatorname{profiniteSolid}$ applied to $R$ is a functor of $\mathrm{Profinite}$ and $\mathrm{CondensedMod}$ applied to $R$ defined as the right Kan extension of $\operatorname{toProfinite}$ and the finite free of $R$.

the profinite solid counit of R (from the name)

Let $R$ be a set. Then the profinite solid counit of $R$ is a homomorphism of the composition of $\operatorname{toProfinite}$ and $\operatorname{profiniteSolid}$ applied to $R$ and the finite free of $R$ defined as the counit of the chosen right Kan extension of $\operatorname{toProfinite}$ and the finite free of $R$.

Let $R$ be a set. Then $\operatorname{IsPointwiseRightKanExtension}$ holds for $\operatorname{mk}$ applied to $\operatorname{profiniteSolid}$ applied to $R$ and the profinite solid counit of $R$. Proof. Let $R$ be arbitrary. By R. By Condensed__profiniteSolid. By R. By Condensed__profiniteSolidCounit. By CategoryTheory__Functor__isPointwiseRightKanExtensionOfIsRightKanExtension.

Let $R$ be a set. Then $\operatorname{profiniteSolidification}$ applied to $R$ is a homomorphism of the profinite free of $R$ and $\operatorname{profiniteSolid}$ applied to $R$ defined as the lift of the profinite free of $R$ and the identity morphism of the composition of $\operatorname{toProfinite}$ and the profinite free of $R$.

A is solid (from the name)

Let $R$ be a set. Let $A$ be an element of $\mathrm{CondensedMod}$ applied to $R$. Then we can say that $A$ is solid.

the adjunction (from the docstring)

The adjunction is an adjunction of $\operatorname{condensedSetToCompactlyGenerated}$ and $\operatorname{compactlyGeneratedToCondensedSet}$ defined as $\operatorname{restrictFullyFaithful}$ applied to the adjunction, the identity functor of the set of condensed sets, $\operatorname{fullyFaithfulCompactlyGeneratedToTop}$, the identity of the composition of the identity of the set of condensed sets and the condensed set to topological category and the identity of the composition of $\operatorname{compactlyGeneratedToTop}$ and the topological category to condensed set.

the counit of the adjunction of X (from the docstring)

Let $X$ be a topological category. Then the counit of the adjunction of $X$ is a homeomorphism of the set of carriers of the topological category of the condensed set of $X$ and the set of carriers of $X$.

the counit of the adjunction of X (from the docstring)

Let $X$ be an element of $\mathrm{CompactlyGenerated}$. Then the counit of the adjunction of $X$ is an isomorphism of the action of $\operatorname{condensedSetToCompactlyGenerated}$ and the action of $\operatorname{compactlyGeneratedToCondensedSet}$ and $X$ and $X$ defined as the isomorphism of the counit of the adjunction of the underlying topological space of $X$.

$\operatorname{compactlyGeneratedToCondensedSet}$ is a functor of $\mathrm{CompactlyGenerated}$ and the set of condensed sets defined as the composition of $\operatorname{compactlyGeneratedToTop}$ and the topological category to condensed set.

$\operatorname{condensedSetToCompactlyGenerated}$ is a functor of the set of condensed sets and $\mathrm{CompactlyGenerated}$.

$\operatorname{fullyFaithfulCompactlyGeneratedToCondensedSet}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{compactlyGeneratedToCondensedSet}$ defined as $\operatorname{fullyFaithfulROfIsIsoCounit}$ applied to the adjunction.

the topological category of X (from the name)

Let $X$ be a condensed set. Then the topological category of $X$ is a topological category defined as $\operatorname{of}$ applied to the action of the object of $X$ and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $\mathrm{PUnit}$.

the map part of the functor of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the map part of the functor of $f$ is a homomorphism of the topological category of $X$ and the topological category of $Y$.

the adjunction (from the docstring)

The adjunction is an adjunction of the condensed set to topological category and the topological category to condensed set.

the counit of the adjunction of X (from the docstring)

Let $X$ be a topological category. Then the counit of the adjunction of $X$ is a homomorphism of the topological category of the condensed set of $X$ and $X$.

the counit of the adjunction of X (from the docstring)

Let $X$ be a topological category. Then the counit of the adjunction of $X$ is an equivalence from the set of carriers of the topological category of the condensed set of $X$ to the set of carriers of $X$.

the unit of the adjunction of X (from the docstring)

Let $X$ be a condensed set. Then the unit of the adjunction of $X$ is a homomorphism of $X$ and the condensed set of the topological category of $X$.

the condensed set to topological category (from the name)

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

the condensed set of X (from the name)

Let $X$ be a topological category. Then the condensed set of $X$ is a condensed set.

Let $P$ be a function from topological categories to propositions. Let $X$ be a topological category. Assume that for all elements $X_{1}$ and $Y$ of $\mathrm{CompHausLike}$ applied to $P$, for all homomorphisms $f$ of $X_{1}$ and $Y$, if $f$ is an effective epimorphism, then $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then $\operatorname{toSheafCompHausLike}$ applied to $P$, $X$ and $\mathrm{hs}$ is a sheaf of the coherent topology of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets.

the topological category to condensed set (from the name)

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

Let $P$ be a function from topological categories to propositions such that for all elements $X$ and $Y$ of $\mathrm{CompHausLike}$ applied to $P$, for all homomorphisms $f$ of $X$ and $Y$, if $f$ is an effective epimorphism, then $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then $\mathrm{topCatToSheafCompHausLike}$ applied to $P$ and $\mathrm{hs}$ is a functor of the set of topological categories and the set of sheaves of the coherent topology of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets.