Require Import HoTT.Basics HoTT.Types.Require Import HoTT.Basics HoTT.Types.
Require Import HFiber Factorization Truncations.Core Truncations.Connectedness HProp.
From HoTT.WildCat Require Import Core Equiv PointedCat NatTrans.
Require Import Pointed.Core Pointed.pEquiv.
Require Import Spaces.Nat.Core.

Local Open Scope pointed_scope.
Local Open Scope path_scope.

(** ** Loop spaces *)

(** The type [x = x] is pointed. *)
Instance ispointed_loops A (a : A) : IsPointed (a = a) := 1.

Definition loops (A : pType) : pType
  := [point A = point A, 1].

Definition iterated_loops (n : nat) (A : pType) : pType
  := nat_iter n loops A.

(* Inner unfolding for iterated loops *)
Definition unfold_iterated_loops (n : nat) (X : pType)
  : iterated_loops n.+1 X = iterated_loops n (loops X)
  := nat_iter_succ_r _ _ _.

(** The loop space decreases the truncation level by one.  We don't bother making this an instance because it is automatically found by typeclass search, but we record it here in case anyone is looking for it. *)
Definition istrunc_loops {n} (A : pType) `{IsTrunc n.+1 A}
  : IsTrunc n (loops A) := _.

(** Similarly for connectedness. *)
Definition isconnected_loops `{Univalence} {n} (A : pType)
  `{IsConnected n.+1 A} : IsConnected n (loops A) := _.

Lemma pequiv_loops_punit : loops pUnit <~>* pUnit.
loops pUnit <~>* pUnit
Proof.
loops pUnit <~>* pUnit
  snapply Build_pEquiv'.
loops pUnit <~> pUnit
?f pt = pt
  {
loops pUnit <~> pUnit srapply (equiv_adjointify (fun _ => tt) (fun _ => idpath)).
(fun _ : pt = pt => tt) o unit_name 1 == idmap
unit_name 1 o (fun _ : pt = pt => tt) == idmap
    1: by intros [].
unit_name 1 o (fun _ : pt = pt => tt) == idmap
    rapply path_contr. }
equiv_adjointify (fun _ : pt = pt => tt) (unit_name 1)
  ((fun x : Unit => match x as u return (tt = u) with
                    | tt => 1
                    end)
   :
   (fun _ : pt = pt => tt) o unit_name 1 == idmap)
  (path_contr 1) pt =
pt
  reflexivity.
Defined. 

(** ** Functoriality of loop spaces *)

(** Action on 1-cells *)
Instance is0functor_loops : Is0Functor loops.
Is0Functor loops
Proof.
Is0Functor loops
  apply Build_Is0Functor.
forall a b : pType, (a $-> b) -> loops a $-> loops b
  intros A B f.
A, B: pType
f: A $-> B
loops A $-> loops B
  refine (Build_pMap (fun p => (point_eq f)^ @ (ap f p @ point_eq f)) _).
A, B: pType
f: A $-> B
(point_eq f)^ @ (ap f pt @ point_eq f) = pt
  refine (_ @ concat_Vp (point_eq f)).
A, B: pType
f: A $-> B
(point_eq f)^ @ (ap f pt @ point_eq f) = (point_eq f)^ @ point_eq f
  apply whiskerL.
A, B: pType
f: A $-> B
ap f pt @ point_eq f = point_eq f apply concat_1p.
Defined.

Instance is1functor_loops : Is1Functor loops.
Is1Functor loops
Proof.
Is1Functor loops
  apply Build_Is1Functor.
forall (a b : pType) (f g : a $-> b),
f $== g -> fmap loops f $== fmap loops g
forall a : pType, fmap loops (Id a) $== Id (loops a)
forall (a b c : pType) (f : a $-> b) (g : b $-> c),
fmap loops (g $o f) $== fmap loops g $o fmap loops f
  (** Action on 2-cells *)
  -
forall (a b : pType) (f g : a $-> b),
f $== g -> fmap loops f $== fmap loops g intros A B f g p.
A, B: pType
f, g: A $-> B
p: f $== g
fmap loops f $== fmap loops g
    pointed_reduce.
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
Build_pMap
  (fun p0 : point0 = point0 => (p point0 @ 1)^ @ (ap f p0 @ (p point0 @ 1)))
  (whiskerL (p point0 @ 1)^ (concat_1p (p point0 @ 1)) @
   concat_Vp (p point0 @ 1)) ==*
Build_pMap (fun p0 : point0 = point0 => 1 @ (ap g p0 @ 1)) 1
    srapply Build_pHomotopy; cbn.
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
(fun p0 : point0 = point0 => (p point0 @ 1)^ @ (ap f p0 @ (p point0 @ 1))) ==
(fun p0 : point0 = point0 => 1 @ (ap g p0 @ 1))
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
?Goal1 1 =
(whiskerL (p point0 @ 1)^ (concat_1p (p point0 @ 1)) @
 concat_Vp (p point0 @ 1)) @
1
    {
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
(fun p0 : point0 = point0 => (p point0 @ 1)^ @ (ap f p0 @ (p point0 @ 1))) ==
(fun p0 : point0 = point0 => 1 @ (ap g p0 @ 1)) intro q.
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
q: point0 = point0
(p point0 @ 1)^ @ (ap f q @ (p point0 @ 1)) = 1 @ (ap g q @ 1)
      refine (_ @ (concat_p1 _)^ @ (concat_1p _)^).
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
q: point0 = point0
(p point0 @ 1)^ @ (ap f q @ (p point0 @ 1)) = ap g q
      apply moveR_Vp.
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
q: point0 = point0
ap f q @ (p point0 @ 1) = (p point0 @ 1) @ ap g q
      apply (concat_Ap (fun x => p x @ 1)). }
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
((fun q : point0 = point0 =>
  (moveR_Vp (ap f q @ (p point0 @ 1)) (ap g q) (p point0 @ 1)
     (concat_Ap (fun x : A => p x @ 1) q) @
   (concat_p1 (ap g q))^) @
  (concat_1p (ap g q @ 1))^)
 :
 (fun p0 : point0 = point0 => (p point0 @ 1)^ @ (ap f p0 @ (p point0 @ 1))) ==
 (fun p0 : point0 = point0 => 1 @ (ap g p0 @ 1))) 1 =
(whiskerL (p point0 @ 1)^ (concat_1p (p point0 @ 1)) @
 concat_Vp (p point0 @ 1)) @
1
    simpl.
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
(moveR_Vp (1 @ (p point0 @ 1)) 1 (p point0 @ 1) (concat_1p_p1 (p point0 @ 1)) @
 1) @
1 =
(whiskerL (p point0 @ 1)^ (concat_1p (p point0 @ 1)) @
 concat_Vp (p point0 @ 1)) @
1 generalize (p point0).
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
forall p0 : f point0 = g point0,
(moveR_Vp (1 @ (p0 @ 1)) 1 (p0 @ 1) (concat_1p_p1 (p0 @ 1)) @ 1) @ 1 =
(whiskerL (p0 @ 1)^ (concat_1p (p0 @ 1)) @ concat_Vp (p0 @ 1)) @ 1 generalize (g point0).
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
forall (b : B) (p0 : f point0 = b),
(moveR_Vp (1 @ (p0 @ 1)) 1 (p0 @ 1) (concat_1p_p1 (p0 @ 1)) @ 1) @ 1 =
(whiskerL (p0 @ 1)^ (concat_1p (p0 @ 1)) @ concat_Vp (p0 @ 1)) @ 1
    intros _ [].
A: Type
point0: IsPointed A
B: Type
f, g: A -> B
p: forall x : A, f x = g x
(moveR_Vp (1 @ (1 @ 1)) 1 (1 @ 1) (concat_1p_p1 (1 @ 1)) @ 1) @ 1 =
(whiskerL (1 @ 1)^ (concat_1p (1 @ 1)) @ concat_Vp (1 @ 1)) @ 1 reflexivity.
  (** Preservation of identity. *)
  -
forall a : pType, fmap loops (Id a) $== Id (loops a) intros A.
A: pType
fmap loops (Id A) $== Id (loops A)
    srapply Build_pHomotopy.
A: pType
fmap loops (Id A) == Id (loops A)
A: pType
?p pt = dpoint_eq (fmap loops (Id A)) @ (dpoint_eq (Id (loops A)))^
    {
A: pType
fmap loops (Id A) == Id (loops A) intro p.
A: pType
p: loops A
fmap loops (Id A) p = Id (loops A) p
      refine (concat_1p _ @ concat_p1 _ @ ap_idmap _). }
A: pType
((fun p : loops A =>
  (concat_1p (ap idmap p @ 1) @ concat_p1 (ap idmap p)) @ ap_idmap p)
 :
 fmap loops (Id A) == Id (loops A)) pt =
dpoint_eq (fmap loops (Id A)) @ (dpoint_eq (Id (loops A)))^
    reflexivity.
  (** Preservation of composition. *)
  -
forall (a b c : pType) (f : a $-> b) (g : b $-> c),
fmap loops (g $o f) $== fmap loops g $o fmap loops f intros A B c g f.
A, B, c: pType
g: A $-> B
f: B $-> c
fmap loops (f $o g) $== fmap loops f $o fmap loops g
    srapply Build_pHomotopy.
A, B, c: pType
g: A $-> B
f: B $-> c
fmap loops (f $o g) == fmap loops f $o fmap loops g
A, B, c: pType
g: A $-> B
f: B $-> c
?p pt =
dpoint_eq (fmap loops (f $o g)) @ (dpoint_eq (fmap loops f $o fmap loops g))^
    {
A, B, c: pType
g: A $-> B
f: B $-> c
fmap loops (f $o g) == fmap loops f $o fmap loops g intros p.
A, B, c: pType
g: A $-> B
f: B $-> c
p: loops A
fmap loops (f $o g) p = (fmap loops f $o fmap loops g) p cbn.
A, B, c: pType
g: A $-> B
f: B $-> c
p: loops A
(ap f (point_eq g) @ point_eq f)^ @
(ap (fun x : A => f (g x)) p @ (ap f (point_eq g) @ point_eq f)) =
(point_eq f)^ @ (ap f ((point_eq g)^ @ (ap g p @ point_eq g)) @ point_eq f)
      refine ((inv_pp _ _ @@ 1) @ concat_pp_p _ _ _ @ _).
A, B, c: pType
g: A $-> B
f: B $-> c
p: loops A
(point_eq f)^ @
((ap f (point_eq g))^ @
 (ap (fun x : A => f (g x)) p @ (ap f (point_eq g) @ point_eq f))) =
(point_eq f)^ @ (ap f ((point_eq g)^ @ (ap g p @ point_eq g)) @ point_eq f)
      apply whiskerL.
A, B, c: pType
g: A $-> B
f: B $-> c
p: loops A
(ap f (point_eq g))^ @
(ap (fun x : A => f (g x)) p @ (ap f (point_eq g) @ point_eq f)) =
ap f ((point_eq g)^ @ (ap g p @ point_eq g)) @ point_eq f
      refine (((ap_V _ _)^ @@ 1) @ _ @ concat_p_pp _ _ _ @ ((ap_pp _ _ _)^ @@ 1)).
A, B, c: pType
g: A $-> B
f: B $-> c
p: loops A
ap f (point_eq g)^ @
(ap (fun x : A => f (g x)) p @ (ap f (point_eq g) @ point_eq f)) =
ap f (point_eq g)^ @ (ap f (ap g p @ point_eq g) @ point_eq f)
      apply whiskerL.
A, B, c: pType
g: A $-> B
f: B $-> c
p: loops A
ap (fun x : A => f (g x)) p @ (ap f (point_eq g) @ point_eq f) =
ap f (ap g p @ point_eq g) @ point_eq f
      refine (_ @ concat_p_pp _ _ _ @ ((ap_pp _ _ _)^ @@ 1)).
A, B, c: pType
g: A $-> B
f: B $-> c
p: loops A
ap (fun x : A => f (g x)) p @ (ap f (point_eq g) @ point_eq f) =
ap f (ap g p) @ (ap f (point_eq g) @ point_eq f)
      apply whiskerR.
A, B, c: pType
g: A $-> B
f: B $-> c
p: loops A
ap (fun x : A => f (g x)) p = ap f (ap g p)
      apply ap_compose. }
A, B, c: pType
g: A $-> B
f: B $-> c
((fun p : loops A =>
  ((inv_pp (ap f (point_eq g)) (point_eq f) @@ 1) @
   concat_pp_p (point_eq f)^ (ap f (point_eq g))^
     (ap (fun x : A => f (g x)) p @ (ap f (point_eq g) @ point_eq f))) @
  whiskerL (point_eq f)^
    (((((ap_V f (point_eq g))^ @@ 1) @
       whiskerL (ap f (point_eq g)^)
         ((whiskerR (ap_compose g f p) (ap f (point_eq g) @ point_eq f) @
           concat_p_pp (ap f (ap g p)) (ap f (point_eq g)) (point_eq f)) @
          ((ap_pp f (ap g p) (point_eq g))^ @@ 1))) @
      concat_p_pp (ap f (point_eq g)^) (ap f (ap g p @ point_eq g))
        (point_eq f)) @
     ((ap_pp f (point_eq g)^ (ap g p @ point_eq g))^ @@ 1))
  :
  fmap loops (f $o g) p = (fmap loops f $o fmap loops g) p)
 :
 fmap loops (f $o g) == fmap loops f $o fmap loops g) pt =
dpoint_eq (fmap loops (f $o g)) @ (dpoint_eq (fmap loops f $o fmap loops g))^
    by pointed_reduce.
Defined.

(** *** Properties of loops functor *)

(** Loops functor distributes over concatenation *)
Lemma fmap_loops_pp {X Y : pType} (f : X ->* Y) (x y : loops X)
  : fmap loops f (x @ y) = fmap loops f x @ fmap loops f y.
X, Y: pType
f: X ->* Y
x, y: loops X
fmap loops f (x @ y) = fmap loops f x @ fmap loops f y
Proof.
X, Y: pType
f: X ->* Y
x, y: loops X
fmap loops f (x @ y) = fmap loops f x @ fmap loops f y
  pointed_reduce_rewrite.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
x, y: point0 = point0
ap f (x @ y) = ap f x @ ap f y
  apply ap_pp.
Defined.

(** Loops is a pointed functor *)
Instance ispointedfunctor_loops : IsPointedFunctor loops.
IsPointedFunctor loops
Proof.
IsPointedFunctor loops
  snapply Build_IsPointedFunctor'.
IsPointedCat pType
IsPointedCat pType
HasEquivs pType
HasEquivs pType
loops zero_object $<~> zero_object
  1-4: exact _.
loops zero_object $<~> zero_object
  exact pequiv_loops_punit.
Defined.

Lemma fmap_loops_pconst {A B : pType} : fmap loops (@pconst A B) ==* pconst.
A, B: pType
fmap loops pconst ==* pconst
Proof.
A, B: pType
fmap loops pconst ==* pconst
  tapply fmap_zero_morphism.
Defined.

(** *** Iterated loops functor *)

(** Action on 1-cells *)
Instance is0functor_iterated_loops n : Is0Functor (iterated_loops n).
n: nat
Is0Functor (iterated_loops n)
Proof.
n: nat
Is0Functor (iterated_loops n)
  induction n.
Is0Functor (iterated_loops 0)
n: nat
IHn: Is0Functor (iterated_loops n)
Is0Functor (iterated_loops n.+1)
  1: exact _.
n: nat
IHn: Is0Functor (iterated_loops n)
Is0Functor (iterated_loops n.+1)
  napply is0functor_compose; exact _.
Defined.

Instance is1functor_iterated_loops n : Is1Functor (iterated_loops n).
n: nat
Is1Functor (iterated_loops n)
Proof.
n: nat
Is1Functor (iterated_loops n)
  induction n.
Is1Functor (iterated_loops 0)
n: nat
IHn: Is1Functor (iterated_loops n)
Is1Functor (iterated_loops n.+1)
  1: exact _.
n: nat
IHn: Is1Functor (iterated_loops n)
Is1Functor (iterated_loops n.+1)
  napply is1functor_compose; exact _.
Defined.

Lemma fmap_iterated_loops_pp {X Y : pType} (f : X ->* Y) n
  (x y : iterated_loops n.+1 X)
  : fmap (iterated_loops n.+1) f (x @ y)
    = fmap (iterated_loops n.+1) f x @ fmap (iterated_loops n.+1) f y.
X, Y: pType
f: X ->* Y
n: nat
x, y: iterated_loops n.+1 X
fmap (iterated_loops n.+1) f (x @ y) =
fmap (iterated_loops n.+1) f x @ fmap (iterated_loops n.+1) f y
Proof.
X, Y: pType
f: X ->* Y
n: nat
x, y: iterated_loops n.+1 X
fmap (iterated_loops n.+1) f (x @ y) =
fmap (iterated_loops n.+1) f x @ fmap (iterated_loops n.+1) f y
  apply fmap_loops_pp.
Defined.

(** The fiber of [fmap loops f] is equivalent to a fiber of [ap f]. *)
Definition hfiber_fmap_loops {A B : pType} (f : A ->* B) (p : loops B)
  : {q : loops A & ap f q = (point_eq f @ p) @ (point_eq f)^}
    <~> hfiber (fmap loops f) p.
A, B: pType
f: A ->* B
p: loops B
{q : loops A & ap f q = (point_eq f @ p) @ (point_eq f)^} <~>
hfiber (fmap loops f) p
Proof.
A, B: pType
f: A ->* B
p: loops B
{q : loops A & ap f q = (point_eq f @ p) @ (point_eq f)^} <~>
hfiber (fmap loops f) p
  apply equiv_functor_sigma_id; intros q.
A, B: pType
f: A ->* B
p: loops B
q: loops A
ap f q = (point_eq f @ p) @ (point_eq f)^ <~> fmap loops f q = p
  refine (equiv_moveR_Vp _ _ _ oE _).
A, B: pType
f: A ->* B
p: loops B
q: loops A
ap f q = (point_eq f @ p) @ (point_eq f)^ <~>
ap f q @ point_eq f = point_eq f @ p
  apply equiv_moveR_pM.
Defined.

(** The loop space functor decreases the truncation level by one.  *)
Instance istrunc_fmap_loops {n} (A B : pType) (f : A ->* B)
  `{IsTruncMap n.+1 _ _ f} : IsTruncMap n (fmap loops f).
n: trunc_index
A, B: pType
f: A ->* B
H: IsTruncMap n.+1 f
IsTruncMap n (fmap loops f)
Proof.
n: trunc_index
A, B: pType
f: A ->* B
H: IsTruncMap n.+1 f
IsTruncMap n (fmap loops f)
  intro p.
n: trunc_index
A, B: pType
f: A ->* B
H: IsTruncMap n.+1 f
p: loops B
IsTrunc n (hfiber (fmap loops f) p) exact (istrunc_equiv_istrunc _ (hfiber_fmap_loops f p)).
Defined.

(** And likewise the connectedness.  *)
Instance conn_map_fmap_loops `{Univalence} {n : trunc_index}
  (A B : pType) (f : A ->* B) `{IsConnMap n.+1 _ _ f}
  : IsConnMap n (fmap loops f).
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
H0: IsConnMap (Tr n.+1) f
IsConnMap (Tr n) (fmap loops f)
Proof.
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
H0: IsConnMap (Tr n.+1) f
IsConnMap (Tr n) (fmap loops f)
  intros p; eapply isconnected_equiv'.
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
H0: IsConnMap (Tr n.+1) f
p: loops B
?A <~> hfiber (fmap loops f) p
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
H0: IsConnMap (Tr n.+1) f
p: loops B
IsConnected (Tr n) ?A
  -
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
H0: IsConnMap (Tr n.+1) f
p: loops B
?A <~> hfiber (fmap loops f) p refine (hfiber_fmap_loops f p oE _).
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
H0: IsConnMap (Tr n.+1) f
p: loops B
?A <~> {q : loops A & ap f q = (point_eq f @ p) @ (point_eq f)^}
    symmetry; apply hfiber_ap.
  -
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
H0: IsConnMap (Tr n.+1) f
p: loops B
IsConnected (Tr n) ((pt; (point_eq f @ p) @ (point_eq f)^) = (pt; 1)) exact _.
Defined.

Definition conn_map_iterated_fmap_loops `{Univalence}
  (n : trunc_index) (k : nat) (A B : pType) (f : A ->* B)
  (C : IsConnMap (trunc_index_inc' n k) f)
  : IsConnMap n (fmap (iterated_loops k) f).
H: Univalence
n: trunc_index
k: nat
A, B: pType
f: A ->* B
C: IsConnMap (Tr (trunc_index_inc' n k)) f
IsConnMap (Tr n) (fmap (iterated_loops k) f)
Proof.
H: Univalence
n: trunc_index
k: nat
A, B: pType
f: A ->* B
C: IsConnMap (Tr (trunc_index_inc' n k)) f
IsConnMap (Tr n) (fmap (iterated_loops k) f)
  induction k in n, C |- *.
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C: IsConnMap (Tr (trunc_index_inc' n 0)) f
IsConnMap (Tr n) (fmap (iterated_loops 0) f)
H: Univalence
n: trunc_index
k: nat
A, B: pType
f: A ->* B
C: IsConnMap (Tr (trunc_index_inc' n k.+1)) f
IHk: forall n0 : trunc_index,
IsConnMap (Tr (trunc_index_inc' n0 k)) f ->
IsConnMap (Tr n0) (fmap (iterated_loops k) f)
IsConnMap (Tr n) (fmap (iterated_loops k.+1) f)
  -
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C: IsConnMap (Tr (trunc_index_inc' n 0)) f
IsConnMap (Tr n) (fmap (iterated_loops 0) f) exact C.
  -
H: Univalence
n: trunc_index
k: nat
A, B: pType
f: A ->* B
C: IsConnMap (Tr (trunc_index_inc' n k.+1)) f
IHk: forall n0 : trunc_index,
IsConnMap (Tr (trunc_index_inc' n0 k)) f ->
IsConnMap (Tr n0) (fmap (iterated_loops k) f)
IsConnMap (Tr n) (fmap (iterated_loops k.+1) f) apply conn_map_fmap_loops.
H: Univalence
n: trunc_index
k: nat
A, B: pType
f: A ->* B
C: IsConnMap (Tr (trunc_index_inc' n k.+1)) f
IHk: forall n0 : trunc_index,
IsConnMap (Tr (trunc_index_inc' n0 k)) f ->
IsConnMap (Tr n0) (fmap (iterated_loops k) f)
IsConnMap (Tr n.+1) (fmap (iterated_loops k) f)
    apply IHk.
H: Univalence
n: trunc_index
k: nat
A, B: pType
f: A ->* B
C: IsConnMap (Tr (trunc_index_inc' n k.+1)) f
IHk: forall n0 : trunc_index,
IsConnMap (Tr (trunc_index_inc' n0 k)) f ->
IsConnMap (Tr n0) (fmap (iterated_loops k) f)
IsConnMap (Tr (trunc_index_inc' n.+1 k)) f
    exact C.
Defined.

(** It follows that loop spaces "commute with images". *)
Definition equiv_loops_image `{Univalence} n {A B : pType} (f : A ->* B)
  : loops ([image n.+1 f, factor1 (image n.+1 f) (point A)])
  <~> image n (fmap loops f).
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
loops [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt] <~>
image (Tr n) (fmap loops f)
Proof.
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
loops [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt] <~>
image (Tr n) (fmap loops f)
  set (C := [image n.+1 f, factor1 (image n.+1 f) (point A)]).
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
loops C <~> image (Tr n) (fmap loops f)
  pose (g := @Build_pMap A C (factor1 (image n.+1 f)) 1).
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
g:= Build_pMap (factor1 (image (Tr n.+1) f)) 1: A ->* C
loops C <~> image (Tr n) (fmap loops f)
  pose (h := @Build_pMap C B (factor2 (image n.+1 f)) (point_eq f)).
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
g:= Build_pMap (factor1 (image (Tr n.+1) f)) 1: A ->* C
h:= Build_pMap (factor2 (image (Tr n.+1) f)) (point_eq f): C ->* B
loops C <~> image (Tr n) (fmap loops f)
  transparent assert (I : (Factorization
    (@IsConnMap n) (@MapIn n) (fmap loops f))).
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
g:= Build_pMap (factor1 (image (Tr n.+1) f)) 1: A ->* C
h:= Build_pMap (factor2 (image (Tr n.+1) f)) (point_eq f): C ->* B
Factorization (@IsConnMap (Tr n)) (@MapIn (Tr n)) (fmap loops f)
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
g:= Build_pMap (factor1 (image (Tr n.+1) f)) 1: A ->* C
h:= Build_pMap (factor2 (image (Tr n.+1) f)) (point_eq f): C ->* B
I:= ?Goal: Factorization (@IsConnMap (Tr n)) (@MapIn (Tr n)) (fmap loops f)
loops C <~> image (Tr n) (fmap loops f)
  {
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
g:= Build_pMap (factor1 (image (Tr n.+1) f)) 1: A ->* C
h:= Build_pMap (factor2 (image (Tr n.+1) f)) (point_eq f): C ->* B
Factorization (@IsConnMap (Tr n)) (@MapIn (Tr n)) (fmap loops f) refine (@Build_Factorization (@IsConnMap n) (@MapIn n)
      (loops A) (loops B) (fmap loops f) (loops C)
      (fmap loops g) (fmap loops h) _ _ _).
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
g:= Build_pMap (factor1 (image (Tr n.+1) f)) 1: A ->* C
h:= Build_pMap (factor2 (image (Tr n.+1) f)) (point_eq f): C ->* B
(fun x : loops A => fmap loops h (fmap loops g x)) == fmap loops f
    intros x; symmetry.
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
g:= Build_pMap (factor1 (image (Tr n.+1) f)) 1: A ->* C
h:= Build_pMap (factor2 (image (Tr n.+1) f)) (point_eq f): C ->* B
x: loops A
fmap loops f x = fmap loops h (fmap loops g x)
    refine (_ @ fmap_comp loops g h x).
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
g:= Build_pMap (factor1 (image (Tr n.+1) f)) 1: A ->* C
h:= Build_pMap (factor2 (image (Tr n.+1) f)) (point_eq f): C ->* B
x: loops A
fmap loops f x = fmap loops (h $o g) x
    simpl.
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
g:= Build_pMap (factor1 (image (Tr n.+1) f)) 1: A ->* C
h:= Build_pMap (factor2 (image (Tr n.+1) f)) (point_eq f): C ->* B
x: loops A
(point_eq f)^ @ (ap f x @ point_eq f) =
(1 @ point_eq f)^ @ (ap (fun x0 : A => f x0) x @ (1 @ point_eq f))
    abstract (rewrite !concat_1p; reflexivity). }
H: Univalence
n: trunc_index
A, B: pType
f: A ->* B
C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
g:= Build_pMap (factor1 (image (Tr n.+1) f)) 1: A ->* C
h:= Build_pMap (factor2 (image (Tr n.+1) f)) (point_eq f): C ->* B
I:= {|
  intermediate := loops C;
  factor1 := fmap loops g;
  factor2 := fmap loops h;
  fact_factors :=
    (fun x : loops A =>
     ((equiv_loops_image_subproof A B f x
       :
       fmap loops f x = fmap loops (h $o g) x) @
      fmap_comp loops g h x)^)
    :
    (fun x : loops A => fmap loops h (fmap loops g x)) == fmap loops f;
  inclass1 := conn_map_fmap_loops A C g;
  inclass2 := mapinO_tr_istruncmap (fmap loops h)
|}: Factorization (@IsConnMap (Tr n)) (@MapIn (Tr n)) (fmap loops f)
loops C <~> image (Tr n) (fmap loops f)
  exact (path_intermediate (path_factor (O_factsys n) (fmap loops f) I
    (image n (fmap loops f)))).
Defined.

(** Loop inversion is a pointed equivalence *)
Definition loops_inv (A : pType) : loops A <~>* loops A.
A: pType
loops A <~>* loops A
Proof.
A: pType
loops A <~>* loops A
  srapply Build_pEquiv.
A: pType
loops A ->* loops A
A: pType
IsEquiv ?pointed_equiv_fun
  1: exact (Build_pMap inverse 1).
A: pType
IsEquiv (Build_pMap inverse 1)
  apply isequiv_path_inverse.
Defined.

(** Loops functor preserves equivalences *)
Definition pequiv_fmap_loops {A B : pType}
  : A $<~> B -> loops A $<~> loops B
  := emap loops.

(** A version of [unfold_iterated_loops] that's an equivalence rather than an equality.  We could get this from the equality, but it's more useful to construct it explicitly since then we can reason about it. *)
Definition unfold_iterated_loops' (n : nat) (X : pType)
  : iterated_loops n.+1 X <~>* iterated_loops n (loops X).
n: nat
X: pType
iterated_loops n.+1 X <~>* iterated_loops n (loops X)
Proof.
n: nat
X: pType
iterated_loops n.+1 X <~>* iterated_loops n (loops X)
  induction n.
X: pType
iterated_loops 1 X <~>* iterated_loops 0 (loops X)
n: nat
X: pType
IHn: iterated_loops n.+1 X <~>* iterated_loops n (loops X)
iterated_loops n.+2 X <~>* iterated_loops n.+1 (loops X)
  1: reflexivity.
n: nat
X: pType
IHn: iterated_loops n.+1 X <~>* iterated_loops n (loops X)
iterated_loops n.+2 X <~>* iterated_loops n.+1 (loops X)
  change (iterated_loops n.+2 X)
    with (loops (iterated_loops n.+1 X)).
n: nat
X: pType
IHn: iterated_loops n.+1 X <~>* iterated_loops n (loops X)
loops (iterated_loops n.+1 X) <~>* iterated_loops n.+1 (loops X)
  apply pequiv_fmap_loops, IHn.
Defined.

(** For instance, we can prove that it's natural. *)
Definition unfold_iterated_fmap_loops {A B : pType} (n : nat) (f : A ->* B)
  : (unfold_iterated_loops' n B) o* (fmap (iterated_loops n.+1) f)
    ==* (fmap (iterated_loops n) (fmap loops f)) o* (unfold_iterated_loops' n A).
A, B: pType
n: nat
f: A ->* B
unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
Proof.
A, B: pType
n: nat
f: A ->* B
unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
  induction n.
A, B: pType
f: A ->* B
unfold_iterated_loops' 0 B o* fmap (iterated_loops 1) f ==*
fmap (iterated_loops 0) (fmap loops f) o* unfold_iterated_loops' 0 A
A, B: pType
n: nat
f: A ->* B
IHn: unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
unfold_iterated_loops' n.+1 B o* fmap (iterated_loops n.+2) f ==*
fmap (iterated_loops n.+1) (fmap loops f) o* unfold_iterated_loops' n.+1 A
  -
A, B: pType
f: A ->* B
unfold_iterated_loops' 0 B o* fmap (iterated_loops 1) f ==*
fmap (iterated_loops 0) (fmap loops f) o* unfold_iterated_loops' 0 A srefine (Build_pHomotopy _ _).
A, B: pType
f: A ->* B
unfold_iterated_loops' 0 B o* fmap (iterated_loops 1) f ==
fmap (iterated_loops 0) (fmap loops f) o* unfold_iterated_loops' 0 A
A, B: pType
f: A ->* B
?p pt =
dpoint_eq (unfold_iterated_loops' 0 B o* fmap (iterated_loops 1) f) @
(dpoint_eq
   (fmap (iterated_loops 0) (fmap loops f) o* unfold_iterated_loops' 0 A))^
    +
A, B: pType
f: A ->* B
unfold_iterated_loops' 0 B o* fmap (iterated_loops 1) f ==
fmap (iterated_loops 0) (fmap loops f) o* unfold_iterated_loops' 0 A reflexivity.
    +
A, B: pType
f: A ->* B
(fun x0 : pt = pt => 1) pt =
dpoint_eq (unfold_iterated_loops' 0 B o* fmap (iterated_loops 1) f) @
(dpoint_eq
   (fmap (iterated_loops 0) (fmap loops f) o* unfold_iterated_loops' 0 A))^ cbn.
A, B: pType
f: A ->* B
1 =
(ap idmap
   (whiskerL (point_eq f)^ (concat_1p (point_eq f)) @ concat_Vp (point_eq f)) @
 1) @
(1 @
 (whiskerL (point_eq f)^ (concat_1p (point_eq f)) @ concat_Vp (point_eq f)))^ apply moveL_pV.
A, B: pType
f: A ->* B
1 @
(1 @
 (whiskerL (point_eq f)^ (concat_1p (point_eq f)) @ concat_Vp (point_eq f))) =
ap idmap
  (whiskerL (point_eq f)^ (concat_1p (point_eq f)) @ concat_Vp (point_eq f)) @
1
      refine (concat_1p _ @ _).
A, B: pType
f: A ->* B
1 @
(whiskerL (point_eq f)^ (concat_1p (point_eq f)) @ concat_Vp (point_eq f)) =
ap idmap
  (whiskerL (point_eq f)^ (concat_1p (point_eq f)) @ concat_Vp (point_eq f)) @
1
      refine (concat_1p _ @ _).
A, B: pType
f: A ->* B
whiskerL (point_eq f)^ (concat_1p (point_eq f)) @ concat_Vp (point_eq f) =
ap idmap
  (whiskerL (point_eq f)^ (concat_1p (point_eq f)) @ concat_Vp (point_eq f)) @
1
      refine (_ @ (concat_p1 _)^).
A, B: pType
f: A ->* B
whiskerL (point_eq f)^ (concat_1p (point_eq f)) @ concat_Vp (point_eq f) =
ap idmap
  (whiskerL (point_eq f)^ (concat_1p (point_eq f)) @ concat_Vp (point_eq f))
      exact ((ap_idmap _)^).
  -
A, B: pType
n: nat
f: A ->* B
IHn: unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
unfold_iterated_loops' n.+1 B o* fmap (iterated_loops n.+2) f ==*
fmap (iterated_loops n.+1) (fmap loops f) o* unfold_iterated_loops' n.+1 A refine ((fmap_comp loops _ _)^* @* _).
A, B: pType
n: nat
f: A ->* B
IHn: unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
fmap loops
  ((fix F (n0 : nat) :
        iterated_loops n0.+1 B <~>* iterated_loops n0 (loops B) :=
      match
        n0 as n1
        return (iterated_loops n1.+1 B <~>* iterated_loops n1 (loops B))
      with
      | 0%nat => pequiv_reflexive (iterated_loops 0 (loops B))
      | n1.+1%nat => pequiv_fmap_loops (F n1)
      end)
     n $o
   fmap (loops o (fun x : pType => nat_iter n loops x)) f) ==*
fmap (iterated_loops n.+1) (fmap loops f) o* unfold_iterated_loops' n.+1 A
    refine (_ @* (fmap_comp loops _ _)).
A, B: pType
n: nat
f: A ->* B
IHn: unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
fmap loops
  ((fix F (n0 : nat) :
        iterated_loops n0.+1 B <~>* iterated_loops n0 (loops B) :=
      match
        n0 as n1
        return (iterated_loops n1.+1 B <~>* iterated_loops n1 (loops B))
      with
      | 0%nat => pequiv_reflexive (iterated_loops 0 (loops B))
      | n1.+1%nat => pequiv_fmap_loops (F n1)
      end)
     n $o
   fmap (loops o (fun x : pType => nat_iter n loops x)) f) ==*
fmap loops
  (fmap (iterated_loops n) (fmap loops f) $o
   (fix F (n0 : nat) :
        iterated_loops n0.+1 A <~>* iterated_loops n0 (loops A) :=
      match
        n0 as n1
        return (iterated_loops n1.+1 A <~>* iterated_loops n1 (loops A))
      with
      | 0%nat => pequiv_reflexive (iterated_loops 0 (loops A))
      | n1.+1%nat => pequiv_fmap_loops (F n1)
      end)
     n)
    tapply (fmap2 loops).
A, B: pType
n: nat
f: A ->* B
IHn: unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
(fix F (n0 : nat) :
     iterated_loops n0.+1 B <~>* iterated_loops n0 (loops B) :=
   match
     n0 as n1
     return (iterated_loops n1.+1 B <~>* iterated_loops n1 (loops B))
   with
   | 0%nat => pequiv_reflexive (iterated_loops 0 (loops B))
   | n1.+1%nat => pequiv_fmap_loops (F n1)
   end)
  n $o
fmap (loops o (fun x : pType => nat_iter n loops x)) f $==
fmap (iterated_loops n) (fmap loops f) $o
(fix F (n0 : nat) :
     iterated_loops n0.+1 A <~>* iterated_loops n0 (loops A) :=
   match
     n0 as n1
     return (iterated_loops n1.+1 A <~>* iterated_loops n1 (loops A))
   with
   | 0%nat => pequiv_reflexive (iterated_loops 0 (loops A))
   | n1.+1%nat => pequiv_fmap_loops (F n1)
   end)
  n
    exact IHn.
Defined.

(** Iterated loops preserves equivalences *)
Definition pequiv_fmap_iterated_loops {A B} n
  : A <~>* B -> iterated_loops n A <~>* iterated_loops n B
  := emap (iterated_loops n).

(** Loops preserves products. *)
Lemma loops_prod (X Y : pType) : loops (X * Y) <~>* loops X * loops Y.
X, Y: pType
loops (X * Y) <~>* loops X * loops Y
Proof.
X, Y: pType
loops (X * Y) <~>* loops X * loops Y
  snapply Build_pEquiv'.
X, Y: pType
loops (X * Y) <~> [loops X * loops Y, ispointed_prod]
X, Y: pType
?f pt = pt
  1: exact (equiv_path_prod (point (X * Y)) (point (X * Y)))^-1%equiv.
X, Y: pType
(equiv_path_prod pt pt)^-1%equiv pt = pt
  reflexivity.
Defined.

(** There is a natural map from [loops (X * Y)] to [loops X * loops Y], and ideally it would definitionally underlie the equivalence [loops_prod].  That's not the case, but we show that [loops_prod] is homotopic to the expected maps after projecting to each factor. *)
Definition pfst_loops_prod (X Y : pType)
  : pfst o* loops_prod X Y ==* fmap loops pfst.
X, Y: pType
pfst o* loops_prod X Y ==* fmap loops pfst
Proof.
X, Y: pType
pfst o* loops_prod X Y ==* fmap loops pfst
  snapply Build_pHomotopy.
X, Y: pType
pfst o* loops_prod X Y == fmap loops pfst
X, Y: pType
?p pt = dpoint_eq (pfst o* loops_prod X Y) @ (dpoint_eq (fmap loops pfst))^
  -
X, Y: pType
pfst o* loops_prod X Y == fmap loops pfst intro p; simpl.
X, Y: pType
p: loops (X * Y)
ap fst p = 1 @ (ap fst p @ 1)
    rhs napply concat_1p.
X, Y: pType
p: loops (X * Y)
ap fst p = ap fst p @ 1
    symmetry; apply concat_p1.
  -
X, Y: pType
((fun p : loops (X * Y) =>
  (concat_p1 (ap fst p))^ @ (concat_1p (ap fst p @ 1))^
  :
  (pfst o* loops_prod X Y) p = fmap loops pfst p)
 :
 pfst o* loops_prod X Y == fmap loops pfst) pt =
dpoint_eq (pfst o* loops_prod X Y) @ (dpoint_eq (fmap loops pfst))^ reflexivity.
Defined.

Definition psnd_loops_prod (X Y : pType)
  : psnd o* loops_prod X Y ==* fmap loops psnd.
X, Y: pType
psnd o* loops_prod X Y ==* fmap loops psnd
Proof.
X, Y: pType
psnd o* loops_prod X Y ==* fmap loops psnd
  snapply Build_pHomotopy.
X, Y: pType
psnd o* loops_prod X Y == fmap loops psnd
X, Y: pType
?p pt = dpoint_eq (psnd o* loops_prod X Y) @ (dpoint_eq (fmap loops psnd))^
  -
X, Y: pType
psnd o* loops_prod X Y == fmap loops psnd intro p; simpl.
X, Y: pType
p: loops (X * Y)
ap snd p = 1 @ (ap snd p @ 1)
    rhs napply concat_1p.
X, Y: pType
p: loops (X * Y)
ap snd p = ap snd p @ 1
    symmetry; apply concat_p1.
  -
X, Y: pType
((fun p : loops (X * Y) =>
  (concat_p1 (ap snd p))^ @ (concat_1p (ap snd p @ 1))^
  :
  (psnd o* loops_prod X Y) p = fmap loops psnd p)
 :
 psnd o* loops_prod X Y == fmap loops psnd) pt =
dpoint_eq (psnd o* loops_prod X Y) @ (dpoint_eq (fmap loops psnd))^ reflexivity.
Defined.

(** Iterated loops of products are products of iterated loops. *)
Lemma iterated_loops_prod (X Y : pType) {n}
  : iterated_loops n (X * Y) <~>* (iterated_loops n X) * (iterated_loops n Y).
X, Y: pType
n: nat
iterated_loops n (X * Y) <~>* iterated_loops n X * iterated_loops n Y
Proof.
X, Y: pType
n: nat
iterated_loops n (X * Y) <~>* iterated_loops n X * iterated_loops n Y
  induction n as [|n IHn].
X, Y: pType
iterated_loops 0 (X * Y) <~>* iterated_loops 0 X * iterated_loops 0 Y
X, Y: pType
n: nat
IHn: iterated_loops n (X * Y) <~>* iterated_loops n X * iterated_loops n Y
iterated_loops n.+1 (X * Y) <~>*
iterated_loops n.+1 X * iterated_loops n.+1 Y
  1: reflexivity.
X, Y: pType
n: nat
IHn: iterated_loops n (X * Y) <~>* iterated_loops n X * iterated_loops n Y
iterated_loops n.+1 (X * Y) <~>*
iterated_loops n.+1 X * iterated_loops n.+1 Y
  exact (loops_prod _ _ o*E emap loops IHn).
Defined.

(** Similarly, we compute the projections here. *)
Definition pfst_iterated_loops_prod (X Y : pType) {n}
  : pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst.
X, Y: pType
n: nat
pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst
Proof.
X, Y: pType
n: nat
pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst
  induction n as [|n IHn].
X, Y: pType
pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops 0) pfst
X, Y: pType
n: nat
IHn: pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst
pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n.+1) pfst
  -
X, Y: pType
pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops 0) pfst reflexivity.
  -
X, Y: pType
n: nat
IHn: pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst
pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n.+1) pfst change (_ ==* ?R) with (pfst o* (loops_prod _ _ o* fmap loops (iterated_loops_prod _ _)) ==* R).
X, Y: pType
n: nat
IHn: pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst
pfst
o* (loops_prod (iterated_loops n X) (iterated_loops n Y)
    o* fmap loops (iterated_loops_prod X Y)) ==*
fmap (iterated_loops n.+1) pfst
    refine ((pmap_compose_assoc _ _ _)^* @* _).
X, Y: pType
n: nat
IHn: pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst
pfst o* loops_prod (iterated_loops n X) (iterated_loops n Y)
o* fmap loops (iterated_loops_prod X Y) ==* fmap (iterated_loops n.+1) pfst
    refine (pmap_prewhisker _ (pfst_loops_prod _ _) @* _).
X, Y: pType
n: nat
IHn: pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst
fmap loops pfst o* fmap loops (iterated_loops_prod X Y) ==*
fmap (iterated_loops n.+1) pfst
    refine ((fmap_comp loops _ _)^* @* _).
X, Y: pType
n: nat
IHn: pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst
fmap loops (pfst $o iterated_loops_prod X Y) ==*
fmap (iterated_loops n.+1) pfst
    change (?L ==* _) with (L ==* fmap loops (fmap (iterated_loops n) pfst)).
X, Y: pType
n: nat
IHn: pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst
fmap loops (pfst $o iterated_loops_prod X Y) ==*
fmap loops (fmap (iterated_loops n) pfst)
    tapply (fmap2 loops); simpl.
X, Y: pType
n: nat
IHn: pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst
pfst o* iterated_loops_prod X Y ==* fmap (iterated_loops n) pfst
    exact IHn.
Defined.

Definition psnd_iterated_loops_prod (X Y : pType) {n}
  : psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd.
X, Y: pType
n: nat
psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
Proof.
X, Y: pType
n: nat
psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
  induction n as [|n IHn].
X, Y: pType
psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops 0) psnd
X, Y: pType
n: nat
IHn: psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n.+1) psnd
  -
X, Y: pType
psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops 0) psnd reflexivity.
  -
X, Y: pType
n: nat
IHn: psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n.+1) psnd change (_ ==* ?R) with (psnd o* (loops_prod _ _ o* fmap loops (iterated_loops_prod _ _)) ==* R).
X, Y: pType
n: nat
IHn: psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
psnd
o* (loops_prod (iterated_loops n X) (iterated_loops n Y)
    o* fmap loops (iterated_loops_prod X Y)) ==*
fmap (iterated_loops n.+1) psnd
    refine ((pmap_compose_assoc _ _ _)^* @* _).
X, Y: pType
n: nat
IHn: psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
psnd o* loops_prod (iterated_loops n X) (iterated_loops n Y)
o* fmap loops (iterated_loops_prod X Y) ==* fmap (iterated_loops n.+1) psnd
    refine (pmap_prewhisker _ (psnd_loops_prod _ _) @* _).
X, Y: pType
n: nat
IHn: psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
fmap loops psnd o* fmap loops (iterated_loops_prod X Y) ==*
fmap (iterated_loops n.+1) psnd
    refine ((fmap_comp loops _ _)^* @* _).
X, Y: pType
n: nat
IHn: psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
fmap loops (psnd $o iterated_loops_prod X Y) ==*
fmap (iterated_loops n.+1) psnd
    change (?L ==* _) with (L ==* fmap loops (fmap (iterated_loops n) psnd)).
X, Y: pType
n: nat
IHn: psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
fmap loops (psnd $o iterated_loops_prod X Y) ==*
fmap loops (fmap (iterated_loops n) psnd)
    tapply (fmap2 loops); simpl.
X, Y: pType
n: nat
IHn: psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
    exact IHn.
Defined.

(* A dependent form of loops *)
Definition loopsD {A} : pFam A -> pFam (loops A)
  := fun Pp => Build_pFam (fun q : loops A => transport Pp q (dpoint Pp) = (dpoint Pp)) 1.

Instance istrunc_pfam_loopsD {n} {A} (P : pFam A)
       {H :IsTrunc_pFam n.+1 P}
  : IsTrunc_pFam n (loopsD P).
n: trunc_index
A: pType
P: pFam A
H: IsTrunc_pFam n.+1 P
IsTrunc_pFam n (loopsD P)
Proof.
n: trunc_index
A: pType
P: pFam A
H: IsTrunc_pFam n.+1 P
IsTrunc_pFam n (loopsD P)
  intros a.
n: trunc_index
A: pType
P: pFam A
H: IsTrunc_pFam n.+1 P
a: loops A
IsTrunc n (loopsD P a) pose (H (point A)).
n: trunc_index
A: pType
P: pFam A
H: IsTrunc_pFam n.+1 P
a: loops A
i:= H pt: IsTrunc n.+1 (P pt)
IsTrunc n (loopsD P a) exact _.
Defined.

(* psigma and loops 'commute' *)
Lemma loops_psigma_commute (A : pType) (P : pFam A)
  : loops (psigma P) <~>* psigma (loopsD P).
A: pType
P: pFam A
loops (psigma P) <~>* psigma (loopsD P)
Proof.
A: pType
P: pFam A
loops (psigma P) <~>* psigma (loopsD P)
  snapply Build_pEquiv'.
A: pType
P: pFam A
loops (psigma P) <~> psigma (loopsD P)
A: pType
P: pFam A
?f pt = pt
  1: exact (equiv_path_sigma _ _ _)^-1%equiv.
A: pType
P: pFam A
(equiv_path_sigma P pt pt)^-1%equiv pt = pt
  reflexivity.
Defined.

(* product and loops 'commute' *)
Lemma loops_pproduct_commute `{Funext} (A : Type) (F : A -> pType)
  : loops (pproduct F) <~>* pproduct (loops o F).
H: Funext
A: Type
F: A -> pType
loops (pproduct F) <~>* pproduct (loops o F)
Proof.
H: Funext
A: Type
F: A -> pType
loops (pproduct F) <~>* pproduct (loops o F)
  snapply Build_pEquiv'.
H: Funext
A: Type
F: A -> pType
loops (pproduct F) <~> pproduct (loops o F)
H: Funext
A: Type
F: A -> pType
?f pt = pt
  1: apply equiv_apD10.
H: Funext
A: Type
F: A -> pType
equiv_apD10 (fun x : A => F x) pt pt pt = pt
  reflexivity.
Defined.

(* product and iterated loops commute *)
Lemma iterated_loops_pproduct_commute `{Funext} (A : Type) (F : A -> pType) (n : nat)
  : iterated_loops n (pproduct F) <~>* pproduct (iterated_loops n o F).
H: Funext
A: Type
F: A -> pType
n: nat
iterated_loops n (pproduct F) <~>* pproduct (iterated_loops n o F)
Proof.
H: Funext
A: Type
F: A -> pType
n: nat
iterated_loops n (pproduct F) <~>* pproduct (iterated_loops n o F)
  induction n.
H: Funext
A: Type
F: A -> pType
iterated_loops 0 (pproduct F) <~>*
pproduct (fun x : A => iterated_loops 0 (F x))
H: Funext
A: Type
F: A -> pType
n: nat
IHn: iterated_loops n (pproduct F) <~>*
pproduct (fun x : A => iterated_loops n (F x))
iterated_loops n.+1 (pproduct F) <~>*
pproduct (fun x : A => iterated_loops n.+1 (F x))
  1: reflexivity.
H: Funext
A: Type
F: A -> pType
n: nat
IHn: iterated_loops n (pproduct F) <~>*
pproduct (fun x : A => iterated_loops n (F x))
iterated_loops n.+1 (pproduct F) <~>*
pproduct (fun x : A => iterated_loops n.+1 (F x))
  refine (loops_pproduct_commute _ _ o*E _).
H: Funext
A: Type
F: A -> pType
n: nat
IHn: iterated_loops n (pproduct F) <~>*
pproduct (fun x : A => iterated_loops n (F x))
iterated_loops n.+1 (pproduct F) <~>*
loops (pproduct (fun x : A => nat_iter n loops (F x)))
  tapply (emap loops).
H: Funext
A: Type
F: A -> pType
n: nat
IHn: iterated_loops n (pproduct F) <~>*
pproduct (fun x : A => iterated_loops n (F x))
nat_iter n loops (pproduct F) $<~>
pproduct (fun x : A => nat_iter n loops (F x))
  exact IHn.
Defined.

(* Loops neutralise sigmas when truncated *)
Lemma loops_psigma_trunc (n : nat) (Aa : pType)
  (Pp : pFam Aa) (istrunc_Pp : IsTrunc_pFam (trunc_index_inc minus_two n) Pp)
  : iterated_loops n (psigma Pp) <~>* iterated_loops n Aa.
n: nat
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) n) Pp
iterated_loops n (psigma Pp) <~>* iterated_loops n Aa
Proof.
n: nat
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) n) Pp
iterated_loops n (psigma Pp) <~>* iterated_loops n Aa
  induction n in Aa, Pp, istrunc_Pp |- *.
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) 0) Pp
iterated_loops 0 (psigma Pp) <~>* iterated_loops 0 Aa
n: nat
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) n.+1) Pp
IHn: forall (Aa0 : pType) (Pp0 : pFam Aa0),
IsTrunc_pFam (trunc_index_inc (-2) n) Pp0 ->
iterated_loops n (psigma Pp0) <~>* iterated_loops n Aa0
iterated_loops n.+1 (psigma Pp) <~>* iterated_loops n.+1 Aa
  {
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) 0) Pp
iterated_loops 0 (psigma Pp) <~>* iterated_loops 0 Aa snapply Build_pEquiv'.
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) 0) Pp
iterated_loops 0 (psigma Pp) <~> iterated_loops 0 Aa
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) 0) Pp
?f pt = pt
    1: exact (@equiv_sigma_contr _ _ istrunc_Pp).
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) 0) Pp
equiv_sigma_contr Pp pt = pt
    reflexivity. }
