Documentation
Mathlib
.
Condensed
.
Light
.
CartesianClosed
Search
return to top
source
Imports
Init
Mathlib.CategoryTheory.Closed.Types
Mathlib.CategoryTheory.Sites.CartesianClosed
Mathlib.CategoryTheory.Sites.Equivalence
Mathlib.Condensed.Light.Basic
Imported by
instCartesianMonoidalCategoryLightCondSet
instCartesianClosedLightCondSet
Light condensed sets form a cartesian closed category
#
source
instance
instCartesianMonoidalCategoryLightCondSet
:
CategoryTheory.CartesianMonoidalCategory
LightCondSet
Equations
instCartesianMonoidalCategoryLightCondSet
=
inferInstanceAs
(
CategoryTheory.CartesianMonoidalCategory
(
CategoryTheory.Sheaf
(
CategoryTheory.coherentTopology
LightProfinite
)
(Type
?u.5))
)
source
instance
instCartesianClosedLightCondSet
:
CategoryTheory.CartesianClosed
LightCondSet
Equations
instCartesianClosedLightCondSet
=
inferInstanceAs
(
CategoryTheory.CartesianClosed
(
CategoryTheory.Sheaf
(
CategoryTheory.coherentTopology
LightProfinite
)
(Type
?u.6))
)