Light condensed sets form a Cartesian closed category

instance instCartesianMonoidalCategoryLightCondSet : CategoryTheory.CartesianMonoidalCategory LightCondSet

Equations

• instCartesianMonoidalCategoryLightCondSet = inferInstanceAs (CategoryTheory.CartesianMonoidalCategory (CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) (Type ?u.5)))

instance instCartesianClosedLightCondSet : CategoryTheory.CartesianClosed LightCondSet

Equations

• instCartesianClosedLightCondSet = inferInstanceAs (CategoryTheory.CartesianClosed (CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) (Type ?u.6)))