proposition: Lemma Pulb_cone_law : Cone_law Pulb_tau.
proof: Proof. unfold Cone_law in |- *; intros x x1 t. elim t; simpl in |- *; unfold FMor at 1 in |- *; simpl in |- *. apply Trans with (t1 o Id (G P1)). apply Idr. apply Comp_l; apply (FId1 G P1). apply Trans with ((t1 o FMor G F12) o Id (G P2)). apply Idr. apply Comp_l; apply (FId1 G P2). apply Trans with (t2 o Id (G P3)). apply Idr. apply Comp_l; apply (FId1 G P3). apply Refl. apply H. Qed.
imports: Limit PULB Pullbacks