proposition: Lemma FPA_comp_law : Fcomp_law FPA_map.
proof: Proof. unfold Fcomp_law in |- *. intros x y z f; elim f. intro g. apply Trans with (FPA_map _ _ g). apply Pres1. apply (Comp_PA_fact1 k (PA_I1 I) g). simpl in |- *; apply Idl1. intro g. apply Trans with (FPA_map _ _ g). apply Pres1. apply (Comp_PA_fact2 k (PA_I2 I) g). simpl in |- *; apply Idl1. intro i; elim z; intro g. apply (PA_21_ind (fun x' : PA_mor I PA2 PA1 => FPA_mor (Comp_PA_mor (PA_f i) g) =_S k i o FPA_mor g) g). simpl in |- *. apply (PA_22_ind (P:=fun x : PA_mor I PA2 PA2 => k i =_S k i o FPA_mor x)). simpl in |- *; apply Idr. Qed.
imports: Equalizers PA Limit