proposition: Lemma Fpulb_map_law : forall x y : PULB_ob, Map_law (Fpulb_mor (x:=x) (y:=y)).
proof: Proof. unfold Map_law in |- *; intros x y h1. elim h1; simpl in |- *. intro h2; lapply (PULB_11_ind (P:=fun t : PULB_mor P1 P1 => Equal_PULB_mor IP1 t -> Id a =_S Fpulb_mor t)). intros H H0; apply (H h2 H0). intro H; simpl in |- *; apply Refl. intro h2; lapply (PULB_22_ind (P:=fun t : PULB_mor P2 P2 => Equal_PULB_mor IP2 t -> Id b =_S Fpulb_mor t)). intros H H0; apply (H h2 H0). intro H; simpl in |- *; apply Refl. intro h2; lapply (PULB_33_ind (P:=fun t : PULB_mor P3 P3 => Equal_PULB_mor IP3 t -> Id c =_S Fpulb_mor t)). intros H H0; apply (H h2 H0). intro H; simpl in |- *; apply Refl. intro h2; lapply (PULB_12_ind (P:=fun t : PULB_mor P1 P2 => Equal_PULB_mor F12 t -> f =_S Fpulb_mor t)). intros H H0; apply (H h2 H0). intro H; simpl in |- *; apply Refl. intro h2; lapply (PULB_32_ind (P:=fun t : PULB_mor P3 P2 => Equal_PULB_mor F32 t -> g =_S Fpulb_mor t)). intros H H0; apply (H h2 H0). intro H; simpl in |- *; apply Refl. Qed.
imports: Limit PULB Pullbacks