Documentation

Mathlib.CategoryTheory.Monoidal.PushoutProduct

Leibniz constructions associated to monoidal categories. #

In a monoidal category with pushouts, the pushout-product is the Leibniz functor associated to the tensor product. This is the bifunctor of arrow categories that sends f : A ⟶ B and g : X ⟶ Y to the canonical map from the pushout of f ◁ X and A ▷ g to B ⊗ Y, induced by the following diagram:

  A ⊗ X --> B ⊗ X
     |          |
     v          v
  A ⊗ Y --> B ⊗ Y

In a monoidal closed category with pullbacks, the pullback-hom is the the Leibniz functor associated to the internal hom. This is the bifunctor of arrow categories that sends f : A ⟶ B and g : X ⟶ Y to the canonical map from B ⟹ X to the pullback of (ihom A).map g : A ⟹ X ⟶ A ⟹ Y and (pre f).app Y : B ⟹ Y ⟶ A ⟹ Y, induced by the following diagram:

  B ⟹ X --> A ⟹ X
     |          |
     v          v
  B ⟹ Y --> A ⟹ Y

In Mathlib.CategoryTheory.Monoidal.Arrow, these constructions are used to define a monoidal (closed) structure on arrow categories.

source
@[reducible, inline]
noncomputable abbrev CategoryTheory.MonoidalCategory.Arrow.pushoutProduct {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] :
Functor (Arrow C) (Functor (Arrow C) (Arrow C))

The Leibniz functor associated to the tensor product on a monoidal category. This is the bifunctor of arrow categories that sends f : A ⟶ B and g : X ⟶ Y to the canonical map from the pushout of f ◁ X and A ▷ g to B ⊗ Y, induced by the following diagram:

  A ⊗ X --> B ⊗ X
     |          |
     v          v
  A ⊗ Y --> B ⊗ Y
