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) ↔ Nonempty (LiftStruct (_ : CommSq g.op p.op i.op f.op))
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 ↔ HasLift (_ : CommSq g.op p.op i.op f.op)
rw [iff, iff]
no goals
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) ↔ Nonempty (LiftStruct (_ : CommSq g.op p.op i.op f.op))
exact Nonempty.congr (LiftStruct.opEquiv sq).toFun (LiftStruct.opEquiv sq).invFun