C : Type u_1
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Nonempty (LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))) ↔
    Nonempty (LiftStruct sq)
C : Type u_1
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ HasLift (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v)) ↔ HasLift sq
simp only [HasLift.iff]
no goals
C : Type u_1
D : Type u_4
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Nonempty (LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))) ↔
    Nonempty (LiftStruct sq)
exact Equiv.nonempty_congr (sq.rightAdjointLiftStructEquiv adj).symm