n: nat
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) n.+1) Pp
IHn: forall (Aa0 : pType) (Pp0 : pFam Aa0),
IsTrunc_pFam (trunc_index_inc (-2) n) Pp0 ->
iterated_loops n (psigma Pp0) <~>* iterated_loops n Aa0
iterated_loops n.+1 (psigma Pp) <~>* iterated_loops n.+1 Aa
  refine (pequiv_inverse (unfold_iterated_loops' _ _) o*E _
    o*E unfold_iterated_loops' _ _).
n: nat
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) n.+1) Pp
IHn: forall (Aa0 : pType) (Pp0 : pFam Aa0),
IsTrunc_pFam (trunc_index_inc (-2) n) Pp0 ->
iterated_loops n (psigma Pp0) <~>* iterated_loops n Aa0
iterated_loops n (loops (psigma Pp)) <~>* iterated_loops n (loops Aa)
  refine (IHn _ _ _ o*E _).
n: nat
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) n.+1) Pp
IHn: forall (Aa0 : pType) (Pp0 : pFam Aa0),
IsTrunc_pFam (trunc_index_inc (-2) n) Pp0 ->
iterated_loops n (psigma Pp0) <~>* iterated_loops n Aa0
iterated_loops n (loops (psigma Pp)) <~>*
iterated_loops n (psigma (loopsD Pp))
  tapply (emap (iterated_loops _)).
