Condensed sets form a cartesian closed category

instance instChosenFiniteProductsCondensedSet : CategoryTheory.ChosenFiniteProducts CondensedSet

Equations

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

instance instCartesianClosedCondensedSet : CategoryTheory.CartesianClosed CondensedSet

Equations

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