Light condensed sets form a cartesian closed category

instance instChosenFiniteProductsLightCondSet : CategoryTheory.ChosenFiniteProducts LightCondSet

Equations

• instChosenFiniteProductsLightCondSet = inferInstanceAs (CategoryTheory.ChosenFiniteProducts (CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) (Type ?u.6)))

instance instCartesianClosedLightCondSet : CategoryTheory.CartesianClosed LightCondSet

Equations

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