Equations
Instances For
    source
    def CategoryTheory.MonoidalCategory.Arrow.«term_□_» :
    Lean.TrailingParserDescr

    Notation for the pushout-product of morphisms.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev CategoryTheory.MonoidalCategory.Arrow.pullbackHom {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [MonoidalCategory C] [MonoidalClosed C] :
      Functor (Arrow C)ᵒᵖ (Functor (Arrow C) (Arrow C))

      The Leibniz functor associated to the internal hom on a monoidal closed category. This is the bifunctor of arrow categories that sends f : A ⟶ B and g : X ⟶ Y to the canonical map from B ⟹ X to the pullback of (ihom A).map g : A ⟹ X ⟶ A ⟹ Y and (pre f).app Y : B ⟹ Y ⟶ A ⟹ Y, induced by the following diagram:

        B ⟹ X --> A ⟹ X
     |          |
     v          v
  B ⟹ Y --> A ⟹ Y
      Equations
      Instances For
        source
        def CategoryTheory.MonoidalCategory.Arrow.«term_⋔_» :
        Lean.TrailingParserDescr

        Notation for the pullback-hom of morphisms.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ : Arrow C) {W : C} [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorLeft W)] :
          Arrow.mk (whiskerLeft W (X₁ □ X₂).hom) ≅ Arrow.mk (whiskerLeft W X₁.hom) □ X₂

          Left-whiskering the pushout-product of X₁ and X₂ with W : C is isomorphic to the pushout-product of W ◁ X₁ and X₂.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso_inv_right {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ : Arrow C) {W : C} [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorLeft W)] :
            (whiskerLeftIso X₁ X₂).inv.right = (MonoidalCategoryStruct.associator W X₁.right X₂.right).hom
            source
            @[simp]
            theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso_inv_left {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ : Arrow C) {W : C} [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorLeft W)] :
            (whiskerLeftIso X₁ X₂).inv.left = CategoryStruct.comp (Limits.HasColimit.isoOfNatIso (Limits.spanExt (MonoidalCategoryStruct.associator W X₁.left X₂.left).symm (MonoidalCategoryStruct.associator W X₁.right X₂.left).symm (MonoidalCategoryStruct.associator W X₁.left X₂.right).symm ⋯ ⋯)).inv ⋯.isoPushout.inv
            source
            @[simp]
            theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso_hom_left {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ : Arrow C) {W : C} [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorLeft W)] :
            (whiskerLeftIso X₁ X₂).hom.left = CategoryStruct.comp ⋯.isoPushout.hom (Limits.HasColimit.isoOfNatIso (Limits.spanExt (MonoidalCategoryStruct.associator W X₁.left X₂.left).symm (MonoidalCategoryStruct.associator W X₁.right X₂.left).symm (MonoidalCategoryStruct.associator W X₁.left X₂.right).symm ⋯ ⋯)).hom
            source
            @[simp]
            theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso_hom_right {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ : Arrow C) {W : C} [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorLeft W)] :
            (whiskerLeftIso X₁ X₂).hom.right = (MonoidalCategoryStruct.associator W X₁.right X₂.right).inv
            source
            noncomputable def CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ : Arrow C) {W : C} [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight W)] :
            Arrow.mk (whiskerRight (X₁ □ X₂).hom W) ≅ X₁ □ Arrow.mk (whiskerRight X₂.hom W)

            Right-whiskering the pushout-product of X₁ and X₂ with W : C is isomorphic to the pushout-product of X₁ and X₂ ▷ W.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso_hom_right {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ : Arrow C) {W : C} [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight W)] :
              (whiskerRightIso X₁ X₂).hom.right = (MonoidalCategoryStruct.associator X₁.right X₂.right W).hom
              source
              @[simp]
              theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso_inv_right {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ : Arrow C) {W : C} [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight W)] :
              (whiskerRightIso X₁ X₂).inv.right = (MonoidalCategoryStruct.associator X₁.right X₂.right W).inv
              source
              @[simp]
              theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso_hom_left {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ : Arrow C) {W : C} [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight W)] :
              (whiskerRightIso X₁ X₂).hom.left = CategoryStruct.comp ⋯.isoPushout.hom (Limits.HasColimit.isoOfNatIso (Limits.spanExt (MonoidalCategoryStruct.associator X₁.left X₂.left W) (MonoidalCategoryStruct.associator X₁.right X₂.left W) (MonoidalCategoryStruct.associator X₁.left X₂.right W) ⋯ ⋯)).hom
              source
              @[simp]
              theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso_inv_left {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ : Arrow C) {W : C} [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight W)] :
              (whiskerRightIso X₁ X₂).inv.left = CategoryStruct.comp (Limits.HasColimit.isoOfNatIso (Limits.spanExt (MonoidalCategoryStruct.associator X₁.left X₂.left W) (MonoidalCategoryStruct.associator X₁.right X₂.left W) (MonoidalCategoryStruct.associator X₁.left X₂.right W) ⋯ ⋯)).inv ⋯.isoPushout.inv
              source
              theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.instPreservesColimitWalkingSpanSpanAppMapFunctorCurriedTensorHomLeftObjOfWhiskerRightWhiskerLeft {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X₁ X₂ : Arrow C) {F : Functor C C} [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) F] :
              Limits.PreservesColimit (Limits.span (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) F
              source
              noncomputable def CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ X₃ : Arrow C) [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight X₃.left)] [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight X₃.right)] [Limits.PreservesColimit (Limits.span (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom)) (tensorLeft X₁.left)] [Limits.PreservesColimit (Limits.span (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom)) (tensorLeft X₁.right)] :
              ((X₁ □ X₂) □ X₃) ≅ X₁ □ X₂ □ X₃

              The pushout-product is associative: (X₁ □ X₂) □ X₃ ≅ X₁ □ X₂ □ X₃.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_hom_left {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ X₃ : Arrow C) [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight X₃.left)] [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight X₃.right)] [Limits.PreservesColimit (Limits.span (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom)) (tensorLeft X₁.left)] [Limits.PreservesColimit (Limits.span (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom)) (tensorLeft X₁.right)] :
                (associator X₁ X₂ X₃).hom.left = Limits.pushout.desc (CategoryStruct.comp (MonoidalCategoryStruct.associator X₁.right X₂.right X₃.left).hom (CategoryStruct.comp (whiskerLeft X₁.right (Limits.pushout.inl (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom))) (Limits.pushout.inl (whiskerRight X₁.hom (Limits.pushout (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom))) (whiskerLeft X₁.left (⋯.desc (whiskerLeft X₂.right X₃.hom) (whiskerRight X₂.hom X₃.right) ⋯))))) (CategoryStruct.comp ⋯.isoPushout.hom (Limits.colimit.desc (Limits.span (whiskerRight (whiskerRight X₁.hom X₂.left) X₃.right) (whiskerRight (whiskerLeft X₁.left X₂.hom) X₃.right)) ((Limits.Cocone.precompose (Limits.spanExt (MonoidalCategoryStruct.associator X₁.left X₂.left X₃.right) (MonoidalCategoryStruct.associator X₁.right X₂.left X₃.right) (MonoidalCategoryStruct.associator X₁.left X₂.right X₃.right) ⋯ ⋯).hom).obj (Limits.PushoutCocone.mk (CategoryStruct.comp (whiskerLeft X₁.right (Limits.pushout.inr (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom))) (Limits.pushout.inl (whiskerRight X₁.hom (Limits.pushout (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom))) (whiskerLeft X₁.left (⋯.desc (whiskerLeft X₂.right X₃.hom) (whiskerRight X₂.hom X₃.right) ⋯)))) (Limits.pushout.inr (whiskerRight X₁.hom (Limits.pushout (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom))) (whiskerLeft X₁.left (⋯.desc (whiskerLeft X₂.right X₃.hom) (whiskerRight X₂.hom X₃.right) ⋯))) ⋯)))) ⋯
                source
                @[simp]
                theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_hom_right {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ X₃ : Arrow C) [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight X₃.left)] [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight X₃.right)] [Limits.PreservesColimit (Limits.span (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom)) (tensorLeft X₁.left)] [Limits.PreservesColimit (Limits.span (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom)) (tensorLeft X₁.right)] :
                (associator X₁ X₂ X₃).hom.right = (MonoidalCategoryStruct.associator X₁.right X₂.right X₃.right).hom
                source
                @[simp]
                theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_inv_right {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ X₃ : Arrow C) [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight X₃.left)] [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight X₃.right)] [Limits.PreservesColimit (Limits.span (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom)) (tensorLeft X₁.left)] [Limits.PreservesColimit (Limits.span (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom)) (tensorLeft X₁.right)] :
                (associator X₁ X₂ X₃).inv.right = (MonoidalCategoryStruct.associator X₁.right X₂.right X₃.right).inv
                source
                @[simp]
                theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator_inv_left {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] (X₁ X₂ X₃ : Arrow C) [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight X₃.left)] [Limits.PreservesColimit (Limits.span (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) (tensorRight X₃.right)] [Limits.PreservesColimit (Limits.span (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom)) (tensorLeft X₁.left)] [Limits.PreservesColimit (Limits.span (whiskerRight X₂.hom X₃.left) (whiskerLeft X₂.left X₃.hom)) (tensorLeft X₁.right)] :
                (associator X₁ X₂ X₃).inv.left = Limits.pushout.desc (CategoryStruct.comp ⋯.isoPushout.hom (Limits.colimit.desc (Limits.span (whiskerLeft X₁.right (whiskerRight X₂.hom X₃.left)) (whiskerLeft X₁.right (whiskerLeft X₂.left X₃.hom))) ((Limits.Cocone.precompose (Limits.spanExt (MonoidalCategoryStruct.associator X₁.right X₂.left X₃.left).symm (MonoidalCategoryStruct.associator X₁.right X₂.right X₃.left).symm (MonoidalCategoryStruct.associator X₁.right X₂.left X₃.right).symm ⋯ ⋯).hom).obj (Limits.PushoutCocone.mk (Limits.pushout.inl (whiskerRight (⋯.desc (whiskerLeft X₁.right X₂.hom) (whiskerRight X₁.hom X₂.right) ⋯) X₃.left) (whiskerLeft (Limits.pushout (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) X₃.hom)) (CategoryStruct.comp (whiskerRight (Limits.pushout.inl (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) X₃.right) (Limits.pushout.inr (whiskerRight (⋯.desc (whiskerLeft X₁.right X₂.hom) (whiskerRight X₁.hom X₂.right) ⋯) X₃.left) (whiskerLeft (Limits.pushout (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) X₃.hom))) ⋯)))) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₁.left X₂.right X₃.right).inv (CategoryStruct.comp (whiskerRight (Limits.pushout.inr (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) X₃.right) (Limits.pushout.inr (whiskerRight (⋯.desc (whiskerLeft X₁.right X₂.hom) (whiskerRight X₁.hom X₂.right) ⋯) X₃.left) (whiskerLeft (Limits.pushout (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)) X₃.hom)))) ⋯
                source
                noncomputable def CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] [BraidedCategory C] (X₁ X₂ : Arrow C) :
                (X₁ □ X₂) ≅ X₂ □ X₁

                The pushout-product is commutative: X₁ □ X₂ ≅ X₂ □ X₁.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding_hom_left {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] [BraidedCategory C] (X₁ X₂ : Arrow C) :
                  (braiding X₁ X₂).hom.left = CategoryStruct.comp (Limits.pushoutSymmetry (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)).hom (Limits.HasColimit.isoOfNatIso (Limits.spanExt (β_ X₁.left X₂.left) (β_ X₁.left X₂.right) (β_ X₁.right X₂.left) ⋯ ⋯)).hom
                  source
                  @[simp]
                  theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding_inv_right {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] [BraidedCategory C] (X₁ X₂ : Arrow C) :
                  (braiding X₁ X₂).inv.right = (β_ X₁.right X₂.right).inv
                  source
                  @[simp]
                  theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding_hom_right {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] [BraidedCategory C] (X₁ X₂ : Arrow C) :
                  (braiding X₁ X₂).hom.right = (β_ X₁.right X₂.right).hom
                  source
                  @[simp]
                  theorem CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding_inv_left {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [MonoidalCategory C] [BraidedCategory C] (X₁ X₂ : Arrow C) :
                  (braiding X₁ X₂).inv.left = CategoryStruct.comp (Limits.HasColimit.isoOfNatIso (Limits.spanExt (β_ X₁.left X₂.left) (β_ X₁.left X₂.right) (β_ X₁.right X₂.left) ⋯ ⋯)).inv (Limits.pushoutSymmetry (whiskerRight X₁.hom X₂.left) (whiskerLeft X₁.left X₂.hom)).inv
                  source
                  noncomputable def CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.rightUnitor {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] (X : Arrow C) :
                  (X □ Arrow.mk (Limits.initial.to (tensorUnit C))) ≅ X

                  If C is a CCC with pushouts and an initial object, then X □ (⊥_ C ⟶ 𝟙_ C) ≅ X.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.leftUnitor {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] [Limits.HasInitial C] [CartesianMonoidalCategory C] [MonoidalClosed C] [BraidedCategory C] (X : Arrow C) :
                    (Arrow.mk (Limits.initial.to (tensorUnit C)) □ X) ≅ X

                    If C is a braided CCC with pushouts and an initial object, then (⊥_ C ⟶ 𝟙_ C) □ X ≅ X.

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