Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Pointed.
Require Import WildCat.Core HFiber.
Require Import Truncations.
Require Import Algebra.Groups.Group.
Require Import Homotopy.HomotopyGroup.

Local Open Scope pointed_scope.
Local Open Scope nat_scope.

(** 8.8.1 *)
Definition isequiv_issurj_tr0_isequiv_ap
           `{Univalence} {A B : Type} (f : A -> B)
           {i  : IsSurjection (Trunc_functor 0 f)}
           {ii : forall x y, IsEquiv (@ap _ _ f x y)}
  : IsEquiv f.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: forall x y : A, IsEquiv (ap f)
IsEquiv f
Proof.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: forall x y : A, IsEquiv (ap f)
IsEquiv f
  apply (equiv_isequiv_ap_isembedding f)^-1 in ii.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
IsEquiv f
  srapply isequiv_surj_emb.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
IsConnMap (Tr (-1)) f
  srapply BuildIsSurjection.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
forall b : B, merely (hfiber f b)
  cbn; intro b.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
b: B
Trunc (-1) (hfiber f b)
  pose proof (@center _ (i (tr b))) as p.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
b: B
p: Tr (-1) (hfiber (Trunc_functor 0 f) (tr b))
Trunc (-1) (hfiber f b)
  revert p.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
b: B
Tr (-1) (hfiber (Trunc_functor 0 f) (tr b)) ->
Trunc (-1) (hfiber f b)
  apply Trunc_functor.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
b: B
hfiber (Trunc_functor 0 f) (tr b) -> hfiber f b
  apply sig_ind.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
b: B
forall proj1 : Tr 0 A,
Trunc_functor 0 f proj1 = tr b -> hfiber f b
  srapply Trunc_ind.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
b: B
forall a : A,
(fun aa : Trunc 0 A =>
 Trunc_functor 0 f aa = tr b -> hfiber f b) (tr a)
  intros a p.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
b: B
a: A
p: Trunc_functor 0 f (tr a) = tr b
hfiber f b
  apply (equiv_path_Tr _ _)^-1 in p.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
b: B
a: A
p: Tr (-1) (f a = b)
hfiber f b
  strip_truncations.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
b: B
a: A
p: f a = b
hfiber f b
  exists a.
H: Univalence
A, B: Type
f: A -> B
i: IsConnMap (Tr (-1)) (Trunc_functor 0 f)
ii: IsEmbedding f
b: B
a: A
p: f a = b
f a = b
  exact p.
Defined.

(** 8.8.2 *)
Definition isequiv_isbij_tr0_isequiv_loops
           `{Univalence} {A B : Type} (f : A -> B)
           {i  : IsEquiv (Trunc_functor 0 f)}
           {ii : forall x, IsEquiv (fmap loops (pmap_from_point f x)) }
  : IsEquiv f.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
IsEquiv f
Proof.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
IsEquiv f
  srapply (isequiv_issurj_tr0_isequiv_ap f).
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
forall x y : A, IsEquiv (ap f)
  intros x y.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
x, y: A
IsEquiv (ap f)
  apply isequiv_inhab_codomain.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
x, y: A
f x = f y -> IsEquiv (ap f)
  intro p.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
x, y: A
p: f x = f y
IsEquiv (ap f)
  apply (ap (@tr 0 _)) in p.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
x, y: A
p: tr (f x) = tr (f y)
IsEquiv (ap f)
  apply (@equiv_inj _ _ _ i (tr x) (tr y)) in p.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
x, y: A
p: tr x = tr y
IsEquiv (ap f)
  apply (equiv_path_Tr _ _)^-1 in p.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
x, y: A
p: Tr (-1) (x = y)
IsEquiv (ap f)
  strip_truncations.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
x, y: A
p: x = y
IsEquiv (ap f)
  destruct p.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
x: A
IsEquiv (ap f)
  cbn in ii.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fun p : x = x => 1 @ (ap f p @ 1))
x: A
IsEquiv (ap f)
  snrapply (isequiv_homotopic _ (H:=ii x)).
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x : A,
IsEquiv (fun p : x = x => 1 @ (ap f p @ 1))
x: A
(fun p : x = x => 1 @ (ap f p @ 1)) == ap f
  exact (fun _ => concat_1p _ @ concat_p1 _).
Defined.

