From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
Require Import Pointed.Core.

Local Open Scope pointed_scope.

(** ** Trivially pointed maps *)

(** Not infrequently we have a map between two unpointed types and want to consider it as a pointed map that trivially respects some given point in the domain. *)
Definition pmap_from_point {A B : Type} (f : A -> B) (a : A)
  : [A, a] ->* [B, f a]
  := Build_pMap f 1%path.

(** A variant of [pmap_from_point] where the domain is pointed, but the codomain is not. *)
Definition pmap_from_pointed {A : pType} {B : Type} (f : A -> B)
  : A ->* [B, f (point A)]
  := Build_pMap f 1%path.

(** The same, for a dependent pointed map. *)
Definition pforall_from_pointed {A : pType} {B : A -> Type} (f : forall x, B x)
  : pForall A (Build_pFam B (f (point A)))
  := Build_pForall A (Build_pFam B (f (point A))) f 1%path.

(* precomposing the zero map is the zero map *)
Lemma precompose_pconst {A B C : pType} (f : B ->* C)
  : f o* @pconst A B ==* pconst.
A, B, C: pType
f: B ->* C
f o* pconst ==* pconst
Proof.
A, B, C: pType
f: B ->* C
f o* pconst ==* pconst
  srapply Build_pHomotopy.
A, B, C: pType
f: B ->* C
f o* pconst == pconst
A, B, C: pType
f: B ->* C
?p pt = dpoint_eq (f o* pconst) @ (dpoint_eq pconst)^
  1: intro; apply point_eq.
A, B, C: pType
f: B ->* C
((fun _ : A => point_eq f) : f o* pconst == pconst) pt =
dpoint_eq (f o* pconst) @ (dpoint_eq pconst)^
  exact (concat_p1 _ @ concat_1p _)^.
Defined.

(* postcomposing the zero map is the zero map *)
Lemma postcompose_pconst {A B C : pType} (f : A ->* B)
  : pconst o* f ==* @pconst A C.
A, B, C: pType
f: A ->* B
pconst o* f ==* pconst
Proof.
A, B, C: pType
f: A ->* B
pconst o* f ==* pconst
  srapply Build_pHomotopy.
A, B, C: pType
f: A ->* B
pconst o* f == pconst
A, B, C: pType
f: A ->* B
?p pt = dpoint_eq (pconst o* f) @ (dpoint_eq pconst)^
  1: reflexivity.
A, B, C: pType
f: A ->* B
(fun x0 : A => 1) pt = dpoint_eq (pconst o* f) @ (dpoint_eq pconst)^
  exact (concat_p1 _ @ concat_p1 _ @ ap_const _ _)^.
Defined.

Lemma pconst_factor {A B : pType} {f : pUnit ->* B} {g : A ->* pUnit}
  : f o* g ==* pconst.
A, B: pType
f: pUnit ->* B
g: A ->* pUnit
f o* g ==* pconst
Proof.
A, B: pType
f: pUnit ->* B
g: A ->* pUnit
f o* g ==* pconst
  refine (_ @* precompose_pconst f).
A, B: pType
f: pUnit ->* B
g: A ->* pUnit
f o* g ==* f o* pconst
  apply pmap_postwhisker.
A, B: pType
f: pUnit ->* B
g: A ->* pUnit
g ==* pconst
  symmetry.
A, B: pType
f: pUnit ->* B
g: A ->* pUnit
pconst ==* g
  apply pmap_punit_pconst.
Defined.

(* We note that the inverse of [path_pmap] computes definitionally on reflexivity, and hence [path_pmap] itself computes typally so.  *)
Definition equiv_inverse_path_pmap_1 `{Funext} {A B} {f : A ->* B}
  : (equiv_path_pforall f f)^-1%equiv 1%path = reflexivity f
  := 1.

(** If we have a fiberwise pointed map, with a variable as codomain, this is an
  induction principle that allows us to assume it respects all basepoints by
  reflexivity*)
Definition fiberwise_pointed_map_rec `{H0 : Funext} {A : Type} {B : A -> pType}
  (P : forall (C : A -> pType) (g : forall a, B a ->* C a), Type)
  (H : forall (C : A -> Type) (g : forall a, B a -> C a),
     P _ (fun a => pmap_from_pointed (g a)))
  : forall (C : A -> pType) (g : forall a, B a ->* C a), P C g.
H0: Funext
A: Type
B: A -> pType
P: forall C : A -> pType, (forall a : A, B a ->* C a) -> Type
H: forall (C : A -> Type) (g : forall a : A, B a -> C a),
P (fun a : A => [C a, g a pt]) (fun a : A => pmap_from_pointed (g a))
forall (C : A -> pType) (g : forall a : A, B a ->* C a), P C g
Proof.
H0: Funext
A: Type
B: A -> pType
P: forall C : A -> pType, (forall a : A, B a ->* C a) -> Type
H: forall (C : A -> Type) (g : forall a : A, B a -> C a),
P (fun a : A => [C a, g a pt]) (fun a : A => pmap_from_pointed (g a))
forall (C : A -> pType) (g : forall a : A, B a ->* C a), P C g
  equiv_intros (equiv_functor_arrow' (equiv_idmap A) issig_ptype oE
    equiv_sig_coind _ _) C.
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g a pt]) (fun a : A => pmap_from_pointed (g a))
C: {f : A -> Type & forall x : A, f x}
forall
g : forall a : A,
    B a ->*
    (equiv_functor_arrow' 1 issig_ptype
     oE equiv_sig_coind (fun _ : A => Type) (fun _ : A => idmap)) C a,
