(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/ac_defs".
-
(* Project started Wed Oct 12, 2005 ***************************************)
+set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/ac_defs".
+include "coq.ma".
(* ACZEL CATEGORIES:
- We use typoids with a compatible membership relation
of the aceq predicate given inside the category. Then we prove the
properties of the equality that usually are axiomatized inside the
category structure. This makes categories easier to use
-*)
+ *)
record AC: Type \def {
ac: Type;
coercion ac.
-inductive eq (A:AC) : A \to A \to Prop \def
- | eq_refl: \forall a. acin ? a \to eq A a a.
+inductive eq (A:AC) (a:A): A \to Prop \def
+ | eq_refl: acin ? a \to eq ? a a
+ | eq_sing_r: \forall b,c.
+ eq ? a b \to acin ? c \to aceq ? b c \to eq ? a c
+ | eq_sing_l: \forall b,c.
+ eq ? a b \to acin ? c \to aceq ? c b \to eq ? a c.
+
+theorem eq_cl: \forall A,a,b. eq ? a b \to acin A a \land acin A b.
+intros; elim H; clear H; clear b;
+ [ auto | decompose H2; auto | decompose H2; auto ].
+qed.
+
+theorem eq_trans: \forall A,b,a,c.
+ eq A b c \to eq ? a b \to eq ? a c.
+intros 5; elim H; clear H; clear c;
+ [ auto
+ | apply eq_sing_r; [||| apply H4 ]; auto
+ | apply eq_sing_l; [||| apply H4 ]; auto
+ ].
+qed.
+
+theorem eq_conf_rev: \forall A,b,a,c.
+ eq A c b \to eq ? a b \to eq ? a c.
+intros 5; elim H; clear H; clear b;
+ [ auto
+ | lapply eq_cl; [ decompose Hletin |||| apply H1 ].
+ apply H2; apply eq_sing_l; [||| apply H4 ]; auto
+ | lapply eq_cl; [ decompose Hletin |||| apply H1 ].
+ apply H2; apply eq_sing_r; [||| apply H4 ]; auto
+ ].
+qed.
+
+theorem eq_sym: \forall A,a,b. eq A a b \to eq A b a.
+intros;
+lapply eq_cl; [ decompose Hletin |||| apply H ].
+auto.
+qed.
+
+theorem eq_conf: \forall A,b,a,c.
+ eq A a b \to eq ? a c \to eq ? b c.
+intros.
+lapply eq_sym; [|||| apply H ].
+apply eq_trans; [| auto | auto ].
+qed.