1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "logic/connectives.ma".
16 include "properties/relations.ma".
18 nrecord setoid : Type[1] ≝
20 eq: carr → carr → CProp;
23 trans: transitive … eq
26 ndefinition proofs: CProp → setoid.
29 ##| #x; #y; napply True;
30 ##|##*: nwhd; nrepeat (#_); napply I;
34 nrecord function_space (A,B: setoid): Type ≝
36 f_ok: ∀a,a':A. proofs (eq … a a') → proofs (eq … (f a) (f a'))
39 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
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]##]
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)
58 interpretation "isomorphism" 'iff x y = (isomorphism x y).
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')))