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 ##| nnormalize; #x; #a; napply (f_ok … x); napply refl
  46   | nnormalize; #x; #y; #H; #a; napply sym; napply H
  47   | nnormalize; #z; #x; #y; #H1; #H2; #a;
  48     napply trans; ##[##2: napply H1 | ##skip | napply H2]##]
  49 nqed.
  50
  51 nrecord isomorphism (A,B: setoid): Type ≝
  52  { map1:> function_space_setoid A B;
  53    map2:> function_space_setoid B A;
  54    inv1: ∀a:A. proofs (eq ? (map2 (map1 a)) a);
  55    inv2: ∀b:B. proofs (eq ? (map1 (map2 b)) b)
  56  }.
  57
  58 interpretation "isomorphism" 'iff x y = (isomorphism x y).
  59
  60 (*
  61 record dependent_product (A:setoid)  (B: A ⇒ setoids): Type ≝
  62  { dp:> ∀a:A.carr (B a);
  63    dp_ok: ∀a,a':A. ∀p:proofs1 (eq1 ? a a'). proofs1 (eq1 ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a')))
  64  }.*)
  65
  66  *)