Library HoTT.TruncType

Universes of truncated types.


Require Import HoTT.Basics HoTT.Types.
Require Import HProp.

Generalizable Variables A B n f.

Universes of truncated types

Now that we have the univalence axiom (from types/Universe), we study further the universes TruncType of truncated types (including hProp and hSet) that were defined in Basics/Trunc.

Paths in TruncType


Section TruncType.
Context `{Univalence}.

Definition issig_trunctype {n : trunc_index}
  : { X : Type & IsTrunc n X } <~> TruncType n.
Proof.
  issig.
Defined.

Global Instance isequiv_ap_trunctype {n : trunc_index} (A B : n-Type)
: IsEquiv (@ap _ _ (@trunctype_type n) A B).
Proof.
  transparent assert (e : ((A = B :> Type) <~> (A = B :> n-Type))).
  { equiv_via ((issig_trunctype ^-1 A) = (issig_trunctype ^-1 B)).
    - simpl. apply (equiv_path_sigma_hprop
                      (trunctype_type A; istrunc_trunctype_type A)
                      (trunctype_type B; istrunc_trunctype_type B)).
    - symmetry. apply equiv_ap. refine _. }
  
  refine (isequiv_homotopic e^-1%equiv _).
  intros p; destruct p; reflexivity.
Defined.

Definition equiv_path_trunctype' {n : trunc_index} (A B : TruncType n)
  : (A = B :> Type) <~> (A = B :> TruncType n).
Proof.
  exact ((Build_Equiv _ _ (@ap _ _ (@trunctype_type n) A B) _)^-1)%equiv.
Defined.

Definition equiv_path_trunctype {n : trunc_index} (A B : TruncType n)
  : (A <~> B) <~> (A = B :> TruncType n).
Proof.
  equiv_via (A = B :> Type).
  - apply equiv_path_universe.
  - exact ((Build_Equiv _ _ (@ap _ _ (@trunctype_type n) A B) _)^-1)%equiv.
Defined.

Definition path_trunctype@{a b c} {n : trunc_index} {A B : TruncType n}
  : A <~> B (A = B :> TruncType n)
:= equiv_path_trunctype@{a b c} A B.

Global Instance isequiv_path_trunctype
       {n : trunc_index} {A B : TruncType n}
: IsEquiv (@path_trunctype n A B).
Proof.
  exact _.
Defined.

path_trunctype is functorial
Definition path_trunctype_1 {n : trunc_index} {A : TruncType n}
: path_trunctype (equiv_idmap A) = idpath.
Proof.
  unfold path_trunctype; simpl.
  rewrite (eta_path_universe_uncurried 1).
  rewrite path_sigma_hprop_1.
  reflexivity.
Qed.

Definition path_trunctype_V {n : trunc_index} {A B : TruncType n}
           (f : A <~> B)
  : path_trunctype f^-1 = (path_trunctype f)^.
Proof.
  unfold path_trunctype; simpl.
  rewrite path_universe_V_uncurried.
  rewrite (path_sigma_hprop_V (path_universe_uncurried f)).
  refine (concat_p1 _ @ concat_1p _ @ _).
  refine (_ @ (ap inverse (concat_1p _))^ @ (ap inverse (concat_p1 _))^).
  refine (ap_V _ _).
Qed.

Definition path_trunctype_pp {n : trunc_index} {A B C : TruncType n}
           (f : A <~> B) (g : B <~> C)
  : path_trunctype (g oE f) = path_trunctype f @ path_trunctype g.
Proof.
  unfold path_trunctype; simpl.
  rewrite path_universe_compose_uncurried.
  rewrite (path_sigma_hprop_pp _ _ _ (istrunc_trunctype_type B)).
  refine (concat_p1 _ @ concat_1p _ @ _).
  refine (_ @ (ap _ (concat_1p _))^ @ (ap _ (concat_p1 _))^).
  refine (_ @ (ap (fun zz @ _) (concat_1p _))^ @ (ap (fun zz @ _) (concat_p1 _))^).
  refine (ap_pp _ _ _).
Qed.

Definition ap_trunctype {n : trunc_index} {A B : TruncType n} {f : A <~> B}
  : ap trunctype_type (path_trunctype f) = path_universe_uncurried f.
Proof.
  destruct A, B.
  cbn in ×.
  cbn; destruct (path_universe_uncurried f).
  rewrite concat_1p, concat_p1.
  rewrite <- 2 ap_compose.
  apply ap_const.
Qed.

Definition path_hset {A B} := @path_trunctype 0 A B.
Definition path_hprop {A B} := @path_trunctype (-1) A B.

Global Instance istrunc_trunctype@{i j k | i < j, j < k} {n : trunc_index}
  : IsTrunc@{j} n.+1 (TruncType@{i} n) | 0.
Proof.
  intros A B.
  refine (trunc_equiv _ (equiv_path_trunctype@{i j k} A B)).
  case n as [ | n'].
  - apply contr_equiv_contr_contr.   - apply istrunc_equiv.
Defined.

Global Instance isset_hProp : IsHSet hProp.
Proof.
  exact _.
Defined.

Global Instance Sn_trunctype: n, IsTrunc n.+1 (sigT (IsTrunc n)) |0.
Proof.
  intro n.
  apply (trunc_equiv' _ issig_trunctype^-1).
Defined.

Some standard inhabitants


Definition Unit_hp : hProp := (BuildhProp Unit).
Definition False_hp : hProp := (BuildhProp Empty).
Definition Negation_hp `{Funext} (hprop : hProp) : hProp := BuildhProp (¬hprop).
We could continue with products etc

The canonical map from Bool to hProp

Definition is_true (b : Bool) : hProp
  := if b then Unit_hp else False_hp.

Facts about HProps using univalence


Global Instance trunc_path_IsHProp X Y `{IsHProp Y}
: IsHProp (X = Y).
Proof.
  apply hprop_allpath.
  intros pf1 pf2.
  apply (equiv_inj (equiv_path X Y)).
  apply path_equiv, path_arrow.
  intros x; by apply path_ishprop.
Qed.

Definition path_iff_ishprop_uncurried `{IsHProp A, IsHProp B}
: (A B) A = B :> Type
  := @path_universe_uncurried _ A B o equiv_iff_hprop_uncurried.

Definition path_iff_hprop_uncurried {A B : hProp}
: (A B) A = B :> hProp
  := (@path_hprop A B) o (@equiv_iff_hprop_uncurried A _ B _).

Global Instance isequiv_path_iff_ishprop_uncurried `{IsHProp A, IsHProp B}
: IsEquiv (@path_iff_ishprop_uncurried A _ B _).
Proof.
  exact _.
Defined.

Global Instance isequiv_path_iff_hprop_uncurried {A B : hProp}
: IsEquiv (@path_iff_hprop_uncurried A B).
Proof.
  exact _.
Defined.

Definition path_iff_ishprop `{IsHProp A, IsHProp B}
: (A B) (B A) A = B :> Type
  := fun f gpath_iff_ishprop_uncurried (f,g).

Definition path_iff_hprop {A B : hProp}
: (A B) (B A) A = B :> hProp
  := fun f gpath_iff_hprop_uncurried (f,g).

End TruncType.