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 "u0_predicates.ma".
17 (* CLASSES ************************************************************)
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
25 interpretation "u0 class membership" 'mem a C = (u0_class_in C a).
27 definition u0_class_all: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∀a. a ∈ C → P a.
29 definition u0_class_ex: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∃a. a ∈ C ∧ P a.
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)