Light condensed sets form a Cartesian closed category

@[implicit_reducible]

instance instCartesianMonoidalCategoryLightCondSet : CategoryTheory.CartesianMonoidalCategory LightCondSet

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance instMonoidalClosedLightCondSet : CategoryTheory.MonoidalClosed LightCondSet

Equations

• instMonoidalClosedLightCondSet = { closed := instMonoidalClosedLightCondSet._aux_1 }