Theorems · Theorem · category theory

TopPair.Homotopy.w_apply

∀ {X Y : TopPair} {f g : X ⟶ Y} (self : TopPair.Homotopy f g)
  (x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj TopPair.snd TopCat.I)),
  self.fst (TopCat.I.homeomorph x.2, (CategoryTheory.ConcreteCategory.hom TopPair.map) x.1) =
    (CategoryTheory.ConcreteCategory.hom TopPair.map) (self.snd (TopCat.I.homeomorph x.2, x.1))

The proof that the homotopies fit into a commutative square with the maps of the pairs.

Defined in

Mathlib.Topology.Category.TopPair

Cited by

1 results in Mathlib

Foundations

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