Library UniMath.Partiality.PartialElements
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.PropExt.
Require Import UniMath.MoreFoundations.WeaklyConstant.
Require Import UniMath.Algebra.DCPO.
Delimit Scope PartialElements with PartialElements.
Local Open Scope PartialElements.
Section lift.
Definition lift (X : UU) := ∑ (P : UU), isaprop P × (P -> X).
Notation "'𝓛'" := lift : PartialElements.
Definition lift_embedding {X : UU} (x : X) : 𝓛 X :=
(unit,, isapropunit,, termfun x).
Notation "'η'" := lift_embedding : PartialElements.
Definition isdefined {X : UU} (l : 𝓛 X) : UU := pr1 l.
Lemma isaprop_isdefined {X : UU} (l : 𝓛 X) : isaprop (isdefined l).
Show proof.
Definition lifteq_isdefined {X : UU} {l m : 𝓛 X} :
l = m -> isdefined l -> isdefined m.
Show proof.
Definition value {X : UU} (l : 𝓛 X) : isdefined l -> X.
Show proof.
Definition weaklyconstant_value {X : UU} (l : 𝓛 X) : weaklyconstant (value l).
Show proof.
Definition lifteq_valueeq {X : UU} {l m : 𝓛 X} :
l = m -> ∏ (d : isdefined l), ∏ (d' : isdefined m), value l d = value m d'.
Show proof.
Definition lifteq_necc {X : UU} {l m : 𝓛 X} :
l = m -> ∑ (e : isdefined l <-> isdefined m), value l ∘ pr2 e ~ value m.
Show proof.
intro eq.
apply total2_paths_equiv in eq.
induction eq as [e1 e2].
exists (weq_to_iff (eqweqmap e1)).
intro d.
assert (lem : value l ∘ pr2 (weq_to_iff (eqweqmap e1)) =
pr2 (transportf _ e1 (pr2 l))).
{ generalize e1 as e1'; induction e1'; apply idpath. }
etrans.
+ apply (eqtohomot lem).
+ change (value m d) with (pr2 (pr2 m) d).
use eqtohomot.
exact (maponpaths dirprod_pr2 e2).
apply total2_paths_equiv in eq.
induction eq as [e1 e2].
exists (weq_to_iff (eqweqmap e1)).
intro d.
assert (lem : value l ∘ pr2 (weq_to_iff (eqweqmap e1)) =
pr2 (transportf _ e1 (pr2 l))).
{ generalize e1 as e1'; induction e1'; apply idpath. }
etrans.
+ apply (eqtohomot lem).
+ change (value m d) with (pr2 (pr2 m) d).
use eqtohomot.
exact (maponpaths dirprod_pr2 e2).
Definition lifteq_suff {X : UU} {l m : 𝓛 X} :
(∑ (e : isdefined l <-> isdefined m), value l ∘ pr2 e ~ value m) -> l = m.
Show proof.
intros [e veq].
apply total2_paths_equiv.
assert (eq : isdefined l = isdefined m).
{ apply propext.
- apply isaprop_isdefined.
- apply isaprop_isdefined.
- exact e. }
split with eq.
apply dirprod_paths.
+ apply proofirrelevance. apply isapropisaprop.
+ assert (lem : pr2 (transportf _ eq (pr2 l)) = value l ∘ pr2 e).
{ assert (inveq : invmap (eqweqmap eq) = pr2 e).
{ apply funextfun. intro d. apply proofirrelevance.
apply isaprop_isdefined. }
rewrite <- inveq.
generalize eq as eq'; induction eq'; apply idpath. }
etrans.
++ apply lem.
++ apply funextfun. exact veq.
apply total2_paths_equiv.
assert (eq : isdefined l = isdefined m).
{ apply propext.
- apply isaprop_isdefined.
- apply isaprop_isdefined.
- exact e. }
split with eq.
apply dirprod_paths.
+ apply proofirrelevance. apply isapropisaprop.
+ assert (lem : pr2 (transportf _ eq (pr2 l)) = value l ∘ pr2 e).
{ assert (inveq : invmap (eqweqmap eq) = pr2 e).
{ apply funextfun. intro d. apply proofirrelevance.
apply isaprop_isdefined. }
rewrite <- inveq.
generalize eq as eq'; induction eq'; apply idpath. }
etrans.
++ apply lem.
++ apply funextfun. exact veq.
Definition isdefined_lift_embedding {X : UU} (l : 𝓛 X) (d : isdefined l) :
l = η (value l d).
Show proof.
End lift.
Make notation available outside the section
Section liftorder.
Definition liftorder {X : UU} (l m : 𝓛 X) : UU :=
isdefined l -> l = m.
Notation "l ⊑ m" := (liftorder l m) (at level 30) : PartialElements.
Definition liftorder_antisymmetric {X : UU} :
∏ (l m : 𝓛 X), l ⊑ m -> m ⊑ l -> l = m.
Show proof.
Definition liftorder_reflexive {X : UU} : ∏ (l : 𝓛 X), l ⊑ l.
Show proof.
Definition liftorder_transitive {X : UU} :
∏ (l m n : 𝓛 X), l ⊑ m -> m ⊑ n -> l ⊑ n.
Show proof.
Definition liftorder_least {X : UU} : 𝓛 X := (empty,, isapropempty,, fromempty).
Notation "'⊥'" := liftorder_least : PartialElements.
Definition liftorder_least_isleast {X : UU} : ∏ (l : 𝓛 X), ⊥ ⊑ l.
Show proof.
End liftorder.
Notation "l ⊑ m" := (liftorder l m) (at level 30) : PartialElements.
Delimit Scope LiftDcpo with LiftDcpo.
Local Open Scope LiftDcpo.
Definition liftorder {X : UU} (l m : 𝓛 X) : UU :=
isdefined l -> l = m.
Notation "l ⊑ m" := (liftorder l m) (at level 30) : PartialElements.
Definition liftorder_antisymmetric {X : UU} :
∏ (l m : 𝓛 X), l ⊑ m -> m ⊑ l -> l = m.
Show proof.
intros l m ineqlm ineqml.
apply lifteq_suff.
assert (e : isdefined l <-> isdefined m).
{ split.
- intro dl.
eapply lifteq_isdefined.
+ exact (ineqlm dl).
+ exact dl.
- intro dm.
eapply lifteq_isdefined.
+ exact (ineqml dm).
+ exact dm. }
exists e.
intro dm.
apply lifteq_valueeq.
exact (!(ineqml dm)).
apply lifteq_suff.
assert (e : isdefined l <-> isdefined m).
{ split.
- intro dl.
eapply lifteq_isdefined.
+ exact (ineqlm dl).
+ exact dl.
- intro dm.
eapply lifteq_isdefined.
+ exact (ineqml dm).
+ exact dm. }
exists e.
intro dm.
apply lifteq_valueeq.
exact (!(ineqml dm)).
Definition liftorder_reflexive {X : UU} : ∏ (l : 𝓛 X), l ⊑ l.
Show proof.
Definition liftorder_transitive {X : UU} :
∏ (l m n : 𝓛 X), l ⊑ m -> m ⊑ n -> l ⊑ n.
Show proof.
intros l m n ineqlm ineqmn.
intro dl.
etrans.
- exact (ineqlm dl).
- apply ineqmn.
exact (transportf isdefined (ineqlm dl) dl).
intro dl.
etrans.
- exact (ineqlm dl).
- apply ineqmn.
exact (transportf isdefined (ineqlm dl) dl).
Definition liftorder_least {X : UU} : 𝓛 X := (empty,, isapropempty,, fromempty).
Notation "'⊥'" := liftorder_least : PartialElements.
Definition liftorder_least_isleast {X : UU} : ∏ (l : 𝓛 X), ⊥ ⊑ l.
Show proof.
intro l. intro dbot.
induction dbot.
induction dbot.
End liftorder.
Notation "l ⊑ m" := (liftorder l m) (at level 30) : PartialElements.
Delimit Scope LiftDcpo with LiftDcpo.
Local Open Scope LiftDcpo.
Section liftdcpo.
Lemma liftofhset_isaset {X : hSet} : isaset (𝓛 X).
Show proof.
Lemma liftorder_ispropvalued {X : hSet} : ∏ (l m : 𝓛 X), isaprop (l ⊑ m).
Show proof.
Close Scope PartialElements.
Definition liftofhSet (X : hSet) : hSet := hSetpair (lift X) liftofhset_isaset.
Delimit Scope LiftIsPoset with LiftIsPoset.
Local Open Scope LiftIsPoset.
Definition liftorder_hrel {X : hSet} (l m : liftofhSet X) :=
hProppair (liftorder l m) (liftorder_ispropvalued l m).
Notation "l ⊑ m" := (liftorder_hrel l m) (at level 30) : LiftIsPoset.
Definition liftposet (X : hSet) : Poset.
Show proof.
Notation "'𝓛'" := liftposet : LiftIsPoset.
Lemma liftofhset_isaset {X : hSet} : isaset (𝓛 X).
Show proof.
intros l m.
eapply (isapropretract) with (f := (total2_paths_equiv _ l m))
(g := invmap (total2_paths_equiv _ l m)).
- apply isofhleveltotal2.
+ apply isaprop_pathsprop.
1-2: apply isaprop_isdefined.
+ intros eq.
assert (helper : isaset (isaprop (pr1 m) × ((pr1 m) -> X))).
{ apply isaset_dirprod.
- apply isasetaprop. apply isapropisaprop.
- apply isaset_set_fun_space. }
apply helper.
- use homotinvweqweq.
eapply (isapropretract) with (f := (total2_paths_equiv _ l m))
(g := invmap (total2_paths_equiv _ l m)).
- apply isofhleveltotal2.
+ apply isaprop_pathsprop.
1-2: apply isaprop_isdefined.
+ intros eq.
assert (helper : isaset (isaprop (pr1 m) × ((pr1 m) -> X))).
{ apply isaset_dirprod.
- apply isasetaprop. apply isapropisaprop.
- apply isaset_set_fun_space. }
apply helper.
- use homotinvweqweq.
Lemma liftorder_ispropvalued {X : hSet} : ∏ (l m : 𝓛 X), isaprop (l ⊑ m).
Show proof.
Close Scope PartialElements.
Definition liftofhSet (X : hSet) : hSet := hSetpair (lift X) liftofhset_isaset.
Delimit Scope LiftIsPoset with LiftIsPoset.
Local Open Scope LiftIsPoset.
Definition liftorder_hrel {X : hSet} (l m : liftofhSet X) :=
hProppair (liftorder l m) (liftorder_ispropvalued l m).
Notation "l ⊑ m" := (liftorder_hrel l m) (at level 30) : LiftIsPoset.
Definition liftposet (X : hSet) : Poset.
Show proof.
use Posetpair.
- exact (liftofhSet X).
- exists liftorder_hrel.
unfold isPartialOrder. split.
+ unfold ispreorder. split.
* use liftorder_transitive.
* use liftorder_reflexive.
+ use liftorder_antisymmetric.
- exact (liftofhSet X).
- exists liftorder_hrel.
unfold isPartialOrder. split.
+ unfold ispreorder. split.
* use liftorder_transitive.
* use liftorder_reflexive.
+ use liftorder_antisymmetric.
Notation "'𝓛'" := liftposet : LiftIsPoset.
The following map will be used to define the value of the lub of a
(directed) family.
Definition lubvaluemap {X : hSet} {I : UU} (u : I -> 𝓛 X) :
(∑ (i : I), isdefined (u i)) -> X.
Show proof.
(∑ (i : I), isdefined (u i)) -> X.
Show proof.
The map is weakly constant if the family is directed.
Definition lubvaluemap_weaklyconstant {X : hSet} {I : UU} (u : I -> 𝓛 X) :
isdirected u -> weaklyconstant (lubvaluemap u).
Show proof.
isdirected u -> weaklyconstant (lubvaluemap u).
Show proof.
intros isdirec [i d] [i' d'].
apply (@factor_through_squash (directeduntruncated u i i')).
- apply setproperty.
- intros [k ineqs].
unfold lubvaluemap.
apply lifteq_valueeq.
etrans.
+ exact (pr1 ineqs d).
+ exact (!(pr2 ineqs d')).
- exact (isdirected_order isdirec i i').
apply (@factor_through_squash (directeduntruncated u i i')).
- apply setproperty.
- intros [k ineqs].
unfold lubvaluemap.
apply lifteq_valueeq.
etrans.
+ exact (pr1 ineqs d).
+ exact (!(pr2 ineqs d')).
- exact (isdirected_order isdirec i i').
The construction of the lub; a proof that this element is actually
the lub follows later.
Definition mkdirectedlubinlift {X : hSet} {I : UU} {u : I -> 𝓛 X}
(isdirec : isdirected u) : 𝓛 X.
Show proof.
Lemma isdefinedlub_toprop' {X : hSet} {I Q : UU} {u : I -> 𝓛 X}
(isdirec : isdirected u) :
((∑ (i : I), isdefined (u i)) -> Q) ->
isaprop Q ->
isdefined (mkdirectedlubinlift isdirec) -> Q.
Show proof.
Lemma liftlub_isdefined' {X : hSet} {I : UU} {u : I -> 𝓛 X}
(isdirec : isdirected u) :
∏ (i : I), isdefined (u i) -> u i = mkdirectedlubinlift isdirec.
Show proof.
Lemma mkdirectedlubinlift_islub {X : hSet} {I : UU} (u : I -> 𝓛 X)
(isdirec : isdirected u) : islub u (mkdirectedlubinlift isdirec).
Show proof.
Lemma isdefinedlub_toprop {X : hSet} {I Q : UU} {u : I -> 𝓛 X} {v : 𝓛 X}
(isdirec : isdirected u) :
islub u v -> ((∑ (i : I), isdefined (u i)) -> Q) ->
isaprop Q ->
isdefined v -> Q.
Show proof.
Lemma liftlub_isdefined {X : hSet} {I : UU} {u : I -> 𝓛 X} {v : 𝓛 X}
(isdirec : isdirected u) :
islub u v -> ∏ (i : I), isdefined (u i) -> u i = v.
Show proof.
Theorem lift_isdirectedcomplete (X : hSet) :
isdirectedcomplete (𝓛 X).
Show proof.
Definition liftdcpo (X : hSet) : dcpo.
Show proof.
Definition liftdcpowithbottom (X : hSet) : dcpowithbottom.
Show proof.
End liftdcpo.
Notation "l ⊑ m" := (liftorder_hrel l m) (at level 30) : LiftDcpo.
Notation "'𝓛'" := liftdcpowithbottom : LiftDcpo.
Notation "'η'" := lift_embedding : LiftDcpo.
(isdirec : isdirected u) : 𝓛 X.
Show proof.
exists (∥∑ (i : I), isdefined (u i)∥).
split.
- apply isapropishinh.
- eapply weaklyconstanttoaset_factorsthroughsquash.
+ apply setproperty.
+ apply lubvaluemap_weaklyconstant.
exact isdirec.
split.
- apply isapropishinh.
- eapply weaklyconstanttoaset_factorsthroughsquash.
+ apply setproperty.
+ apply lubvaluemap_weaklyconstant.
exact isdirec.
Lemma isdefinedlub_toprop' {X : hSet} {I Q : UU} {u : I -> 𝓛 X}
(isdirec : isdirected u) :
((∑ (i : I), isdefined (u i)) -> Q) ->
isaprop Q ->
isdefined (mkdirectedlubinlift isdirec) -> Q.
Show proof.
Lemma liftlub_isdefined' {X : hSet} {I : UU} {u : I -> 𝓛 X}
(isdirec : isdirected u) :
∏ (i : I), isdefined (u i) -> u i = mkdirectedlubinlift isdirec.
Show proof.
intros i di.
apply lifteq_suff.
assert (e : isdefined (u i) <-> isdefined (mkdirectedlubinlift isdirec)).
{ split.
- exact (λ d, hinhpr (i,,d)).
- exact (λ _, di). }
exists e.
intro d.
unfold mkdirectedlubinlift; cbn.
assert (dinsquash : d = hinhpr (i,,di)).
{ apply proofirrelevance, isapropishinh. }
unfold funcomp.
assert (defeq : pr2 e d = di).
{ apply proofirrelevance, isaprop_isdefined. }
rewrite defeq.
change (value (u i) di) with (lubvaluemap u (i,,di)).
rewrite dinsquash.
use weaklyconstanttoaset_factorsthroughsquash_eq.
- apply setproperty.
- apply weaklyconstant_value.
apply lifteq_suff.
assert (e : isdefined (u i) <-> isdefined (mkdirectedlubinlift isdirec)).
{ split.
- exact (λ d, hinhpr (i,,d)).
- exact (λ _, di). }
exists e.
intro d.
unfold mkdirectedlubinlift; cbn.
assert (dinsquash : d = hinhpr (i,,di)).
{ apply proofirrelevance, isapropishinh. }
unfold funcomp.
assert (defeq : pr2 e d = di).
{ apply proofirrelevance, isaprop_isdefined. }
rewrite defeq.
change (value (u i) di) with (lubvaluemap u (i,,di)).
rewrite dinsquash.
use weaklyconstanttoaset_factorsthroughsquash_eq.
- apply setproperty.
- apply weaklyconstant_value.
Lemma mkdirectedlubinlift_islub {X : hSet} {I : UU} (u : I -> 𝓛 X)
(isdirec : isdirected u) : islub u (mkdirectedlubinlift isdirec).
Show proof.
split.
- intro i.
intro di.
exact (liftlub_isdefined' isdirec i di).
- intros v upperbound.
intro d.
apply (isdefinedlub_toprop' isdirec).
+ intros [i di].
etrans.
* exact (!(liftlub_isdefined' isdirec i di)).
* exact (upperbound i di).
+ apply liftofhset_isaset.
+ exact d.
- intro i.
intro di.
exact (liftlub_isdefined' isdirec i di).
- intros v upperbound.
intro d.
apply (isdefinedlub_toprop' isdirec).
+ intros [i di].
etrans.
* exact (!(liftlub_isdefined' isdirec i di)).
* exact (upperbound i di).
+ apply liftofhset_isaset.
+ exact d.
Lemma isdefinedlub_toprop {X : hSet} {I Q : UU} {u : I -> 𝓛 X} {v : 𝓛 X}
(isdirec : isdirected u) :
islub u v -> ((∑ (i : I), isdefined (u i)) -> Q) ->
isaprop Q ->
isdefined v -> Q.
Show proof.
intro vislub.
assert (eq : v = mkdirectedlubinlift isdirec).
{ apply (lubsareunique u).
- exact vislub.
- apply mkdirectedlubinlift_islub. }
rewrite eq. apply isdefinedlub_toprop'.
assert (eq : v = mkdirectedlubinlift isdirec).
{ apply (lubsareunique u).
- exact vislub.
- apply mkdirectedlubinlift_islub. }
rewrite eq. apply isdefinedlub_toprop'.
Lemma liftlub_isdefined {X : hSet} {I : UU} {u : I -> 𝓛 X} {v : 𝓛 X}
(isdirec : isdirected u) :
islub u v -> ∏ (i : I), isdefined (u i) -> u i = v.
Show proof.
intro vislub.
assert (eq : v = mkdirectedlubinlift isdirec).
{ apply (lubsareunique u).
- exact vislub.
- apply mkdirectedlubinlift_islub. }
rewrite eq.
apply liftlub_isdefined'.
assert (eq : v = mkdirectedlubinlift isdirec).
{ apply (lubsareunique u).
- exact vislub.
- apply mkdirectedlubinlift_islub. }
rewrite eq.
apply liftlub_isdefined'.
Theorem lift_isdirectedcomplete (X : hSet) :
isdirectedcomplete (𝓛 X).
Show proof.
unfold isdirectedcomplete. intros I u isdirec.
exists (mkdirectedlubinlift isdirec).
apply mkdirectedlubinlift_islub.
Close Scope LiftIsPoset.exists (mkdirectedlubinlift isdirec).
apply mkdirectedlubinlift_islub.
Definition liftdcpo (X : hSet) : dcpo.
Show proof.
Definition liftdcpowithbottom (X : hSet) : dcpowithbottom.
Show proof.
End liftdcpo.
Notation "l ⊑ m" := (liftorder_hrel l m) (at level 30) : LiftDcpo.
Notation "'𝓛'" := liftdcpowithbottom : LiftDcpo.
Notation "'η'" := lift_embedding : LiftDcpo.