[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : HasZeroObject C
X Y : C
⊢ Unique (X ⟶ Y)
[PROOFSTEP]
haveI : HasInitial C := HasZeroObject.hasInitial
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ Unique (X ⟶ Y)
[PROOFSTEP]
apply uniqueHomsetOfInitialIsoTerminal _ X Y
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ ⊥_ C ≅ ⊤_ C
[PROOFSTEP]
refine' ⟨default, (default : ⊤_ C ⟶ 0) ≫ default, _, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ default ≫ default ≫ default = 𝟙 (⊥_ C)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteProducts C
inst✝¹ : CartesianClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ (default ≫ default) ≫ default = 𝟙 (⊤_ C)
[PROOFSTEP]
simp