P
  ((equiv_functor_arrow' 1 issig_ptype
    oE equiv_sig_coind (fun _ : A => Type) (fun _ : A => idmap)) C)
  g
  destruct C as [C c0].
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g a pt]) (fun a : A => pmap_from_pointed (g a))
C: A -> Type
c0: forall x : A, C x
forall
g : forall a : A,
    B a ->*
    (equiv_functor_arrow' 1 issig_ptype
     oE equiv_sig_coind (fun _ : A => Type) (fun _ : A => idmap)) 
      (C; c0) a,
P
  ((equiv_functor_arrow' 1 issig_ptype
    oE equiv_sig_coind (fun _ : A => Type) (fun _ : A => idmap)) 
     (C; c0))
  g
  equiv_intros (@equiv_functor_forall_id _ A _ _
    (fun a => issig_pmap (B a) [C a, c0 a]) oE
    equiv_sig_coind _ _) g.
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g0 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g0 a pt]) (fun a : A => pmap_from_pointed (g0 a))
C: A -> Type
c0: forall x : A, C x
g: {f : forall x : A, B x -> [C x, c0 x] & forall x : A, f x pt = pt}
P
  ((equiv_functor_arrow' 1 issig_ptype
    oE equiv_sig_coind (fun _ : A => Type) (fun _ : A => idmap)) 
     (C; c0))
  ((equiv_functor_forall_id (fun a : A => issig_pmap (B a) [C a, c0 a])
    oE equiv_sig_coind (fun x : A => B x -> [C x, c0 x])
         (fun (x : A) (f : B x -> [C x, c0 x]) => f pt = pt))
     g)
  simpl in *.
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g0 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g0 a pt]) (fun a : A => pmap_from_pointed (g0 a))
C: A -> Type
c0: forall x : A, C x
g: {f : forall x : A, B x -> C x & forall x : A, f x pt = pt}
P
  (functor_forall idmap (fun (_ : A) (u : {X : Type & X}) => [u.1, u.2])
     (sig_coind_uncurried (fun _ : A => idmap) (C; c0)))
  (functor_forall idmap
     (fun (a : A) (u : {f : B a -> C a & f pt = pt}) =>
      {| pointed_fun := u.1; dpoint_eq := u.2 |})
     (sig_coind_uncurried (fun (x : A) (f : B x -> C x) => f pt = pt) g)) destruct g as [g g0].
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g1 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g1 a pt]) (fun a : A => pmap_from_pointed (g1 a))
C: A -> Type
c0: forall x : A, C x
g: forall x : A, B x -> C x
g0: forall x : A, g x pt = pt
P
  (functor_forall idmap (fun (_ : A) (u : {X : Type & X}) => [u.1, u.2])
     (sig_coind_uncurried (fun _ : A => idmap) (C; c0)))
  (functor_forall idmap
     (fun (a : A) (u : {f : B a -> C a & f pt = pt}) =>
      {| pointed_fun := u.1; dpoint_eq := u.2 |})
     (sig_coind_uncurried (fun (x : A) (f : B x -> C x) => f pt = pt) (g; g0)))
  unfold point in g0.
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g1 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g1 a pt]) (fun a : A => pmap_from_pointed (g1 a))
C: A -> Type
c0: forall x : A, C x
g: forall x : A, B x -> C x
g0: forall x : A, g x (ispointed_type (B x)) = c0 x
P
  (functor_forall idmap (fun (_ : A) (u : {X : Type & X}) => [u.1, u.2])
     (sig_coind_uncurried (fun _ : A => idmap) (C; c0)))
  (functor_forall idmap
     (fun (a : A) (u : {f : B a -> C a & f pt = pt}) =>
      {| pointed_fun := u.1; dpoint_eq := u.2 |})
     (sig_coind_uncurried (fun (x : A) (f : B x -> C x) => f pt = pt) (g; g0))) unfold functor_forall, sig_coind_uncurried.
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g1 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g1 a pt]) (fun a : A => pmap_from_pointed (g1 a))
C: A -> Type
c0: forall x : A, C x
g: forall x : A, B x -> C x
g0: forall x : A, g x (ispointed_type (B x)) = c0 x
P (fun b : A => [((C; c0).1 b; (C; c0).2 b).1, ((C; c0).1 b; (C; c0).2 b).2])
  (fun b : A =>
   {|
     pointed_fun := ((g; g0).1 b; (g; g0).2 b).1;
     dpoint_eq := ((g; g0).1 b; (g; g0).2 b).2
   |}) simpl.
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g1 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g1 a pt]) (fun a : A => pmap_from_pointed (g1 a))
C: A -> Type
c0: forall x : A, C x
g: forall x : A, B x -> C x
g0: forall x : A, g x (ispointed_type (B x)) = c0 x
P (fun b : A => [C b, c0 b])
  (fun b : A => {| pointed_fun := g b; dpoint_eq := g0 b |})
  (* now we need to apply path induction on the homotopy g0 *)
  pose (path_forall _ c0 g0).
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g1 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g1 a pt]) (fun a : A => pmap_from_pointed (g1 a))
C: A -> Type
c0: forall x : A, C x
g: forall x : A, B x -> C x
g0: forall x : A, g x (ispointed_type (B x)) = c0 x
p:= path_forall (fun x : A => g x (ispointed_type (B x))) c0 g0: (fun x : A => g x (ispointed_type (B x))) = c0
P (fun b : A => [C b, c0 b])
  (fun b : A => {| pointed_fun := g b; dpoint_eq := g0 b |})
  assert (p = path_forall (fun x : A => g x (ispointed_type (B x))) c0 g0).
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g1 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g1 a pt]) (fun a : A => pmap_from_pointed (g1 a))
C: A -> Type
c0: forall x : A, C x
g: forall x : A, B x -> C x
g0: forall x : A, g x (ispointed_type (B x)) = c0 x
p:= path_forall (fun x : A => g x (ispointed_type (B x))) c0 g0: (fun x : A => g x (ispointed_type (B x))) = c0
p = path_forall (fun x : A => g x (ispointed_type (B x))) c0 g0
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g1 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g1 a pt]) (fun a : A => pmap_from_pointed (g1 a))
C: A -> Type
c0: forall x : A, C x
g: forall x : A, B x -> C x
g0: forall x : A, g x (ispointed_type (B x)) = c0 x
p:= path_forall (fun x : A => g x (ispointed_type (B x))) c0 g0: (fun x : A => g x (ispointed_type (B x))) = c0
X: p = path_forall (fun x : A => g x (ispointed_type (B x))) c0 g0
P (fun b : A => [C b, c0 b])
  (fun b : A => {| pointed_fun := g b; dpoint_eq := g0 b |})
  1: reflexivity.
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g1 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g1 a pt]) (fun a : A => pmap_from_pointed (g1 a))
C: A -> Type
c0: forall x : A, C x
g: forall x : A, B x -> C x
g0: forall x : A, g x (ispointed_type (B x)) = c0 x
p:= path_forall (fun x : A => g x (ispointed_type (B x))) c0 g0: (fun x : A => g x (ispointed_type (B x))) = c0
X: p = path_forall (fun x : A => g x (ispointed_type (B x))) c0 g0
P (fun b : A => [C b, c0 b])
  (fun b : A => {| pointed_fun := g b; dpoint_eq := g0 b |})
  induction p.
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g1 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g1 a pt]) (fun a : A => pmap_from_pointed (g1 a))
C: A -> Type
g: forall x : A, B x -> C x
g0: forall x : A, g x (ispointed_type (B x)) = g x (ispointed_type (B x))
X: 1 =
path_forall (fun x : A => g x (ispointed_type (B x)))
  (fun x : A => g x (ispointed_type (B x))) g0
