Library UniMath.OrderTheory.DCPOs.Examples.Unit
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.
Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow.
Require Import UniMath.OrderTheory.DCPOs.Basis.Basis.
Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.
Local Open Scope dcpo.
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.
Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow.
Require Import UniMath.OrderTheory.DCPOs.Basis.Basis.
Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.
Local Open Scope dcpo.
1. The unit DCPO
Definition unit_dcpo_struct
: dcpo_struct unitset.
Show proof.
Definition unit_dcpo
: dcpo
:= _ ,, 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).
- 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.
Definition unit_dcppo
: dcppo
:= _ ,, unit_dcppo_struct.
: dcppo_struct unitset.
Show proof.
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.
{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.
- 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.
(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)).
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.
Proposition unit_dcpo_basis_laws
: dcpo_basis_laws unit_dcpo unit_dcpo_basis_data.
Show proof.
Definition unit_dcpo_basis
: dcpo_basis unit_dcpo.
Show proof.
Definition dcpo_continuous_struct_unit
: continuous_dcpo_struct unit_dcpo.
Show proof.
: dcpo_basis_data unit_dcpo.
Show proof.
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.
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.
Definition dcpo_continuous_struct_unit
: continuous_dcpo_struct unit_dcpo.
Show proof.