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.

If the predicate P is preserved under taking type-theoretic sums, we provide an explicit coproduct cocone in CompHausLike P. When we have the dual of CartesianMonoidalCategory, this can be used to provide an instance of that on CompHausLike P.

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 (CompHausLike.ofHom P { toFun := Prod.fst, continuous_toFun := ⋯ }) (CompHausLike.ofHom P { 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.

def CompHausLike.coproductCocone {P : TopCat → Prop} (X Y : CompHausLike P) [HasProp P (↑X.toTop ⊕ ↑Y.toTop)] : CategoryTheory.Limits.BinaryCofan X Y

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

Equations

• X.coproductCocone Y = CategoryTheory.Limits.BinaryCofan.mk (CompHausLike.ofHom P { toFun := Sum.inl, continuous_toFun := ⋯ }) (CompHausLike.ofHom P { toFun := Sum.inr, continuous_toFun := ⋯ })

def CompHausLike.coproductIsColimit {P : TopCat → Prop} (X Y : CompHausLike P) [HasProp P (↑X.toTop ⊕ ↑Y.toTop)] : CategoryTheory.Limits.IsColimit (X.coproductCocone Y)

When the predicate P is preserved under taking type-theoretic sums, that sum is a category-theoretic coproduct in CompHausLike P.

Equations

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