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_class.ma".
17 (* EXPONENTIAL CLASS **************************************************)
19 definition u0_exp_eq (D,C): u0_predicate2 (u0_fun D C) ≝
20 λf,g. (u0_xeq … (u0_class_in D) … (u0_class_eq C) f g).
22 definition u0_exp (D,C): u0_class ≝
23 mk_u0_class (u0_fun D C) (is_u0_fun …) (u0_exp_eq D C).
25 definition u0_proj1 (D1,D2): u0_fun D1 (u0_exp D2 D1) ≝
26 mk_u0_fun … (λa. mk_u0_fun … (u0_k … a)).
28 (* Basic properties ***************************************************)
30 lemma u0_class_exp: ∀D,C. is_u0_class C → is_u0_class (u0_exp D C).
31 /4 width=7 by mk_is_u0_class, u0_class_refl, u0_class_repl, u0_fun_hom1/ qed.
33 lemma u0_fun_proj1: ∀D2,D1. is_u0_class D1 → is_u0_fun … (u0_proj1 D1 D2).
34 #D2 #D1 #HD1 @mk_is_u0_fun /3 width=1 by mk_is_u0_fun, u0_class_refl/