(* -*- mode: coq; mode: visual-line -*-  *)
Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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.
H: Univalence
n: trunc_index
{X : Type & IsTrunc n X} <~> n -Type
  Proof.
H: Univalence
n: trunc_index
{X : Type & IsTrunc n X} <~> n -Type
    issig.
  Defined.

  Definition equiv_path_trunctype' {n : trunc_index} (A B : TruncType n)
    : (A = B :> Type) <~> (A = B :> TruncType n).
H: Univalence
n: trunc_index
A, B: n -Type
A = B <~> A = B
  Proof.
H: Univalence
n: trunc_index
A, B: n -Type
A = B <~> A = B
    refine ((equiv_ap' issig_trunctype^-1 _ _)^-1 oE _).
H: Univalence
n: trunc_index
A, B: n -Type
A = B <~>
(issig_trunctype^-1)%equiv A =
(issig_trunctype^-1)%equiv B
    exact (equiv_path_sigma_hprop (_;_) (_;_)).
  Defined.

  Global Instance isequiv_ap_trunctype {n : trunc_index} (A B : n-Type)
    : IsEquiv (@ap _ _ (@trunctype_type n) A B).
H: Univalence
n: trunc_index
A, B: n -Type
IsEquiv (ap trunctype_type)
  Proof.
H: Univalence
n: trunc_index
A, B: n -Type
IsEquiv (ap trunctype_type)
    srefine (isequiv_homotopic _^-1%equiv _).
H: Univalence
n: trunc_index
A, B: n -Type
A = B <~> A = B
H: Univalence
n: trunc_index
A, B: n -Type
(?Goal^-1)%equiv == ap trunctype_type
    1: apply equiv_path_trunctype'.
H: Univalence
n: trunc_index
A, B: n -Type
((equiv_path_trunctype' A B)^-1)%equiv ==
ap trunctype_type
    intros []; reflexivity.
  Defined.

  Definition equiv_path_trunctype {n : trunc_index} (A B : TruncType n)
    : (A <~> B) <~> (A = B :> TruncType n)
    := equiv_path_trunctype' _ _ oE equiv_path_universe _ _.

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

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

  (** [path_trunctype] is functorial *)
  Definition path_trunctype_1 {n : trunc_index} {A : TruncType n}
  : path_trunctype (equiv_idmap A) = idpath.
H: Univalence
n: trunc_index
A: n -Type
path_trunctype 1 = 1
  Proof.
H: Univalence
n: trunc_index
A: n -Type
path_trunctype 1 = 1
    unfold path_trunctype; simpl.
H: Univalence
n: trunc_index
A: n -Type
(1 @
 ap
   (fun u : {X : Type & IsTrunc n X} =>
    {|
      trunctype_type := u.1; trunctype_istrunc := u.2
    |})
   (path_sigma_hprop (A; trunctype_istrunc A)
      (A; trunctype_istrunc A)
      (path_universe_uncurried 1))) @ 1 = 1
    rewrite (eta_path_universe_uncurried 1).
H: Univalence
n: trunc_index
A: n -Type
(1 @
 ap
   (fun u : {X : Type & IsTrunc n X} =>
    {|
      trunctype_type := u.1; trunctype_istrunc := u.2
    |})
   (path_sigma_hprop (A; trunctype_istrunc A)
      (A; trunctype_istrunc A) 1)) @ 1 = 1
    rewrite path_sigma_hprop_1.
H: Univalence
n: trunc_index
A: n -Type
(1 @
 ap
   (fun u : {X : Type & IsTrunc n X} =>
    {|
      trunctype_type := u.1; trunctype_istrunc := u.2
    |}) 1) @ 1 = 1
    reflexivity.
  Qed.

  Definition path_trunctype_V {n : trunc_index} {A B : TruncType n}
             (f : A <~> B)
    : path_trunctype f^-1 = (path_trunctype f)^.
H: Univalence
n: trunc_index
A, B: n -Type
f: A <~> B
path_trunctype f^-1 = (path_trunctype f)^
  Proof.
H: Univalence
n: trunc_index
A, B: n -Type
f: A <~> B
path_trunctype f^-1 = (path_trunctype f)^
    unfold path_trunctype; simpl.
H: Univalence
n: trunc_index
A, B: n -Type
f: A <~> B
(1 @
 ap
   (fun u : {X : Type & IsTrunc n X} =>
    {|
      trunctype_type := u.1; trunctype_istrunc := u.2
    |})
   (path_sigma_hprop (B; trunctype_istrunc B)
      (A; trunctype_istrunc A)
      (path_universe_uncurried f^-1))) @ 1 =
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (A; trunctype_istrunc A)
       (B; trunctype_istrunc B)
       (path_universe_uncurried f))) @ 1)^
    rewrite path_universe_V_uncurried.
H: Univalence
n: trunc_index
A, B: n -Type
f: A <~> B
(1 @
 ap
   (fun u : {X : Type & IsTrunc n X} =>
    {|
      trunctype_type := u.1; trunctype_istrunc := u.2
    |})
   (path_sigma_hprop (B; trunctype_istrunc B)
      (A; trunctype_istrunc A)
      (path_universe_uncurried f)^)) @ 1 =
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (A; trunctype_istrunc A)
       (B; trunctype_istrunc B)
       (path_universe_uncurried f))) @ 1)^
    rewrite (path_sigma_hprop_V (path_universe_uncurried f)).
