C : Type u
inst✝³ : Category C
X✝ Y✝ : C
inst✝² : Category C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ desc (desc inl (inl ≫ inr)) (inr ≫ inr) ≫ map (𝟙 X) (desc (initial.to Y) (𝟙 Y)) =
    map (desc (𝟙 X) (initial.to X)) (𝟙 Y)
C : Type u
inst✝³ : Category C
X✝ Y✝ : C
inst✝² : Category C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial 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✝² : Category C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inl ≫ desc (desc inl (inl ≫ inr)) (inr ≫ inr) ≫ map (𝟙 X) (desc (initial.to Y) (𝟙 Y)) =
    inl ≫ map (desc (𝟙 X) (initial.to X)) (𝟙 Y)

case h₂
C : Type u
inst✝³ : Category C
X✝ Y✝ : C
inst✝² : Category C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inr ≫ desc (desc inl (inl ≫ inr)) (inr ≫ inr) ≫ map (𝟙 X) (desc (initial.to Y) (𝟙 Y)) =
    inr ≫ map (desc (𝟙 X) (initial.to X)) (𝟙 Y)
C : Type u
inst✝³ : Category C
X✝ Y✝ : C
inst✝² : Category C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ desc (desc inl (inl ≫ inr)) (inr ≫ inr) ≫ map (𝟙 X) (desc (initial.to Y) (𝟙 Y)) =
    map (desc (𝟙 X) (initial.to X)) (𝟙 Y)
apply coprod.hom_ext
case h₂
C : Type u
inst✝³ : Category C
X✝ Y✝ : C
inst✝² : Category C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inr ≫ desc (desc inl (inl ≫ inr)) (inr ≫ inr) ≫ map (𝟙 X) (desc (initial.to Y) (𝟙 Y)) =
    inr ≫ map (desc (𝟙 X) (initial.to X)) (𝟙 Y)
case h₁
C : Type u
inst✝³ : Category C
X✝ Y✝ : C
inst✝² : Category C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inl ≫ desc (desc inl (inl ≫ inr)) (inr ≫ inr) ≫ map (𝟙 X) (desc (initial.to Y) (𝟙 Y)) =
    inl ≫ map (desc (𝟙 X) (initial.to X)) (𝟙 Y)

case h₂
C : Type u
inst✝³ : Category C
X✝ Y✝ : C
inst✝² : Category C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inr ≫ desc (desc inl (inl ≫ inr)) (inr ≫ inr) ≫ map (𝟙 X) (desc (initial.to Y) (𝟙 Y)) =
    inr ≫ map (desc (𝟙 X) (initial.to X)) (𝟙 Y)
simp
no goals
case h₂
C : Type u
inst✝³ : Category C
X✝ Y✝ : C
inst✝² : Category C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ inr ≫ desc (desc inl (inl ≫ inr)) (inr ≫ inr) ≫ map (𝟙 X) (desc (initial.to Y) (𝟙 Y)) =
    inr ≫ map (desc (𝟙 X) (initial.to X)) (𝟙 Y)
simp