n: nat
Aa: pType
Pp: pFam Aa
istrunc_Pp: IsTrunc_pFam (trunc_index_inc (-2) n.+1) Pp
IHn: forall (Aa0 : pType) (Pp0 : pFam Aa0),
IsTrunc_pFam (trunc_index_inc (-2) n) Pp0 ->
iterated_loops n (psigma Pp0) <~>* iterated_loops n Aa0
loops (psigma Pp) $<~> psigma (loopsD Pp)
  apply loops_psigma_commute.
Defined.

(* We can convert between loops in a type and loops in [Type] at that type. *)
Definition loops_type `{Univalence} (A : Type@{i})
  : loops [Type@{i}, A] <~>* [A <~> A, equiv_idmap].
H: Univalence
A: Type
loops [Type, A] <~>* [A <~> A, 1%equiv]
Proof.
H: Univalence
A: Type
loops [Type, A] <~>* [A <~> A, 1%equiv]
  apply issig_pequiv'.
H: Univalence
A: Type
{f : loops [Type, A] <~> [A <~> A, 1%equiv] & f pt = pt}
  exists (equiv_equiv_path A A).
H: Univalence
A: Type
equiv_equiv_path A A pt = pt
  reflexivity.
Defined.

(* An iterated version.  Note that the statement with "-1" substituted for [n] is [loops [Type, A] <~>* [A -> A, idmap]], which is not true in general. Compare the previous result. *)
Lemma local_global_looping `{Univalence} (A : Type@{i}) (n : nat)
  : iterated_loops@{j} n.+2 [Type@{i}, A]
    <~>* pproduct (fun a => iterated_loops@{j} n.+1 [A, a]).
