Condensed sets form a Cartesian closed category

instance instCartesianMonoidalCategoryCondensedSet : CategoryTheory.CartesianMonoidalCategory CondensedSet

Equations

• instCartesianMonoidalCategoryCondensedSet = inferInstanceAs (CategoryTheory.CartesianMonoidalCategory (CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) (Type (?u.5 + 1))))

instance instMonoidalClosedCondensedSet : CategoryTheory.MonoidalClosed CondensedSet

Equations

• instMonoidalClosedCondensedSet = inferInstanceAs (CategoryTheory.MonoidalClosed (CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) (Type (?u.6 + 1))))