C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (NatIso.removeOp (leftAdjointUniq (opAdjointOpOfAdjoint G F adj1) (opAdjointOpOfAdjoint G F adj1))).hom = 𝟙 G
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (rightAdjointUniq adj1 adj1).hom = 𝟙 G
delta rightAdjointUniq
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (NatIso.removeOp (leftAdjointUniq (opAdjointOpOfAdjoint G F adj1) (opAdjointOpOfAdjoint G F adj1))).hom = 𝟙 G
simp