H: Univalence
A: Type
n: nat
iterated_loops n.+2 [Type, A] <~>*
pproduct (fun a : IsPointed A => iterated_loops n.+1 [A, a])
Proof.
H: Univalence
A: Type
n: nat
iterated_loops n.+2 [Type, A] <~>*
pproduct (fun a : IsPointed A => iterated_loops n.+1 [A, a])
  induction n.
H: Univalence
A: Type
iterated_loops 2 [Type, A] <~>*
pproduct (fun a : IsPointed A => iterated_loops 1 [A, a])
H: Univalence
A: Type
n: nat
IHn: iterated_loops n.+2 [Type, A] <~>*
pproduct (fun a : IsPointed A => iterated_loops n.+1 [A, a])
iterated_loops n.+3 [Type, A] <~>*
pproduct (fun a : IsPointed A => iterated_loops n.+2 [A, a])
  {
H: Univalence
A: Type
iterated_loops 2 [Type, A] <~>*
pproduct (fun a : IsPointed A => iterated_loops 1 [A, a]) refine (_ o*E emap loops (loops_type A)).
H: Univalence
A: Type
loops [A <~> A, 1%equiv] <~>*
pproduct (fun a : IsPointed A => iterated_loops 1 [A, a])
    apply issig_pequiv'.
H: Univalence
A: Type
{f
: loops [A <~> A, 1%equiv] <~>
  pproduct (fun a : IsPointed A => iterated_loops 1 [A, a])
& f pt = pt}
    exists (equiv_inverse (equiv_path_arrow 1%equiv 1%equiv)
            oE equiv_inverse (equiv_path_equiv 1%equiv 1%equiv)).
H: Univalence
A: Type
((equiv_path_arrow 1 1)^-1 oE (equiv_path_equiv 1 1)^-1) pt = pt
    reflexivity. }
