Documentation
Mathlib
.
Condensed
.
Light
.
CartesianClosed
Search
Google site search
return to top
source
Imports
Init
Mathlib.CategoryTheory.Closed.Types
Mathlib.CategoryTheory.Sites.CartesianClosed
Mathlib.Condensed.Light.Limits
Imported by
instCartesianClosedLightCondSet
Light condensed sets form a cartesian closed category
#
source
instance
instCartesianClosedLightCondSet
:
CategoryTheory.CartesianClosed
LightCondSet
Equations
instCartesianClosedLightCondSet
=
inferInstanceAs
(
CategoryTheory.CartesianClosed
(
CategoryTheory.Sheaf
(
CategoryTheory.coherentTopology
LightProfinite
)
(Type
?u.7))
)