case mp
C : Type u_1
inst✝ : Category C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ HasLift sq → Nonempty (LiftStruct sq)

case mpr
C : Type u_1
inst✝ : Category C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty (LiftStruct sq) → HasLift sq
C : Type u_1
inst✝ : Category C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ HasLift sq ↔ Nonempty (LiftStruct sq)
constructor
no goals
case mp
C : Type u_1
inst✝ : Category C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ HasLift sq → Nonempty (LiftStruct sq)

case mpr
C : Type u_1
inst✝ : Category C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty (LiftStruct sq) → HasLift sq
exacts [fun h => h.exists_lift, fun h => mk h]