case mp
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f✝ f g : Y ⟶ X
⊢ singleton f g → f = g

case mpr
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f✝ f g : Y ⟶ X
⊢ f = g → singleton f g
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f✝ f g : Y ⟶ X
⊢ singleton f g ↔ f = g
constructor
case mp.mk
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y✝ Z : C
f✝ f : Y✝ ⟶ X
Y : C
⊢ f = f
case mp
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f✝ f g : Y ⟶ X
⊢ singleton f g → f = g
rintro ⟨a, rfl⟩
no goals
case mp.mk
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y✝ Z : C
f✝ f : Y✝ ⟶ X
Y : C
⊢ f = f
rfl
case mpr
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f✝ f : Y ⟶ X
⊢ singleton f f
case mpr
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f✝ f g : Y ⟶ X
⊢ f = g → singleton f g
rintro rfl
no goals
case mpr
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f✝ f : Y ⟶ X
⊢ singleton f f
apply singleton.mk