matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.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 (* STATO: COMPILA *)
  16
  17 (* Project started Wed Oct 12, 2005 ***************************************)
  18
  19 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_defs".
  20
  21 include "logic/connectives.ma".
  22
  23 (* ACZEL CATEGORIES:
  24    - We use typoids with a compatible membership relation
  25    - The category is intended to be the domain of the membership relation
  26    - The membership relation is necessary because we need to regard the
  27      domain of a propositional function (ie a predicative subset) as a
  28      quantification domain and therefore as a category, but there is no
  29      type in CIC representing the domain of a propositional function
  30    - We set up a single equality predicate, parametric on the category,
  31      defined as the reflexive, symmetic, transitive and compatible closure
  32      of the cle1 predicate given inside the category. Then we prove the
  33      properties of the equality that usually are axiomatized inside the
  34      category structure. This makes categories easier to use
  35 *)
  36
  37 definition true_f \def \lambda (X:Type). \lambda (_:X). True.
  38
  39 definition false_f \def \lambda (X:Type). \lambda (_:X). False.
  40
  41 record Class: Type \def {
  42    class:> Type;
  43    cin: class \to Prop;
  44    ceq: class \to class \to Prop;
  45    cin_repl: \forall c1,c2. cin c1 \to ceq c1 c2 \to cin c2;
  46    ceq_repl: \forall c1,c2,d1,d2. cin c1 \to
  47       ceq c1 c2 \to ceq c1 d1 \to ceq c2 d2 \to ceq d1 d2;
  48    ceq_refl: \forall c. cin c \to ceq c c
  49 }.
  50
  51 (* external universal quantification *)
  52 inductive call (C:Class) (P:C \to Prop) : Prop \def
  53    | call_intro: (\forall c. cin ? c \to P c) \to call C P.
  54
  55 inductive call2 (C1,C2:Class) (P:C1 \to C2 \to Prop) : Prop \def
  56    | call2_intro:
  57       (\forall c1,c2. cin ? c1 \to cin ? c2 \to P c1 c2) \to call2 C1 C2 P.
  58
  59 (* notations **************************************************************)
  60
  61 (*CSC: the URI must disappear: there is a bug now *)
  62 interpretation "external for all" 'xforall \eta.x =
  63   (cic:/matita/PREDICATIVE-TOPOLOGY/class_defs/call.ind#xpointer(1/1) _ x).
  64
  65 notation > "hvbox(\xforall ident i opt (: ty) break . p)"
  66   right associative with precedence 20
  67 for @{ 'xforall ${default
  68   @{\lambda ${ident i} : $ty. $p}
  69   @{\lambda ${ident i} . $p}}}.
  70
  71 (*CSC: the URI must disappear: there is a bug now *)
  72 interpretation "external for all 2" 'xforall2 \eta.x \eta.y =
  73   (cic:/matita/PREDICATIVE-TOPOLOGY/class_defs/call2.ind#xpointer(1/1) _ _ x y).
  74
  75 notation > "hvbox(\xforall ident i1 opt (: ty1) ident i2 opt (: ty2) break . p)"
  76   right associative with precedence 20
  77 for @{ 'xforall2 ${default
  78   @{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p}
  79   @{\lambda ${ident i1}, ${ident i2}. $p}}}.