proposition: Lemma Fpulb_comp_law : Fcomp_law Fpulb_map.
proof: Proof. unfold Fcomp_law in |- *; simpl in |- *; intros x y z h1. elim h1; simpl in |- *. elim z; intro h2. simpl in |- *; lapply (PULB_11_ind (P:=fun t : PULB_mor P1 P1 => Id a =_S Id a o Fpulb_mor t)). intro H; apply (H h2). simpl in |- *; apply Idr. simpl in |- *; lapply (PULB_12_ind (P:=fun t : PULB_mor P1 P2 => f =_S Id a o Fpulb_mor t)). intro H; apply (H h2). simpl in |- *; apply Idl1. apply (PULB_13_ind (fun t : PULB_mor P1 P3 => Fpulb_mor (Comp_PULB_mor IP1 h2) =_S Id a o Fpulb_mor h2) h2). elim z; intro h2. apply (PULB_21_ind (fun a : PULB_mor P2 P1 => Fpulb_mor (Comp_PULB_mor IP2 h2) =_S Id b o Fpulb_mor h2) h2). simpl in |- *; lapply (PULB_22_ind (P:=fun t : PULB_mor P2 P2 => Id b =_S Id b o Fpulb_mor t)). intro H; apply (H h2). simpl in |- *; apply Idr. apply (PULB_23_ind (fun a : PULB_mor P2 P3 => Fpulb_mor (Comp_PULB_mor IP2 h2) =_S Id b o Fpulb_mor h2) h2). elim z; intro h2. apply (PULB_31_ind (fun a : PULB_mor P3 P1 => Fpulb_mor (Comp_PULB_mor IP3 h2) =_S Id c o Fpulb_mor h2) h2). simpl in |- *; apply (PULB_32_ind (P:=fun a : PULB_mor P3 P2 => g =_S Id c o Fpulb_mor a)). simpl in |- *; apply Idl1. simpl in |- *; lapply (PULB_33_ind (P:=fun t : PULB_mor P3 P3 => Id c =_S Id c o Fpulb_mor t)). intro H; apply (H h2). simpl in |- *; apply Idr. elim z; intro h2. apply (PULB_21_ind (fun a : PULB_mor P2 P1 => Fpulb_mor (Comp_PULB_mor F12 h2) =_S f o Fpulb_mor h2) h2). simpl in |- *; lapply (PULB_22_ind (P:=fun t : PULB_mor P2 P2 => f =_S f o Fpulb_mor t)). intro H; apply (H h2). simpl in |- *; apply Idr. apply (PULB_23_ind (fun a : PULB_mor P2 P3 => Fpulb_mor (Comp_PULB_mor F12 h2) =_S f o Fpulb_mor h2) h2). elim z; intro h2. apply (PULB_21_ind (fun a : PULB_mor P2 P1 => Fpulb_mor (Comp_PULB_mor F32 h2) =_S g o Fpulb_mor h2) h2). simpl in |- *; lapply (PULB_22_ind (P:=fun t : PULB_mor P2 P2 => g =_S g o Fpulb_mor t)). intro H; apply (H h2). simpl in |- *; apply Idr. apply (PULB_23_ind (fun a : PULB_mor P2 P3 => Fpulb_mor (Comp_PULB_mor F32 h2) =_S g o Fpulb_mor h2) h2). Qed.
imports: Limit PULB Pullbacks