Library UniMath.Foundations.HLevels
HLevel(n) is of hlevel n+1
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.UnivalenceAxiom.
Weak equivalence between identity types in HLevel and U
Local Lemma weq1 (P : UU -> hProp) (X X' : UU)
(p : P X) (p' : P X')
: (X,, p) = (X',, p' : ∑ (T : UU), P T )
≃
(∑ w : X = X', transportf P w p = p').
Show proof.
This helper lemma is needed to show that our fibration
is indeed a predicate, so that we can instantiate
the hProposition P with this fibration.
Local Lemma ident_is_prop (P : UU -> hProp) (X X' : UU)
(p : P X) (p' : P X') (w : X = X')
: isaprop (transportf P w p = p').
Show proof.
We construct the equivalence weq2 as a projection
from a total space, which, by the previous lemma, is
a weak equivalence.
Local Lemma weq2 (P : UU -> hProp) (X X' : UU)
(p : P X) (p' : P X')
: (∑ w : X = X', transportf P w p = p')
≃
(X = X').
Show proof.
Local Lemma Id_p_weq_Id (P : UU -> hProp) (X X' : UU)
(p : P X) (p' : P X')
: (X ,, p) = (X',, p' : ∑ T , P T)
≃
X = X'.
Show proof.
Hlevel of path spaces
The case n = 0
Lemma iscontr_weq (X Y : UU)
: iscontr X → iscontr Y → iscontr (X ≃ Y).
Show proof.
intros cX cY.
exists (weqcontrcontr cX cY ).
intro f.
apply subtypePath.
{ exact isapropisweq. }
apply funextfun. cbn. intro x. apply (pr2 cY).
exists (weqcontrcontr cX cY ).
intro f.
apply subtypePath.
{ exact isapropisweq. }
apply funextfun. cbn. intro x. apply (pr2 cY).
Lemma isofhlevel0pathspace (X Y : UU)
: iscontr X -> iscontr Y -> iscontr (X = Y).
Show proof.
intros pX pY.
set (H := isofhlevelweqb 0 (eqweqmap ,, univalenceAxiom X Y)).
apply H. clear H.
apply iscontr_weq;
assumption.
set (H := isofhlevelweqb 0 (eqweqmap ,, univalenceAxiom X Y)).
apply H. clear H.
apply iscontr_weq;
assumption.
Lemma isofhlevelSnpathspace : ∏ n : nat, ∏ X Y : UU,
isofhlevel (S n) Y -> isofhlevel (S n) (X = Y).
Show proof.
intros n X Y pY.
set (H:=isofhlevelweqb (S n) (eqweqmap ,, univalenceAxiom X Y)).
apply H.
apply isofhlevelsnweqtohlevelsn.
assumption.
set (H:=isofhlevelweqb (S n) (eqweqmap ,, univalenceAxiom X Y)).
apply H.
apply isofhlevelsnweqtohlevelsn.
assumption.
Lemma isofhlevelpathspace : ∏ n : nat, ∏ X Y : UU,
isofhlevel n X -> isofhlevel n Y -> isofhlevel n (X = Y).
Show proof.
intros n.
induction n as [| n _ ].
- intros X Y pX pY.
apply isofhlevel0pathspace;
assumption.
- intros.
apply isofhlevelSnpathspace;
assumption.
induction n as [| n _ ].
- intros X Y pX pY.
apply isofhlevel0pathspace;
assumption.
- intros.
apply isofhlevelSnpathspace;
assumption.
Lemma isofhlevel_HLevel (n : nat) : isofhlevel (S n) (HLevel n).
Show proof.
cbn.
intros X X'.
induction X as [X p].
induction X' as [X' p'].
set (H := isofhlevelweqb n
(Id_p_weq_Id (λ X, (isofhlevel n X,, isapropisofhlevel _ _)) X X' p p')).
cbn in H.
apply H.
apply isofhlevelpathspace;
assumption.
intros X X'.
induction X as [X p].
induction X' as [X' p'].
set (H := isofhlevelweqb n
(Id_p_weq_Id (λ X, (isofhlevel n X,, isapropisofhlevel _ _)) X X' p p')).
cbn in H.
apply H.
apply isofhlevelpathspace;
assumption.
Aside: Univalence for predicates and hlevels
Lemma UA_for_Predicates (P : UU -> hProp) (X X' : UU)
(pX : P X) (pX' : P X') :
(tpair _ X pX) = (tpair P X' pX') ≃ (X ≃ X').
Show proof.
set (f := Id_p_weq_Id P X X' pX pX').
set (g := tpair _ _ (univalenceAxiom X X')).
exact (weqcomp f g).
set (g := tpair _ _ (univalenceAxiom X X')).
exact (weqcomp f g).
Corollary UA_for_HLevels : ∏ (n : nat) (X X' : HLevel n),
(X = X') ≃ (pr1 X ≃ pr1 X').
Show proof.
intros n [X pX] [X' pX'].
simpl.
apply (UA_for_Predicates
(λ X, tpair isaprop (isofhlevel n X)
(isapropisofhlevel _ _))).
simpl.
apply (UA_for_Predicates
(λ X, tpair isaprop (isofhlevel n X)
(isapropisofhlevel _ _))).