# Additionnals theorems for Sets.v

Previous theorems about hSet and order

Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.Sets.

Require Export UniMath.Foundations.Sets
UniMath.MoreFoundations.QuotientSet.
Require Import UniMath.Algebra.BinaryOperations
UniMath.Algebra.Apartness.

Definition unop (X : UU) := X X.

Definition islinv' {X : hSet} (x1 : X) (op : binop X) (exinv : hsubtype X) (inv : subset exinv X) :=
(x : X) (Hx : exinv x), op (inv (x ,, Hx)) x = x1.
Definition isrinv' {X : hSet} (x1 : X) (op : binop X) (exinv : hsubtype X) (inv : subset exinv X) :=
(x : X) (Hx : exinv x), op x (inv (x ,, Hx)) = x1.
Definition isinv' {X : hSet} (x1 : X) (op : binop X) (exinv : hsubtype X) (inv : subset exinv X) :=
islinv' x1 op exinv inv × isrinv' x1 op exinv inv.

## Properties of po

Section po_pty.

Context {X : UU}.
Context (R : po X).

Definition istrans_po : istrans R :=
pr1 (pr2 R).
Definition isrefl_po : isrefl R :=
pr2 (pr2 R).

End po_pty.

## Strong Order

Definition isStrongOrder {X : UU} (R : hrel X) := istrans R × iscotrans R × isirrefl R.
Definition StrongOrder (X : UU) := R : hrel X, isStrongOrder R.
Definition pairStrongOrder {X : UU} (R : hrel X) (is : isStrongOrder R) : StrongOrder X :=
tpair (λ R : hrel X, isStrongOrder R ) R is.
Definition pr1StrongOrder {X : UU} : StrongOrder X hrel X := pr1.
Coercion pr1StrongOrder : StrongOrder >-> hrel.

Section so_pty.

Context {X : UU}.
Context (R : StrongOrder X).

Definition istrans_StrongOrder : istrans R :=
pr1 (pr2 R).
Definition iscotrans_StrongOrder : iscotrans R :=
pr1 (pr2 (pr2 R)).
Definition isirrefl_StrongOrder : isirrefl R :=
pr2 (pr2 (pr2 R)).

End so_pty.

Definition isStrongOrder_quotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L) :
isStrongOrder L isStrongOrder (quotrel is).
Proof.
intros H.
repeat split.
- apply istransquotrel, (pr1 H).
- apply iscotransquotrel, (pr1 (pr2 H)).
- apply isirreflquotrel, (pr2 (pr2 H)).
Defined.

## Reverse orderse

or how easily define ge x y := le x y

Definition hrel_reverse {X : UU} (l : hrel X) := λ x y, l y x.

Lemma istrans_reverse {X : UU} (l : hrel X) :
istrans l istrans (hrel_reverse l).
Proof.
intros Hl x y z Hxy Hyz.
now apply (Hl z y x).
Qed.

Lemma isrefl_reverse {X : UU} (l : hrel X) :
isrefl l isrefl (hrel_reverse l).
Proof.
intros Hl x.
now apply Hl.
Qed.

Lemma ispreorder_reverse {X : UU} (l : hrel X) :
ispreorder l ispreorder (hrel_reverse l).
Proof.
intros H.
split.
now apply istrans_reverse, (pr1 H).
now apply isrefl_reverse, (pr2 H).
Qed.
Definition po_reverse {X : UU} (l : po X) :=
make_po (hrel_reverse l) (ispreorder_reverse l (pr2 l)).
Lemma po_reverse_correct {X : UU} (l : po X) :
x y : X, po_reverse l x y = l y x.
Proof.
intros x y.
now apply paths_refl.
Qed.

Lemma issymm_reverse {X : UU} (l : hrel X) :
issymm l issymm (hrel_reverse l).
Proof.
intros Hl x y.
now apply Hl.
Qed.

