Condensed sets form a Cartesian closed category

@[implicit_reducible]

instance instCartesianMonoidalCategoryCondensedSet : CategoryTheory.CartesianMonoidalCategory CondensedSet

Equations

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

@[implicit_reducible]

noncomputable instance instMonoidalClosedCondensedSet : CategoryTheory.MonoidalClosed CondensedSet

Equations

• instMonoidalClosedCondensedSet = { closed := instMonoidalClosedCondensedSet._aux_1 }