case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x✝ : D
⊢ ((rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom).app x✝ = (rightAdjointUniq adj1 adj3).hom.app x✝
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
⊢ (rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom = (rightAdjointUniq adj1 adj3).hom
ext
no goals
case w.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x✝ : D
⊢ ((rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom).app x✝ = (rightAdjointUniq adj1 adj3).hom.app x✝
simp