Library UniMath.OrderTheory.DCPOs.Examples.Propositions

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.OrderTheory.Posets.Basics.
Require Import UniMath.OrderTheory.Posets.PointedPosets.
Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.
Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.
Require Import UniMath.OrderTheory.DCPOs.Core.Basics.
Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous.

Local Open Scope dcpo.

1. hProp is a DCPO

Proposition isPartialOrder_hProp
: isPartialOrder (λ (P₁ P₂ : hProp ), (P₁ ⇒ P₂)%logic).
Show proof.

  refine ((_ ,, _) ,, _).
  - exact (λ P₁ P₂ P₃ f g x , g(f x)).
  - exact (λ P x , x).
  - exact (λ P₁ P₂ f g , hPropUnivalence _ _ f g).

Definition hProp_PartialOrder
: PartialOrder hProp_set.
Show proof.

  use make_PartialOrder.
  - exact (λ (P₁ P₂ : hProp ), P₁ ⇒ P₂)%logic.
  - exact isPartialOrder_hProp.

Definition hProp_lub
           {D : UU}
           {f : D → hProp}
           (Hf : is_directed hProp_PartialOrder f)
  : lub hProp_PartialOrder f.
Show proof.

  use make_lub.
  - exact (∃ (d : D), f d).
  - refine (_ ,, _).
    + exact (λ d x , hinhpr (d ,, x)).
    + abstract
        (intros P HP ;
         use factor_through_squash ; [ apply propproperty | ] ;
         intro x ;
         exact (HP (pr1 x) (pr2 x))).

Definition hProp_dcpo_struct
: dcpo_struct hProp_set.
Show proof.

  use make_dcpo_struct.
  - exact hProp_PartialOrder.
  - exact (λ D f Hf , hProp_lub Hf).

Definition hProp_dcpo
: dcpo
:= _ ,, hProp_dcpo_struct.

2. hProp is pointed

Definition hProp_dcppo
: dcppo.
Show proof.

  refine (_ ,, hProp_dcpo_struct ,, hfalse ,, _).
  abstract
    (intros P ;
     exact fromempty).