no goals
C : Type u₁
inst✝³ : Category C
J : Type u₂
inst✝² : Category J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ (PullbackCone.unop (limit.cone (cospan f.op g.op))).ι.app WalkingSpan.right = pullback.snd.unop
simp