Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        [inst_3 : CategoryTheory.MonoidalClosed C] →
          (X : CategoryTheory.Arrow C) →
            {T : C} →
              (t : CategoryTheory.Limits.IsTerminal T) →
                {W : C} →
                  (Opposite.op X ⋔ CategoryTheory.Arrow.mk (t.from W)) ≅
                    CategoryTheory.Arrow.mk ((CategoryTheory.MonoidalClosed.pre X.hom).app W)

The arrow isomorphism (f : A ⟶ B) ⋔ (W ⟶ ⋆) ≅ (B ⟹ W ⟶ A ⟹ W) in a monoidal closed category with pullbacks and a terminal object.

Defined in

Mathlib.CategoryTheory.Monoidal.PushoutProduct

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbacksCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalClosed