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✝
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.unop p.unop i.unop f.unop))
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✝
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.unop p.unop i.unop f.unop)
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✝
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.unop p.unop i.unop f.unop))
exact Nonempty.congr (LiftStruct.unopEquiv sq).toFun (LiftStruct.unopEquiv sq).invFun