C : Type u
inst✝² : Category C
X✝ Y✝ W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift fst snd ≫ map g g' = map g g'
C : Type u
inst✝² : Category C
X✝ Y✝ W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst ≫ g) (snd ≫ g') = map g g'
rw [← prod.lift_map]
no goals
C : Type u
inst✝² : Category C
X✝ Y✝ W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift fst snd ≫ map g g' = map g g'
simp