matita/matita/contribs/limits/u0_class.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "notation/equiv_3.ma".
  16 include "u0_preds.ma".
  17 include "u0_apps.ma".
  18
  19 (* CLASS **************************************************************)
  20 (* - a class is defined as a category in the sense of Per Martin-Lof
  21    - a membership predicate defines the domain of the category
  22    - an equivalence relation on the domain defines equality in the category
  23    - a function between classes is an application respecting
  24    -   both membership and equality
  25 *)
  26
  27 record u0_class: Type[1] ≝ {
  28    u0_class_t :> Type[0];
  29    u0_class_in:  u0_predicate1 u0_class_t;
  30    u0_class_eq:  u0_predicate2 u0_class_t
  31 }.
  32
  33 interpretation "u0 class membership" 'mem a D = (u0_class_in D a).
  34
  35 interpretation "u0 class equivalence" 'Equiv D a1 a2 = (u0_class_eq D a1 a2).
  36
  37 record is_u0_class (D:u0_class): Prop ≝ {
  38    u0_class_refl: u0_refl D (u0_class_in D) (u0_class_eq D);
  39    u0_class_repl: u0_repl2 D (u0_class_in D) (u0_class_eq D) (u0_class_eq D)
  40 }.
  41
  42 record u0_fun (D,C:u0_class): Type[0] ≝ {
  43    u0_fun_a :1> D → C
  44 }.
  45
  46 record is_u0_fun (D,C) (f:u0_fun D C): Prop ≝ {
  47    u0_fun_hom1: u0_hom1 D (u0_class_in D) C f (u0_class_in D) (u0_class_in C);
  48    u0_fun_hom2: u0_hom2 D (u0_class_in D) C f (u0_class_eq D) (u0_class_eq C)
  49 }.
  50
  51 definition u0_id (D): u0_fun D D ≝
  52                  mk_u0_fun D D (u0_i D).
  53
  54 (* Basic properties ***************************************************)
  55
  56 (* auto width 7 in the next lemmas is due to automatic η expansion *)
  57 lemma u0_class_sym: ∀D. is_u0_class D → u0_sym D (u0_class_in D) (u0_class_eq D).
  58 #D #HD @u0_refl_repl_sym /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
  59
  60 lemma u0_class_trans: ∀D. is_u0_class D → u0_trans D (u0_class_in D) (u0_class_eq D).
  61 #D #HD @u0_refl_repl_trans /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
  62
  63 lemma u0_class_conf: ∀D. is_u0_class D → u0_conf D (u0_class_in D) (u0_class_eq D).
  64 #D #HD @u0_refl_repl_conf /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
  65
  66 lemma u0_class_div: ∀D. is_u0_class D → u0_div D (u0_class_in D) (u0_class_eq D).
  67 #D #HD @u0_refl_repl_div /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
  68
  69 lemma u0_fun_id: ∀D. is_u0_class D → is_u0_fun D D (u0_id D).
  70 /2 width=1 by mk_is_u0_fun/ qed.