Library UniMath.OrderTheory.DCPOs.Core.WayBelow

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.
Require Import UniMath.OrderTheory.DCPOs.Core.Basics.

Local Open Scope dcpo.

1. Definition of the way-below relation

Definition way_below
           {X : dcpo}
           (x y : X)
  : hProp
  := (∀ (D : directed_set X ), y ⊑ ⨆ D ⇒ ∃ (i : D ), x ⊑ D i)%logic.

Notation "x ≪ y" := (way_below x y) (at level 70).
Proposition way_below_elem
            {X : dcpo}
            {x y : X}
            (p : x ≪ y)
            (D : directed_set X)
            (HD : y ⊑ ⨆ D)
  : ∃ (i : D ), x ⊑ D i.
Show proof.

exact (p D HD).

Section PropertiesOfWayBelow.
Context {X : dcpo}.

2. Transitivity of the way-below relation

  Proposition trans_way_below
              {x y z : X}
              (p : x ≪ y)
              (q : y ≪ z)
    : x ≪ z.
  Show proof.

    intros D HD.
    assert (H := way_below_elem q D HD).
    revert H.
    use factor_through_squash.
    {
      apply propproperty.
    }
    intros H.
    induction H as [ i H ].
    assert (H' : y ⊑ ⨆ D).
    {
      refine (trans_dcpo H _).
      use (less_than_dcpo_lub D _ i).
      apply refl_dcpo.
    }
    exact (way_below_elem p D H').

3. Interaction between the order of the DCPO and the way-below relation

  Proposition trans_way_below_le
              {x y z : X}
              (p : x ≪ y)
              (q : y ⊑ z)
    : x ≪ z.
  Show proof.

intros D HD.
exact (way_below_elem p D (trans_dcpo q HD)).

  Proposition trans_le_way_below
              {x y z : X}
              (p : x ⊑ y)
              (q : y ≪ z)
    : x ≪ z.
  Show proof.

    intros D HD.
    assert (H := way_below_elem q D HD).
    revert H.
    use factor_through_squash.
    {
      apply propproperty.
    }
    intros H.
    induction H as [ i H ].
    refine (hinhpr (i ,, _)).
    exact (trans_dcpo p H).

  Proposition way_below_to_le
              {x y : X}
              (p : x ≪ y)
    : x ⊑ y.
  Show proof.

    pose (D := nat_directed_set X (λ _, y) (λ _, refl_dcpo _)).
    assert (q : y ⊑ ⨆ D).
    {
      exact (less_than_dcpo_lub D y 0 (refl_dcpo _)).
    }
    assert (H := way_below_elem p D q).
    revert H.
    use factor_through_squash.
    {
      apply propproperty.
    }
    intros H.
    exact (pr2 H).

4. Antisymmetry of the way-below relation

  Proposition antisymm_way_below
              {x y : X}
              (p : x ≪ y)
              (q : y ≪ x)
    : x = y.
  Show proof.

    use antisymm_dcpo.
    - apply way_below_to_le.
      exact p.
    - apply way_below_to_le.
      exact q.

End PropertiesOfWayBelow.

5. The bottom is way-below every element

Proposition bot_way_below
            {X : dcppo}
            (x : X)
  : ⊥_{X } ≪ x.
Show proof.

  intros D HD.
  assert (H := directed_set_el D).
  revert H.
  use factor_through_squash.
  {
    apply propproperty.
  }
  intro i.
  refine (hinhpr (i ,, _)).
  apply is_min_bottom_dcppo.

6. Principal lower sets for the way-below relation

Definition way_below_principal
           {X : dcpo}
           (x : X)
  : UU
  := ∑ (y : X ), y ≪ x.

Notation "↡ x" := (way_below_principal x) (at level 10).
Definition way_below_principal_incl
           {X : dcpo}
           (x : X)
  : ↡ x → X
  := pr1.