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