P (fun b : A => [C b, g b (ispointed_type (B b))])
  (fun b : A => {| pointed_fun := g b; dpoint_eq := g0 b |})
  apply moveR_equiv_V in X.
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g1 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g1 a pt]) (fun a : A => pmap_from_pointed (g1 a))
C: A -> Type
g: forall x : A, B x -> C x
g0: forall x : A, g x (ispointed_type (B x)) = g x (ispointed_type (B x))
X: (path_forall (fun x : A => g x (ispointed_type (B x)))
   (fun x : A => g x (ispointed_type (B x))))^-1
  1 =
g0
P (fun b : A => [C b, g b (ispointed_type (B b))])
  (fun b : A => {| pointed_fun := g b; dpoint_eq := g0 b |}) induction X.
H0: Funext
A: Type
B: A -> pType
P: forall C0 : A -> pType, (forall a : A, B a ->* C0 a) -> Type
H: forall (C0 : A -> Type) (g0 : forall a : A, B a -> C0 a),
P (fun a : A => [C0 a, g0 a pt]) (fun a : A => pmap_from_pointed (g0 a))
C: A -> Type
g: forall x : A, B x -> C x
P (fun b : A => [C b, g b (ispointed_type (B b))])
  (fun b : A =>
   {|
     pointed_fun := g b;
     dpoint_eq :=
       (path_forall (fun x : A => g x (ispointed_type (B x)))
          (fun x : A => g x (ispointed_type (B x))))^-1
         1 b
   |})
  apply H.
Defined.