(** When the types are 0-connected and the map is pointed, just one [loops_functor] needs to be checked. *)
Definition isequiv_is0connected_isequiv_loops
           `{Univalence} {A B : pType} `{IsConnected 0 A} `{IsConnected 0 B}
           (f : A ->* B)
           (e : IsEquiv (fmap loops f))
  : IsEquiv f.
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
IsEquiv f
Proof.
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
IsEquiv f
  apply isequiv_isbij_tr0_isequiv_loops.
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
IsEquiv (Trunc_functor 0 f)
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
  (** The pi_0 condition is trivial because [A] and [B] are 0-connected. *)
  1: apply isequiv_contr_contr.
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
  (** Since [A] is 0-connected, it's enough to check the [loops_functor] condition for the basepoint. *)
  rapply conn_point_elim.
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
IsEquiv (fmap loops (pmap_from_point f pt))
  (** The [loops_functor] condition for [pmap_from_point f _] is equivalent to the [loops_functor] condition for [f] with its given pointing. *)
  srapply isequiv_homotopic'.
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
loops [A, pt] <~> loops [B, f pt]
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
?f == fmap loops (pmap_from_point f pt)
  -
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
loops [A, pt] <~> loops [B, f pt] exact (equiv_concat_lr (point_eq f) (point_eq f)^ oE (Build_Equiv _ _ _ e)).
  -
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
equiv_concat_lr (point_eq f) (point_eq f)^
oE {| equiv_fun := fmap loops f; equiv_isequiv := e |} ==
fmap loops (pmap_from_point f pt) intro r.
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
r: loops [A, pt]
(equiv_concat_lr (point_eq f) (point_eq f)^
 oE {|
      equiv_fun := fmap loops f; equiv_isequiv := e
    |}) r = fmap loops (pmap_from_point f pt) r
    simpl.
H: Univalence
A, B: pType
H0: IsConnected (Tr 0%nat) A
H1: IsConnected (Tr 0%nat) B
f: A ->* B
e: IsEquiv (fmap loops f)
r: loops [A, pt]
(point_eq f @ ((point_eq f)^ @ (ap f r @ point_eq f))) @
(point_eq f)^ = 1 @ (ap f r @ 1)
    hott_simpl.
Defined.

(** Truncated Whitehead's principle (8.8.3) *)
Definition whiteheads_principle
           {ua : Univalence} {A B : Type} {f : A -> B}
           (n : trunc_index) {H0 : IsTrunc n A} {H1 : IsTrunc n B}
           {i  : IsEquiv (Trunc_functor 0 f)}
           {ii : forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x)) }
  : IsEquiv f.
ua: Univalence
A, B: Type
f: A -> B
n: trunc_index
H0: IsTrunc n A
H1: IsTrunc n B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
IsEquiv f
Proof.
ua: Univalence
A, B: Type
f: A -> B
n: trunc_index
H0: IsTrunc n A
H1: IsTrunc n B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
IsEquiv f
  revert A B H0 H1 f i ii.
ua: Univalence
n: trunc_index
forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat),
 IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
  induction n as [|n IHn].
ua: Univalence
forall A B : Type,
Contr A ->
Contr B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat),
 IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
forall A B : Type,
IsTrunc n.+1 A ->
IsTrunc n.+1 B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat),
 IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
  1: intros; apply isequiv_contr_contr.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
forall A B : Type,
IsTrunc n.+1 A ->
IsTrunc n.+1 B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat),
 IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
  intros A B H0 H1 f i ii.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
IsEquiv f
  nrefine (@isequiv_isbij_tr0_isequiv_loops ua _ _ f i _).
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
forall x : A,
IsEquiv (fmap loops (pmap_from_point f x))
  intro x.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
IsEquiv (fmap loops (pmap_from_point f x))
  nrefine (isequiv_homotopic (@ap _ _ f x x) _).
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
IsEquiv (ap f)
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
ap f == fmap loops (pmap_from_point f x)
  2:{
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
ap f == fmap loops (pmap_from_point f x)intros p; cbn.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
p: x = x
ap f p = 1 @ (ap f p @ 1)
     symmetry; exact (concat_1p _ @ concat_p1 _). }
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
IsEquiv (ap f)
  pose proof (@istrunc_paths _ _ H0 x x) as h0.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
IsEquiv (ap f)
  pose proof (@istrunc_paths _ _ H1 (f x) (f x)) as h1.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
IsEquiv (ap f)
  nrefine (IHn (x=x) (f x=f x) h0 h1 (@ap _ _ f x x) _ _).
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
IsEquiv (Trunc_functor 0 (ap f))
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
forall (x0 : x = x) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point (ap f) x0))
  -
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
IsEquiv (Trunc_functor 0 (ap f)) pose proof (ii x 0) as h2.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
h2: IsEquiv (fmap (Pi 1) (pmap_from_point f x))
IsEquiv (Trunc_functor 0 (ap f))
    unfold is0functor_pi in h2; cbn in h2.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
h2: IsEquiv
  (Trunc_functor 0
     (fun p : x = x => 1 @ (ap f p @ 1)))
IsEquiv (Trunc_functor 0 (ap f))
    refine (@isequiv_homotopic _ _ _ _ h2 _).
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
h2: IsEquiv
  (Trunc_functor 0
     (fun p : x = x => 1 @ (ap f p @ 1)))
Trunc_functor 0 (fun p : x = x => 1 @ (ap f p @ 1)) ==
Trunc_functor 0 (ap f)
    apply (O_functor_homotopy (Tr 0)); intros p.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
h2: IsEquiv
  (Trunc_functor 0
     (fun p : x = x => 1 @ (ap f p @ 1)))
p: x = x
1 @ (ap f p @ 1) = ap f p
    exact (concat_1p _ @ concat_p1 _).
  -
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
forall (x0 : x = x) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point (ap f) x0)) intros p k; revert p.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
forall p : x = x,
IsEquiv (fmap (Pi k.+1) (pmap_from_point (ap f) p))
    assert (h3 : forall (y:A) (q:x=y),
               IsEquiv (fmap (Pi k.+1) (pmap_from_point (@ap _ _ f x y) q))).
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
forall (y : A) (q : x = y),
IsEquiv (fmap (Pi k.+1) (pmap_from_point (ap f) q))
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
h3: forall (y : A) (q : x = y),
IsEquiv
  (fmap (Pi k.+1) (pmap_from_point (ap f) q))
forall p : x = x,
IsEquiv (fmap (Pi k.+1) (pmap_from_point (ap f) p))
    2:exact (h3 x).
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
forall (y : A) (q : x = y),
IsEquiv (fmap (Pi k.+1) (pmap_from_point (ap f) q))
    intros y q.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
y: A
q: x = y
IsEquiv (fmap (Pi k.+1) (pmap_from_point (ap f) q)) destruct q.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
IsEquiv (fmap (Pi k.+1) (pmap_from_point (ap f) 1))
    snrefine (isequiv_homotopic _ _).
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
Pi k.+1 [x = x, 1] -> Pi k.+1 [f x = f x, ap f 1]
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
IsEquiv ?f
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
?f == fmap (Pi k.+1) (pmap_from_point (ap f) 1)
    1: exact (fmap (Pi k.+1) (fmap loops (pmap_from_point f x))).
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
IsEquiv
  (fmap (Pi k.+1) (fmap loops (pmap_from_point f x)))
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
fmap (Pi k.+1) (fmap loops (pmap_from_point f x)) ==
fmap (Pi k.+1) (pmap_from_point (ap f) 1)
    2:{
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
fmap (Pi k.+1) (fmap loops (pmap_from_point f x)) ==
fmap (Pi k.+1) (pmap_from_point (ap f) 1) rapply (fmap2 (Pi k.+1)); srefine (Build_pHomotopy _ _).
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
fmap loops (pmap_from_point f x) ==
pmap_from_point (ap f) 1
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
?p pt =
dpoint_eq (fmap loops (pmap_from_point f x)) @
(dpoint_eq (pmap_from_point (ap f) 1))^
        -
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
fmap loops (pmap_from_point f x) ==
pmap_from_point (ap f) 1 intros p; cbn.
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
p: [x = x, 1]
1 @ (ap f p @ 1) = ap f p
          refine (concat_1p _ @ concat_p1 _).
        -
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
((fun p : [x = x, 1] =>
  concat_1p (ap f p @ 1) @ concat_p1 (ap f p)
  :
  fmap loops (pmap_from_point f x) p =
  pmap_from_point (ap f) 1 p)
 :
 fmap loops (pmap_from_point f x) ==
 pmap_from_point (ap f) 1) pt =
dpoint_eq (fmap loops (pmap_from_point f x)) @
(dpoint_eq (pmap_from_point (ap f) 1))^ reflexivity. }
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
IsEquiv
  (fmap (Pi k.+1) (fmap loops (pmap_from_point f x)))
    nrefine (isequiv_commsq _ _ _ _ (fmap_pi_loops k.+1 (pmap_from_point f x))).
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
IsEquiv (fmap (Pi k.+2) (pmap_from_point f x))
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
IsEquiv (pi_loops k.+1 [A, x])
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
IsEquiv (pi_loops k.+1 [B, f x])
    2-3:refine (equiv_isequiv (pi_loops _ _)).
ua: Univalence
n: trunc_index
IHn: forall A B : Type,
IsTrunc n A ->
IsTrunc n B ->
forall f : A -> B,
IsEquiv (Trunc_functor 0 f) ->
(forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))) ->
IsEquiv f
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x : A) (k : nat),
IsEquiv (fmap (Pi k.+1) (pmap_from_point f x))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
k: nat
IsEquiv (fmap (Pi k.+2) (pmap_from_point f x))
    exact (ii x k.+1).
Defined.