Require Import interfaces.Category.
Require Import interfaces.ConcreteCategory.
Require Import coqrel.LogicalRelations.

Class PartialOrder (P : Type) :=
  {
    le : P → P → Prop;
    le_preo :> PreOrder le;
    le_po :> Antisymmetric P eq le;
  }.

Infix "[= " := le (at level 70).

Module Poset <: ConcreteCategory.

  Definition Structure (P : Type) :=
    PartialOrder P.

  Definition Morphism {P Q} `{Ple: PartialOrder P} `{Qle: PartialOrder Q} (f : P → Q) :=
    Monotonic f (le ++> le).

  Instance id_mor `{PartialOrder} :
    Monotonic (fun x ⇒ x) (le ++> le).

  Instance compose_mor {A B C} `{PartialOrder A} `{PartialOrder B} `{PartialOrder C} :
    ∀ (g: B → C) (f: A → B),
      Monotonic g (le ++> le) →
      Monotonic f (le ++> le) →
      Monotonic (fun x ⇒ g (f x)) (le ++> le).

  Include ConcreteCategoryTheory.
End Poset.

Class Directed `{PartialOrder} (D : P → Prop) :=
  directed : ∀ x y, D x → D y → ∃ z, D z ∧ x [= z ∧ y [= z.

Class IsSup `{PartialOrder} (D : P → Prop) (u : P) :=
  {
    sup_ub x : D x → x [= u;
    sup_lub y : (∀ x, D x → x [= y) → u [= y;
  }.

Lemma sup_unique `{PartialOrder} (D : P → Prop) (u v : P) :
  IsSup D u →
  IsSup D v →
  u = v.

Class DirectedComplete (P : Type) :=
  {
    dc_po :> PartialOrder P;
    dsup : ∀ D `{HD: !Directed D}, P;
    dsup_is_sup D `{!Directed D} :> IsSup D (dsup D);
  }.

Variant im {A B} (f : A → B) (X : A → Prop) : B → Prop :=
  im_intro a : X a → im f X (f a).

Require Import PropExtensionality.
Require Import FunctionalExtensionality.

Lemma im_id {A} (X : A → Prop) :
  im (fun a ⇒ a) X = X.

Lemma im_compose {A B C} (g : B → C) (f : A → B) (X : A → Prop) :
  im (fun a ⇒ g (f a)) X = im g (im f X).

Class ScottContinuous {P Q} `{HP: DirectedComplete P} `{HQ: PartialOrder Q} (f : P → Q) :=
  {
    sc_dsup_sup :>
      ∀ D `{!Directed D}, IsSup (im f D) (f (dsup D));
  }.

Lemma le_directed `{PartialOrder} p q :
  p [= q → Directed (fun x ⇒ x = p ∨ x = q).

Instance sc_le `{ScottContinuous} :
  Monotonic f (le ++> le).

Instance im_directed {P Q} `{!PartialOrder P} `{!PartialOrder Q} (f : P → Q) (D : P → Prop) :
  Monotonic f (le ++> le) →
  Directed D →
  Directed (im f D).

Lemma sc_dsup {P Q} `{!DirectedComplete P} `{!DirectedComplete Q} (f:P→Q) `{!ScottContinuous f}:
  ∀ D `{!Directed D}, f (dsup D) = dsup (im f D).

Module DCPO <: ConcreteCategory.

  Definition Structure :=
    DirectedComplete.

  Definition Morphism {P Q} `{!DirectedComplete P} `{!DirectedComplete Q} (f: P→Q) :=
    ScottContinuous f.

  Instance id_mor `{DirectedComplete} :
    ScottContinuous (fun p ⇒ p).

  Instance compose_mor {A B C} `{DirectedComplete A} `{DirectedComplete B} `{DirectedComplete C} :
    ∀ (g: B → C) (f: A → B),
      ScottContinuous g →
      ScottContinuous f →
      ScottContinuous (fun x ⇒ g (f x)).

  Include ConcreteCategoryTheory.
End DCPO.