Lemma iseqrel_reverse {X : UU} (l : hrel X) :
iseqrel l iseqrel (hrel_reverse l).
Proof.
intros H.
split.
now apply ispreorder_reverse, (pr1 H).
now apply issymm_reverse, (pr2 H).
Qed.
Definition eqrel_reverse {X : UU} (l : eqrel X) :=
make_eqrel (hrel_reverse l) (iseqrel_reverse l (pr2 l)).
Lemma eqrel_reverse_correct {X : UU} (l : eqrel X) :
x y : X, eqrel_reverse l x y = l y x.
Proof.
intros x y.
now apply paths_refl.
Qed.

Lemma isirrefl_reverse {X : UU} (l : hrel X) :
isirrefl l isirrefl (hrel_reverse l).
Proof.
intros Hl x.
now apply Hl.
Qed.
Lemma iscotrans_reverse {X : UU} (l : hrel X) :
iscotrans l iscotrans (hrel_reverse l).
Proof.
intros Hl x y z H.
now apply islogeqcommhdisj, Hl.
Qed.

Lemma isStrongOrder_reverse {X : UU} (l : hrel X) :
isStrongOrder l isStrongOrder (hrel_reverse l).
Proof.
intros H.
repeat split.
now apply istrans_reverse, (pr1 H).
now apply iscotrans_reverse, (pr1 (pr2 H)).
now apply isirrefl_reverse, (pr2 (pr2 H)).
Qed.
Definition StrongOrder_reverse {X : UU} (l : StrongOrder X) :=
pairStrongOrder (hrel_reverse l) (isStrongOrder_reverse l (pr2 l)).
Lemma StrongOrder_reverse_correct {X : UU} (l : StrongOrder X) :
x y : X, StrongOrder_reverse l x y = l y x.
Proof.
intros x y.
now apply paths_refl.
Qed.

Lemma isasymm_reverse {X : UU} (l : hrel X) :
isasymm l isasymm (hrel_reverse l).
Proof.
intros Hl x y.
now apply Hl.
Qed.

Lemma iscoasymm_reverse {X : UU} (l : hrel X) :
iscoasymm l iscoasymm (hrel_reverse l).
Proof.
intros Hl x y.
now apply Hl.
Qed.

Lemma istotal_reverse {X : UU} (l : hrel X) :
istotal l istotal (hrel_reverse l).
Proof.
intros Hl x y.
now apply Hl.
Qed.

## Effectively Ordered

An alternative of total orders

Definition isEffectiveOrder {X : UU} (le lt : hrel X) :=
dirprod ((ispreorder le) × (isStrongOrder lt))
(( x y : X, (¬ lt x y) (le y x))
× ( x y z : X, lt x y le y z lt x z)
× ( x y z : X, le x y lt y z lt x z)).
Definition EffectiveOrder (X : UU) :=
le lt : hrel X, isEffectiveOrder le lt.
Definition pairEffectiveOrder {X : UU} (le lt : hrel X) (is : isEffectiveOrder le lt) : EffectiveOrder X :=
(le,,lt,,is).

Definition EffectivelyOrderedSet :=
X : hSet, EffectiveOrder X.
Definition pairEffectivelyOrderedSet {X : hSet} (is : EffectiveOrder X) : EffectivelyOrderedSet
:= tpair _ X is.
Definition pr1EffectivelyOrderedSet : EffectivelyOrderedSet hSet := pr1.
Coercion pr1EffectivelyOrderedSet : EffectivelyOrderedSet >-> hSet.

Definition EOle {X : EffectivelyOrderedSet} : po X :=
let R := pr2 X in
make_po (pr1 R) (pr1 (pr1 (pr2 (pr2 R)))).
Definition EOle_rel {X : EffectivelyOrderedSet} : hrel X :=
pr1 EOle.
Arguments EOle_rel {X} x y: simpl never.
Definition EOge {X : EffectivelyOrderedSet} : po X :=
po_reverse (@EOle X).
Definition EOge_rel {X : EffectivelyOrderedSet} : hrel X :=
pr1 EOge.
Arguments EOge_rel {X} x y: simpl never.

