proposition: Lemma Equal_PA_mor_Equiv : forall x y : PA_ob, Equivalence (Equal_PA_mor (x:=x) (y:=y)).
proof: Proof. intros x y; apply Build_Equivalence; [ red in |- * | apply Build_Partial_equivalence; red in |- * ]. intro f; elim f. simpl in |- *; trivial. simpl in |- *; trivial. intro i; simpl in |- *; apply Refl. intros f; elim f. intros g h e1 e2. apply (PA_11_ind (P:=fun h : PA_mor PA1 PA1 => Equal_PA_mor PA_I1 h)). simpl in |- *; trivial. intros g h e1 e2. apply (PA_22_ind (P:=fun h : PA_mor PA2 PA2 => Equal_PA_mor PA_I2 h)). simpl in |- *; trivial. intros i g h. lapply (PA_12_ind (P:=fun x : PA_mor PA1 PA2 => Equal_PA_mor (PA_f i) x -> Equal_PA_mor x h -> Equal_PA_mor (PA_f i) h)). intros H H0 H1; apply (H g H0 H1). intro j; unfold Equal_PA_mor at 1 in |- *; intro eqij. lapply (PA_12_ind (P:=fun x : PA_mor PA1 PA2 => Equal_PA_mor (PA_f j) x -> Equal_PA_mor (PA_f i) x)). intros H H0; apply (H h H0). simpl in |- *; intros l eqjl. apply Trans with (k j); trivial. intros f; elim f. intros g e1. apply (PA_11_ind (P:=fun g : PA_mor PA1 PA1 => Equal_PA_mor g PA_I1)). simpl in |- *; trivial. intros g e1. apply (PA_22_ind (P:=fun g : PA_mor PA2 PA2 => Equal_PA_mor g PA_I2)). simpl in |- *; trivial. intros i g. lapply (PA_12_ind (P:=fun g : PA_mor PA1 PA2 => Equal_PA_mor (PA_f i) g -> Equal_PA_mor g (PA_f i))). intros H H0; apply (H g H0). intro j; simpl in |- *; intro eqij; apply Sym; trivial. Qed.
imports: BasicTypes Category