Documentation

Mathlib.Condensed.Light.CartesianClosed

Light condensed sets form a Cartesian closed category #

source
🔸 coverage
@[implicit_reducible]
instance instCartesianMonoidalCategoryLightCondSet :
CategoryTheory.CartesianMonoidalCategory LightCondSet
source
🔸 coverage
@[implicit_reducible]
noncomputable instance instMonoidalClosedLightCondSet :
CategoryTheory.MonoidalClosed LightCondSet