helm/software/matita/nlibrary/sets/setoids.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 "logic/connectives.ma".
  16 include "properties/relations.ma".
  17
  18 nrecord setoid : Type[1] ≝
  19  { carr:> Type;
  20    eq: carr → carr → CProp;
  21    refl: reflexive ? eq;
  22    sym: symmetric ? eq;
  23    trans: transitive ? eq
  24  }.
  25
  26 ndefinition proofs: CProp → setoid.
  27 #P; napply (mk_setoid ?????);
  28 ##[ napply P;
  29 ##| #x; #y; napply True;
  30 ##|##*: nwhd; nrepeat (#_); napply I;
  31 ##]
  32 nqed.
  33
  34 nrecord function_space (A,B: setoid): Type ≝
  35  { f:1> A → B;
  36    f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a'))
  37  }.
  38
  39 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
  40 (*
  41 ndefinition function_space_setoid: setoid → setoid → setoid.
  42  #A; #B; napply (mk_setoid ?????);
  43 ##[ napply (function_space A B);
  44 ##| #f; #f1; napply (∀a:A. proofs (eq ? (f a) (f1 a)));
  45 ##| nwhd; #x; #a;
  46     napply (f_ok ? ? x ? ? ?); (* QUI!! *)
  47     unfold carr; unfold proofs; simplify;
  48     apply (refl A)
  49   | simplify;
  50     intros;
  51     unfold carr; unfold proofs; simplify;
  52     apply (sym B);
  53     apply (f a)
  54   | simplify;
  55     intros;
  56     unfold carr; unfold proofs; simplify;
  57     apply (trans B ? (y a));
  58     [ apply (f a)
  59     | apply (f1 a)]]
  60 qed.
  61
  62 nrecord isomorphism (A,B: setoid): Type ≝
  63  { map1:> function_space_setoid A B;
  64    map2:> function_space_setoid B A;
  65    inv1: ∀a:A. proofs (eq ? (map2 (map1 a)) a);
  66    inv2: ∀b:B. proofs (eq ? (map1 (map2 b)) b)
  67  }.
  68
  69 interpretation "isomorphism" 'iff x y = (isomorphism x y).
  70
  71 (*
  72 record dependent_product (A:setoid)  (B: A ⇒ setoids): Type ≝
  73  { dp:> ∀a:A.carr (B a);
  74    dp_ok: ∀a,a':A. ∀p:proofs1 (eq1 ? a a'). proofs1 (eq1 ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a')))
  75  }.*)
  76
  77  *)