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.
27 #P; napply (mk_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)));
46 napply (f_ok ? ? x ? ? ?); (* QUI!! *)
47 (* unfold carr; unfold proofs; simplify;
51 unfold carr; unfold proofs; simplify;
56 unfold carr; unfold proofs; simplify;
57 apply (trans B ? (y a));
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)
69 interpretation "isomorphism" 'iff x y = (isomorphism x y).
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')))