matita/matita/contribs/limits/u0_class.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 "u0_predicates.ma".
  16
  17 (* CLASSES ************************************************************)
  18
  19 record u0_class: Type[1] ≝ {
  20    u0_class_t :> Type[0];
  21    u0_class_in:  u0_predicate1 u0_class_t;
  22    u0_class_eq:  u0_predicate2 u0_class_t
  23 }.
  24
  25 interpretation "u0 class membership" 'mem a C = (u0_class_in C a).
  26
  27 definition u0_class_all: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∀a. a ∈ C → P a.
  28
  29 definition u0_class_ex: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∃a. a ∈ C ∧ P a.
  30
  31 record is_u0_class (C:u0_class): Prop ≝ {
  32    u0_class_repl1: can_u0_replace1 C (u0_class_all C) (u0_class_eq C) (u0_class_in C);
  33    u0_class_refl : is_u0_reflexive C (u0_class_all C) (u0_class_eq C)
  34 }.