H: Univalence
n: trunc_index
A, B: n -Type
f: A <~> B
(1 @
 ap
   (fun u : {X : Type & IsTrunc n X} =>
    {|
      trunctype_type := u.1; trunctype_istrunc := u.2
    |})
   (path_sigma_hprop (A; trunctype_istrunc A)
      (B; trunctype_istrunc B)
      (path_universe_uncurried f))^) @ 1 =
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (A; trunctype_istrunc A)
       (B; trunctype_istrunc B)
       (path_universe_uncurried f))) @ 1)^
    refine (concat_p1 _ @ concat_1p _ @ _).
H: Univalence
n: trunc_index
A, B: n -Type
f: A <~> B
ap
  (fun u : {X : Type & IsTrunc n X} =>
   {|
     trunctype_type := u.1; trunctype_istrunc := u.2
   |})
  (path_sigma_hprop (A; trunctype_istrunc A)
     (B; trunctype_istrunc B)
     (path_universe_uncurried f))^ =
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (A; trunctype_istrunc A)
       (B; trunctype_istrunc B)
       (path_universe_uncurried f))) @ 1)^
    refine (_ @ (ap inverse (concat_1p _))^ @ (ap inverse (concat_p1 _))^).
H: Univalence
n: trunc_index
A, B: n -Type
f: A <~> B
ap
  (fun u : {X : Type & IsTrunc n X} =>
   {|
     trunctype_type := u.1; trunctype_istrunc := u.2
   |})
  (path_sigma_hprop (A; trunctype_istrunc A)
     (B; trunctype_istrunc B)
     (path_universe_uncurried f))^ =
(ap
   (fun u : {X : Type & IsTrunc n X} =>
    {|
      trunctype_type := u.1; trunctype_istrunc := u.2
    |})
   (path_sigma_hprop (A; trunctype_istrunc A)
      (B; trunctype_istrunc B)
      (path_universe_uncurried f)))^
    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.
H: Univalence
n: trunc_index
A, B, C: n -Type
f: A <~> B
g: B <~> C
path_trunctype (g oE f) =
path_trunctype f @ path_trunctype g
  Proof.
H: Univalence
n: trunc_index
A, B, C: n -Type
f: A <~> B
g: B <~> C
path_trunctype (g oE f) =
path_trunctype f @ path_trunctype g
    unfold path_trunctype; simpl.
H: Univalence
n: trunc_index
A, B, C: n -Type
f: A <~> B
g: B <~> C
(1 @
 ap
   (fun u : {X : Type & IsTrunc n X} =>
    {|
      trunctype_type := u.1; trunctype_istrunc := u.2
    |})
   (path_sigma_hprop (A; trunctype_istrunc A)
      (C; trunctype_istrunc C)
      (path_universe_uncurried (g oE f)))) @ 1 =
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (A; trunctype_istrunc A)
       (B; trunctype_istrunc B)
       (path_universe_uncurried f))) @ 1) @
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (B; trunctype_istrunc B)
       (C; trunctype_istrunc C)
       (path_universe_uncurried g))) @ 1)
    rewrite path_universe_compose_uncurried.
