Library UniMath.OrderTheory.DCPOs.Examples.Unit

1. The unit DCPO
Definition unit_dcpo_struct
  : dcpo_struct unitset.
Show proof.
  use make_dcpo_struct.
  - exact unit_PartialOrder.
  - intros I D HD.
    use make_lub.
    + exact tt.
    + split.
      * abstract
          (intro i ; cbn ;
           exact tt).
      * abstract
          (intros i Hi ; cbn ;
           exact tt).

Definition unit_dcpo
  : dcpo
  := _ ,, unit_dcpo_struct.

2. The unit DCPO is pointed
Definition unit_dcppo_struct
  : dcppo_struct unitset.
Show proof.
  refine (unit_dcpo_struct ,, _).
  refine (tt ,, _).
  abstract
    (intro x ;
     cbn ;
     exact tt).

Definition unit_dcppo
  : dcppo
  := _ ,, unit_dcppo_struct.

3. The universal property
Proposition is_scott_continuous_to_unit
            {X : hSet}
            (DX : dcpo_struct X)
  : is_scott_continuous DX unit_dcpo_struct (λ _, tt).
Show proof.
  split.
  - intros x y p.
    exact tt.
  - intros I D HD x Hx.
    split.
    + intro ; cbn.
      exact tt.
    + intros ? ? ; cbn.
      exact tt.

4. The way below relation
Proposition unit_dcpo_way_below
            (x y : unit_dcpo)
  : x y.
Show proof.
  intros D HD.
  assert (H := directed_set_el D).
  revert H.
  use factor_through_squash.
  {
    apply propproperty.
  }
  intro d.
  exact (hinhpr (d ,, tt)).

5. A basis for the unit DCPO
Definition unit_dcpo_basis_data
  : dcpo_basis_data unit_dcpo.
Show proof.
  use make_dcpo_basis_data.
  - exact unit.
  - exact (λ _, tt).

Proposition unit_dcpo_basis_laws
  : dcpo_basis_laws unit_dcpo unit_dcpo_basis_data.
Show proof.
  intro x.
  split.
  - split.
    + refine (hinhpr (tt ,, _)).
      apply unit_dcpo_way_below.
    + intros i j.
      refine (hinhpr ((tt ,, _) ,, (tt ,, tt))).
      apply unit_dcpo_way_below.
  - split.
    + intro ; exact tt.
    + intros ? ?.
      exact tt.

Definition unit_dcpo_basis
  : dcpo_basis unit_dcpo.
Show proof.
  use make_dcpo_basis.
  - exact unit_dcpo_basis_data.
  - exact unit_dcpo_basis_laws.

Definition dcpo_continuous_struct_unit
  : continuous_dcpo_struct unit_dcpo.
Show proof.