H: Univalence
A: Type
n: nat
IHn: iterated_loops n.+2 [Type, A] <~>*
pproduct (fun a : IsPointed A => iterated_loops n.+1 [A, a])
iterated_loops n.+3 [Type, A] <~>*
pproduct (fun a : IsPointed A => iterated_loops n.+2 [A, a])
  exact (loops_pproduct_commute _ _ o*E emap loops IHn).
Defined.

(* 7.2.7 *)
Theorem equiv_istrunc_istrunc_loops `{Funext} n X
  : IsTrunc n.+2 X <~> forall (x : X), IsTrunc n.+1 (loops [X, x]).
H: Funext
n: trunc_index
X: Type
IsTrunc n.+2 X <~> (forall x : X, IsTrunc n.+1 (loops [X, x]))
Proof.
H: Funext
n: trunc_index
X: Type
IsTrunc n.+2 X <~> (forall x : X, IsTrunc n.+1 (loops [X, x]))
  srapply equiv_iff_hprop.
H: Funext
n: trunc_index
X: Type
(forall x : X, IsTrunc n.+1 (loops [X, x])) -> IsTrunc n.+2 X
  intro tr_loops.
H: Funext
n: trunc_index
X: Type
tr_loops: forall x : X, IsTrunc n.+1 (loops [X, x])
IsTrunc n.+2 X
  apply istrunc_S; intros x y.
H: Funext
n: trunc_index
X: Type
tr_loops: forall x0 : X, IsTrunc n.+1 (loops [X, x0])
x, y: X
IsTrunc n.+1 (x = y)
  apply istrunc_S; intros p.
H: Funext
n: trunc_index
X: Type
tr_loops: forall x0 : X, IsTrunc n.+1 (loops [X, x0])
x, y: X
p: x = y
forall y0 : x = y, IsTrunc n (p = y0)
  destruct p.
H: Funext
n: trunc_index
X: Type
tr_loops: forall x0 : X, IsTrunc n.+1 (loops [X, x0])
x: X
forall y : x = x, IsTrunc n (1 = y)
  napply tr_loops.
Defined.

(* 7.2.9, with [n] here meaning the same as [n-1] there. Note that [n.-1] in the statement is short for [trunc_index_pred (nat_to_trunc_index n)] which is definitionally equal to [(trunc_index_inc minus_two n).+1]. *)
Theorem equiv_istrunc_contr_iterated_loops `{Funext} (n : nat) (A : Type)
  : IsTrunc n.-1 A <~> forall a : A, Contr (iterated_loops n [A, a]).
H: Funext
n: nat
A: Type
IsTrunc n.-1 A <~> (forall a : A, Contr (iterated_loops n [A, a]))
Proof.
H: Funext
n: nat
A: Type
IsTrunc n.-1 A <~> (forall a : A, Contr (iterated_loops n [A, a]))
  induction n in A |- *.
H: Funext
A: Type
IsTrunc 0%nat.-1 A <~> (forall a : A, Contr (iterated_loops 0 [A, a]))
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a : A0, Contr (iterated_loops n [A0, a]))
IsTrunc n.+1%nat.-1 A <~> (forall a : A, Contr (iterated_loops n.+1 [A, a]))
  {
H: Funext
A: Type
IsTrunc 0%nat.-1 A <~> (forall a : A, Contr (iterated_loops 0 [A, a])) cbn.
H: Funext
A: Type
IsHProp A <~> (A -> Contr A) exact equiv_hprop_inhabited_contr. }
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a : A0, Contr (iterated_loops n [A0, a]))
IsTrunc n.+1%nat.-1 A <~> (forall a : A, Contr (iterated_loops n.+1 [A, a]))
  refine (_ oE equiv_istrunc_istrunc_loops n.-2 _).
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a : A0, Contr (iterated_loops n [A0, a]))
(forall x : A, IsTrunc n.-2.+1 (loops [A, x])) <~>
(forall a : A, Contr (iterated_loops n.+1 [A, a]))
  srapply equiv_functor_forall_id.
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a : A0, Contr (iterated_loops n [A0, a]))
forall a : A,
(fun a0 : A => IsTrunc n.-2.+1 (loops [A, a0])) a <~>
(fun a0 : A => Contr (iterated_loops n.+1 [A, a0])) a
  intro a.
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
(fun a0 : A => IsTrunc n.-2.+1 (loops [A, a0])) a <~>
(fun a0 : A => Contr (iterated_loops n.+1 [A, a0])) a
  cbn beta.
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
IsTrunc n.-2.+1 (loops [A, a]) <~> Contr (iterated_loops n.+1 [A, a])
  refine (_ oE IHn (loops [A, a])).
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
(forall a0 : loops [A, a], Contr (iterated_loops n [loops [A, a], a0])) <~>
Contr (iterated_loops n.+1 [A, a])
  refine (equiv_inO_equiv (-2) (unfold_iterated_loops' n [A,a])^-1 oE _).
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
(forall a0 : loops [A, a], Contr (iterated_loops n [loops [A, a], a0])) <~>
In (Tr (-2)) (iterated_loops n (loops [A, a]))
  rapply equiv_iff_hprop.
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
In (Tr (-2)) (iterated_loops n (loops [A, a])) ->
forall a0 : loops [A, a], Contr (iterated_loops n [loops [A, a], a0])
  intros X p.
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
X: In (Tr (-2)) (iterated_loops n (loops [A, a]))
p: loops [A, a]
Contr (iterated_loops n [loops [A, a], p])
  refine (@contr_equiv' _ _ _ X).
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
X: In (Tr (-2)) (iterated_loops n (loops [A, a]))
p: loops [A, a]
iterated_loops n (loops [A, a]) <~> iterated_loops n [loops [A, a], p]
  tapply (emap (iterated_loops _)).
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
X: In (Tr (-2)) (iterated_loops n (loops [A, a]))
p: loops [A, a]
loops [A, a] $<~> [loops [A, a], p]
  srapply Build_pEquiv'.
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
X: In (Tr (-2)) (iterated_loops n (loops [A, a]))
p: loops [A, a]
loops [A, a] <~> [loops [A, a], p]
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
X: In (Tr (-2)) (iterated_loops n (loops [A, a]))
p: loops [A, a]
?f pt = pt
  1: exact (equiv_concat_lr p 1).
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
X: In (Tr (-2)) (iterated_loops n (loops [A, a]))
p: loops [A, a]
equiv_concat_lr p 1 pt = pt
  cbn; unfold ispointed_loops.
H: Funext
n: nat
A: Type
IHn: forall A0 : Type,
IsTrunc n.-1 A0 <~> (forall a0 : A0, Contr (iterated_loops n [A0, a0]))
a: A
X: In (Tr (-2)) (iterated_loops n (loops [A, a]))
p: loops [A, a]
(p @ 1) @ 1 = p
  exact (concat_p1 _ @ concat_p1 _).
Defined.

(** [loops_inv] is a natural transformation. *)
Instance is1natural_loops_inv : Is1Natural loops loops loops_inv.
Is1Natural loops loops (fun A : pType => loops_inv A)
Proof.
Is1Natural loops loops (fun A : pType => loops_inv A)
  snapply Build_Is1Natural.
forall (a a' : pType) (f : a $-> a'),
(fun A : pType => pointed_equiv_fun (loops A) (loops A) (loops_inv A)) a' $o
fmap loops f $==
fmap loops f $o
(fun A : pType => pointed_equiv_fun (loops A) (loops A) (loops_inv A)) a
  intros A B f.
A, B: pType
f: A $-> B
(fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0)) B $o
fmap loops f $==
fmap loops f $o
(fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0)) A
  srapply Build_pHomotopy.
A, B: pType
f: A $-> B
(fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0)) B $o
fmap loops f ==
fmap loops f $o
(fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0)) A
A, B: pType
f: A $-> B
?p pt =
dpoint_eq
  ((fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0))
     B $o
   fmap loops f) @