H: Univalence
n: trunc_index
A, B, C: n -Type
f: A <~> B
g: B <~> C
(1 @
 ap
   (fun u : {X : Type & IsTrunc n X} =>
    {|
      trunctype_type := u.1; trunctype_istrunc := u.2
    |})
   (path_sigma_hprop (A; trunctype_istrunc A)
      (C; trunctype_istrunc C)
      (path_universe_uncurried f @
       path_universe_uncurried g))) @ 1 =
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (A; trunctype_istrunc A)
       (B; trunctype_istrunc B)
       (path_universe_uncurried f))) @ 1) @
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (B; trunctype_istrunc B)
       (C; trunctype_istrunc C)
       (path_universe_uncurried g))) @ 1)
    rewrite (path_sigma_hprop_pp (path_universe_uncurried f) _ _ (trunctype_istrunc B)).
H: Univalence
n: trunc_index
A, B, C: n -Type
f: A <~> B
g: B <~> C
(1 @
 ap
   (fun u : {X : Type & IsTrunc n X} =>
    {|
      trunctype_type := u.1; trunctype_istrunc := u.2
    |})
   (path_sigma_hprop (A; trunctype_istrunc A)
      (B; trunctype_istrunc B)
      (path_universe_uncurried f) @
    path_sigma_hprop (B; trunctype_istrunc B)
      (C; trunctype_istrunc C)
      (path_universe_uncurried g))) @ 1 =
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (A; trunctype_istrunc A)
       (B; trunctype_istrunc B)
       (path_universe_uncurried f))) @ 1) @
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (B; trunctype_istrunc B)
       (C; trunctype_istrunc C)
       (path_universe_uncurried g))) @ 1)
    refine (concat_p1 _ @ concat_1p _ @ _).
H: Univalence
n: trunc_index
A, B, C: n -Type
f: A <~> B
g: B <~> C
ap
  (fun u : {X : Type & IsTrunc n X} =>
   {|
     trunctype_type := u.1; trunctype_istrunc := u.2
   |})
  (path_sigma_hprop (A; trunctype_istrunc A)
     (B; trunctype_istrunc B)
     (path_universe_uncurried f) @
   path_sigma_hprop (B; trunctype_istrunc B)
     (C; trunctype_istrunc C)
     (path_universe_uncurried g)) =
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (A; trunctype_istrunc A)
       (B; trunctype_istrunc B)
       (path_universe_uncurried f))) @ 1) @
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (B; trunctype_istrunc B)
       (C; trunctype_istrunc C)
       (path_universe_uncurried g))) @ 1)
    refine (_ @ (ap _ (concat_1p _))^ @ (ap _ (concat_p1 _))^).
H: Univalence
n: trunc_index
A, B, C: n -Type
f: A <~> B
g: B <~> C
ap
  (fun u : {X : Type & IsTrunc n X} =>
   {|
     trunctype_type := u.1; trunctype_istrunc := u.2
   |})
  (path_sigma_hprop (A; trunctype_istrunc A)
     (B; trunctype_istrunc B)
     (path_universe_uncurried f) @
   path_sigma_hprop (B; trunctype_istrunc B)
     (C; trunctype_istrunc C)
     (path_universe_uncurried g)) =
((1 @
  ap
    (fun u : {X : Type & IsTrunc n X} =>
     {|
       trunctype_type := u.1; trunctype_istrunc := u.2
     |})
    (path_sigma_hprop (A; trunctype_istrunc A)
       (B; trunctype_istrunc B)
       (path_universe_uncurried f))) @ 1) @
ap
  (fun u : {X : Type & IsTrunc n X} =>
   {|
     trunctype_type := u.1; trunctype_istrunc := u.2
   |})
  (path_sigma_hprop (B; trunctype_istrunc B)
     (C; trunctype_istrunc C)
     (path_universe_uncurried g))
    refine (_ @ (ap (fun z => z @ _) (concat_1p _))^ @ (ap (fun z => z @ _) (concat_p1 _))^).
H: Univalence
n: trunc_index
A, B, C: n -Type
f: A <~> B
g: B <~> C
ap
  (fun u : {X : Type & IsTrunc n X} =>
   {|
     trunctype_type := u.1; trunctype_istrunc := u.2
   |})
  (path_sigma_hprop (A; trunctype_istrunc A)
     (B; trunctype_istrunc B)
     (path_universe_uncurried f) @
   path_sigma_hprop (B; trunctype_istrunc B)
     (C; trunctype_istrunc C)
     (path_universe_uncurried g)) =