(** A alternative constructor to build a [pHomotopy] between maps into [pForall] *)
Definition Build_pHomotopy_pForall `{Funext} {A B : pType} {C : B -> pType}
  {f g : A ->* ppforall b, C b} (p : forall a, f a ==* g a)
  (q : p (point A) ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*)
  : f ==* g.
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
f ==* g
Proof.
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
f ==* g
  snapply Build_pHomotopy.
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
f == g
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
?p pt = dpoint_eq f @ (dpoint_eq g)^
  1: intro a; exact (path_pforall (p a)).
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
((fun a : A => path_pforall (p a)) : f == g) pt =
dpoint_eq f @ (dpoint_eq g)^
  hnf; rapply moveR_equiv_M'.
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
p pt = (equiv_path_pforall (f pt) (g pt))^-1 (dpoint_eq f @ (dpoint_eq g)^)
  refine (_^ @ ap10 _ _).
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
?Goal0 (dpoint_eq f @ (dpoint_eq g)^) = p pt
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
?Goal0 = (equiv_path_pforall (f pt) (g pt))^-1
  2: exact path_equiv_path_pforall_phomotopy_path.
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
phomotopy_path (dpoint_eq f @ (dpoint_eq g)^) = p pt
  apply path_pforall.
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
phomotopy_path (dpoint_eq f @ (dpoint_eq g)^) ==* p pt
  refine (phomotopy_path_pp _ _ @* _ @* q^*).
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
phomotopy_path (dpoint_eq f) @* phomotopy_path (dpoint_eq g)^ ==*
phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
  apply phomotopy_prewhisker.
H: Funext
A, B: pType
C: B -> pType
f, g: A ->* (ppforall b : B, C b)
p: forall a : A, f a ==* g a
q: p pt ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*
phomotopy_path (dpoint_eq g)^ ==* (phomotopy_path (point_eq g))^*
  apply phomotopy_path_V.
Defined.

(** Operations on dependent pointed maps *)

(* functorial action of [pForall A B] in [B] *)
Definition functor_pforall_right {A : pType} {B B' : pFam A}
  (f : forall a, B a -> B' a)
  (p : f (point A) (dpoint B) = dpoint B') (g : pForall A B)
    : pForall A B' :=
  Build_pForall A B' (fun a => f a (g a)) (ap (f (point A)) (dpoint_eq g) @ p).

Definition equiv_functor_pforall_id `{Funext} {A : pType} {B B' : pFam A}
  (f : forall a, B a <~> B' a) (p : f (point A) (dpoint B) = dpoint B')
  : pForall A B <~> pForall A B'.
H: Funext
A: pType
B, B': pFam A
f: forall a : A, B a <~> B' a
p: f pt (dpoint B) = dpoint B'
pForall A B <~> pForall A B'
Proof.
H: Funext
A: pType
B, B': pFam A
f: forall a : A, B a <~> B' a
p: f pt (dpoint B) = dpoint B'
pForall A B <~> pForall A B'
  refine (issig_pforall _ _ oE _ oE (issig_pforall _ _)^-1).
H: Funext
A: pType
B, B': pFam A
f: forall a : A, B a <~> B' a
p: f pt (dpoint B) = dpoint B'
{f0 : forall x : A, B x & f0 pt = dpoint B} <~>
{f0 : forall x : A, B' x & f0 pt = dpoint B'}
  srapply equiv_functor_sigma'.
H: Funext
A: pType
B, B': pFam A
f: forall a : A, B a <~> B' a
p: f pt (dpoint B) = dpoint B'
(forall x : A, B x) <~> (forall x : A, B' x)
H: Funext
A: pType
B, B': pFam A
f: forall a : A, B a <~> B' a
p: f pt (dpoint B) = dpoint B'
forall a : forall x : A, B x,
(fun f0 : forall x : A, B x => f0 pt = dpoint B) a <~>
(fun f0 : forall x : A, B' x => f0 pt = dpoint B') (?f a)
  1: exact (equiv_functor_forall_id f).
H: Funext
A: pType
B, B': pFam A
f: forall a : A, B a <~> B' a
p: f pt (dpoint B) = dpoint B'
forall a : forall x : A, B x,
(fun f0 : forall x : A, B x => f0 pt = dpoint B) a <~>
(fun f0 : forall x : A, B' x => f0 pt = dpoint B')
  (equiv_functor_forall_id f a)
  intro s; cbn.
H: Funext
A: pType
B, B': pFam A
f: forall a : A, B a <~> B' a
p: f pt (dpoint B) = dpoint B'
s: forall x : A, B x
s pt = dpoint B <~> functor_forall idmap (fun a : A => f a) s pt = dpoint B'
  refine (equiv_concat_r p _ oE _).
H: Funext
A: pType
B, B': pFam A
f: forall a : A, B a <~> B' a
p: f pt (dpoint B) = dpoint B'
s: forall x : A, B x
s pt = dpoint B <~>
functor_forall idmap (fun a : A => f a) s pt = f pt (dpoint B)
  apply (equiv_ap' (f (point A))).
Defined.

Definition functor2_pforall_right {A : pType} {B C : pFam A}
  {g g' : forall (a : A), B a -> C a}
  {g₀ : g (point A) (dpoint B) = dpoint C}
  {g₀' : g' (point A) (dpoint B) = dpoint C} {f f' : pForall A B}
  (p : forall a, g a == g' a) (q : f ==* f')
  (r : p (point A) (dpoint B) @ g₀' = g₀)
  : functor_pforall_right g g₀ f ==* functor_pforall_right g' g₀' f'.
A: pType
B, C: pFam A
g, g': forall a : A, B a -> C a
g₀: g pt (dpoint B) = dpoint C
g₀': g' pt (dpoint B) = dpoint C
f, f': pForall A B
p: forall a : A, g a == g' a
q: f ==* f'
r: p pt (dpoint B) @ g₀' = g₀
functor_pforall_right g g₀ f ==* functor_pforall_right g' g₀' f'
Proof.
A: pType
B, C: pFam A
g, g': forall a : A, B a -> C a
g₀: g pt (dpoint B) = dpoint C
g₀': g' pt (dpoint B) = dpoint C
f, f': pForall A B
p: forall a : A, g a == g' a
q: f ==* f'
r: p pt (dpoint B) @ g₀' = g₀
functor_pforall_right g g₀ f ==* functor_pforall_right g' g₀' f'
  srapply Build_pHomotopy.
A: pType
B, C: pFam A
g, g': forall a : A, B a -> C a
g₀: g pt (dpoint B) = dpoint C
g₀': g' pt (dpoint B) = dpoint C
f, f': pForall A B
p: forall a : A, g a == g' a
q: f ==* f'
r: p pt (dpoint B) @ g₀' = g₀
functor_pforall_right g g₀ f == functor_pforall_right g' g₀' f'
A: pType
B, C: pFam A
g, g': forall a : A, B a -> C a
g₀: g pt (dpoint B) = dpoint C
g₀': g' pt (dpoint B) = dpoint C
f, f': pForall A B
p: forall a : A, g a == g' a
q: f ==* f'
r: p pt (dpoint B) @ g₀' = g₀
?p pt =
dpoint_eq (functor_pforall_right g g₀ f) @
(dpoint_eq (functor_pforall_right g' g₀' f'))^
  1: {
A: pType
B, C: pFam A
g, g': forall a : A, B a -> C a
g₀: g pt (dpoint B) = dpoint C
g₀': g' pt (dpoint B) = dpoint C
f, f': pForall A B
p: forall a : A, g a == g' a
q: f ==* f'
r: p pt (dpoint B) @ g₀' = g₀
functor_pforall_right g g₀ f == functor_pforall_right g' g₀' f' intro a.
A: pType
B, C: pFam A
g, g': forall a0 : A, B a0 -> C a0
g₀: g pt (dpoint B) = dpoint C
g₀': g' pt (dpoint B) = dpoint C
f, f': pForall A B
p: forall a0 : A, g a0 == g' a0
q: f ==* f'
r: p pt (dpoint B) @ g₀' = g₀
a: A
functor_pforall_right g g₀ f a = functor_pforall_right g' g₀' f' a exact (p a (f a) @ ap (g' a) (q a)). }
A: pType
B, C: pFam A
g, g': forall a : A, B a -> C a
g₀: g pt (dpoint B) = dpoint C
g₀': g' pt (dpoint B) = dpoint C
f, f': pForall A B
p: forall a : A, g a == g' a
q: f ==* f'
r: p pt (dpoint B) @ g₀' = g₀
((fun a : A => p a (f a) @ ap (g' a) (q a))
 :
 functor_pforall_right g g₀ f == functor_pforall_right g' g₀' f') pt =
dpoint_eq (functor_pforall_right g g₀ f) @
(dpoint_eq (functor_pforall_right g' g₀' f'))^
  pointed_reduce_rewrite.
A: Type
point: IsPointed A
B, C: A -> Type
g, g': forall a : A, B a -> C a
f', f: forall x : A, B x
p: forall a : A, g a == g' a
q: forall x : A, f x = f' x
p point (f point) @ ap (g' point) (q point) =
ap (g point) (q point) @ p point (f' point) symmetry.
A: Type
point: IsPointed A
B, C: A -> Type
g, g': forall a : A, B a -> C a
f', f: forall x : A, B x
p: forall a : A, g a == g' a
q: forall x : A, f x = f' x
ap (g point) (q point) @ p point (f' point) =
p point (f point) @ ap (g' point) (q point) apply concat_Ap.
Defined.

Definition functor2_pforall_right_refl {A : pType} {B C : pFam A}
  (g : forall a, B a -> C a) (g₀ : g (point A) (dpoint B) = dpoint C)
  (f : pForall A B)
  : functor2_pforall_right (fun a => reflexivity (g a)) (phomotopy_reflexive f)
      (concat_1p _)
    ==* phomotopy_reflexive (functor_pforall_right g g₀ f).
A: pType
B, C: pFam A
g: forall a : A, B a -> C a
g₀: g pt (dpoint B) = dpoint C
f: pForall A B
functor2_pforall_right (fun a : A => reflexivity (g a))
  (phomotopy_reflexive f) (concat_1p g₀) ==*
phomotopy_reflexive (functor_pforall_right g g₀ f)
Proof.
A: pType
B, C: pFam A
g: forall a : A, B a -> C a
g₀: g pt (dpoint B) = dpoint C
f: pForall A B
functor2_pforall_right (fun a : A => reflexivity (g a))
  (phomotopy_reflexive f) (concat_1p g₀) ==*
phomotopy_reflexive (functor_pforall_right g g₀ f)
  pointed_reduce.
A: Type
point: IsPointed A
B, C: A -> Type
g: forall a : A, B a -> C a
f: forall x : A, B x
functor2_pforall_right (fun (a : A) (x0 : B a) => 1)
  (phomotopy_reflexive {| pointed_fun := f; dpoint_eq := 1 |}) 1 ==*
phomotopy_reflexive
  (functor_pforall_right g 1 {| pointed_fun := f; dpoint_eq := 1 |}) reflexivity.
Defined.

(* functorial action of [pForall A (pointed_fam B)] in [B]. *)
Definition pmap_compose_ppforall {A : pType} {B B' : A -> pType}
  (g : forall a, B a ->* B' a) (f : ppforall a, B a) : ppforall a, B' a.
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
f: ppforall a : A, B a
ppforall a : A, B' a
Proof.
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
f: ppforall a : A, B a
ppforall a : A, B' a
  simple refine (functor_pforall_right _ _ f).
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
f: ppforall a : A, B a
forall a : A,
pointed_fam (fun a0 : A => B a0) a -> pointed_fam (fun a0 : A => B' a0) a
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
f: ppforall a : A, B a
?f pt (dpoint (pointed_fam (fun a : A => B a))) =
dpoint (pointed_fam (fun a : A => B' a))
  +
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
f: ppforall a : A, B a
forall a : A,
pointed_fam (fun a0 : A => B a0) a -> pointed_fam (fun a0 : A => B' a0) a exact g.
  +
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
f: ppforall a : A, B a
(fun a : A => pointed_fun (g a)) pt (dpoint (pointed_fam (fun a : A => B a))) =
dpoint (pointed_fam (fun a : A => B' a)) exact (point_eq (g (point A))).
Defined.

Definition pmap_compose_ppforall_point {A : pType} {B B' : A -> pType}
  (g : forall a, B a ->* B' a)
  : pmap_compose_ppforall g (point_pforall B) ==* point_pforall B'.
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
pmap_compose_ppforall g (point_pforall B) ==* point_pforall B'
Proof.
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
pmap_compose_ppforall g (point_pforall B) ==* point_pforall B'
  srapply Build_pHomotopy.
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
pmap_compose_ppforall g (point_pforall B) == point_pforall B'
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
?p pt =
dpoint_eq (pmap_compose_ppforall g (point_pforall B)) @
(dpoint_eq (point_pforall B'))^
  +
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
pmap_compose_ppforall g (point_pforall B) == point_pforall B' intro x.
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
x: A
pmap_compose_ppforall g (point_pforall B) x = point_pforall B' x exact (point_eq (g x)).
  +
A: pType
B, B': A -> pType
g: forall a : A, B a ->* B' a
((fun x : A => point_eq (g x))
 :
 pmap_compose_ppforall g (point_pforall B) == point_pforall B') pt =
dpoint_eq (pmap_compose_ppforall g (point_pforall B)) @
(dpoint_eq (point_pforall B'))^ exact (concat_p1 _ @ concat_1p _)^.
Defined.

Definition pmap_compose_ppforall_compose {A : pType} {P Q R : A -> pType}
  (h : forall (a : A), Q a ->* R a) (g : forall (a : A), P a ->* Q a)
  (f : ppforall a, P a)
  : pmap_compose_ppforall (fun a => h a o* g a) f ==* pmap_compose_ppforall h (pmap_compose_ppforall g f).
A: pType
P, Q, R: A -> pType
h: forall a : A, Q a ->* R a
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
pmap_compose_ppforall (fun a : A => h a o* g a) f ==*
pmap_compose_ppforall h (pmap_compose_ppforall g f)
Proof.
A: pType
P, Q, R: A -> pType
h: forall a : A, Q a ->* R a
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
pmap_compose_ppforall (fun a : A => h a o* g a) f ==*
pmap_compose_ppforall h (pmap_compose_ppforall g f)
  srapply Build_pHomotopy.
A: pType
P, Q, R: A -> pType
h: forall a : A, Q a ->* R a
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
pmap_compose_ppforall (fun a : A => h a o* g a) f ==
pmap_compose_ppforall h (pmap_compose_ppforall g f)
A: pType
P, Q, R: A -> pType
h: forall a : A, Q a ->* R a
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
?p pt =
dpoint_eq (pmap_compose_ppforall (fun a : A => h a o* g a) f) @
(dpoint_eq (pmap_compose_ppforall h (pmap_compose_ppforall g f)))^
  +
A: pType
P, Q, R: A -> pType
h: forall a : A, Q a ->* R a
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
pmap_compose_ppforall (fun a : A => h a o* g a) f ==
pmap_compose_ppforall h (pmap_compose_ppforall g f) reflexivity.
  +
A: pType
P, Q, R: A -> pType
h: forall a : A, Q a ->* R a
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
(fun x0 : A => 1) pt =
dpoint_eq (pmap_compose_ppforall (fun a : A => h a o* g a) f) @
(dpoint_eq (pmap_compose_ppforall h (pmap_compose_ppforall g f)))^ simpl.
A: pType
P, Q, R: A -> pType
h: forall a : A, Q a ->* R a
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
1 =
(ap (fun x : P pt => h pt (g pt x)) (dpoint_eq f) @
 (ap (h pt) (point_eq (g pt)) @ point_eq (h pt))) @
(ap (h pt) (ap (g pt) (dpoint_eq f) @ point_eq (g pt)) @ point_eq (h pt))^ refine ((whiskerL _ (inverse2 _)) @ concat_pV _)^.
A: pType
P, Q, R: A -> pType
h: forall a : A, Q a ->* R a
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
ap (h pt) (ap (g pt) (dpoint_eq f) @ point_eq (g pt)) @ point_eq (h pt) =
ap (fun x : P pt => h pt (g pt x)) (dpoint_eq f) @
(ap (h pt) (point_eq (g pt)) @ point_eq (h pt))
    refine (whiskerR _ _ @ concat_pp_p _ _ _).
A: pType
P, Q, R: A -> pType
h: forall a : A, Q a ->* R a
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
ap (h pt) (ap (g pt) (dpoint_eq f) @ point_eq (g pt)) =
ap (fun x : P pt => h pt (g pt x)) (dpoint_eq f) @
ap (h pt) (point_eq (g pt))
    refine (ap_pp _ _ _ @ whiskerR (ap_compose _ _ _)^ _).
Defined.

Definition pmap_compose_ppforall2 {A : pType} {P Q : A -> pType} {g g' : forall (a : A), P a ->* Q a}
  {f f' : ppforall (a : A), P a} (p : forall a, g a ==* g' a) (q : f ==* f')
  : pmap_compose_ppforall g f ==* pmap_compose_ppforall g' f'.
A: pType
P, Q: A -> pType
g, g': forall a : A, P a ->* Q a
f, f': ppforall a : A, P a
p: forall a : A, g a ==* g' a
q: f ==* f'
pmap_compose_ppforall g f ==* pmap_compose_ppforall g' f'
Proof.
A: pType
P, Q: A -> pType
g, g': forall a : A, P a ->* Q a
f, f': ppforall a : A, P a
p: forall a : A, g a ==* g' a
q: f ==* f'
pmap_compose_ppforall g f ==* pmap_compose_ppforall g' f'
  srapply functor2_pforall_right.
A: pType
P, Q: A -> pType
g, g': forall a : A, P a ->* Q a
f, f': ppforall a : A, P a
p: forall a : A, g a ==* g' a
q: f ==* f'
forall a : A,
(fun a0 : A => pointed_fun (g a0)) a == (fun a0 : A => pointed_fun (g' a0)) a
A: pType
P, Q: A -> pType
g, g': forall a : A, P a ->* Q a
f, f': ppforall a : A, P a
p: forall a : A, g a ==* g' a
q: f ==* f'
f ==* f'
A: pType
P, Q: A -> pType
g, g': forall a : A, P a ->* Q a
f, f': ppforall a : A, P a
p: forall a : A, g a ==* g' a
q: f ==* f'
?p pt (dpoint (pointed_fam (fun a : A => P a))) @ point_eq (g' pt) =
point_eq (g pt)
  +
A: pType
P, Q: A -> pType
g, g': forall a : A, P a ->* Q a
f, f': ppforall a : A, P a
p: forall a : A, g a ==* g' a
q: f ==* f'
forall a : A,
(fun a0 : A => pointed_fun (g a0)) a == (fun a0 : A => pointed_fun (g' a0)) a exact p.
  +
A: pType
P, Q: A -> pType
g, g': forall a : A, P a ->* Q a
f, f': ppforall a : A, P a
p: forall a : A, g a ==* g' a
q: f ==* f'
f ==* f' exact q.
  +
A: pType
P, Q: A -> pType
g, g': forall a : A, P a ->* Q a
f, f': ppforall a : A, P a
p: forall a : A, g a ==* g' a
q: f ==* f'
(fun a : A => pointed_htpy (p a)) pt
  (dpoint (pointed_fam (fun a : A => P a))) @
point_eq (g' pt) = point_eq (g pt) exact (point_htpy (p (point A))).
Defined.

Definition pmap_compose_ppforall2_left {A : pType} {P Q : A -> pType} {g g' : forall (a : A), P a ->* Q a}
  (f : ppforall (a : A), P a) (p : forall a, g a ==* g' a)
  : pmap_compose_ppforall g f ==* pmap_compose_ppforall g' f :=
  pmap_compose_ppforall2 p (phomotopy_reflexive f).

Definition pmap_compose_ppforall2_right {A : pType} {P Q : A -> pType} (g : forall (a : A), P a ->* Q a)
  {f f' : ppforall (a : A), P a} (q : f ==* f')
  : pmap_compose_ppforall g f ==* pmap_compose_ppforall g f' :=
  pmap_compose_ppforall2 (fun a => phomotopy_reflexive (g a)) q.

Definition pmap_compose_ppforall2_refl `{Funext} {A : pType} {P Q : A -> pType}
  (g : forall (a : A), P a ->* Q a) (f : ppforall (a : A), P a)
  : pmap_compose_ppforall2 (fun a => phomotopy_reflexive (g a)) (phomotopy_reflexive f)
    ==* phomotopy_reflexive _.
H: Funext
A: pType
P, Q: A -> pType
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
pmap_compose_ppforall2 (fun a : A => phomotopy_reflexive (g a))
  (phomotopy_reflexive f) ==*
phomotopy_reflexive (pmap_compose_ppforall g f)
Proof.
H: Funext
A: pType
P, Q: A -> pType
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
pmap_compose_ppforall2 (fun a : A => phomotopy_reflexive (g a))
  (phomotopy_reflexive f) ==*
phomotopy_reflexive (pmap_compose_ppforall g f)
  unfold pmap_compose_ppforall2.
H: Funext
A: pType
P, Q: A -> pType
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
functor2_pforall_right (fun a : A => phomotopy_reflexive (g a))
  (phomotopy_reflexive f) (point_htpy (phomotopy_reflexive (g pt))) ==*
phomotopy_reflexive (pmap_compose_ppforall g f)
  revert Q g.
H: Funext
A: pType
P: A -> pType
f: ppforall a : A, P a
forall (Q : A -> pType) (g : forall a : A, P a ->* Q a),
functor2_pforall_right (fun a : A => phomotopy_reflexive (g a))
  (phomotopy_reflexive f) (point_htpy (phomotopy_reflexive (g pt))) ==*
phomotopy_reflexive (pmap_compose_ppforall g f) refine (fiberwise_pointed_map_rec _ _).
H: Funext
A: pType
P: A -> pType
f: ppforall a : A, P a
forall (C : A -> Type) (g : forall a : A, P a -> C a),
functor2_pforall_right
  (fun a : A => phomotopy_reflexive (pmap_from_pointed (g a)))
  (phomotopy_reflexive f)
  (point_htpy (phomotopy_reflexive (pmap_from_pointed (g pt)))) ==*
phomotopy_reflexive
  (pmap_compose_ppforall (fun a : A => pmap_from_pointed (g a)) f) intros Q g.
H: Funext
A: pType
P: A -> pType
f: ppforall a : A, P a
Q: A -> Type
g: forall a : A, P a -> Q a
functor2_pforall_right
  (fun a : A => phomotopy_reflexive (pmap_from_pointed (g a)))
  (phomotopy_reflexive f)
  (point_htpy (phomotopy_reflexive (pmap_from_pointed (g pt)))) ==*
phomotopy_reflexive
  (pmap_compose_ppforall (fun a : A => pmap_from_pointed (g a)) f)
  srapply functor2_pforall_right_refl.
Defined.

Definition pmap_compose_ppforall_pid_left {A : pType} {P : A -> pType}
  (f : ppforall (a : A), P a) : pmap_compose_ppforall (fun a => pmap_idmap) f ==* f.
A: pType
P: A -> pType
f: ppforall a : A, P a
pmap_compose_ppforall (fun a : A => pmap_idmap) f ==* f
Proof.
A: pType
P: A -> pType
f: ppforall a : A, P a
pmap_compose_ppforall (fun a : A => pmap_idmap) f ==* f
  srapply Build_pHomotopy.
A: pType
P: A -> pType
f: ppforall a : A, P a
pmap_compose_ppforall (fun a : A => pmap_idmap) f == f
A: pType
P: A -> pType
f: ppforall a : A, P a
?p pt =
dpoint_eq (pmap_compose_ppforall (fun a : A => pmap_idmap) f) @
(dpoint_eq f)^
  +
A: pType
P: A -> pType
f: ppforall a : A, P a
pmap_compose_ppforall (fun a : A => pmap_idmap) f == f reflexivity.
  +
A: pType
P: A -> pType
f: ppforall a : A, P a
(fun x0 : A => 1) pt =
dpoint_eq (pmap_compose_ppforall (fun a : A => pmap_idmap) f) @
(dpoint_eq f)^ symmetry.
A: pType
P: A -> pType
f: ppforall a : A, P a
dpoint_eq (pmap_compose_ppforall (fun a : A => pmap_idmap) f) @
(dpoint_eq f)^ = (fun x0 : A => 1) pt exact (whiskerR (concat_p1 _ @ ap_idmap _) _ @ concat_pV _).
Defined.

Definition pmap_compose_ppforall_path_pforall `{Funext} {A : pType} {P Q : A -> pType}
  (g : forall a, P a ->* Q a) {f f' : ppforall a, P a} (p : f ==* f') :
  ap (pmap_compose_ppforall g) (path_pforall p) =
  path_pforall (pmap_compose_ppforall2_right g p).
H: Funext
A: pType
P, Q: A -> pType
g: forall a : A, P a ->* Q a
f, f': ppforall a : A, P a
p: f ==* f'
ap (pmap_compose_ppforall g) (path_pforall p) =
path_pforall (pmap_compose_ppforall2_right g p)
Proof.
H: Funext
A: pType
P, Q: A -> pType
g: forall a : A, P a ->* Q a
f, f': ppforall a : A, P a
p: f ==* f'
ap (pmap_compose_ppforall g) (path_pforall p) =
path_pforall (pmap_compose_ppforall2_right g p)
  revert f' p.
H: Funext
A: pType
P, Q: A -> pType
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
forall (f' : ppforall a : A, P a) (p : f ==* f'),
ap (pmap_compose_ppforall g) (path_pforall p) =
path_pforall (pmap_compose_ppforall2_right g p) refine (phomotopy_ind _ _).
H: Funext
A: pType
P, Q: A -> pType
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
ap (pmap_compose_ppforall g) (path_pforall (reflexivity f)) =
path_pforall (pmap_compose_ppforall2_right g (reflexivity f))
  refine (ap _ path_pforall_1 @ path_pforall_1^ @ ap _ _^).
H: Funext
A: pType
P, Q: A -> pType
g: forall a : A, P a ->* Q a
f: ppforall a : A, P a
pmap_compose_ppforall2_right g (reflexivity f) =
reflexivity (pmap_compose_ppforall g f)
  exact (path_pforall (pmap_compose_ppforall2_refl _ _)).
Defined.