(dpoint_eq
   (fmap loops f $o
    (fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0))
      A))^
  +
A, B: pType
f: A $-> B
(fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0)) B $o
fmap loops f ==
fmap loops f $o
(fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0)) A intros p.
A, B: pType
f: A $-> B
p: loops A
(loops_inv B $o fmap loops f) p = (fmap loops f $o loops_inv A) p refine (inv_Vp _ _ @ whiskerR _ (point_eq f) @ concat_pp_p _ _ _).
A, B: pType
f: A $-> B
p: loops A
(ap f p @ point_eq f)^ = (point_eq f)^ @ ap f (loops_inv A p)
    exact (inv_pp _ _ @ whiskerL (point_eq f)^ (ap_V f p)^).
  +
A, B: pType
f: A $-> B
((fun p : loops A =>
  (inv_Vp (point_eq f) (ap f p @ point_eq f) @
   whiskerR
     (inv_pp (ap f p) (point_eq f) @ whiskerL (point_eq f)^ (ap_V f p)^)
     (point_eq f)) @
  concat_pp_p (point_eq f)^ (ap f (loops_inv A p)) (point_eq f))
 :
 (fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0)) B $o
 fmap loops f ==
 fmap loops f $o
 (fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0)) A)
  pt =
dpoint_eq
  ((fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0))
     B $o
   fmap loops f) @