ap
  (fun u : {X : Type & IsTrunc n X} =>
   {|
     trunctype_type := u.1; trunctype_istrunc := u.2
   |})
  (path_sigma_hprop (A; trunctype_istrunc A)
     (B; trunctype_istrunc B)
     (path_universe_uncurried f)) @
ap
  (fun u : {X : Type & IsTrunc n X} =>
   {|
     trunctype_type := u.1; trunctype_istrunc := u.2
   |})
  (path_sigma_hprop (B; trunctype_istrunc B)
     (C; trunctype_istrunc C)
     (path_universe_uncurried g))
    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.
H: Univalence
n: trunc_index
A, B: n -Type
f: A <~> B
ap trunctype_type (path_trunctype f) =
path_universe_uncurried f
  Proof.
H: Univalence
n: trunc_index
A, B: n -Type
f: A <~> B
ap trunctype_type (path_trunctype f) =
path_universe_uncurried f
    destruct A, B.
H: Univalence
n: trunc_index
trunctype_type: Type
trunctype_istrunc: IsTrunc n trunctype_type
trunctype_type0: Type
trunctype_istrunc0: IsTrunc n trunctype_type0
f: {|
  trunctype_type := trunctype_type;
  trunctype_istrunc := trunctype_istrunc
|} <~>
{|
  trunctype_type := trunctype_type0;
  trunctype_istrunc := trunctype_istrunc0
|}
ap Trunc.trunctype_type (path_trunctype f) =
path_universe_uncurried f
    cbn in *.
H: Univalence
n: trunc_index
trunctype_type: Type
trunctype_istrunc: IsTrunc n trunctype_type
trunctype_type0: Type
trunctype_istrunc0: IsTrunc n trunctype_type0
f: trunctype_type <~> trunctype_type0
ap Trunc.trunctype_type
  ((1 @
    ap
      (fun u : {X : Type & IsTrunc n X} =>
       {|
         trunctype_type := u.1;
         trunctype_istrunc := u.2
       |})
      (path_sigma_hprop
         (trunctype_type; trunctype_istrunc)
         (trunctype_type0; trunctype_istrunc0)
         (path_universe_uncurried f))) @ 1) =
path_universe_uncurried f
    cbn; destruct (path_universe_uncurried f).
H: Univalence
n: trunc_index
trunctype_type: Type
trunctype_istrunc, trunctype_istrunc0: IsTrunc n trunctype_type
f: trunctype_type <~> trunctype_type
ap Trunc.trunctype_type
  ((1 @
    ap
      (fun u : {X : Type & IsTrunc n X} =>
       {|
         trunctype_type := u.1;
         trunctype_istrunc := u.2
       |})
      (path_sigma_hprop
         (trunctype_type; trunctype_istrunc)
         (trunctype_type; trunctype_istrunc0) 1)) @ 1) =
1
    rewrite concat_1p, concat_p1.
H: Univalence
n: trunc_index
trunctype_type: Type
trunctype_istrunc, trunctype_istrunc0: IsTrunc n trunctype_type
f: trunctype_type <~> trunctype_type
ap Trunc.trunctype_type
  (ap
     (fun u : {X : Type & IsTrunc n X} =>
      {|
        trunctype_type := u.1;
        trunctype_istrunc := u.2
      |})
     (path_sigma_hprop
        (trunctype_type; trunctype_istrunc)
        (trunctype_type; trunctype_istrunc0) 1)) = 1
    rewrite <- 2 ap_compose.
H: Univalence
n: trunc_index
trunctype_type: Type
trunctype_istrunc, trunctype_istrunc0: IsTrunc n trunctype_type
f: trunctype_type <~> trunctype_type
ap
  (fun
     x : IsTrunc n
           (trunctype_type; trunctype_istrunc0).1 =>
   {|
     trunctype_type :=
       ((trunctype_type; trunctype_istrunc0).1; x).1;
     trunctype_istrunc :=
       ((trunctype_type; trunctype_istrunc0).1; x).2
   |}) (pr1^-1 1).2 = 1
    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 {n : trunc_index}
    : IsTrunc n.+1 (TruncType n) | 0.
