(* Definition 2.1 *)
record half_ordered_set: Type ≝ {
hos_carr:> Type;
- wloss: ∀A:Type. (A → A → CProp) → A → A → CProp;
- wloss_prop: (∀T,P,x,y.P x y = wloss T P x y) ∨ (∀T,P,x,y.P y x = wloss T P x y);
+ wloss: ∀A,B:Type. (A → A → B) → A → A → B;
+ wloss_prop: (∀T,R,P,x,y.P x y = wloss T R P x y) ∨ (∀T,R,P,x,y.P y x = wloss T R P x y);
hos_excess_: hos_carr → hos_carr → CProp;
- hos_coreflexive: coreflexive ? (wloss ? hos_excess_);
- hos_cotransitive: cotransitive ? (wloss ? hos_excess_)
+ hos_coreflexive: coreflexive ? (wloss ?? hos_excess_);
+ hos_cotransitive: cotransitive ? (wloss ?? hos_excess_)
}.
-definition hos_excess ≝ λO:half_ordered_set.wloss O ? (hos_excess_ O).
+definition hos_excess ≝ λO:half_ordered_set.wloss O ?? (hos_excess_ O).
(*
lemma find_leq : half_ordered_set → half_ordered_set.
definition dual_hos : half_ordered_set → half_ordered_set.
intro; constructor 1;
[ apply (hos_carr h);
-| apply (λT,f,x,y.wloss h T f y x);
+| apply (λT,R,f,x,y.wloss h T R f y x);
| intros; cases (wloss_prop h);[right|left]intros;apply H;
| apply (hos_excess_ h);
| apply (hos_coreflexive h);
[1: apply (wloss O);
|2: intros; cases (wloss_prop O); [left|right] intros; apply H;
|3: apply (square_exc O);
-|4: intro x; cases (wloss_prop O); rewrite < (H ? (square_exc O) x x); clear H;
+|4: intro x; cases (wloss_prop O); rewrite < (H ?? (square_exc O) x x); clear H;
cases x; clear x; unfold square_exc; intro H; cases H; clear H; simplify in H1;
[1,3: apply (hos_coreflexive O h H1);
|*: apply (hos_coreflexive O h1 H1);]
|5: intros 3 (x0 y0 z0); cases (wloss_prop O);
- do 3 rewrite < (H ? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0;
+ do 3 rewrite < (H ?? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0;
simplify; intro H; cases H; clear H;
[1: cases (hos_cotransitive ? h h2 h4 H1); [left;left|right;left] assumption;
|2: cases (hos_cotransitive ? h1 h3 h5 H1); [left;right|right;right] assumption;