first constructions with classes

[helm.git] / matita / matita / contribs / limits / u0_class.ma

diff --git a/matita/matita/contribs/limits/u0_class.ma b/matita/matita/contribs/limits/u0_class.ma
index 49c715a01dd08dc622cce4f183707468f9a6af79..37168bb821a1f30438179580275ce8e79f32b339 100644 (file)
--- a/matita/matita/contribs/limits/u0_class.ma
+++ b/matita/matita/contribs/limits/u0_class.ma
@@ -12,9 +12,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "u0_predicates.ma".
+include "notation/equiv_3.ma".
+include "u0_preds.ma".
+include "u0_apps.ma".
 
-(* CLASSES ************************************************************)
+(* CLASS **************************************************************)
+(* - a class is defined as a category in the sense of Per Martin-Lof 
+   - a membership predicate defines the domain of the category
+   - an equivalence relation on the domain defines equality in the category 
+   - a function between classes is an application respecting
+   -   both membership and equality
+*)
 
 record u0_class: Type[1] ≝ {
    u0_class_t :> Type[0];
@@ -22,13 +30,41 @@ record u0_class: Type[1] ≝ {
    u0_class_eq:  u0_predicate2 u0_class_t
 }.
 
-interpretation "u0 class membership" 'mem a C = (u0_class_in C a).
+interpretation "u0 class membership" 'mem a D = (u0_class_in D a).
 
-definition u0_class_all: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∀a. a ∈ C → P a.
+interpretation "u0 class equivalence" 'Equiv D a1 a2 = (u0_class_eq D a1 a2).
 
-definition u0_class_ex: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∃a. a ∈ C ∧ P a.
+record is_u0_class (D:u0_class): Prop ≝ {
+   u0_class_refl: u0_refl D (u0_class_in D) (u0_class_eq D);
+   u0_class_repl: u0_repl2 D (u0_class_in D) (u0_class_eq D) (u0_class_eq D)
+}.
+
+record u0_fun (D,C:u0_class): Type[0] ≝ {
+   u0_fun_a :1> D → C
+}.
 
-record is_u0_class (C:u0_class): Prop ≝ {
-   u0_class_repl1: can_u0_replace1 C (u0_class_all C) (u0_class_eq C) (u0_class_in C);
-   u0_class_refl : is_u0_reflexive C (u0_class_all C) (u0_class_eq C)
+record is_u0_fun (D,C) (f:u0_fun D C): Prop ≝ {
+   u0_fun_hom1: u0_hom1 D (u0_class_in D) C f (u0_class_in D) (u0_class_in C);
+   u0_fun_hom2: u0_hom2 D (u0_class_in D) C f (u0_class_eq D) (u0_class_eq C)
 }.
+
+definition u0_id (D): u0_fun D D ≝
+                 mk_u0_fun D D (u0_i D).
+
+(* Basic properties ***************************************************)
+
+(* auto width 7 in the next lemmas is due to automatic η expansion *)
+lemma u0_class_sym: ∀D. is_u0_class D → u0_sym D (u0_class_in D) (u0_class_eq D).
+#D #HD @u0_refl_repl_sym /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
+
+lemma u0_class_trans: ∀D. is_u0_class D → u0_trans D (u0_class_in D) (u0_class_eq D).
+#D #HD @u0_refl_repl_trans /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
+
+lemma u0_class_conf: ∀D. is_u0_class D → u0_conf D (u0_class_in D) (u0_class_eq D).
+#D #HD @u0_refl_repl_conf /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
+
+lemma u0_class_div: ∀D. is_u0_class D → u0_div D (u0_class_in D) (u0_class_eq D).
+#D #HD @u0_refl_repl_div /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
+
+lemma u0_fun_id: ∀D. is_u0_class D → is_u0_fun D D (u0_id D).
+/2 width=1 by mk_is_u0_fun/ qed.