Library UniMath.OrderTheory.DCPOs.Examples.Products
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.Examples.Propositions.
Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO.
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.Examples.Propositions.
Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO.
Local Open Scope dcpo.
1. Type indexed products
Section TypeIndexedProductsDCPO.
Context {I : UU}
(D : I → dcpo).
Definition app_directed_set_depfun
(E : directed_set
(depfunction_poset (λ i, D i) (λ i, D i)))
(i : I)
: directed_set (D i).
Show proof.
Section DepFunctionLub.
Context (E : directed_set
(depfunction_poset (λ i, D i) (λ i, D i))).
Definition type_prod_pointwise_lub
(i : I)
: D i
:= ⨆ (app_directed_set_depfun E i).
Proposition is_lub_type_prod_pointwise_lub
: is_least_upperbound
(depfunction_poset (λ i : I, D i) (λ i : I, D i))
E
type_prod_pointwise_lub.
Show proof.
Definition directed_complete_depfunction
: directed_complete_poset
(depfunction_poset (λ i, D i) (λ i, D i)).
Show proof.
Definition depfunction_dcpo_struct
: dcpo_struct (∏ y, D y)%set
:= depfunction_poset _ (λ i, D i) ,, directed_complete_depfunction.
Definition depfunction_dcpo
: dcpo
:= _ ,, depfunction_dcpo_struct.
Context {I : UU}
(D : I → dcpo).
Definition app_directed_set_depfun
(E : directed_set
(depfunction_poset (λ i, D i) (λ i, D i)))
(i : I)
: directed_set (D i).
Show proof.
use make_directed_set.
- exact E.
- exact (λ e, E e i).
- split.
+ exact (directed_set_el E).
+ abstract
(intros e₁ e₂ ;
assert (k := directed_set_top E e₁ e₂) ;
revert k ;
use factor_through_squash ; [ apply propproperty | ] ;
intros k ;
induction k as [ k [ H₁ H₂ ]] ;
exact (hinhpr (k ,, (H₁ i ,, H₂ i)))).
- exact E.
- exact (λ e, E e i).
- split.
+ exact (directed_set_el E).
+ abstract
(intros e₁ e₂ ;
assert (k := directed_set_top E e₁ e₂) ;
revert k ;
use factor_through_squash ; [ apply propproperty | ] ;
intros k ;
induction k as [ k [ H₁ H₂ ]] ;
exact (hinhpr (k ,, (H₁ i ,, H₂ i)))).
Section DepFunctionLub.
Context (E : directed_set
(depfunction_poset (λ i, D i) (λ i, D i))).
Definition type_prod_pointwise_lub
(i : I)
: D i
:= ⨆ (app_directed_set_depfun E i).
Proposition is_lub_type_prod_pointwise_lub
: is_least_upperbound
(depfunction_poset (λ i : I, D i) (λ i : I, D i))
E
type_prod_pointwise_lub.
Show proof.
split.
- intros e i ; cbn.
use less_than_dcpo_lub ; [ exact e | ] ; cbn.
apply refl_dcpo.
- intros f Hf i.
use dcpo_lub_is_least.
intro e ; cbn.
exact (Hf e i).
End DepFunctionLub.- intros e i ; cbn.
use less_than_dcpo_lub ; [ exact e | ] ; cbn.
apply refl_dcpo.
- intros f Hf i.
use dcpo_lub_is_least.
intro e ; cbn.
exact (Hf e i).
Definition directed_complete_depfunction
: directed_complete_poset
(depfunction_poset (λ i, D i) (λ i, D i)).
Show proof.
intros J E HE.
use make_lub.
- exact (type_prod_pointwise_lub (J ,, (E ,, HE))).
- exact (is_lub_type_prod_pointwise_lub (J ,, (E ,, HE))).
use make_lub.
- exact (type_prod_pointwise_lub (J ,, (E ,, HE))).
- exact (is_lub_type_prod_pointwise_lub (J ,, (E ,, HE))).
Definition depfunction_dcpo_struct
: dcpo_struct (∏ y, D y)%set
:= depfunction_poset _ (λ i, D i) ,, directed_complete_depfunction.
Definition depfunction_dcpo
: dcpo
:= _ ,, depfunction_dcpo_struct.
2. The universal property
Proposition is_scott_continuous_depfunction_pr
(i : I)
: is_scott_continuous
depfunction_dcpo
(D i)
(λ f, f i).
Show proof.
Proposition is_scott_continuous_depfunction_map
{W : dcpo}
(fs : ∏ (i : I), scott_continuous_map W (D i))
: is_scott_continuous W depfunction_dcpo (λ w i, fs i w).
Show proof.
(i : I)
: is_scott_continuous
depfunction_dcpo
(D i)
(λ f, f i).
Show proof.
use make_is_scott_continuous.
- exact (is_monotone_depfunction_poset_pr (λ i, D i) (λ i, D i) i).
- intros E.
cbn ; unfold type_prod_pointwise_lub.
use antisymm_dcpo.
+ use dcpo_lub_is_least ; cbn.
intro e.
use less_than_dcpo_lub ; [ exact e | ] ; cbn.
apply refl_dcpo.
+ use dcpo_lub_is_least ; cbn.
intro e.
use less_than_dcpo_lub ; [ exact e | ] ; cbn.
apply refl_dcpo.
- exact (is_monotone_depfunction_poset_pr (λ i, D i) (λ i, D i) i).
- intros E.
cbn ; unfold type_prod_pointwise_lub.
use antisymm_dcpo.
+ use dcpo_lub_is_least ; cbn.
intro e.
use less_than_dcpo_lub ; [ exact e | ] ; cbn.
apply refl_dcpo.
+ use dcpo_lub_is_least ; cbn.
intro e.
use less_than_dcpo_lub ; [ exact e | ] ; cbn.
apply refl_dcpo.
Proposition is_scott_continuous_depfunction_map
{W : dcpo}
(fs : ∏ (i : I), scott_continuous_map W (D i))
: is_scott_continuous W depfunction_dcpo (λ w i, fs i w).
Show proof.
use make_is_scott_continuous.
- exact (is_monotone_depfunction_poset_pair fs (λ i, pr12 (fs i))).
- intros E.
use funextsec ; intro i.
cbn ; unfold type_prod_pointwise_lub.
rewrite scott_continuous_map_on_lub.
use antisymm_dcpo.
+ use dcpo_lub_is_least ; cbn.
intro e.
use less_than_dcpo_lub ; [ exact e | ] ; cbn.
apply refl_dcpo.
+ use dcpo_lub_is_least ; cbn.
intro e.
use less_than_dcpo_lub ; [ exact e | ] ; cbn.
apply refl_dcpo.
End TypeIndexedProductsDCPO.- exact (is_monotone_depfunction_poset_pair fs (λ i, pr12 (fs i))).
- intros E.
use funextsec ; intro i.
cbn ; unfold type_prod_pointwise_lub.
rewrite scott_continuous_map_on_lub.
use antisymm_dcpo.
+ use dcpo_lub_is_least ; cbn.
intro e.
use less_than_dcpo_lub ; [ exact e | ] ; cbn.
apply refl_dcpo.
+ use dcpo_lub_is_least ; cbn.
intro e.
use less_than_dcpo_lub ; [ exact e | ] ; cbn.
apply refl_dcpo.
3. It is pointed
Definition depfunction_dcppo_struct
{I : UU}
(D : I → dcppo)
: dcppo_struct (∏ y, D y)%set.
Show proof.
Definition depfunction_dcppo
{I : UU}
(D : I → dcppo)
: dcppo
:= _ ,, depfunction_dcppo_struct D.
Proposition is_strict_scott_continuous_depfunction_pr
{I : UU}
(D : I → dcppo)
(i : I)
: is_strict_scott_continuous
(depfunction_dcppo_struct D)
(D i)
(λ f, f i).
Show proof.
Proposition is_strict_scott_continuous_depfunction_map
{I : UU}
(D : I → dcppo)
{W : dcppo}
(fs : ∏ (i : I), strict_scott_continuous_map W (D i))
: is_strict_scott_continuous
W
(depfunction_dcppo D)
(λ w i, fs i w).
Show proof.
{I : UU}
(D : I → dcppo)
: dcppo_struct (∏ y, D y)%set.
Show proof.
simple refine (depfunction_dcpo_struct (λ i, D i) ,, _ ,, _).
- exact (λ i, ⊥_{ D i }).
- abstract
(intros f i ; cbn ;
apply is_min_bottom_dcppo).
- exact (λ i, ⊥_{ D i }).
- abstract
(intros f i ; cbn ;
apply is_min_bottom_dcppo).
Definition depfunction_dcppo
{I : UU}
(D : I → dcppo)
: dcppo
:= _ ,, depfunction_dcppo_struct D.
Proposition is_strict_scott_continuous_depfunction_pr
{I : UU}
(D : I → dcppo)
(i : I)
: is_strict_scott_continuous
(depfunction_dcppo_struct D)
(D i)
(λ f, f i).
Show proof.
Proposition is_strict_scott_continuous_depfunction_map
{I : UU}
(D : I → dcppo)
{W : dcppo}
(fs : ∏ (i : I), strict_scott_continuous_map W (D i))
: is_strict_scott_continuous
W
(depfunction_dcppo D)
(λ w i, fs i w).
Show proof.
simple refine (_ ,, _).
- exact (is_scott_continuous_depfunction_map D fs).
- use funextsec.
intro.
apply strict_scott_continuous_map_on_point.
- exact (is_scott_continuous_depfunction_map D fs).
- use funextsec.
intro.
apply strict_scott_continuous_map_on_point.
4. Functions to a fixed DCPO
Definition funset_dcpo
(X : UU)
(D : dcpo)
: dcpo
:= @depfunction_dcpo X (λ _, D).
Definition funset_dcppo
(X : UU)
(D : dcppo)
: dcppo
:= @depfunction_dcppo X (λ _, D).
(X : UU)
(D : dcpo)
: dcpo
:= @depfunction_dcpo X (λ _, D).
Definition funset_dcppo
(X : UU)
(D : dcppo)
: dcppo
:= @depfunction_dcppo X (λ _, D).
5. The subtype DCPO
6. The DCPO of monotone functions
Proposition lub_is_monotone
{X Y : dcpo}
(D : directed_set (funset_dcpo X Y))
(HD : ∏ (d : D), is_monotone X Y (D d))
: is_monotone X Y (⨆ D).
Show proof.
Definition monotone_map_dcpo
(X Y : dcpo)
: dcpo
:= sub_dcpo
(funset_dcpo X Y)
(λ f, make_hProp (is_monotone X Y f) (isaprop_is_monotone _ _ _))
lub_is_monotone.
{X Y : dcpo}
(D : directed_set (funset_dcpo X Y))
(HD : ∏ (d : D), is_monotone X Y (D d))
: is_monotone X Y (⨆ D).
Show proof.
intros x y p.
use dcpo_lub_is_least.
intro d ; cbn in d ; cbn.
use less_than_dcpo_lub.
{
exact d.
}
cbn.
apply HD.
exact p.
use dcpo_lub_is_least.
intro d ; cbn in d ; cbn.
use less_than_dcpo_lub.
{
exact d.
}
cbn.
apply HD.
exact p.
Definition monotone_map_dcpo
(X Y : dcpo)
: dcpo
:= sub_dcpo
(funset_dcpo X Y)
(λ f, make_hProp (is_monotone X Y f) (isaprop_is_monotone _ _ _))
lub_is_monotone.