Definition EOlt {X : EffectivelyOrderedSet} : StrongOrder (pr1 X) :=
let R := pr2 X in
pairStrongOrder (pr1 (pr2 R)) (pr2 (pr1 (pr2 (pr2 R)))).
Definition EOlt_rel {X : EffectivelyOrderedSet} : hrel X :=
pr1 EOlt.
Arguments EOlt_rel {X} x y: simpl never.
Definition EOgt {X : EffectivelyOrderedSet} : StrongOrder (pr1 X) :=
StrongOrder_reverse (@EOlt X).
Definition EOgt_rel {X : EffectivelyOrderedSet} : hrel X :=
pr1 EOgt.
Arguments EOgt_rel {X} x y: simpl never.

Definition PreorderedSetEffectiveOrder (X : EffectivelyOrderedSet) : PreorderedSet :=
PreorderedSetPair _ (@EOle X).

Declare Scope eo_scope.
Delimit Scope eo_scope with eo.

Notation "x <= y" := (EOle_rel x y) : eo_scope.
Notation "x >= y" := (EOge_rel x y) : eo_scope.
Notation "x < y" := (EOlt_rel x y) : eo_scope.
Notation "x > y" := (EOgt_rel x y) : eo_scope.

Section eo_pty.

Context {X : EffectivelyOrderedSet}.

Local Open Scope eo_scope.

Lemma not_EOlt_le :
x y : X, (¬ (x < y)) (y x).
Proof.
exact (pr1 (pr2 (pr2 (pr2 (pr2 X))))).
Qed.
Lemma EOge_le:
x y : X, (x y) (y x).
Proof.
now split.
Qed.
Lemma EOgt_lt:
x y : X, (x > y) (y < x).
Proof.
now split.
Qed.

Definition isrefl_EOle:
x : X, x x
:= isrefl_po EOle.
Definition istrans_EOle:
x y z : X, x y y z x z
:= istrans_po EOle.

Definition isirrefl_EOgt:
x : X, ¬ (x > x)
:= isirrefl_StrongOrder EOgt.
Definition istrans_EOgt:
x y z : X, x > y y > z x > z
:= istrans_StrongOrder EOgt.

Definition isirrefl_EOlt:
x : X, ¬ (x < x)
:= isirrefl_StrongOrder EOlt.
Definition istrans_EOlt:
x y z : X, x < y y < z x < z
:= istrans_StrongOrder EOlt.

Lemma EOlt_le :
x y : X, x < y x y.
Proof.
intros x y Hxy.
apply not_EOlt_le.
intros H.
refine (isirrefl_EOlt _ _).
refine (istrans_EOlt _ _ _ _ _).
exact Hxy.
exact H.
Qed.

Lemma istrans_EOlt_le:
x y z : X, x < y y z x < z.
Proof.
exact (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 X)))))).
Qed.
Lemma istrans_EOle_lt:
x y z : X, x y y < z x < z.
Proof.
exact (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 X)))))).
Qed.

Lemma EOlt_noteq :
x y : X, x < y x != y.
Proof.
intros x y Hgt Heq.
rewrite Heq in Hgt.
now apply isirrefl_EOgt in Hgt.
Qed.
Lemma EOgt_noteq :
x y : X, x > y x != y.
Proof.
intros x y Hgt Heq.
rewrite Heq in Hgt.
now apply isirrefl_EOgt in Hgt.
Qed.

Close Scope eo_scope.

End eo_pty.

## Complete Ordered Space

Section LeastUpperBound.

Context {X : PreorderedSet}.
Local Notation "x <= y" := (pr1 (pr2 X) x y).

