Library UniMath.OrderTheory.DCPOs.Basis.Continuous
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.
Require Import UniMath.OrderTheory.DCPOs.Core.Basics.
Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow.
Local Open Scope dcpo.
Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.
Require Import UniMath.OrderTheory.DCPOs.Core.Basics.
Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow.
Local Open Scope dcpo.
1. Continuous DCPOs (as structure)
Definition continuous_dcpo_struct
(X : dcpo)
: UU
:= ∏ (x : X),
∑ (D : directed_set X),
(∏ (i : D), D i ≪ x)
×
is_least_upperbound X D x.
(X : dcpo)
: UU
:= ∏ (x : X),
∑ (D : directed_set X),
(∏ (i : D), D i ≪ x)
×
is_least_upperbound X D x.
2. Continuous DCPOs (as property)
Definition is_continuous_dcpo
(X : dcpo)
: hProp
:= ∥ continuous_dcpo_struct X ∥.
Section ContinuousDCPOAccessors.
Context {X : dcpo}
(CX : continuous_dcpo_struct X).
Definition approximating_family
(x : X)
: directed_set X
:= pr1 (CX x).
Proposition approximating_family_way_below
(x : X)
(i : approximating_family x)
: approximating_family x i ≪ x.
Show proof.
Proposition approximating_family_lub
(x : X)
: ⨆ (approximating_family x) = x.
Show proof.
Section PropertiesContinuousDCPO.
Context {X : dcpo}
(CX : continuous_dcpo_struct X).
(X : dcpo)
: hProp
:= ∥ continuous_dcpo_struct X ∥.
Section ContinuousDCPOAccessors.
Context {X : dcpo}
(CX : continuous_dcpo_struct X).
Definition approximating_family
(x : X)
: directed_set X
:= pr1 (CX x).
Proposition approximating_family_way_below
(x : X)
(i : approximating_family x)
: approximating_family x i ≪ x.
Show proof.
Proposition approximating_family_lub
(x : X)
: ⨆ (approximating_family x) = x.
Show proof.
use antisymm_dcpo.
- use dcpo_lub_is_least.
intro i.
apply way_below_to_le.
exact (approximating_family_way_below x i).
- use (is_least_upperbound_is_least (pr22 (CX x))).
apply is_least_upperbound_is_upperbound.
apply is_least_upperbound_dcpo_lub.
End ContinuousDCPOAccessors.- use dcpo_lub_is_least.
intro i.
apply way_below_to_le.
exact (approximating_family_way_below x i).
- use (is_least_upperbound_is_least (pr22 (CX x))).
apply is_least_upperbound_is_upperbound.
apply is_least_upperbound_dcpo_lub.
Section PropertiesContinuousDCPO.
Context {X : dcpo}
(CX : continuous_dcpo_struct X).
3. Equivalent formulations of inequality in continuous DCPOs
Proposition continuous_dcpo_struct_le_to_way_below
{x y : X}
(p : x ⊑ y)
(i : approximating_family CX x)
: approximating_family CX x i ≪ y.
Show proof.
Proposition continuous_dcpo_struct_approx_way_below_to_le
{x y : X}
(p : ∏ (i : approximating_family CX x),
approximating_family CX x i ≪ y)
(i : approximating_family CX x)
: approximating_family CX x i ⊑ y.
Show proof.
Proposition continuous_dcpo_struct_approx_le_to_le
{x y : X}
(p : ∏ (i : approximating_family CX x),
approximating_family CX x i ⊑ y)
: x ⊑ y.
Show proof.
Proposition continuous_dcpo_struct_le_weq_approx_le
(x y : X)
: x ⊑ y
≃
∀ (i : approximating_family CX x),
approximating_family CX x i ⊑ y.
Show proof.
Proposition continuous_dcpo_struct_le_weq_approx_way_below
(x y : X)
: x ⊑ y
≃
∀ (i : approximating_family CX x),
approximating_family CX x i ≪ y.
Show proof.
Proposition continuous_dcpo_struct_le_via_approximation
(x y : X)
: x ⊑ y
≃
∀ (z : X), (z ≪ x ⇒ z ≪ y)%logic.
Show proof.
{x y : X}
(p : x ⊑ y)
(i : approximating_family CX x)
: approximating_family CX x i ≪ y.
Show proof.
Proposition continuous_dcpo_struct_approx_way_below_to_le
{x y : X}
(p : ∏ (i : approximating_family CX x),
approximating_family CX x i ≪ y)
(i : approximating_family CX x)
: approximating_family CX x i ⊑ y.
Show proof.
Proposition continuous_dcpo_struct_approx_le_to_le
{x y : X}
(p : ∏ (i : approximating_family CX x),
approximating_family CX x i ⊑ y)
: x ⊑ y.
Show proof.
Proposition continuous_dcpo_struct_le_weq_approx_le
(x y : X)
: x ⊑ y
≃
∀ (i : approximating_family CX x),
approximating_family CX x i ⊑ y.
Show proof.
use weqimplimpl.
- intros p i.
apply continuous_dcpo_struct_approx_way_below_to_le.
intro j.
apply continuous_dcpo_struct_le_to_way_below.
exact p.
- intros H.
apply continuous_dcpo_struct_approx_le_to_le.
exact H.
- apply propproperty.
- apply propproperty.
- intros p i.
apply continuous_dcpo_struct_approx_way_below_to_le.
intro j.
apply continuous_dcpo_struct_le_to_way_below.
exact p.
- intros H.
apply continuous_dcpo_struct_approx_le_to_le.
exact H.
- apply propproperty.
- apply propproperty.
Proposition continuous_dcpo_struct_le_weq_approx_way_below
(x y : X)
: x ⊑ y
≃
∀ (i : approximating_family CX x),
approximating_family CX x i ≪ y.
Show proof.
use weqimplimpl.
- exact continuous_dcpo_struct_le_to_way_below.
- intros H.
apply continuous_dcpo_struct_approx_le_to_le.
intro i.
apply continuous_dcpo_struct_approx_way_below_to_le.
exact H.
- apply propproperty.
- apply propproperty.
- exact continuous_dcpo_struct_le_to_way_below.
- intros H.
apply continuous_dcpo_struct_approx_le_to_le.
intro i.
apply continuous_dcpo_struct_approx_way_below_to_le.
exact H.
- apply propproperty.
- apply propproperty.
Proposition continuous_dcpo_struct_le_via_approximation
(x y : X)
: x ⊑ y
≃
∀ (z : X), (z ≪ x ⇒ z ≪ y)%logic.
Show proof.
use weqimplimpl.
- intros p z q.
exact (trans_way_below_le q p).
- intros H.
rewrite <- (approximating_family_lub CX x).
use dcpo_lub_is_least.
pose (D := approximating_family CX x).
fold D.
intro i.
apply way_below_to_le.
apply (H (D i)).
apply approximating_family_way_below.
- apply propproperty.
- apply propproperty.
- intros p z q.
exact (trans_way_below_le q p).
- intros H.
rewrite <- (approximating_family_lub CX x).
use dcpo_lub_is_least.
pose (D := approximating_family CX x).
fold D.
intro i.
apply way_below_to_le.
apply (H (D i)).
apply approximating_family_way_below.
- apply propproperty.
- apply propproperty.
4. Characterization of the way-below relation in continuous DCPOs
Proposition continuous_dcpo_struct_way_below
(x y : X)
: x ≪ y
≃
∃ (i : approximating_family CX y), x ⊑ approximating_family CX y i.
Show proof.
(x y : X)
: x ≪ y
≃
∃ (i : approximating_family CX y), x ⊑ approximating_family CX y i.
Show proof.
use weqimplimpl.
- intro p.
apply (p (approximating_family CX y)).
rewrite approximating_family_lub.
apply refl_dcpo.
- use factor_through_squash.
{
apply propproperty.
}
intro H.
induction H as [ i p ].
refine (trans_le_way_below p _).
apply approximating_family_way_below.
- apply propproperty.
- apply propproperty.
- intro p.
apply (p (approximating_family CX y)).
rewrite approximating_family_lub.
apply refl_dcpo.
- use factor_through_squash.
{
apply propproperty.
}
intro H.
induction H as [ i p ].
refine (trans_le_way_below p _).
apply approximating_family_way_below.
- apply propproperty.
- apply propproperty.
5. Nullary interpolation
Proposition nullary_interpolation
(x : X)
: ∃ (y : X), y ≪ x.
Show proof.
(x : X)
: ∃ (y : X), y ≪ x.
Show proof.
pose (D := approximating_family CX x).
assert (H := directed_set_el D).
revert H.
use factor_through_squash.
{
apply propproperty.
}
intro i.
refine (hinhpr (D i ,, _)).
apply approximating_family_way_below.
assert (H := directed_set_el D).
revert H.
use factor_through_squash.
{
apply propproperty.
}
intro i.
refine (hinhpr (D i ,, _)).
apply approximating_family_way_below.
6. Unary interpolation
Section UnaryInterpolation.
Context {x y : X}
(p : x ≪ y).
Let D : directed_set X := approximating_family CX y.
Let D_a : D → directed_set X := λ i, approximating_family CX (D i).
Proposition unary_interpolation_cofinal_lem
{i₁ i₂ : D}
(q : D i₁ ⊑ D i₂)
(j₁ : D_a i₁)
: D_a i₁ j₁ ≪ ⨆ (D_a i₂).
Show proof.
Proposition unary_interpolation_cofinal
{i₁ i₂ : D}
(q : D i₁ ⊑ D i₂)
(j₁ : D_a i₁)
: ∃ (j₂ : D_a i₂), D_a i₁ j₁ ⊑ D_a i₂ j₂.
Show proof.
Proposition is_directed_unary_interpolation_directed_set
: is_directed X (λ (ij : ∑ (i : D), D_a i), D_a (pr1 ij) (pr2 ij)).
Show proof.
Definition unary_interpolation_directed_set
: directed_set X.
Show proof.
Proposition unary_interpolation
: ∃ (z : X), x ≪ z ∧ z ≪ y.
Show proof.
Context {x y : X}
(p : x ≪ y).
Let D : directed_set X := approximating_family CX y.
Let D_a : D → directed_set X := λ i, approximating_family CX (D i).
Proposition unary_interpolation_cofinal_lem
{i₁ i₂ : D}
(q : D i₁ ⊑ D i₂)
(j₁ : D_a i₁)
: D_a i₁ j₁ ≪ ⨆ (D_a i₂).
Show proof.
refine (trans_way_below_le _ _).
- apply approximating_family_way_below.
- refine (trans_dcpo q _).
unfold D_a.
rewrite approximating_family_lub.
apply refl_dcpo.
- apply approximating_family_way_below.
- refine (trans_dcpo q _).
unfold D_a.
rewrite approximating_family_lub.
apply refl_dcpo.
Proposition unary_interpolation_cofinal
{i₁ i₂ : D}
(q : D i₁ ⊑ D i₂)
(j₁ : D_a i₁)
: ∃ (j₂ : D_a i₂), D_a i₁ j₁ ⊑ D_a i₂ j₂.
Show proof.
Proposition is_directed_unary_interpolation_directed_set
: is_directed X (λ (ij : ∑ (i : D), D_a i), D_a (pr1 ij) (pr2 ij)).
Show proof.
split.
- assert (H := directed_set_el D).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intro i.
assert (H := directed_set_el (D_a i)).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intro j.
exact (hinhpr (i ,, j)).
- intros ij₁ ij₂.
induction ij₁ as [ i₁ j₁ ].
induction ij₂ as [ i₂ j₂ ].
assert (H := directed_set_top D i₁ i₂).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intros k.
induction k as [ k [ q₁ q₂ ]].
assert (H := unary_interpolation_cofinal q₁ j₁).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intros H₁.
induction H₁ as [ l₁ H₁ ].
assert (H := unary_interpolation_cofinal q₂ j₂).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intros H₂.
induction H₂ as [ l₂ H₂ ].
assert (H := directed_set_top (D_a k) l₁ l₂).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intros H.
induction H as [ m [ r₁ r₂ ]].
refine (hinhpr ((k ,, m) ,, _ ,, _)).
+ exact (trans_dcpo H₁ r₁).
+ exact (trans_dcpo H₂ r₂).
- assert (H := directed_set_el D).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intro i.
assert (H := directed_set_el (D_a i)).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intro j.
exact (hinhpr (i ,, j)).
- intros ij₁ ij₂.
induction ij₁ as [ i₁ j₁ ].
induction ij₂ as [ i₂ j₂ ].
assert (H := directed_set_top D i₁ i₂).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intros k.
induction k as [ k [ q₁ q₂ ]].
assert (H := unary_interpolation_cofinal q₁ j₁).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intros H₁.
induction H₁ as [ l₁ H₁ ].
assert (H := unary_interpolation_cofinal q₂ j₂).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intros H₂.
induction H₂ as [ l₂ H₂ ].
assert (H := directed_set_top (D_a k) l₁ l₂).
revert H.
use factor_through_squash ; [ apply propproperty | ].
intros H.
induction H as [ m [ r₁ r₂ ]].
refine (hinhpr ((k ,, m) ,, _ ,, _)).
+ exact (trans_dcpo H₁ r₁).
+ exact (trans_dcpo H₂ r₂).
Definition unary_interpolation_directed_set
: directed_set X.
Show proof.
use make_directed_set.
- exact (∑ (i : D), D_a i).
- exact (λ ij, D_a (pr1 ij) (pr2 ij)).
- exact is_directed_unary_interpolation_directed_set.
- exact (∑ (i : D), D_a i).
- exact (λ ij, D_a (pr1 ij) (pr2 ij)).
- exact is_directed_unary_interpolation_directed_set.
Proposition unary_interpolation
: ∃ (z : X), x ≪ z ∧ z ≪ y.
Show proof.
assert (s : y ⊑ ⨆ unary_interpolation_directed_set).
{
apply continuous_dcpo_struct_approx_le_to_le.
intro i.
use continuous_dcpo_struct_approx_le_to_le.
intro j.
use less_than_dcpo_lub.
{
exact (i ,, j).
}
apply refl_dcpo.
}
assert (H := p unary_interpolation_directed_set s).
revert H.
use factor_through_squash.
{
apply propproperty.
}
intro i.
induction i as [ i r ].
refine (hinhpr (D (pr1 i) ,, _ ,, _)).
- refine (trans_le_way_below r _).
apply approximating_family_way_below.
- apply approximating_family_way_below.
End UnaryInterpolation.{
apply continuous_dcpo_struct_approx_le_to_le.
intro i.
use continuous_dcpo_struct_approx_le_to_le.
intro j.
use less_than_dcpo_lub.
{
exact (i ,, j).
}
apply refl_dcpo.
}
assert (H := p unary_interpolation_directed_set s).
revert H.
use factor_through_squash.
{
apply propproperty.
}
intro i.
induction i as [ i r ].
refine (hinhpr (D (pr1 i) ,, _ ,, _)).
- refine (trans_le_way_below r _).
apply approximating_family_way_below.
- apply approximating_family_way_below.
7. Binary interpolation
Proposition binary_interpolation
{x₁ x₂ y : X}
(p₁ : x₁ ≪ y)
(p₂ : x₂ ≪ y)
: ∃ (z : X), x₁ ≪ z ∧ x₂ ≪ z ∧ z ≪ y.
Show proof.
{x₁ x₂ y : X}
(p₁ : x₁ ≪ y)
(p₂ : x₂ ≪ y)
: ∃ (z : X), x₁ ≪ z ∧ x₂ ≪ z ∧ z ≪ y.
Show proof.
pose (D := approximating_family CX y).
assert (s : y ⊑ ⨆ D).
{
unfold D.
rewrite approximating_family_lub.
apply refl_dcpo.
}
assert (z₁ := unary_interpolation p₁).
revert z₁.
use factor_through_squash.
{
apply propproperty.
}
intro z₁.
induction z₁ as [ z₁ [ q₁ r₁ ]].
assert (H := r₁ D s).
revert H.
use factor_through_squash.
{
apply propproperty.
}
intro H.
induction H as [ i₁ H₁ ].
assert (z₂ := unary_interpolation p₂).
revert z₂.
use factor_through_squash.
{
apply propproperty.
}
intro z₂.
induction z₂ as [ z₂ [ q₂ r₂ ]].
assert (H := r₂ D s).
revert H.
use factor_through_squash.
{
apply propproperty.
}
intro H.
induction H as [ i₂ H₂ ].
assert (H := directed_set_top D i₁ i₂).
revert H.
use factor_through_squash.
{
apply propproperty.
}
intros H.
induction H as [ k [ w₁ w₂ ]].
refine (hinhpr (D k ,, _ ,, _ ,, _)).
- exact (trans_way_below_le q₁ (trans_dcpo H₁ w₁)).
- exact (trans_way_below_le q₂ (trans_dcpo H₂ w₂)).
- apply approximating_family_way_below.
End PropertiesContinuousDCPO.assert (s : y ⊑ ⨆ D).
{
unfold D.
rewrite approximating_family_lub.
apply refl_dcpo.
}
assert (z₁ := unary_interpolation p₁).
revert z₁.
use factor_through_squash.
{
apply propproperty.
}
intro z₁.
induction z₁ as [ z₁ [ q₁ r₁ ]].
assert (H := r₁ D s).
revert H.
use factor_through_squash.
{
apply propproperty.
}
intro H.
induction H as [ i₁ H₁ ].
assert (z₂ := unary_interpolation p₂).
revert z₂.
use factor_through_squash.
{
apply propproperty.
}
intro z₂.
induction z₂ as [ z₂ [ q₂ r₂ ]].
assert (H := r₂ D s).
revert H.
use factor_through_squash.
{
apply propproperty.
}
intro H.
induction H as [ i₂ H₂ ].
assert (H := directed_set_top D i₁ i₂).
revert H.
use factor_through_squash.
{
apply propproperty.
}
intros H.
induction H as [ k [ w₁ w₂ ]].
refine (hinhpr (D k ,, _ ,, _ ,, _)).
- exact (trans_way_below_le q₁ (trans_dcpo H₁ w₁)).
- exact (trans_way_below_le q₂ (trans_dcpo H₂ w₂)).
- apply approximating_family_way_below.
8. Continuity structure from the property
Proposition is_continuous_dcpo_is_directed
{X : dcpo}
(CX : is_continuous_dcpo X)
(x : X)
: is_directed X (λ (z : ∑ (b : X), b ≪ x), pr1 z).
Show proof.
Definition is_continuous_dcpo_directed_set
{X : dcpo}
(CX : is_continuous_dcpo X)
(x : X)
: directed_set X.
Show proof.
Proposition is_continuous_dcpo_directed_set_lub
{X : dcpo}
(CX : is_continuous_dcpo X)
(x : X)
: ⨆ (is_continuous_dcpo_directed_set CX x) = x.
Show proof.
Definition is_continuous_to_continuous_struct
{X : dcpo}
(CX : is_continuous_dcpo X)
: continuous_dcpo_struct X.
Show proof.
{X : dcpo}
(CX : is_continuous_dcpo X)
(x : X)
: is_directed X (λ (z : ∑ (b : X), b ≪ x), pr1 z).
Show proof.
revert CX.
use factor_through_squash_hProp.
intros CX.
pose (D := approximating_family CX x).
split.
- assert (H := directed_set_el D).
revert H.
use factor_through_squash_hProp.
intros d.
use hinhpr.
refine (D d ,, _).
apply approximating_family_way_below.
- intros [ b₁ p₁ ] [ b₂ p₂ ].
assert (x ⊑ ⨆ D) as q.
{
rewrite <- (approximating_family_lub CX x).
apply refl_dcpo.
}
assert (H := way_below_elem p₁ D q).
revert H.
use factor_through_squash_hProp.
intros [ c₁ r₁ ].
assert (H := way_below_elem p₂ D q).
revert H.
use factor_through_squash_hProp.
intros [ c₂ r₂ ].
assert (H := directed_set_top D c₁ c₂).
revert H.
use factor_through_squash_hProp.
intros [ k [ s₂ s₃ ]].
use hinhpr.
simple refine ((D k ,, _) ,, _ ,, _).
+ apply approximating_family_way_below.
+ exact (trans_dcpo r₁ s₂).
+ exact (trans_dcpo r₂ s₃).
use factor_through_squash_hProp.
intros CX.
pose (D := approximating_family CX x).
split.
- assert (H := directed_set_el D).
revert H.
use factor_through_squash_hProp.
intros d.
use hinhpr.
refine (D d ,, _).
apply approximating_family_way_below.
- intros [ b₁ p₁ ] [ b₂ p₂ ].
assert (x ⊑ ⨆ D) as q.
{
rewrite <- (approximating_family_lub CX x).
apply refl_dcpo.
}
assert (H := way_below_elem p₁ D q).
revert H.
use factor_through_squash_hProp.
intros [ c₁ r₁ ].
assert (H := way_below_elem p₂ D q).
revert H.
use factor_through_squash_hProp.
intros [ c₂ r₂ ].
assert (H := directed_set_top D c₁ c₂).
revert H.
use factor_through_squash_hProp.
intros [ k [ s₂ s₃ ]].
use hinhpr.
simple refine ((D k ,, _) ,, _ ,, _).
+ apply approximating_family_way_below.
+ exact (trans_dcpo r₁ s₂).
+ exact (trans_dcpo r₂ s₃).
Definition is_continuous_dcpo_directed_set
{X : dcpo}
(CX : is_continuous_dcpo X)
(x : X)
: directed_set X.
Show proof.
use make_directed_set.
- exact (∑ (b : X), b ≪ x).
- exact (λ z, pr1 z).
- exact (is_continuous_dcpo_is_directed CX x).
- exact (∑ (b : X), b ≪ x).
- exact (λ z, pr1 z).
- exact (is_continuous_dcpo_is_directed CX x).
Proposition is_continuous_dcpo_directed_set_lub
{X : dcpo}
(CX : is_continuous_dcpo X)
(x : X)
: ⨆ (is_continuous_dcpo_directed_set CX x) = x.
Show proof.
revert CX.
use factor_dep_through_squash.
{
intro.
apply setproperty.
}
intros CX.
pose (D := approximating_family CX x).
cbn.
use antisymm_dcpo.
- use dcpo_lub_is_least.
intros i.
apply way_below_to_le.
exact (pr2 i).
- refine (trans_dcpo _ _).
{
apply eq_to_le_dcpo.
exact (!(approximating_family_lub CX x)).
}
use dcpo_lub_is_least.
intros i.
use less_than_dcpo_lub ; cbn -[way_below].
+ refine (D i ,, _).
apply approximating_family_way_below.
+ apply refl_dcpo.
use factor_dep_through_squash.
{
intro.
apply setproperty.
}
intros CX.
pose (D := approximating_family CX x).
cbn.
use antisymm_dcpo.
- use dcpo_lub_is_least.
intros i.
apply way_below_to_le.
exact (pr2 i).
- refine (trans_dcpo _ _).
{
apply eq_to_le_dcpo.
exact (!(approximating_family_lub CX x)).
}
use dcpo_lub_is_least.
intros i.
use less_than_dcpo_lub ; cbn -[way_below].
+ refine (D i ,, _).
apply approximating_family_way_below.
+ apply refl_dcpo.
Definition is_continuous_to_continuous_struct
{X : dcpo}
(CX : is_continuous_dcpo X)
: continuous_dcpo_struct X.
Show proof.
intros x.
refine (is_continuous_dcpo_directed_set CX x ,, _ ,, _).
- abstract
(intros i ;
apply i).
- abstract
(pose (is_least_upperbound_dcpo_lub (is_continuous_dcpo_directed_set CX x)) as h ;
rewrite (is_continuous_dcpo_directed_set_lub CX x) in h ;
exact h).
refine (is_continuous_dcpo_directed_set CX x ,, _ ,, _).
- abstract
(intros i ;
apply i).
- abstract
(pose (is_least_upperbound_dcpo_lub (is_continuous_dcpo_directed_set CX x)) as h ;
rewrite (is_continuous_dcpo_directed_set_lub CX x) in h ;
exact h).