Theorems · Theorem · category theory

TopPair.Homotopy.mk.inj

∀ {X Y : TopPair} {f g : X ⟶ Y} {fst : TopCat.Homotopy (TopPair.Hom.fst f) (TopPair.Hom.fst g)}
  {snd : TopCat.Homotopy (TopPair.Hom.snd f) (TopPair.Hom.snd g)}
  {w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight TopPair.map TopCat.I)
          fst.h =
        CategoryTheory.CategoryStruct.comp snd.h TopPair.map)
      TopPair.Homotopy.w._autoParam}
  {fst_1 : TopCat.Homotopy (TopPair.Hom.fst f) (TopPair.Hom.fst g)}
  {snd_1 : TopCat.Homotopy (TopPair.Hom.snd f) (TopPair.Hom.snd g)}
  {w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight TopPair.map TopCat.I)
          fst_1.h =
        CategoryTheory.CategoryStruct.comp snd_1.h TopPair.map)
      TopPair.Homotopy.w._autoParam},
  { fst := fst, snd := snd, w := w } = { fst := fst_1, snd := snd_1, w := w_1 } → fst = fst_1 ∧ snd = snd_1

Defined in

Mathlib.Topology.Category.TopPair

Cited by

1 results in Mathlib

Foundations

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