Definition isUpperBound (E : hsubtype X) (ub : X) : UU :=
x : X, E x x ub.
Definition isSmallerThanUpperBounds (E : hsubtype X) (lub : X) : UU :=
ub : X, isUpperBound E ub lub ub.

Definition isLeastUpperBound (E : hsubtype X) (lub : X) : UU :=
(isUpperBound E lub) × (isSmallerThanUpperBounds E lub).
Definition LeastUpperBound (E : hsubtype X) : UU :=
lub : X, isLeastUpperBound E lub.
Definition pairLeastUpperBound (E : hsubtype X) (lub : X)
(is : isLeastUpperBound E lub) : LeastUpperBound E :=
tpair (isLeastUpperBound E) lub is.
Definition pr1LeastUpperBound {E : hsubtype X} :
LeastUpperBound E X := pr1.

Lemma isapropLeastUpperBound (E : hsubtype X) (H : isantisymm (λ x y : X, x y)) :
isaprop (LeastUpperBound E).
Proof.
intros x y.
apply (iscontrweqf (X := (pr1 x) = (pr1 y))).
- apply invweq, subtypeInjectivity.
intro t.
apply isapropdirprod.
apply impred_isaprop ; intro.
apply isapropimpl.
now apply pr2.
apply impred_isaprop ; intro.
apply isapropimpl.
now apply pr2.
- assert (Heq : (pr1 x) = (pr1 y)).
{ apply H.
now apply (pr2 (pr2 x)), (pr1 (pr2 y)).
now apply (pr2 (pr2 y)), (pr1 (pr2 x)). }
rewrite <- Heq.
apply iscontrloopsifisaset.
apply pr2.
Qed.

End LeastUpperBound.

Section GreatestLowerBound.

Context {X : PreorderedSet}.
Local Notation "x >= y" := (pr1 (pr2 X) y x).

Definition isLowerBound (E : hsubtype X) (ub : X) : UU :=
x : X, E x x ub.
Definition isBiggerThanLowerBounds (E : hsubtype X) (lub : X) : UU :=
ub : X, isLowerBound E ub lub ub.

Definition isGreatestLowerBound (E : hsubtype X) (glb : X) : UU :=
(isLowerBound E glb) × (isBiggerThanLowerBounds E glb).
Definition GreatestLowerBound (E : hsubtype X) : UU :=
glb : X, isGreatestLowerBound E glb.
Definition pairGreatestLowerBound (E : hsubtype X) (glb : X)
(is : isGreatestLowerBound E glb) : GreatestLowerBound E :=
tpair (isGreatestLowerBound E) glb is.
Definition pr1GreatestLowerBound {E : hsubtype X} :
GreatestLowerBound E X := pr1.

Lemma isapropGreatestLowerBound (E : hsubtype X) (H : isantisymm (λ x y : X, x y)) :
isaprop (GreatestLowerBound E).
Proof.
intros x y.
apply (iscontrweqf (X := (pr1 x) = (pr1 y))).
- apply invweq, subtypeInjectivity.
intro t.
apply isapropdirprod.
apply impred_isaprop ; intro.
apply isapropimpl.
now apply pr2.
apply impred_isaprop ; intro.
apply isapropimpl.
now apply pr2.
- assert (Heq : (pr1 x) = (pr1 y)).
{ apply H.
now apply (pr2 (pr2 x)), (pr1 (pr2 y)).
now apply (pr2 (pr2 y)), (pr1 (pr2 x)). }
rewrite <- Heq.
apply iscontrloopsifisaset.
apply pr2.
Qed.

End GreatestLowerBound.

Definition isCompleteSpace (X : PreorderedSet) :=
E : hsubtype X,
hexists (isUpperBound E) hexists E LeastUpperBound E.
Definition CompleteSpace :=
X : PreorderedSet, isCompleteSpace X.
Definition pr1CompleteSpace : CompleteSpace UU := pr1.
Coercion pr1CompleteSpace : CompleteSpace >-> UU.