C : Type u
inst✝² : Category C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ lift (fst ≫ fst) (lift (fst ≫ snd) snd) ≫ map (𝟙 X) snd = map fst (𝟙 Y)
C : Type u
inst✝² : Category C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ (associator X (⊤_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = map (rightUnitor X).hom (𝟙 Y)
dsimp
case h₁
C : Type u
inst✝² : Category C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ (lift (fst ≫ fst) (lift (fst ≫ snd) snd) ≫ map (𝟙 X) snd) ≫ fst = map fst (𝟙 Y) ≫ fst

case h₂
C : Type u
inst✝² : Category C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ (lift (fst ≫ fst) (lift (fst ≫ snd) snd) ≫ map (𝟙 X) snd) ≫ snd = map fst (𝟙 Y) ≫ snd
C : Type u
inst✝² : Category C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ lift (fst ≫ fst) (lift (fst ≫ snd) snd) ≫ map (𝟙 X) snd = map fst (𝟙 Y)
apply prod.hom_ext
case h₂
C : Type u
inst✝² : Category C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ (lift (fst ≫ fst) (lift (fst ≫ snd) snd) ≫ map (𝟙 X) snd) ≫ snd = map fst (𝟙 Y) ≫ snd
case h₁
C : Type u
inst✝² : Category C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ (lift (fst ≫ fst) (lift (fst ≫ snd) snd) ≫ map (𝟙 X) snd) ≫ fst = map fst (𝟙 Y) ≫ fst

case h₂
C : Type u
inst✝² : Category C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ (lift (fst ≫ fst) (lift (fst ≫ snd) snd) ≫ map (𝟙 X) snd) ≫ snd = map fst (𝟙 Y) ≫ snd
simp
no goals
case h₂
C : Type u
inst✝² : Category C
X✝ Y✝ : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ (lift (fst ≫ fst) (lift (fst ≫ snd) snd) ≫ map (𝟙 X) snd) ≫ snd = map fst (𝟙 Y) ≫ snd
simp