(* *)
(**************************************************************************)
-include "datatypes/categories.ma".
+include "categories.ma".
include "logic/cprop_connectives.ma".
-inductive bool : Type := true : bool | false : bool.
+inductive bool : Type0 := true : bool | false : bool.
lemma BOOL : objs1 SET.
constructor 1; [apply bool] constructor 1;
qed.
lemma IF_THEN_ELSE_p :
- ∀S:setoid.∀a,b:S.∀x,y:BOOL.x = y →
+ ∀S:setoid1.∀a,b:S.∀x,y:BOOL.x = y →
(λm.match m with [ true ⇒ a | false ⇒ b ]) x =
(λm.match m with [ true ⇒ a | false ⇒ b ]) y.
whd in ⊢ (?→?→?→%→?);
-intros; cases x in H; cases y; simplify; intros; try apply refl; whd in H; cases H;
-qed.
+intros; cases x in e; cases y; simplify; intros; try apply refl1; whd in e; cases e;
+qed.
interpretation "unary morphism comprehension with no proof" 'comprehension T P =
(mk_unary_morphism T _ P _).
+interpretation "unary morphism1 comprehension with no proof" 'comprehension T P =
+ (mk_unary_morphism1 T _ P _).
notation > "hvbox({ ident i ∈ s | term 19 p | by })" with precedence 90
for @{ 'comprehension_by $s (λ${ident i}. $p) $by}.
interpretation "unary morphism comprehension with proof" 'comprehension_by s \eta.f p =
(mk_unary_morphism s _ f p).
+interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \eta.f p =
+ (mk_unary_morphism1 s _ f p).
+
+definition hint: Type_OF_category2 SET1 → setoid2.
+ intro; apply (setoid2_of_setoid1 t); qed.
+coercion hint.
+
+definition hint2: Type_OF_category1 SET → objs2 SET1.
+ intro; apply (setoid1_of_setoid t); qed.
+coercion hint2.
(* per il set-indexing vedere capitolo BPTools (foundational tools), Sect. 0.3.4 complete
lattices, Definizione 0.9 *)
(* USARE L'ESISTENZIALE DEBOLE *)
-(* Far salire SET usando setoidi1 *)
-record OAlgebra : Type := {
- oa_P :> SET;
+(*alias symbol "comprehension_by" = "unary morphism comprehension with proof".*)
+record OAlgebra : Type2 := {
+ oa_P :> SET1;
oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1, CPROP importante che sia small *)
oa_overlap: binary_morphism1 oa_P oa_P CPROP;
- oa_meet: ∀I:SET.unary_morphism (arrows1 SET I oa_P) oa_P;
- oa_join: ∀I:SET.unary_morphism (arrows1 SET I oa_P) oa_P;
+ oa_meet: ∀I:SET.unary_morphism2 (arrows2 SET1 I oa_P) oa_P;
+ oa_join: ∀I:SET.unary_morphism2 (arrows2 SET1 I oa_P) oa_P;
oa_one: oa_P;
oa_zero: oa_P;
oa_leq_refl: ∀a:oa_P. oa_leq a a;
oa_join_sup: ∀I.∀p_i.∀p:oa_P.oa_leq (oa_join I p_i) p → ∀i:I.oa_leq (p_i i) p;
oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
oa_one_top: ∀p:oa_P.oa_leq p oa_one;
- (* preservers!! (typo) *)
- oa_overlap_preservers_meet_:
- ∀p,q.oa_overlap p q → oa_overlap p
+ oa_overlap_preserves_meet_:
+ ∀p,q:oa_P.oa_overlap p q → oa_overlap p
(oa_meet ? { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q });
(* ⇔ deve essere =, l'esiste debole *)
oa_join_split:
- ∀I:SET.∀p.∀q:arrows1 SET I oa_P.oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i);
+ ∀I:SET.∀p.∀q:arrows2 SET1 I oa_P.
+ oa_overlap p (oa_join I q) ⇔ ∃i:I.oa_overlap p (q i);
(*oa_base : setoid;
1) enum non e' il nome giusto perche' non e' suriettiva
2) manca (vedere altro capitolo) la "suriettivita'" come immagine di insiemi di oa_base
∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
}.
-interpretation "o-algebra leq" 'leq a b = (fun1 ___ (oa_leq _) a b).
+interpretation "o-algebra leq" 'leq a b = (fun21 ___ (oa_leq _) a b).
notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
for @{ 'overlap $a $b}.
-interpretation "o-algebra overlap" 'overlap a b = (fun1 ___ (oa_overlap _) a b).
+interpretation "o-algebra overlap" 'overlap a b = (fun22 ___ (oa_overlap _) a b).
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)"
non associative with precedence 50 for @{ 'oa_meet $p }.
for @{ 'oa_meet (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
*)
interpretation "o-algebra meet" 'oa_meet f =
- (fun_1 __ (oa_meet __) f).
+ (fun11 __ (oa_meet __) f).
interpretation "o-algebra meet with explicit function" 'oa_meet_mk f =
- (fun_1 __ (oa_meet __) (mk_unary_morphism _ _ f _)).
+ (fun11 __ (oa_meet __) (mk_unary_morphism _ _ f _)).
+
+(*
definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
intros; split;
| intros; split; unfold ORelation_composition; simplify; apply id_neutral_left1;
| intros; split; unfold ORelation_composition; simplify; apply id_neutral_right1;]
qed.
+*)
\ No newline at end of file