proposition: Lemma F_pres_weak_pullback_arr: forall (X Y Z:Set) (f:X->Z) (g:Y->Z) (wxy:weak_pullback _ _ _ (lift_F_ _ _ f) (lift_F_ _ _ g)), lift_F_ (weak_pullback _ _ _ f g) X (fun xy=>fst (proj1_sig xy)) (wkpk_id_rht _ _ _ _ _ wxy) = fst (proj1_sig wxy) /\ lift_F_ (weak_pullback _ _ _ f g) Y (fun xy=>snd (proj1_sig xy)) (wkpk_id_rht _ _ _ _ _ wxy) = snd (proj1_sig wxy).
proof: Proof. intros X Y Z f g [[[b0 x] [b1 y]] h]. simpl in h. unfold wkpk_id_rht. unfold lift_F_. simpl; split; trivial. f_equal. change (fst (b0, f x) = fst (b1, g y)). rewrite h; reflexivity. Qed.
imports: WeaklyFinalCoalgebra