Library UniMath.CategoryTheory.DisplayedCats.Examples.PointedDCPOStrict

1. Structures of dcppos with strict functions
Definition struct_pointed_dcppo_strict_data
  : hset_struct_data.
Show proof.
  simple refine (_ ,, _).
  - exact (λ X, dcppo_struct X).
  - exact (λ X Y DX DY f, is_strict_scott_continuous DX DY f).

Definition struct_dcpoo_strict_laws
  : hset_struct_laws struct_pointed_dcppo_strict_data.
Show proof.
  split5.
  - intro X.
    use isaset_total2.
    + apply isaset_dcpo_struct.
    + intro PX.
      use isaset_total2.
      * apply setproperty.
      * intro.
        use impred_isaset.
        intro.
        apply isasetaprop.
        apply propproperty.
  - intros X Y DX DY f.
    apply isaprop_is_strict_scott_continuous.
  - intros X DX.
    apply id_is_strict_scott_continuous.
  - intros X Y Z DX DY DZ f g Df Dg.
    exact (comp_is_strict_scott_continuous Df Dg).
  - intros X PX PX' p q ; cbn in *.
    exact (eq_dcppo_strict_struct _ _ p q).

Definition struct_dcppo_strict
  : hset_struct
  := struct_pointed_dcppo_strict_data ,, struct_dcpoo_strict_laws.

Definition DCPPO_strict
  : univalent_category
  := univalent_category_of_hset_struct struct_dcppo_strict.

Definition DCPPO_strict_underlying
  : DCPPO_strict SET
  := underlying_of_hset_struct struct_dcppo_strict.

2. The cartesian structure of dcppos
Definition cartesian_struct_dcppo_strict_data
  : hset_cartesian_struct_data
  := struct_dcppo_strict
     ,,
     unit_dcppo_struct
     ,,
     λ X Y DX DY, prod_dcppo_struct DX DY.

Definition cartesian_struct_dcppo_strict_laws
  : hset_cartesian_struct_laws cartesian_struct_dcppo_strict_data.
Show proof.
  refine (_ ,, _ ,, _ ,, _).
  - intros X DX ; cbn in *.
    apply is_strict_scott_continuous_constant.
  - intros X Y DX DY.
    apply is_strict_scott_continuous_dirprod_pr1.
  - intros X Y DX DY.
    apply is_strict_scott_continuous_dirprod_pr2.
  - intros W X Y DW DX DY f g Df Dg.
    exact (is_strict_scott_continuous_prodtofun Df Dg).

Definition cartesian_struct_dcppo_strict
  : hset_cartesian_struct
  := cartesian_struct_dcppo_strict_data
     ,,
     cartesian_struct_dcppo_strict_laws.

3. Structure on the category of DCPPOs
Definition equalizers_struct_dcppo_strict
  : hset_equalizer_struct struct_dcppo_strict.
Show proof.
  simple refine (_ ,, _).
  - intros X Y f g DX DY Df Dg.
    exact (@equalizer_dcppo_struct (X ,, DX) (Y ,, DY) (f ,, Df) (g ,, Dg)).
  - split.
    + abstract
        (intros X Y f g DX DY Df Dg ; cbn in * ;
         exact (@is_strict_scott_continuous_equalizer_pr1
                  (X ,, DX) (Y ,, DY) (f ,, Df) (g ,, Dg))).
    + abstract
        (intros X Y f g DX DY Df Dg W DW h Dh q ;
         exact (@is_strict_scott_continuous_equalizer_map
                  (X ,, DX) (Y ,, DY)
                  (f ,, Df) (g ,, Dg)
                  (W ,, DW)
                  (h ,, Dh)
                  q)).

Definition type_products_struct_dcppo_strict
           (I : UU)
  : hset_struct_type_prod struct_dcppo_strict I.
Show proof.
  simple refine (_ ,, _).
  - exact (λ D PD, depfunction_dcppo_struct (λ i, D i ,, PD i)).
  - split ; cbn.
    + abstract
        (intros D PD i ;
         exact (@is_strict_scott_continuous_depfunction_pr
                  I
                  (λ i, D i ,, PD i)
                  i)).
    + abstract
        (intros D PD W DW fs Hfs ;
         exact (@is_strict_scott_continuous_depfunction_map
                  I
                  (λ i, D i ,, PD i)
                  (W ,, DW)
                  (λ i, fs i ,, Hfs i))).

Definition Terminal_DCPPO_strict
  : Terminal DCPPO_strict
  := Terminal_category_of_hset_struct cartesian_struct_dcppo_strict.

Definition BinProducts_DCPPO_strict
  : BinProducts DCPPO_strict
  := BinProducts_category_of_hset_struct cartesian_struct_dcppo_strict.

Definition Equalizers_DCPPO_strict
  : Equalizers DCPPO_strict
  := Equalizers_category_of_hset_struct equalizers_struct_dcppo_strict.

Definition Products_DCPPO_strict
           (I : UU)
  : Products I DCPPO_strict
  := Products_category_of_hset_struct_type_prod
       (type_products_struct_dcppo_strict I).

Definition Initial_DCPPO_strict
  : Initial DCPPO_strict.
Show proof.
  use make_Initial.
  - exact unit_dcppo.
  - intros Y.
    use iscontraprop1.
    + abstract
        (use invproofirrelevance ;
         intros f₁ f₂ ;
         use (@eq_strict_scott_continuous_map unit_dcppo Y f₁ f₂) ;
         intro x ;
         induction x ;
         refine (@strict_scott_continuous_map_on_point unit_dcppo _ f₁ @ !_) ;
         exact (@strict_scott_continuous_map_on_point unit_dcppo _ f₂)).
    + refine ((λ _, _{Y}) ,, _).
      abstract
        (cbn ;
         apply is_strict_scott_continuous_constant).

4. Dcppos form a pointed structure