(dpoint_eq
   (fmap loops f $o
    (fun A0 : pType => pointed_equiv_fun (loops A0) (loops A0) (loops_inv A0))
      A))^ pointed_reduce.
A: Type
point0: IsPointed A
B: Type
f: A -> B
1 = 1 reflexivity.
Defined.

(** Loops on the pointed type of dependent pointed maps correspond to pointed dependent maps into a family of loops.  We define this in this direction, because the forward map is pointed by reflexivity. *)
Definition equiv_loops_ppforall `{Funext} {A : pType} (B : A -> pType)
  : loops (ppforall x : A, B x) <~>* (ppforall x : A, loops (B x)).
H: Funext
A: pType
B: A -> pType
loops (ppforall x : A, B x) <~>* (ppforall x : A, loops (B x))
Proof.
H: Funext
A: pType
B: A -> pType
loops (ppforall x : A, B x) <~>* (ppforall x : A, loops (B x))
  srapply Build_pEquiv'.
H: Funext
A: pType
B: A -> pType
loops (ppforall x : A, B x) <~> (ppforall x : A, loops (B x))
H: Funext
A: pType
B: A -> pType
?f pt = pt
  1: symmetry; exact (equiv_path_pforall (point_pforall B) (point_pforall B)).
H: Funext
A: pType
B: A -> pType
(equiv_path_pforall (point_pforall B) (point_pforall B))^-1%equiv pt = pt
  reflexivity.
Defined.