Pullbacks along equal maps

When the right-hand map g' of a pullback is equal to another map g, the two pullback objects are equal, and the resulting eqToHom between them commutes with the projections (CategoryTheory.Limits.eqToHom_comp_pullback_fst and CategoryTheory.Limits.eqToHom_comp_pullback_snd). This is useful when a coherence statement involves base change along maps that agree only propositionally, such as f ≫ 𝟙 Y and f.

theorem CategoryTheory.Limits.eqToHom_comp_pullback_fst {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) {g g' : Y ⟶ Z} (e : g' = g) [HasPullback f g] [HasPullback f g'] (e' : pullback f g' = pullback f g) : CategoryStruct.comp (eqToHom e') (pullback.fst f g) = pullback.fst f g'

Rewriting the right-hand map g' of a pullback to an equal map g transports the first projection along the resulting eqToHom.

theorem CategoryTheory.Limits.eqToHom_comp_pullback_fst_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) {g g' : Y ⟶ Z} (e : g' = g) [HasPullback f g] [HasPullback f g'] (e' : pullback f g' = pullback f g) {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (eqToHom e') (CategoryStruct.comp (pullback.fst f g) h) = CategoryStruct.comp (pullback.fst f g') h

Rewriting the right-hand map g' of a pullback to an equal map g transports the first projection along the resulting eqToHom.

theorem CategoryTheory.Limits.eqToHom_comp_pullback_snd {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) {g g' : Y ⟶ Z} (e : g' = g) [HasPullback f g] [HasPullback f g'] (e' : pullback f g' = pullback f g) : CategoryStruct.comp (eqToHom e') (pullback.snd f g) = pullback.snd f g'

Rewriting the right-hand map g' of a pullback to an equal map g transports the second projection along the resulting eqToHom.

theorem CategoryTheory.Limits.eqToHom_comp_pullback_snd_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) {g g' : Y ⟶ Z} (e : g' = g) [HasPullback f g] [HasPullback f g'] (e' : pullback f g' = pullback f g) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (eqToHom e') (CategoryStruct.comp (pullback.snd f g) h) = CategoryStruct.comp (pullback.snd f g') h

Rewriting the right-hand map g' of a pullback to an equal map g transports the second projection along the resulting eqToHom.