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 (* Project started Wed Oct 12, 2005 ***************************************)
17 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_defs".
19 include "../../library/logic/connectives.ma".
22 - We use typoids with a compatible membership relation
23 - The category is intended to be the domain of the membership relation
24 - The membership relation is necessary because we need to regard the
25 domain of a propositional function (ie a predicative subset) as a
26 quantification domain and therefore as a category, but there is no
27 type in CIC representing the domain of a propositional function
28 - We set up a single equality predicate, parametric on the category,
29 defined as the reflexive, symmetic, transitive and compatible closure
30 of the cle1 predicate given inside the category. Then we prove the
31 properties of the equality that usually are axiomatized inside the
32 category structure. This makes categories easier to use
35 definition true_f \def \lambda (X:Type). \lambda (_:X). True.
37 definition false_f \def \lambda (X:Type). \lambda (_:X). False.
39 record Class: Type \def {
42 cle1 : class \to class \to Prop
45 inductive ceq (C:Class) (c1:C): C \to Prop \def
46 | ceq_refl: cin ? c1 \to ceq ? c1 c1
47 | ceq_sing_r: \forall c2,c3.
48 ceq ? c1 c2 \to cin ? c3 \to cle1 ? c2 c3 \to ceq ? c1 c3
49 | ceq_sing_l: \forall c2,c3.
50 ceq ? c1 c2 \to cin ? c3 \to cle1 ? c3 c2 \to ceq ? c1 c3.