From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
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 x0 : A, IsEquiv (fmap loops (pmap_from_point f x0))
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 x0 : A, IsEquiv (fmap loops (pmap_from_point f x0))
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 x0 : A, IsEquiv (fmap loops (pmap_from_point f x0))
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 x0 : A, IsEquiv (fmap loops (pmap_from_point f x0))
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 x0 : A, IsEquiv (fmap loops (pmap_from_point f x0))
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 x0 : A, IsEquiv (fmap loops (pmap_from_point f x0))
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 x0 : A, IsEquiv (fmap loops (pmap_from_point f x0))
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 x0 : A, IsEquiv (fmap loops (pmap_from_point f x0))
x: A
IsEquiv (ap f)
  cbn in ii.
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x0 : A, IsEquiv (fun p : x0 = x0 => 1 @ (ap f p @ 1))
x: A
IsEquiv (ap f)
  snapply (isequiv_homotopic _ (H:=ii x)).
H: Univalence
A, B: Type
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall x0 : A, IsEquiv (fun p : x0 = x0 => 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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x))) ->
IsEquiv f0
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x))) ->
IsEquiv f0
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
x: A
IsEquiv (fmap loops (pmap_from_point f x))
  nrefine (isequiv_homotopic (@ap _ _ f x x) _).
ua: Univalence
n: trunc_index
IHn: forall A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
x: A
IsEquiv (ap f)
ua: Univalence
n: trunc_index
IHn: forall A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
x: A
ap f == fmap loops (pmap_from_point f x)
  2:{
ua: Univalence
n: trunc_index
IHn: forall A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
x: A
ap f == fmap loops (pmap_from_point f x)intros p; cbn.
ua: Univalence
n: trunc_index
IHn: forall A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
x: A
IsEquiv (ap f)
  pose proof (@istrunc_paths _ _ H0 x x) as h0.
ua: Univalence
n: trunc_index
IHn: forall A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
x: A
h0: IsTrunc n (x = x)
h1: IsTrunc n (f x = f x)
h2: IsEquiv (Trunc_functor 0 (fun p0 : x = x => 1 @ (ap f p0 @ 1)))
p: x = x
1 @ (ap f p @ 1) = ap f p
    exact (concat_1p _ @ concat_p1 _).
  -
ua: Univalence
n: trunc_index
IHn: forall A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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) tapply (fmap2 (Pi k.+1)); srefine (Build_pHomotopy _ _).
ua: Univalence
n: trunc_index
IHn: forall A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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
          exact (concat_1p _ @ concat_p1 _).
        -
ua: Univalence
n: trunc_index
IHn: forall A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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 A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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:exact (equiv_isequiv (pi_loops _ _)).
ua: Univalence
n: trunc_index
IHn: forall A0 B0 : Type,
IsTrunc n A0 ->
IsTrunc n B0 ->
forall f0 : A0 -> B0,
IsEquiv (Trunc_functor 0 f0) ->
(forall (x0 : A0) (k0 : nat),
 IsEquiv (fmap (Pi k0.+1) (pmap_from_point f0 x0))) ->
IsEquiv f0
A, B: Type
H0: IsTrunc n.+1 A
H1: IsTrunc n.+1 B
f: A -> B
i: IsEquiv (Trunc_functor 0 f)
ii: forall (x0 : A) (k0 : nat), IsEquiv (fmap (Pi k0.+1) (pmap_from_point f x0))
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.