C : Type u_1
inst✝ : Category C
A✝ B✝ B' X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Y.unop ⟶ B.unop
g : X.unop ⟶ A.unop
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift (_ : CommSq g.op i.unop.op p.unop.op f.op)
C : Type u_1
inst✝ : Category C
A✝ B✝ B' X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Y.unop ⟶ B.unop
g : X.unop ⟶ A.unop
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift sq
rw [CommSq.HasLift.iff_op]
C : Type u_1
inst✝ : Category C
A✝ B✝ B' X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Y.unop ⟶ B.unop
g : X.unop ⟶ A.unop
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift (_ : CommSq g.op i p f.op)
C : Type u_1
inst✝ : Category C
A✝ B✝ B' X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Y.unop ⟶ B.unop
g : X.unop ⟶ A.unop
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift (_ : CommSq g.op i.unop.op p.unop.op f.op)
simp only [Quiver.Hom.op_unop]
no goals
C : Type u_1
inst✝ : Category C
A✝ B✝ B' X✝ Y✝ Y' : C
i✝ : A✝ ⟶ B✝
i' : B✝ ⟶ B'
p✝ : X✝ ⟶ Y✝
p' : Y✝ ⟶ Y'
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Y.unop ⟶ B.unop
g : X.unop ⟶ A.unop
sq : CommSq f p.unop i.unop g
⊢ CommSq.HasLift (_ : CommSq g.op i p f.op)
infer_instance