(* *)
(**************************************************************************)
-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 *)
-(* The category is intended to be the domain of the membership relation *)
-(* The membership relation is necessary because we need to regard the *)
-(* domain of a propositional function (ie a subset in the predicative *)
-(* setting) as a quantification domain and therefore as a category, but *)
-(* there is no type in CIC representing the domain of a propositional *)
-(* function *)
+(* ACZEL CATEGORIES:
+ - We use typoids with a compatible membership relation
+ - The category is intended to be the domain of the membership relation
+ - The membership relation is necessary because we need to regard the
+ domain of a propositional function (ie a predicative subset) as a
+ quantification domain and therefore as a category, but there is no
+ type in CIC representing the domain of a propositional function
+ - We set up a single equality predicate, parametric on the category,
+ defined as the reflexive, symmetic, transitive and compatible closure
+ 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;
aceq: ac \to ac \to Prop
}.
-definition a \def \lambda A. ac A.
+coercion ac.
+
+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.
-coercion a.
+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.
-inductive eq (A:AC) : ac A \to ac A \to Prop \def
- | eq_refl: \forall a. acin ? a \to eq A a a.
+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.