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 instCartesianClosedCondensedSet : CategoryTheory.CartesianClosed CondensedSet

Equations

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