[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Quiver.IsThin C
X Y : C
⊢ ∀ (a b : X ≅ Y), a = b
[PROOFSTEP]
intro i₁ i₂
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Quiver.IsThin C
X Y : C
i₁ i₂ : X ≅ Y
⊢ i₁ = i₂
[PROOFSTEP]
ext1
[GOAL]
case w
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Quiver.IsThin C
X Y : C
i₁ i₂ : X ≅ Y
⊢ i₁.hom = i₂.hom
[PROOFSTEP]
apply Subsingleton.elim
