Theorems · Definition · category theory

CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C) →
      ((X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) →
        CategoryTheory.CartesianMonoidalCategory C

Construct an instance of CartesianMonoidalCategory C given a terminal object and limit cones over arbitrary pairs of objects.

Defined in

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Cited by

0 results in Mathlib

Foundations

Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category