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 "preamble.ma".
18 - We use typoids with a compatible membership relation
19 - The category is intended to be the domain of the membership relation
20 - The membership relation is necessary because we need to regard the
21 domain of a propositional function (ie a predicative subset) as a
22 quantification domain and therefore as a category, but there is no
23 type in CIC representing the domain of a propositional function
24 - We set up a single equality predicate, parametric on the category,
25 defined as the reflexive, symmetic, transitive and compatible closure
26 of the "ces" (class equality step) predicate given inside the category.
29 record Class: Type ≝ {
32 ces: class → class \to Prop
35 (* default inhabitance predicates *)
36 definition true_f ≝ λ(X:Type). λ(_:X). True.
37 definition false_f ≝ λ(X:Type). λ(_:X). False.
39 (* equality predicate *)
40 inductive ceq (C:Class): class C → class C → Prop ≝
41 | ceq_refl : ∀c. cin ? c → ceq ? c c
42 | ceq_trans: ∀c1,c,c2. cin ? c1 → ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
43 | ceq_conf : ∀c1,c,c2. cin ? c1 → ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
46 (* external universal quantification *)
47 inductive call (C:Class) (P:C \to Prop) : Prop ≝
48 | call_intro: (\forall c. cin ? c \to P c) \to call C P.
50 inductive call2 (C1,C2:Class) (P:C1 \to C2 \to Prop) : Prop \def
52 (\forall c1,c2. cin ? c1 \to cin ? c2 \to P c1 c2) \to call2 C1 C2 P.
54 (* notations **************************************************************)
56 (*CSC: the URI must disappear: there is a bug now *)
57 interpretation "external for all" 'xforall \eta.x =
58 (cic:/matita/limits/Class/defs/call.ind#xpointer(1/1) _ x).
60 notation < "hvbox(\xforall ident i opt (: ty) break . p)"
61 right associative with precedence 20
62 for @{ 'xforall ${default
63 @{\lambda ${ident i} : $ty. $p}
64 @{\lambda ${ident i} . $p}}}.
66 notation > "\forall list1 ident x sep , opt (: T). term 19 Px"
69 @{ ${ fold right @{$Px} rec acc @{'xforall (λ${ident x}:$T.$acc)} } }
70 @{ ${ fold right @{$Px} rec acc @{'xforall (λ${ident x}.$acc)} } }
73 (*CSC: the URI must disappear: there is a bug now *)
74 interpretation "external for all 2" 'xforall2 \eta.x \eta.y =
75 (cic:/matita/limits/Class/defs/call2.ind#xpointer(1/1) _ _ x y).
77 notation > "hvbox(\xforall ident i1 opt (: ty1) ident i2 opt (: ty2) break . p)"
79 for @{ 'xforall2 ${default
80 @{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p}
81 @{\lambda ${ident i1}, ${ident i2}. $p}}}.