Cartesian monoidal structure on CompHausLike

If the predicate P is preserved under taking type-theoretic products and PUnit satisfies it, then CompHausLike P is a cartesian monoidal category.

def CompHausLike.productCone {P : TopCat → Prop} (X Y : CompHausLike P) [HasProp P (↑X.toTop × ↑Y.toTop)] : CategoryTheory.Limits.BinaryFan X Y

Explicit binary fan in CompHausLike P, given that the predicate P is preserved under taking type-theoretic products.

Equations

• X.productCone Y = CategoryTheory.Limits.BinaryFan.mk (TopCat.ofHom { toFun := Prod.fst, continuous_toFun := ⋯ }) (TopCat.ofHom { toFun := Prod.snd, continuous_toFun := ⋯ })

def CompHausLike.productIsLimit {P : TopCat → Prop} (X Y : CompHausLike P) [HasProp P (↑X.toTop × ↑Y.toTop)] : CategoryTheory.Limits.IsLimit (X.productCone Y)

When the predicate P is preserved under taking type-theoretic products, that product is a category-theoretic product in CompHausLike P.

Equations

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

def CompHausLike.cartesianMonoidalCategory {P : TopCat → Prop} [∀ (X Y : CompHausLike P), HasProp P (↑X.toTop × ↑Y.toTop)] [HasProp P PUnit.{u + 1}] : CategoryTheory.CartesianMonoidalCategory (CompHausLike P)

When the predicate P is preserved under taking type-theoretic products and PUnit satisfies it, then CompHausLike P is a cartesian monoidal category.

This could be an instance but that causes some slowness issues with typeclass search, therefore we keep it as a def and turn it on as an instance for the explicit examples of CompHausLike as needed.

Equations

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