H: Univalence
n: trunc_index
IsTrunc n.+1 n -Type
  Proof.
H: Univalence
n: trunc_index
IsTrunc n.+1 n -Type
    apply istrunc_S.
H: Univalence
n: trunc_index
forall x y : n -Type, IsTrunc n (x = y)
    intros A B.
H: Univalence
n: trunc_index
A, B: n -Type
IsTrunc n (A = B)
    refine (istrunc_equiv_istrunc _ (equiv_path_trunctype@{i j} A B)).
H: Univalence
n: trunc_index
A, B: n -Type
IsTrunc n (A <~> B)
    case n as [ | n'].
H: Univalence
A, B: (-2) -Type
Contr (A <~> B)
H: Univalence
n': trunc_index
A, B: (n'.+1) -Type
IsTrunc n'.+1 (A <~> B)
    -
H: Univalence
A, B: (-2) -Type
Contr (A <~> B) apply contr_equiv_contr_contr. (* The reason is different in this case. *)
    -
H: Univalence
n': trunc_index
A, B: (n'.+1) -Type
IsTrunc n'.+1 (A <~> B) apply istrunc_equiv.
  Defined.

  Global Instance isset_HProp : IsHSet HProp := _.

  Global Instance istrunc_sig_istrunc : forall n, IsTrunc n.+1 { A : Type & IsTrunc n A } | 0.
H: Univalence
forall n : trunc_index,
IsTrunc n.+1 {A : Type & IsTrunc n A}
  Proof.
H: Univalence
forall n : trunc_index,
IsTrunc n.+1 {A : Type & IsTrunc n A}
    intro n.
H: Univalence
n: trunc_index
IsTrunc n.+1 {A : Type & IsTrunc n A}
    apply (istrunc_equiv_istrunc _ issig_trunctype^-1).
  Defined.

  (** ** Some standard inhabitants *)

  Definition Unit_hp : HProp := (Build_HProp Unit).
  Definition False_hp : HProp := (Build_HProp Empty).
  Definition Negation_hp `{Funext} (hprop : HProp) : HProp := Build_HProp (~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).
H: Univalence
X, Y: Type
IsHProp0: IsHProp Y
IsHProp (X = Y)
  Proof.
H: Univalence
X, Y: Type
IsHProp0: IsHProp Y
IsHProp (X = Y)
    apply hprop_allpath.
H: Univalence
X, Y: Type
IsHProp0: IsHProp Y
forall x y : X = Y, x = y
    intros pf1 pf2.
H: Univalence
X, Y: Type
IsHProp0: IsHProp Y
pf1, pf2: X = Y
pf1 = pf2
    apply (equiv_inj (equiv_path X Y)).
H: Univalence
X, Y: Type
IsHProp0: IsHProp Y
pf1, pf2: X = Y
equiv_path X Y pf1 = equiv_path X Y pf2
    apply path_equiv, path_arrow.
H: Univalence
X, Y: Type
IsHProp0: IsHProp Y
pf1, pf2: X = Y
equiv_path X Y pf1 == equiv_path X Y pf2
    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 _) := _.

  Global Instance isequiv_path_iff_hprop_uncurried {A B : HProp}
  : IsEquiv (@path_iff_hprop_uncurried A B) := _.

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

  Definition path_iff_hprop {A B : HProp}
  : (A -> B) -> (B -> A) -> A = B :> HProp
    := fun f g => path_iff_hprop_uncurried (f,g).

  Lemma equiv_path_iff_ishprop {A B : Type} `{IsHProp A, IsHProp B}
    : (A <-> B) <~> (A = B).
H: Univalence
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
(A <-> B) <~> A = B
  Proof.
H: Univalence
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
(A <-> B) <~> A = B
    exact (Build_Equiv _ _ path_iff_ishprop_uncurried _).
  Defined.

  Lemma equiv_path_iff_hprop {A B : HProp}
    : (A <-> B) <~> (A = B).
H: Univalence
A, B: HProp
(A <-> B) <~> A = B
  Proof.
H: Univalence
A, B: HProp
(A <-> B) <~> A = B
    refine (equiv_path_trunctype' _ _ oE equiv_path_iff_ishprop).
  Defined.

End TruncType.