proposition: Lemma FPA_map_law : forall x y : PA_ob, Map_law (FPA_mor (x:=x) (y:=y)).
proof: Proof. unfold Map_law in |- *; simpl in |- *. intros x y f; elim f. simpl in |- *; intros g H; apply (PA_11_ind (P:=fun x : PA_mor_setoid k PA1 PA1 => Id a =_S FPA_mor x)). simpl in |- *; apply Refl. simpl in |- *; intros g H; apply (PA_22_ind (P:=fun x' : PA_mor_setoid k PA2 PA2 => Id b =_S FPA_mor x')). simpl in |- *; apply Refl. intros i g; lapply (PA_12_ind (P:=fun x' : PA_mor_setoid k PA1 PA2 => Equal_PA_mor k (PA_f i) x' -> k i =_S FPA_mor x')). intros H H0; apply (H g H0). simpl in |- *; auto. Qed.
imports: Equalizers PA Limit