helm/software/matita/contribs/limits/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 include "preamble.ma".
  16
  17 (* ACZEL CATEGORIES:
  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.
  27 *)
  28
  29 record Class: Type ≝ {
  30    class:> Type;
  31    cin: class → Prop;
  32    ces: class → class \to Prop
  33 }.
  34
  35 (* default inhabitance predicates *)
  36 definition true_f ≝ λ(X:Type). λ(_:X). True.
  37 definition false_f ≝ λ(X:Type). λ(_:X). False.
  38
  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
  44 .
  45 (*
  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.
  49
  50 inductive call2 (C1,C2:Class) (P:C1 \to C2 \to Prop) : Prop \def
  51    | call2_intro:
  52       (\forall c1,c2. cin ? c1 \to cin ? c2 \to P c1 c2) \to call2 C1 C2 P.
  53 *)
  54 (* notations **************************************************************)
  55 (*
  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).
  59
  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}}}.
  65
  66 notation > "\forall list1 ident x sep , opt (: T). term 19 Px"
  67   with precedence 20
  68   for ${ default
  69           @{ ${ fold right @{$Px} rec acc @{'xforall (λ${ident x}:$T.$acc)} } }
  70           @{ ${ fold right @{$Px} rec acc @{'xforall (λ${ident x}.$acc)} } }
  71        }.
  72
  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).
  76
  77 notation > "hvbox(\xforall ident i1 opt (: ty1) ident i2 opt (: ty2) break . p)"
  78   with precedence 20
  79 for @{ 'xforall2 ${default
  80   @{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p}
  81   @{\lambda ${ident i1}, ${ident i2}. $p}}}.
  82 *)