Require Import Classical.

Set Implicit Arguments.

Notation set X := (X -> Prop).
Notation relation X := (X -> X -> Prop).
Notation "p '<<=' q" := (forall x, p x -> q x) (at level 70).
Notation "p '===' q" := (forall x, p x <-> q x) (at level 70).
Notation "p << q" := (p <<= q /\ ~ q === p) (at level 70).
Notation "p :|: q" := (fun x : _ => p x \/ q x) (at level 70).
Notation complement p := (fun x => ~ p x).
Notation set0 := (fun _ => False).
Notation set1 x := (fun z => z = x).
Notation setT := (fun _ => True).

Section Predicates.
  Variable (X : Type).
  Implicit Types (p q : set X) (F G : set X -> Prop).

  Definition inhab p := ex p.
  Definition single p := exists2 x, p x & forall y, p y -> y = x.
  Definition cmp p q := p <<= q \/ q <<= p.
  Definition linears F := forall p q, F p -> F q -> cmp p q.
  Definition Union F x := exists2 p, F p & p x.
  Definition Inter F x := forall p, F p -> p x.
  Definition unique p := forall x y, p x -> p y -> x = y.
  Definition setU1 p x := fun z => p z \/ z = x.
  Definition incl p q := p <<= q.

  Lemma sub_refl p : incl p p.

  Lemma set_eq p q : p <<= q -> q <<= p -> p === q.

  Lemma sub_linear F G : G <<= F -> linears F -> linears G.

  Lemma sub_trans p q r : p <<= q -> q <<= r -> p <<= r.

  Lemma eq_sub p q : p = q -> p === q.

  Lemma sub_union F p : F p -> p <<= Union F.

End Predicates.

Definition least X (R : relation X) x p := p x /\ forall y, p y -> R x y.

Section OrderOn.
  Variables (X : Type) (p : set X) (R : relation X).

  Definition refl_on := forall x, p x -> R x x.

  Definition trans_on :=
    forall x y z, p x -> p y -> p z -> R x y -> R y z -> R x z.

  Definition anti_on :=
    forall x y, p x -> p y -> R x y -> R y x -> x = y.

  Definition linear_on :=
    forall x y, p x -> p y -> R x y \/ R y x.

  Definition ELE_on :=
    forall q : set X, q <<= p -> inhab q -> exists x, least R x q.

  Lemma ELE_linear : ELE_on -> linear_on.

  Fact linear_refl : linear_on -> refl_on.

  Definition po_on := refl_on /\ trans_on /\ anti_on.

  Definition lo_on := po_on /\ linear_on.

  Definition wo_on := po_on /\ ELE_on.

End OrderOn.

Lemma po_sub (X : Type) (R : relation X) (p q : set X) :
  p <<= q -> po_on q R -> po_on p R.

Lemma wo_sub (X : Type) (R : relation X) (p q : set X) :
  p <<= q -> wo_on q R -> wo_on p R.

Definition injective X Y (f : X -> Y) :=
  forall x y, f x = f y -> x = y.

Definition into X Y p q (f : X -> Y) := forall x, p x -> q (f x).

Lemma transfer_on X Y (f : X -> Y) (p : set X) (q : set Y) (R : relation Y) :
  injective f -> into p q f -> wo_on q R -> wo_on p (fun x y => R (f x) (f y)).

Section Chains.
  Variables (X : Type) (R : relation X).
  Definition chain p := linear_on p R.

  Lemma chainU F :
    linears F -> (forall p, F p -> chain p) -> chain (Union F).
End Chains.

Record ExtType :=
  { ext_sort :> Type ;
    set_ext (p q : set ext_sort) : p === q -> p = q }.

Section ExtTypeFacts.
  Variables (X : ExtType).
  Implicit Types (p q : set X) (x : X) (F G : set (set X)).

  Lemma set_eqx p q : p <<= q -> q <<= p -> p = q.

  Lemma unique_eq1 p x : unique p -> p x -> p = set1 x.

  Lemma setU0 p : p :|: set0 = p.

  Lemma inter_eq F G : F === G -> Inter F = Inter G.

  Lemma inter1 p : Inter (set1 p) = p.

  Lemma inter_full F : inhab F -> (forall x, Inter F x) -> F === set1 setT.

  Lemma po_incl (F : set (set X)) : po_on F (@incl X).

End ExtTypeFacts.

Record ExtChoiceType :=
  { sort :> ExtType ;
    gamma : set sort -> set sort ;
    gammaP1 (p : set sort) : gamma p <<= p ;
    gammaP2 (p : set sort) : inhab p -> single (gamma p) }.

Section ExtChoiceFacts.
  Variable (X : ExtChoiceType).
  Implicit Types (p q : set X).

  Lemma inhab_gamma p : inhab p -> inhab (gamma p).

  Lemma gamma0Vx p :
    gamma p = set0 \/ exists2 x, p x & gamma p = set1 x.

  Lemma gamma_unique p : unique (gamma p).
End ExtChoiceFacts.