proposition: Lemma Prf_pb1_law2 : Pullback_law2 Fibred1_p Pb1_diese.
proof: Proof. unfold Pullback_law2, Pullback_eq1, Pullback_eq2 in |- *; intros r t1 t2 H. apply Sym; apply (Prf_limit1 l (Pulb_cone H) P1). Qed.
imports: Limit PULB Pullbacks