(* -*- mode: coq; mode: visual-line -*- *)
(** * Theorems about Sigma-types (dependent sums) *)

Require Import HoTT.Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Arrow Types.Paths.
Local Open Scope path_scope.


Generalizable Variables X A B C f g n.

(** In homotopy type theory, We think of elements of [Type] as spaces, homotopy types, or weak omega-groupoids. A type family [P : A -> Type] corresponds to a fibration whose base is [A] and whose fiber over [x] is [P x].

From such a [P] we can build a total space over the base space [A] so that the fiber over [x : A] is [P x]. This is just Coq's dependent sum construction, written as [sig P] or [{x : A & P x}]. The elements of [{x : A & P x}] are pairs, written [exist P x y] in Coq, where [x : A] and [y : P x].  In [Common.v] we defined the notation [(x;y)] to mean [exist _ x y].

The base and fiber components of a point in the total space are extracted with the two projections [pr1] and [pr2]. *)

(** ** Unpacking *)

(** Sometimes we would like to prove [Q u] where [u : {x : A & P x}] by writing [u] as a pair [(pr1 u ; pr2 u)]. This is accomplished by [sig_unpack]. We want tight control over the proof, so we just write it down even though is looks a bit scary. *)

Definition unpack_sigma `{P : A -> Type} (Q : sig P -> Type) (u : sig P)
: Q (u.1; u.2) -> Q u
  := idmap.

Arguments unpack_sigma / .

(** ** Eta conversion *)

Definition eta_sigma `{P : A -> Type} (u : sig P)
  : (u.1; u.2) = u
  := 1.

Arguments eta_sigma / .

Definition eta2_sigma `{P : forall (a : A) (b : B a), Type}
           (u : sig (fun a => sig (P a)))
  : (u.1; u.2.1; u.2.2) = u
  := 1.

Arguments eta2_sigma / .

Definition eta3_sigma `{P : forall (a : A) (b : B a) (c : C a b), Type}
           (u : sig (fun a => sig (fun b => sig (P a b))))
  : (u.1; u.2.1; u.2.2.1; u.2.2.2) = u
  := 1.

Arguments eta3_sigma / .

(** ** Paths *)

(** A path in a total space is commonly shown component wise. Because we use this over and over, we write down the proofs by hand to make sure they are what we think they should be. *)

(** With this version of the function, we often have to give [u] and [v] explicitly, so we make them explicit arguments. *)
Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sig P)
           (pq : {p : u.1 = v.1 & p # u.2 = v.2})
: u = v
  := match pq.2 in (_ = v2) return u = (v.1; v2) with
       | 1 => match pq.1 as p in (_ = v1) return u = (v1; p # u.2) with
                | 1 => 1
              end
     end.

(** This is the curried one you usually want to use in practice.  We define it in terms of the uncurried one, since it's the uncurried one that is proven below to be an equivalence. *)
Definition path_sigma {A : Type} (P : A -> Type) (u v : sig P)
           (p : u.1 = v.1) (q : p # u.2 = v.2)
: u = v
  := path_sigma_uncurried P u v (p;q).

(** A contravariant instance of [path_sigma_uncurried] *)
Definition path_sigma_uncurried_contra {A : Type} (P : A -> Type) (u v : sig P)
           (pq : {p : u.1 = v.1 & u.2 = p^ # v.2})
: u = v
  := (path_sigma_uncurried P v u (pq.1^;pq.2^))^.

(** A variant of [Forall.dpath_forall] from which uses dependent sums to package things. It cannot go into [Forall] because [Sigma] depends on [Forall]. *)

Definition dpath_forall'
           {A : Type } (P : A -> Type) (Q: sig P -> Type) {x y : A} (h : x = y)
           (f : forall p, Q (x ; p)) (g : forall p, Q (y ; p))
:
  (forall p, transport Q (path_sigma P (x ; p) (y; _) h 1) (f p) = g (h # p))
    <~>
    (forall p, transportD P (fun x => fun p => Q ( x ; p)) h p (f p) = g (transport P h p)).
A: Type
P: A -> Type
Q: {x : _ & P x} -> Type
x, y: A
h: x = y
f: forall p : P x, Q (x; p)
g: forall p : P y, Q (y; p)
(forall p : P x,
 transport Q
   (path_sigma P (x; p)
      (y;
      match h in (_ = a) return (P a) with
      | 1 => (x; p).2
      end) h 1) (f p) = g (transport P h p)) <~>
(forall p : P x,
 transportD P (fun (x : A) (p0 : P x) => Q (x; p0)) h
   p (f p) = g (transport P h p))
Proof.
A: Type
P: A -> Type
Q: {x : _ & P x} -> Type
x, y: A
h: x = y
f: forall p : P x, Q (x; p)
g: forall p : P y, Q (y; p)
(forall p : P x,
 transport Q
   (path_sigma P (x; p)
      (y;
      match h in (_ = a) return (P a) with
      | 1 => (x; p).2
      end) h 1) (f p) = g (transport P h p)) <~>
(forall p : P x,
 transportD P (fun (x : A) (p0 : P x) => Q (x; p0)) h
   p (f p) = g (transport P h p))
  destruct h.
A: Type
P: A -> Type
Q: {x : _ & P x} -> Type
x: A
f, g: forall p : P x, Q (x; p)
(forall p : P x,
 transport Q (path_sigma P (x; p) (x; (x; p).2) 1 1)
   (f p) = g (transport P 1 p)) <~>
(forall p : P x,
 transportD P (fun (x : A) (p0 : P x) => Q (x; p0)) 1
   p (f p) = g (transport P 1 p))
  apply 1%equiv.
Defined.


(** This version produces only paths between pairs, as opposed to paths between arbitrary inhabitants of dependent sum types.  But it has the advantage that the components of those pairs can more often be inferred, so we make them implicit arguments. *)
Definition path_sigma' {A : Type} (P : A -> Type) {x x' : A} {y : P x} {y' : P x'}
           (p : x = x') (q : p # y = y')
: (x;y) = (x';y')
  := path_sigma P (x;y) (x';y') p q.


(** Projections of paths from a total space. *)

Definition pr1_path `{P : A -> Type} {u v : sig P} (p : u = v)
: u.1 = v.1
  :=
    ap pr1 p.
(* match p with idpath => 1 end. *)

Notation "p ..1" := (pr1_path p) : fibration_scope.

Definition pr2_path `{P : A -> Type} {u v : sig P} (p : u = v)
: p..1 # u.2 = v.2
  := (transport_compose P pr1 p u.2)^
     @ (@apD {x:A & P x} _ pr2 _ _ p).

Notation "p ..2" := (pr2_path p) : fibration_scope.

(** Now we show how these things compute. *)

Definition pr1_path_sigma_uncurried `{P : A -> Type} {u v : sig P}
           (pq : { p : u.1 = v.1 & p # u.2 = v.2 })
: (path_sigma_uncurried _ _ _ pq)..1 = pq.1.
A: Type
P: A -> Type
u, v: {x : _ & P x}
pq: {p : u.1 = v.1 & transport P p u.2 = v.2}
(path_sigma_uncurried P u v pq) ..1 = pq.1
Proof.
A: Type
P: A -> Type
u, v: {x : _ & P x}
pq: {p : u.1 = v.1 & transport P p u.2 = v.2}
(path_sigma_uncurried P u v pq) ..1 = pq.1
  destruct u as [u1 u2]; destruct v as [v1 v2]; simpl in *.
A: Type
P: A -> Type
u1: A
u2: P u1
v1: A
v2: P v1
pq: {p : u1 = v1 & transport P p u2 = v2}
(path_sigma_uncurried P (u1; u2) (v1; v2) pq) ..1 =
pq.1
  destruct pq as [p q].
A: Type
P: A -> Type
u1: A
u2: P u1
v1: A
v2: P v1
p: u1 = v1
q: transport P p u2 = v2
(path_sigma_uncurried P (u1; u2) (v1; v2) (p; q)) ..1 =
(p; q).1
  destruct p; simpl in q; destruct q; reflexivity.
Defined.

Definition pr2_path_sigma_uncurried `{P : A -> Type} {u v : sig P}
           (pq : { p : u.1 = v.1 & p # u.2 = v.2 })
: (path_sigma_uncurried _ _ _ pq)..2
  = ap (fun s => transport P s u.2) (pr1_path_sigma_uncurried pq) @ pq.2.
A: Type
P: A -> Type
u, v: {x : _ & P x}
pq: {p : u.1 = v.1 & transport P p u.2 = v.2}
(path_sigma_uncurried P u v pq) ..2 =
ap (fun s : u.1 = v.1 => transport P s u.2)
  (pr1_path_sigma_uncurried pq) @ pq.2
Proof.
A: Type
P: A -> Type
u, v: {x : _ & P x}
pq: {p : u.1 = v.1 & transport P p u.2 = v.2}
(path_sigma_uncurried P u v pq) ..2 =
ap (fun s : u.1 = v.1 => transport P s u.2)
  (pr1_path_sigma_uncurried pq) @ pq.2
  destruct u as [u1 u2]; destruct v as [v1 v2]; simpl in *.
A: Type
P: A -> Type
u1: A
u2: P u1
v1: A
v2: P v1
pq: {p : u1 = v1 & transport P p u2 = v2}
(path_sigma_uncurried P (u1; u2) (v1; v2) pq) ..2 =
ap (fun s : u1 = v1 => transport P s u2)
  (pr1_path_sigma_uncurried pq) @ pq.2
  destruct pq as [p q].
A: Type
P: A -> Type
u1: A
u2: P u1
v1: A
v2: P v1
p: u1 = v1
q: transport P p u2 = v2
(path_sigma_uncurried P (u1; u2) (v1; v2) (p; q)) ..2 =
ap (fun s : u1 = v1 => transport P s u2)
  (pr1_path_sigma_uncurried (p; q)) @ (p; q).2
  destruct p; simpl in q; destruct q; reflexivity.
Defined.

Definition eta_path_sigma_uncurried `{P : A -> Type} {u v : sig P}
           (p : u = v)
: path_sigma_uncurried _ _ _ (p..1; p..2) = p.
A: Type
P: A -> Type
u, v: {x : _ & P x}
p: u = v
path_sigma_uncurried P u v (p ..1; p ..2) = p
Proof.
A: Type
P: A -> Type
u, v: {x : _ & P x}
p: u = v
path_sigma_uncurried P u v (p ..1; p ..2) = p
  destruct p.
A: Type
P: A -> Type
u: {x : _ & P x}
path_sigma_uncurried P u u (1 ..1; 1 ..2) = 1 reflexivity.
Defined.

Lemma transport_pr1_path_sigma_uncurried
      `{P : A -> Type} {u v : sig P}
      (pq : { p : u.1 = v.1 & transport P p u.2 = v.2 })
      Q
: transport (fun x => Q x.1) (@path_sigma_uncurried A P u v pq)
  = transport _ pq.1.
A: Type
P: A -> Type
u, v: {x : _ & P x}
pq: {p : u.1 = v.1 & transport P p u.2 = v.2}
Q: A -> Type
transport (fun x : {x : _ & P x} => Q x.1)
  (path_sigma_uncurried P u v pq) = transport Q pq.1
Proof.
A: Type
P: A -> Type
u, v: {x : _ & P x}
pq: {p : u.1 = v.1 & transport P p u.2 = v.2}
Q: A -> Type
transport (fun x : {x : _ & P x} => Q x.1)
  (path_sigma_uncurried P u v pq) = transport Q pq.1
  destruct pq as [p q], u, v; simpl in *.
A: Type
P: A -> Type
proj1: A
proj2: P proj1
proj0: A
proj3: P proj0
p: proj1 = proj0
q: transport P p proj2 = proj3
Q: A -> Type
transport (fun x : {x : _ & P x} => Q x.1)
  match
    q in (_ = v2)
    return ((proj1; proj2) = (proj0; v2))
  with
  | 1 =>
      match
        p in (_ = v1)
        return
          ((proj1; proj2) = (v1; transport P p proj2))
      with
      | 1 => 1
      end
  end = transport Q p
  destruct p, q; simpl in *.
A: Type
P: A -> Type
proj1: A
proj2: P proj1
Q: A -> Type
transport (fun x : {x : _ & P x} => Q x.1) 1 =
transport Q 1
  reflexivity.
Defined.

Definition pr1_path_sigma `{P : A -> Type} {u v : sig P}
           (p : u.1 = v.1) (q : p # u.2 = v.2)
: (path_sigma _ _ _ p q)..1 = p
  := pr1_path_sigma_uncurried (p; q).

(* Writing it the other way can help [rewrite]. *)
Definition ap_pr1_path_sigma {A:Type} {P : A -> Type} {u v : sig P}
           (p : u.1 = v.1) (q : p # u.2 = v.2)
  : ap pr1 (path_sigma _ _ _ p q) = p
  := pr1_path_sigma p q.

Definition pr2_path_sigma `{P : A -> Type} {u v : sig P}
           (p : u.1 = v.1) (q : p # u.2 = v.2)
: (path_sigma _ _ _ p q)..2
  = ap (fun s => transport P s u.2) (pr1_path_sigma p q) @ q
  := pr2_path_sigma_uncurried (p; q).

Definition eta_path_sigma `{P : A -> Type} {u v : sig P} (p : u = v)
: path_sigma _ _ _ (p..1) (p..2) = p
  := eta_path_sigma_uncurried p.

Definition transport_pr1_path_sigma
           `{P : A -> Type} {u v : sig P}
           (p : u.1 = v.1) (q : p # u.2 = v.2)
           Q
: transport (fun x => Q x.1) (@path_sigma A P u v p q)
  = transport _ p
  := transport_pr1_path_sigma_uncurried (p; q) Q.

(** This lets us identify the path space of a sigma-type, up to equivalence. *)

Global Instance isequiv_path_sigma `{P : A -> Type} {u v : sig P}
: IsEquiv (path_sigma_uncurried P u v) | 0.
A: Type
P: A -> Type
u, v: {x : _ & P x}
IsEquiv (path_sigma_uncurried P u v)
Proof.
A: Type
P: A -> Type
u, v: {x : _ & P x}
IsEquiv (path_sigma_uncurried P u v)
  simple refine (Build_IsEquiv
            _ _
            _ (fun r => (r..1; r..2))
            eta_path_sigma
            _ _).
A: Type
P: A -> Type
u, v: {x : _ & P x}
(fun r : u = v => (r ..1; r ..2))
o path_sigma_uncurried P u v == idmap
A: Type
P: A -> Type
u, v: {x : _ & P x}
forall x : {p : u.1 = v.1 & transport P p u.2 = v.2},
eta_path_sigma (path_sigma_uncurried P u v x) =
ap (path_sigma_uncurried P u v) (?eissect x)
  all: destruct u, v; intros [p q].
A: Type
P: A -> Type
proj1: A
proj2: P proj1
proj0: A
proj3: P proj0
p: (proj1; proj2).1 = (proj0; proj3).1
q: transport P p (proj1; proj2).2 = (proj0; proj3).2
((path_sigma_uncurried P (proj1; proj2) (proj0; proj3)
    (p; q)) ..1;
(path_sigma_uncurried P (proj1; proj2) (proj0; proj3)
   (p; q)) ..2) = (p; q)
A: Type
P: A -> Type
proj1: A
proj2: P proj1
proj0: A
proj3: P proj0
p: (proj1; proj2).1 = (proj0; proj3).1
q: transport P p (proj1; proj2).2 = (proj0; proj3).2
eta_path_sigma
  (path_sigma_uncurried P 
     (proj1; proj2) (proj0; proj3) 
     (p; q)) =
ap
  (path_sigma_uncurried P 
     (proj1; proj2) (proj0; proj3)) 
  ?Goal
  all: simpl in *.
A: Type
P: A -> Type
proj1: A
proj2: P proj1
proj0: A
proj3: P proj0
p: proj1 = proj0
q: transport P p proj2 = proj3
(match
   q in (_ = v2) return ((proj1; proj2) = (proj0; v2))
 with
 | 1 =>
     match
       p in (_ = v1)
       return
         ((proj1; proj2) = (v1; transport P p proj2))
     with
     | 1 => 1
     end
 end ..1;
match
  q in (_ = v2) return ((proj1; proj2) = (proj0; v2))
with
| 1 =>
    match
      p in (_ = v1)
      return
        ((proj1; proj2) = (v1; transport P p proj2))
    with
    | 1 => 1
    end
end ..2) = (p; q)
A: Type
P: A -> Type
proj1: A
proj2: P proj1
proj0: A
proj3: P proj0
p: proj1 = proj0
q: transport P p proj2 = proj3
eta_path_sigma
  match
    q in (_ = v2)
    return ((proj1; proj2) = (proj0; v2))
  with
  | 1 =>
      match
        p in (_ = v1)
        return
          ((proj1; proj2) = (v1; transport P p proj2))
      with
      | 1 => 1
      end
  end =
ap
  (path_sigma_uncurried P 
     (proj1; proj2) (proj0; proj3)) 
  ?Goal
  all: destruct q, p; simpl in *.
A: Type
P: A -> Type
proj1: A
proj2: P proj1
(1; 1 ..2) = (1; 1)
A: Type
P: A -> Type
proj1: A
proj2: P proj1
1 =
ap
  (path_sigma_uncurried P 
     (proj1; proj2) (proj1; proj2)) 
  ?Goal
  all: reflexivity.
Defined.

Definition equiv_path_sigma `(P : A -> Type) (u v : sig P)
: {p : u.1 = v.1 &  p # u.2 = v.2} <~> (u = v)
  := Build_Equiv _ _ (path_sigma_uncurried P u v) _.

(* A contravariant version of [isequiv_path_sigma'] *)
Global Instance isequiv_path_sigma_contra `{P : A -> Type} {u v : sig P}
  : IsEquiv (path_sigma_uncurried_contra P u v) | 0.
A: Type
P: A -> Type
u, v: {x : _ & P x}
IsEquiv (path_sigma_uncurried_contra P u v)
  apply (isequiv_adjointify (path_sigma_uncurried_contra P u v)
        (fun r => match r with idpath => (1; 1) end)).
A: Type
P: A -> Type
u, v: {x : _ & P x}
(fun x : u = v =>
 path_sigma_uncurried_contra P u v
   match
     x in (_ = s)
     return {p : u.1 = s.1 & u.2 = transport P p^ s.2}
   with
   | 1 => (1; 1)
   end) == idmap
A: Type
P: A -> Type
u, v: {x : _ & P x}
(fun x : {p : u.1 = v.1 & u.2 = transport P p^ v.2} =>
 match
   path_sigma_uncurried_contra P u v x in (_ = s)
   return {p : u.1 = s.1 & u.2 = transport P p^ s.2}
 with
 | 1 => (1; 1)
 end) == idmap
-
A: Type
P: A -> Type
u, v: {x : _ & P x}
(fun x : u = v =>
 path_sigma_uncurried_contra P u v
   match
     x in (_ = s)
     return {p : u.1 = s.1 & u.2 = transport P p^ s.2}
   with
   | 1 => (1; 1)
   end) == idmap by intro r; induction r; destruct u as [u1 u2]; reflexivity.
-
A: Type
P: A -> Type
u, v: {x : _ & P x}
(fun x : {p : u.1 = v.1 & u.2 = transport P p^ v.2} =>
 match
   path_sigma_uncurried_contra P u v x in (_ = s)
   return {p : u.1 = s.1 & u.2 = transport P p^ s.2}
 with
 | 1 => (1; 1)
 end) == idmap destruct u, v; intros [p q].
A: Type
P: A -> Type
proj1: A
proj2: P proj1
proj0: A
proj3: P proj0
p: (proj1; proj2).1 = (proj0; proj3).1
q: (proj1; proj2).2 = transport P p^ (proj0; proj3).2
match
  path_sigma_uncurried_contra P (proj1; proj2)
    (proj0; proj3) (p; q) in (_ = s)
  return
    {p : (proj1; proj2).1 = s.1 &
    (proj1; proj2).2 = transport P p^ s.2}
with
| 1 => (1; 1)
end = (p; q)
  simpl in *.
A: Type
P: A -> Type
proj1: A
proj2: P proj1
proj0: A
proj3: P proj0
p: proj1 = proj0
q: proj2 = transport P p^ proj3
match
  path_sigma_uncurried_contra P 
    (proj1; proj2) (proj0; proj3) 
    (p; q) in (_ = s)
  return
    {p : proj1 = s.1 & proj2 = transport P p^ s.2}
with
| 1 => (1; 1)
end = (p; q)
  destruct p; simpl in q.
A: Type
P: A -> Type
proj1: A
proj2, proj3: P proj1
q: proj2 = proj3
match
  path_sigma_uncurried_contra P 
    (proj1; proj2) (proj1; proj3) 
    (1; q) in (_ = s)
  return
    {p : proj1 = s.1 & proj2 = transport P p^ s.2}
with
| 1 => (1; 1)
end = (1; q)
  destruct q; reflexivity.
Defined.

(* A contravariant version of [equiv_path_sigma] *)
Definition equiv_path_sigma_contra {A : Type} `(P : A -> Type) (u v : sig P)
  : {p : u.1 = v.1 & u.2 = p^ # v.2} <~> (u = v)
  := Build_Equiv _ _ (path_sigma_uncurried_contra P u v) _.

(** This identification respects path concatenation. *)

Definition path_sigma_pp_pp {A : Type} (P : A -> Type) {u v w : sig P}
           (p1 : u.1 = v.1) (q1 : p1 # u.2 = v.2)
           (p2 : v.1 = w.1) (q2 : p2 # v.2 = w.2)
: path_sigma P u w (p1 @ p2)
             (transport_pp P p1 p2 u.2 @ ap (transport P p2) q1 @ q2)
  = path_sigma P u v p1 q1 @ path_sigma P v w p2 q2.
A: Type
P: A -> Type
u, v, w: {x : _ & P x}
p1: u.1 = v.1
q1: transport P p1 u.2 = v.2
p2: v.1 = w.1
q2: transport P p2 v.2 = w.2
path_sigma P u w (p1 @ p2)
  ((transport_pp P p1 p2 u.2 @ ap (transport P p2) q1) @
   q2) =
path_sigma P u v p1 q1 @ path_sigma P v w p2 q2
Proof.
A: Type
P: A -> Type
u, v, w: {x : _ & P x}
p1: u.1 = v.1
q1: transport P p1 u.2 = v.2
p2: v.1 = w.1
q2: transport P p2 v.2 = w.2
path_sigma P u w (p1 @ p2)
  ((transport_pp P p1 p2 u.2 @ ap (transport P p2) q1) @
   q2) =
path_sigma P u v p1 q1 @ path_sigma P v w p2 q2
  destruct u, v, w.
A: Type
P: A -> Type
proj1: A
proj2: P proj1
proj0: A
proj3: P proj0
proj4: A
proj5: P proj4
p1: (proj1; proj2).1 = (proj0; proj3).1
q1: transport P p1 (proj1; proj2).2 =
(proj0; proj3).2
p2: (proj0; proj3).1 = (proj4; proj5).1
q2: transport P p2 (proj0; proj3).2 =
(proj4; proj5).2
path_sigma P (proj1; proj2) (proj4; proj5) (p1 @ p2)
  ((transport_pp P p1 p2 (proj1; proj2).2 @
    ap (transport P p2) q1) @ q2) =
path_sigma P (proj1; proj2) (proj0; proj3) p1 q1 @
path_sigma P (proj0; proj3) (proj4; proj5) p2 q2 simpl in *.
A: Type
P: A -> Type
proj1: A
proj2: P proj1
proj0: A
proj3: P proj0
proj4: A
proj5: P proj4
p1: proj1 = proj0
q1: transport P p1 proj2 = proj3
p2: proj0 = proj4
q2: transport P p2 proj3 = proj5
path_sigma P (proj1; proj2) 
  (proj4; proj5) (p1 @ p2)
  ((transport_pp P p1 p2 proj2 @
    ap (transport P p2) q1) @ q2) =
path_sigma P (proj1; proj2) (proj0; proj3) p1 q1 @
path_sigma P (proj0; proj3) (proj4; proj5) p2 q2
  destruct p1, p2, q1, q2.
A: Type
P: A -> Type
proj1: A
proj2: P proj1
path_sigma P (proj1; proj2)
  (proj1; transport P 1 (transport P 1 proj2)) 
  (1 @ 1)
  ((transport_pp P 1 1 proj2 @ ap (transport P 1) 1) @
   1) =
path_sigma P (proj1; proj2)
  (proj1; transport P 1 proj2) 1 1 @
path_sigma P (proj1; transport P 1 proj2)
  (proj1; transport P 1 (transport P 1 proj2)) 1 1
  reflexivity.
Defined.

Definition path_sigma_pp_pp' {A : Type} (P : A -> Type)
           {u1 v1 w1 : A} {u2 : P u1} {v2 : P v1} {w2 : P w1}
           (p1 : u1 = v1) (q1 : p1 # u2 = v2)
           (p2 : v1 = w1) (q2 : p2 # v2 = w2)
: path_sigma' P (p1 @ p2)
              (transport_pp P p1 p2 u2 @ ap (transport P p2) q1 @ q2)
  = path_sigma' P p1 q1 @ path_sigma' P p2 q2
  := @path_sigma_pp_pp A P (u1;u2) (v1;v2) (w1;w2) p1 q1 p2 q2.

Definition path_sigma_p1_1p' {A : Type} (P : A -> Type)
           {u1 v1 : A} {u2 : P u1} {v2 : P v1}
           (p : u1 = v1) (q : p # u2 = v2)
: path_sigma' P p q
  = path_sigma' P p 1 @ path_sigma' P 1 q.
A: Type
P: A -> Type
u1, v1: A
u2: P u1
v2: P v1
p: u1 = v1
q: transport P p u2 = v2
path_sigma' P p q =
path_sigma' P p 1 @ path_sigma' P 1 q
Proof.
A: Type
P: A -> Type
u1, v1: A
u2: P u1
v2: P v1
p: u1 = v1
q: transport P p u2 = v2
path_sigma' P p q =
path_sigma' P p 1 @ path_sigma' P 1 q
  destruct p, q.
A: Type
P: A -> Type
u1: A
u2: P u1
path_sigma' P 1 1 =
path_sigma' P 1 1 @ path_sigma' P 1 1
  reflexivity.
Defined.

(** [pr1_path] also commutes with the groupoid structure. *)

Definition pr1_path_1 {A : Type} {P : A -> Type} (u : sig P)
: (idpath u) ..1 = idpath (u .1)
  := 1.

Definition pr1_path_pp {A : Type} {P : A -> Type} {u v w : sig P}
           (p : u = v) (q : v = w)
: (p @ q) ..1 = (p ..1) @ (q ..1)
  := ap_pp _ _ _.

Definition pr1_path_V {A : Type} {P : A -> Type} {u v : sig P} (p : u = v)
: p^ ..1 = (p ..1)^
  := ap_V _ _.

(** Applying [exist] to one argument is the same as [path_sigma] with reflexivity in the first place. *)

Definition ap_exist {A : Type} (P : A -> Type) (x : A) (y1 y2 : P x)
           (q : y1 = y2)
: ap (exist P x) q = path_sigma' P 1 q.
A: Type
P: A -> Type
x: A
y1, y2: P x
q: y1 = y2
ap (exist P x) q = path_sigma' P 1 q
Proof.
A: Type
P: A -> Type
x: A
y1, y2: P x
q: y1 = y2
ap (exist P x) q = path_sigma' P 1 q
  destruct q; reflexivity.
Defined.

(** Dependent transport is the same as transport along a [path_sigma]. *)

Definition transportD_is_transport
           {A:Type} (B:A->Type) (C:sig B -> Type)
           (x1 x2:A) (p:x1=x2) (y:B x1) (z:C (x1;y))
: transportD B (fun a b => C (a;b)) p y z
  = transport C (path_sigma' B p 1) z.
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
x1, x2: A
p: x1 = x2
y: B x1
z: C (x1; y)
transportD B (fun (a : A) (b : B a) => C (a; b)) p y z =
transport C (path_sigma' B p 1) z
Proof.
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
x1, x2: A
p: x1 = x2
y: B x1
z: C (x1; y)
transportD B (fun (a : A) (b : B a) => C (a; b)) p y z =
transport C (path_sigma' B p 1) z
  destruct p.
A: Type
B: A -> Type
C: {x : _ & B x} -> Type
x1: A
y: B x1
z: C (x1; y)
transportD B (fun (a : A) (b : B a) => C (a; b)) 1 y z =
transport C (path_sigma' B 1 1) z reflexivity.
Defined.


(** Applying a two variable function to a [path_sigma]. *)

Definition ap_path_sigma {A B} (P : A -> Type) (F : forall a : A, P a -> B)
           {x x' : A} {y : P x} {y' : P x'} (p : x = x') (q : p # y = y')
  : ap (fun w => F w.1 w.2) (path_sigma' P p q)
    = ap _ (moveL_transport_V _ p _ _ q)
         @ (transport_arrow_toconst _ _ _)^ @ ap10 (apD F p) y'.
A, B: Type
P: A -> Type
F: forall a : A, P a -> B
x, x': A
y: P x
y': P x'
p: x = x'
q: transport P p y = y'
ap (fun w : {x : _ & P x} => F w.1 w.2)
  (path_sigma' P p q) =
(ap (F x) (moveL_transport_V P p y y' q) @
 (transport_arrow_toconst p (F x) y')^) @
ap10 (apD F p) y'
Proof.
A, B: Type
P: A -> Type
F: forall a : A, P a -> B
x, x': A
y: P x
y': P x'
p: x = x'
q: transport P p y = y'
ap (fun w : {x : _ & P x} => F w.1 w.2)
  (path_sigma' P p q) =
(ap (F x) (moveL_transport_V P p y y' q) @
 (transport_arrow_toconst p (F x) y')^) @
ap10 (apD F p) y'
  destruct p, q; reflexivity.
Defined.
(* Remark: this is also equal to: *)
(*     = ap10 (apD F p^)^ y @ transport_arrow_toconst _ _ _ *)
(*                          @ ap (F x') (transport2 _ (inv_V p) y @ q). *)



(** And we can simplify when the first equality is [1]. *)
Lemma ap_path_sigma_1p {A B : Type} {P : A -> Type} (F : forall a, P a -> B)
      (a : A) {x y : P a} (p : x = y)
  : ap (fun w => F w.1 w.2) (path_sigma' P 1 p) = ap (fun z => F a z) p.
A, B: Type
P: A -> Type
F: forall a : A, P a -> B
a: A
x, y: P a
p: x = y
ap (fun w : {x : _ & P x} => F w.1 w.2)
  (path_sigma' P 1 p) = ap (fun z : P a => F a z) p
Proof.
A, B: Type
P: A -> Type
F: forall a : A, P a -> B
a: A
x, y: P a
p: x = y
ap (fun w : {x : _ & P x} => F w.1 w.2)
  (path_sigma' P 1 p) = ap (fun z : P a => F a z) p
  destruct p; reflexivity.
Defined.


(** Applying a function constructed with [sig_rec] to a [path_sigma] can be computed.  Technically this computation should probably go by way of a 2-variable [ap], and should be done in the dependently typed case. *)
Definition ap_sig_rec_path_sigma {A : Type} (P : A -> Type) {Q : Type}
           (x1 x2:A) (p:x1=x2) (y1:P x1) (y2:P x2) (q:p # y1 = y2)
           (d : forall a, P a -> Q)
: ap (sig_rec _ _ Q d) (path_sigma' P p q)
  = (transport_const p _)^
    @ (ap ((transport (fun _ => Q) p) o (d x1)) (transport_Vp _ p y1))^
    @ (transport_arrow p _ _)^
    @ ap10 (apD d p) (p # y1)
      @ ap (d x2) q.
A: Type
P: A -> Type
Q: Type
x1, x2: A
p: x1 = x2
y1: P x1
y2: P x2
q: transport P p y1 = y2
d: forall a : A, P a -> Q
ap (sig_rec A P Q d) (path_sigma' P p q) =
((((transport_const p (d x1 y1))^ @
   (ap (transport (fun _ : A => Q) p o d x1)
      (transport_Vp P p y1))^) @
  (transport_arrow p (d x1) (transport P p y1))^) @
 ap10 (apD d p) (transport P p y1)) @ ap (d x2) q
Proof.
A: Type
P: A -> Type
Q: Type
x1, x2: A
p: x1 = x2
y1: P x1
y2: P x2
q: transport P p y1 = y2
d: forall a : A, P a -> Q
ap (sig_rec A P Q d) (path_sigma' P p q) =
((((transport_const p (d x1 y1))^ @
   (ap (transport (fun _ : A => Q) p o d x1)
      (transport_Vp P p y1))^) @
  (transport_arrow p (d x1) (transport P p y1))^) @
 ap10 (apD d p) (transport P p y1)) @ ap (d x2) q
  destruct p.
A: Type
P: A -> Type
Q: Type
x1: A
y1, y2: P x1
q: transport P 1 y1 = y2
d: forall a : A, P a -> Q
ap (sig_rec A P Q d) (path_sigma' P 1 q) =
((((transport_const 1 (d x1 y1))^ @
   (ap
      (fun x : P x1 =>
       transport (fun _ : A => Q) 1 (d x1 x))
      (transport_Vp P 1 y1))^) @
  (transport_arrow 1 (d x1) (transport P 1 y1))^) @
 ap10 (apD d 1) (transport P 1 y1)) @ ap (d x1) q destruct q.
A: Type
P: A -> Type
Q: Type
x1: A
y1: P x1
d: forall a : A, P a -> Q
ap (sig_rec A P Q d) (path_sigma' P 1 1) =
((((transport_const 1 (d x1 y1))^ @
   (ap
      (fun x : P x1 =>
       transport (fun _ : A => Q) 1 (d x1 x))
      (transport_Vp P 1 y1))^) @
  (transport_arrow 1 (d x1) (transport P 1 y1))^) @
 ap10 (apD d 1) (transport P 1 y1)) @ ap (d x1) 1 reflexivity.
Defined.


(** A path between paths in a total space is commonly shown component wise. *)

(** With this version of the function, we often have to give [u] and [v] explicitly, so we make them explicit arguments. *)
Definition path_path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sig P)
           (p q : u = v)
           (rs : {r : p..1 = q..1 & transport (fun x => transport P x u.2 = v.2) r p..2 = q..2})
: p = q.
A: Type
P: A -> Type
u, v: {x : _ & P x}
p, q: u = v
rs: {r : p ..1 = q ..1 &
transport
  (fun x : u.1 = v.1 => transport P x u.2 = v.2)
  r p ..2 = q ..2}
p = q
Proof.
A: Type
P: A -> Type
u, v: {x : _ & P x}
p, q: u = v
rs: {r : p ..1 = q ..1 &
transport
  (fun x : u.1 = v.1 => transport P x u.2 = v.2)
  r p ..2 = q ..2}
p = q
  destruct rs, p, u.
A: Type
P: A -> Type
proj0: A
proj3: P proj0
q: (proj0; proj3) = (proj0; proj3)
proj1: 1 ..1 = q ..1
proj2: transport
  (fun x : (proj0; proj3).1 = (proj0; proj3).1
   =>
   transport P x (proj0; proj3).2 =
   (proj0; proj3).2) proj1 
  1 ..2 = q ..2
1 = q
  etransitivity; [ | apply eta_path_sigma ].
A: Type
P: A -> Type
proj0: A
proj3: P proj0
q: (proj0; proj3) = (proj0; proj3)
proj1: 1 ..1 = q ..1
proj2: transport
  (fun x : (proj0; proj3).1 = (proj0; proj3).1
   =>
   transport P x (proj0; proj3).2 =
   (proj0; proj3).2) proj1 
  1 ..2 = q ..2
1 =
path_sigma P (proj0; proj3) (proj0; proj3) q ..1 q ..2
  path_induction.
A: Type
P: A -> Type
proj0: A
proj3: P proj0
q: (proj0; proj3) = (proj0; proj3)
1 =
path_sigma P (proj0; proj3) 
  (proj0; proj3) 1 ..1
  (transport
     (fun x : (proj0; proj3).1 = (proj0; proj3).1 =>
      transport P x (proj0; proj3).2 =
      (proj0; proj3).2) 1 
     1 ..2)
  reflexivity.
Defined.

(** This is the curried one you usually want to use in practice.  We define it in terms of the uncurried one, since it's the uncurried one that is proven below to be an equivalence. *)
Definition path_path_sigma {A : Type} (P : A -> Type) (u v : sig P)
           (p q : u = v)
           (r : p..1 = q..1)
           (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2)
: p = q
  := path_path_sigma_uncurried P u v p q (r; s).

(** ** Transport *)

(** The concrete description of transport in sigmas (and also pis) is rather trickier than in the other types.  In particular, these cannot be described just in terms of transport in simpler types; they require also the dependent transport [transportD].

  In particular, this indicates why "transport" alone cannot be fully defined by induction on the structure of types, although Id-elim/transportD can be (cf. Observational Type Theory).  A more thorough set of lemmas, along the lines of the present ones but dealing with Id-elim rather than just transport, might be nice to have eventually? *)

Definition transport_sigma {A : Type} {B : A -> Type} {C : forall a:A, B a -> Type}
           {x1 x2 : A} (p : x1 = x2) (yz : { y : B x1 & C x1 y })
: transport (fun x => { y : B x & C x y }) p yz
  = (p # yz.1 ; transportD _ _ p yz.1 yz.2).
A: Type
B: A -> Type
C: forall a : A, B a -> Type
x1, x2: A
p: x1 = x2
yz: {y : B x1 & C x1 y}
transport (fun x : A => {y : B x & C x y}) p yz =
(transport B p yz.1; transportD B C p yz.1 yz.2)
Proof.
A: Type
B: A -> Type
C: forall a : A, B a -> Type
x1, x2: A
p: x1 = x2
yz: {y : B x1 & C x1 y}
transport (fun x : A => {y : B x & C x y}) p yz =
(transport B p yz.1; transportD B C p yz.1 yz.2)
  destruct p.
A: Type
B: A -> Type
C: forall a : A, B a -> Type
x1: A
yz: {y : B x1 & C x1 y}
transport (fun x : A => {y : B x & C x y}) 1 yz =
(transport B 1 yz.1; transportD B C 1 yz.1 yz.2)  destruct yz as [y z].
A: Type
B: A -> Type
C: forall a : A, B a -> Type
x1: A
y: B x1
z: C x1 y
transport (fun x : A => {y : B x & C x y}) 1 (y; z) =
(transport B 1 (y; z).1;
transportD B C 1 (y; z).1 (y; z).2) reflexivity.
Defined.

(** The special case when the second variable doesn't depend on the first is simpler. *)
Definition transport_sigma' {A B : Type} {C : A -> B -> Type}
           {x1 x2 : A} (p : x1 = x2) (yz : { y : B & C x1 y })
: transport (fun x => { y : B & C x y }) p yz =
  (yz.1 ; transport (fun x => C x yz.1) p yz.2).
A, B: Type
C: A -> B -> Type
x1, x2: A
p: x1 = x2
yz: {y : B & C x1 y}
transport (fun x : A => {y : B & C x y}) p yz =
(yz.1; transport (fun x : A => C x yz.1) p yz.2)
Proof.
A, B: Type
C: A -> B -> Type
x1, x2: A
p: x1 = x2
yz: {y : B & C x1 y}
transport (fun x : A => {y : B & C x y}) p yz =
(yz.1; transport (fun x : A => C x yz.1) p yz.2)
  destruct p.
A, B: Type
C: A -> B -> Type
x1: A
yz: {y : B & C x1 y}
transport (fun x : A => {y : B & C x y}) 1 yz =
(yz.1; transport (fun x : A => C x yz.1) 1 yz.2) destruct yz.
A, B: Type
C: A -> B -> Type
x1: A
proj1: B
proj2: C x1 proj1
transport (fun x : A => {y : B & C x y}) 1
  (proj1; proj2) =
((proj1; proj2).1;
transport (fun x : A => C x (proj1; proj2).1) 1
  (proj1; proj2).2) reflexivity.
Defined.

(** Or if the second variable contains a first component that doesn't depend on the first.  Need to think about the naming of these. *)

Definition transport_sigma_' {A : Type} {B C : A -> Type}
           {D : forall a:A, B a -> C a -> Type}
           {x1 x2 : A} (p : x1 = x2)
           (yzw : { y : B x1 & { z : C x1 & D x1 y z } })
: transport (fun x => { y : B x & { z : C x & D x y z } }) p yzw
  = (p # yzw.1 ; p # yzw.2.1 ; transportD2 _ _ _ p yzw.1 yzw.2.1 yzw.2.2).
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
x1, x2: A
p: x1 = x2
yzw: {y : B x1 & {z : C x1 & D x1 y z}}
transport
  (fun x : A => {y : B x & {z : C x & D x y z}}) p yzw =
(transport B p yzw.1; transport C p (yzw.2).1;
transportD2 B C D p yzw.1 (yzw.2).1 (yzw.2).2)
Proof.
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
x1, x2: A
p: x1 = x2
yzw: {y : B x1 & {z : C x1 & D x1 y z}}
transport
  (fun x : A => {y : B x & {z : C x & D x y z}}) p yzw =
(transport B p yzw.1; transport C p (yzw.2).1;
transportD2 B C D p yzw.1 (yzw.2).1 (yzw.2).2)
  destruct p.
A: Type
B, C: A -> Type
D: forall a : A, B a -> C a -> Type
x1: A
yzw: {y : B x1 & {z : C x1 & D x1 y z}}
transport
  (fun x : A => {y : B x & {z : C x & D x y z}}) 1 yzw =
(transport B 1 yzw.1; transport C 1 (yzw.2).1;
transportD2 B C D 1 yzw.1 (yzw.2).1 (yzw.2).2) reflexivity.
Defined.

(** ** Functorial action *)

Definition functor_sigma `{P : A -> Type} `{Q : B -> Type}
           (f : A -> B) (g : forall a, P a -> Q (f a))
: sig P -> sig Q
  := fun u => (f u.1 ; g u.1 u.2).

Definition ap_functor_sigma `{P : A -> Type} `{Q : B -> Type}
           (f : A -> B) (g : forall a, P a -> Q (f a))
           (u v : sig P) (p : u.1 = v.1) (q : p # u.2 = v.2)
: ap (functor_sigma f g) (path_sigma P u v p q)
  = path_sigma Q (functor_sigma f g u) (functor_sigma f g v)
               (ap f p)
               ((transport_compose Q f p (g u.1 u.2))^
                @ (@ap_transport _ P (fun x => Q (f x)) _ _ p g u.2)^
                @ ap (g v.1) q).
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
u, v: {x : _ & P x}
p: u.1 = v.1
q: transport P p u.2 = v.2
ap (functor_sigma f g) (path_sigma P u v p q) =
path_sigma Q (functor_sigma f g u)
  (functor_sigma f g v) (ap f p)
  (((transport_compose Q f p (g u.1 u.2))^ @
    (ap_transport p g u.2)^) @ ap (g v.1) q)
Proof.
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
u, v: {x : _ & P x}
p: u.1 = v.1
q: transport P p u.2 = v.2
ap (functor_sigma f g) (path_sigma P u v p q) =
path_sigma Q (functor_sigma f g u)
  (functor_sigma f g v) (ap f p)
  (((transport_compose Q f p (g u.1 u.2))^ @
    (ap_transport p g u.2)^) @ ap (g v.1) q)
  destruct u as [u1 u2]; destruct v as [v1 v2]; simpl in p, q.
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
u1: A
u2: P u1
v1: A
v2: P v1
p: u1 = v1
q: transport P p u2 = v2
ap (functor_sigma f g)
  (path_sigma P (u1; u2) (v1; v2) p q) =
path_sigma Q (functor_sigma f g (u1; u2))
  (functor_sigma f g (v1; v2)) (ap f p)
  (((transport_compose Q f p (g (u1; u2).1 (u1; u2).2))^ @
    (ap_transport p g (u1; u2).2)^) @
   ap (g (v1; v2).1) q)
  destruct p; simpl in q.
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
u1: A
u2, v2: P u1
q: u2 = v2
ap (functor_sigma f g)
  (path_sigma P (u1; u2) (u1; v2) 1 q) =
path_sigma Q (functor_sigma f g (u1; u2))
  (functor_sigma f g (u1; v2)) (ap f 1)
  (((transport_compose Q f 1 (g (u1; u2).1 (u1; u2).2))^ @
    (ap_transport 1 g (u1; u2).2)^) @
   ap (g (u1; v2).1) q)
  destruct q.
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
u1: A
u2: P u1
ap (functor_sigma f g)
  (path_sigma P (u1; u2) (u1; u2) 1 1) =
path_sigma Q (functor_sigma f g (u1; u2))
  (functor_sigma f g (u1; u2)) (ap f 1)
  (((transport_compose Q f 1 (g (u1; u2).1 (u1; u2).2))^ @
    (ap_transport 1 g (u1; u2).2)^) @
   ap (g (u1; u2).1) 1)
  reflexivity.
Defined.

(** ** Equivalences *)

Global Instance isequiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
         `{IsEquiv A B f} `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
: IsEquiv (functor_sigma f g) | 1000.
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
H: IsEquiv f
g: forall x : A, P x -> Q (f x)
H0: forall a : A, IsEquiv (g a)
IsEquiv (functor_sigma f g)
Proof.
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
H: IsEquiv f
g: forall x : A, P x -> Q (f x)
H0: forall a : A, IsEquiv (g a)
IsEquiv (functor_sigma f g)
  refine (isequiv_adjointify (functor_sigma f g)
                             (functor_sigma (f^-1)
                                            (fun x y => ((g (f^-1 x))^-1 ((eisretr f x)^ # y)))) _ _);
  intros [x y].
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
H: IsEquiv f
g: forall x : A, P x -> Q (f x)
H0: forall a : A, IsEquiv (g a)
x: B
y: Q x
functor_sigma f g
  (functor_sigma f^-1
     (fun (x : B) (y : Q x) =>
      (g (f^-1 x))^-1 (transport Q (eisretr f x)^ y))
     (x; y)) = (x; y)
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
H: IsEquiv f
g: forall x : A, P x -> Q (f x)
H0: forall a : A, IsEquiv (g a)
x: A
y: P x
functor_sigma f^-1
  (fun (x : B) (y : Q x) =>
   (g (f^-1 x))^-1 (transport Q (eisretr f x)^ y))
  (functor_sigma f g (x; y)) = (x; y)
  -
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
H: IsEquiv f
g: forall x : A, P x -> Q (f x)
H0: forall a : A, IsEquiv (g a)
x: B
y: Q x
functor_sigma f g
  (functor_sigma f^-1
     (fun (x : B) (y : Q x) =>
      (g (f^-1 x))^-1 (transport Q (eisretr f x)^ y))
     (x; y)) = (x; y) refine (path_sigma' _ (eisretr f x) _); simpl.
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
H: IsEquiv f
g: forall x : A, P x -> Q (f x)
H0: forall a : A, IsEquiv (g a)
x: B
y: Q x
transport Q (eisretr f x)
  (g (f^-1 x)
     ((g (f^-1 x))^-1 (transport Q (eisretr f x)^ y))) =
y
    abstract (
        rewrite (eisretr (g (f^-1 x)));
        apply transport_pV
      ).
  -
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
H: IsEquiv f
g: forall x : A, P x -> Q (f x)
H0: forall a : A, IsEquiv (g a)
x: A
y: P x
functor_sigma f^-1
  (fun (x : B) (y : Q x) =>
   (g (f^-1 x))^-1 (transport Q (eisretr f x)^ y))
  (functor_sigma f g (x; y)) = (x; y) refine (path_sigma' _ (eissect f x) _); simpl.
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
H: IsEquiv f
g: forall x : A, P x -> Q (f x)
H0: forall a : A, IsEquiv (g a)
x: A
y: P x
transport P (eissect f x)
  ((g (f^-1 (f x)))^-1
     (transport Q (eisretr f (f x))^ (g x y))) = y
    refine ((ap_transport (eissect f x) (fun x' => (g x') ^-1)
                          (transport Q (eisretr f (f x)) ^ (g x y)))^ @ _).
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: A -> B
H: IsEquiv f
g: forall x : A, P x -> Q (f x)
H0: forall a : A, IsEquiv (g a)
x: A
y: P x
(g x)^-1
  (transport (fun x' : A => Q (f x')) (eissect f x)
     (transport Q (eisretr f (f x))^ (g x y))) = y
    abstract (
        rewrite transport_compose, eisadj, transport_pV;
        apply eissect
      ).
Defined.

Definition equiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
           (f : A -> B) `{IsEquiv A B f}
           (g : forall a, P a -> Q (f a))
           `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
: sig P <~> sig Q
  := Build_Equiv _ _ (functor_sigma f g) _.

Definition equiv_functor_sigma' `{P : A -> Type} `{Q : B -> Type}
           (f : A <~> B)
           (g : forall a, P a <~> Q (f a))
: sig P <~> sig Q
  := equiv_functor_sigma f g.

Definition equiv_functor_sigma_id `{P : A -> Type} `{Q : A -> Type}
           (g : forall a, P a <~> Q a)
: sig P <~> sig Q
  := equiv_functor_sigma' 1 g.

Definition equiv_functor_sigma_pb {A B : Type} {Q : B -> Type}
           (f : A <~> B)
: sig (Q o f) <~> sig Q
  := equiv_functor_sigma f (fun a => 1%equiv).

(** Lemma 3.11.9(i): Summing up a contractible family of types does nothing. *)

Global Instance isequiv_pr1_contr {A} {P : A -> Type}
         `{forall a, Contr (P a)}
: IsEquiv (@pr1 A P) | 100.
A: Type
P: A -> Type
H: forall a : A, Contr (P a)
IsEquiv pr1
Proof.
A: Type
P: A -> Type
H: forall a : A, Contr (P a)
IsEquiv pr1
  refine (isequiv_adjointify (@pr1 A P)
                             (fun a => (a ; center (P a))) _ _).
A: Type
P: A -> Type
H: forall a : A, Contr (P a)
(fun x : A => (x; center (P x)).1) == idmap
A: Type
P: A -> Type
H: forall a : A, Contr (P a)
(fun x : {x : _ & P x} => (x.1; center (P x.1))) ==
idmap
  -
A: Type
P: A -> Type
H: forall a : A, Contr (P a)
(fun x : A => (x; center (P x)).1) == idmap intros a; reflexivity.
  -
A: Type
P: A -> Type
H: forall a : A, Contr (P a)
(fun x : {x : _ & P x} => (x.1; center (P x.1))) ==
idmap intros [a p].
A: Type
P: A -> Type
H: forall a : A, Contr (P a)
a: A
p: P a
((a; p).1; center (P (a; p).1)) = (a; p)
    refine (path_sigma' P 1 (contr _)).
Defined.

Definition equiv_sigma_contr {A : Type} (P : A -> Type)
           `{forall a, Contr (P a)}
: sig P <~> A
  := Build_Equiv _ _ pr1 _.

(** Lemma 3.11.9(ii): Dually, summing up over a contractible type does nothing. *)

Definition equiv_contr_sigma {A : Type} (P : A -> Type) `{Contr A}
: { x : A & P x } <~> P (center A).
A: Type
P: A -> Type
Contr0: Contr A
{x : A & P x} <~> P (center A)
Proof.
A: Type
P: A -> Type
Contr0: Contr A
{x : A & P x} <~> P (center A)
  refine (equiv_adjointify (fun xp => (contr xp.1)^ # xp.2)
                           (fun p => (center A ; p)) _ _).
A: Type
P: A -> Type
Contr0: Contr A
(fun x : P (center A) =>
 transport (fun x0 : A => P x0)
   (contr (center A; x).1)^ 
   (center A; x).2) == idmap
A: Type
P: A -> Type
Contr0: Contr A
(fun x : {x : A & P x} =>
 (center A;
 transport (fun x0 : A => P x0) (contr x.1)^ x.2)) ==
idmap
  -
A: Type
P: A -> Type
Contr0: Contr A
(fun x : P (center A) =>
 transport (fun x0 : A => P x0)
   (contr (center A; x).1)^ 
   (center A; x).2) == idmap intros p; simpl.
A: Type
P: A -> Type
Contr0: Contr A
p: P (center A)
transport (fun x : A => P x) (contr (center A))^ p = p
    exact (ap (fun q => q # p) (path_contr _ 1)).
  -
A: Type
P: A -> Type
Contr0: Contr A
(fun x : {x : A & P x} =>
 (center A;
 transport (fun x0 : A => P x0) (contr x.1)^ x.2)) ==
idmap intros [a p].
A: Type
P: A -> Type
Contr0: Contr A
a: A
p: P a
(center A;
transport (fun x : A => P x) 
  (contr (a; p).1)^ (a; p).2) = 
(a; p)
    refine (path_sigma' _ (contr a) _).
A: Type
P: A -> Type
Contr0: Contr A
a: A
p: P a
transport (fun x : A => P x) 
  (contr a)
  (transport (fun x : A => P x) 
     (contr (a; p).1)^ (a; p).2) = p
    apply transport_pV.
Defined.


(** ** Associativity *)

(** All of the following lemmas are proven easily with the [make_equiv] tactic.  If you have a more complicated rearrangement of sigma-types to do, it is usually possible to do it by putting together these equivalences, but it is often simpler and faster to just use [make_equiv] directly. *)

Definition equiv_sigma_assoc `(P : A -> Type) (Q : {a : A & P a} -> Type)
  : {a : A & {p : P a & Q (a;p)}} <~> sig Q.
A: Type
P: A -> Type
Q: {a : A & P a} -> Type
{a : A & {p : P a & Q (a; p)}} <~> {x : _ & Q x}
Proof.
A: Type
P: A -> Type
Q: {a : A & P a} -> Type
{a : A & {p : P a & Q (a; p)}} <~> {x : _ & Q x}
  make_equiv.
Defined.

Definition equiv_sigma_assoc' `(P : A -> Type) (Q : forall a : A, P a -> Type)
  : {a : A & {p : P a & Q a p}} <~> {ap : sig P & Q ap.1 ap.2}.
A: Type
P: A -> Type
Q: forall a : A, P a -> Type
{a : A & {p : P a & Q a p}} <~>
{ap : {x : _ & P x} & Q ap.1 ap.2}
Proof.
A: Type
P: A -> Type
Q: forall a : A, P a -> Type
{a : A & {p : P a & Q a p}} <~>
{ap : {x : _ & P x} & Q ap.1 ap.2}
  make_equiv.
Defined.

Definition equiv_sigma_prod `(Q : (A * B) -> Type)
  : {a : A & {b : B & Q (a,b)}} <~> sig Q.
A, B: Type
Q: A * B -> Type
{a : A & {b : B & Q (a, b)}} <~> {x : _ & Q x}
Proof.
A, B: Type
Q: A * B -> Type
{a : A & {b : B & Q (a, b)}} <~> {x : _ & Q x}
  make_equiv.
Defined.

Definition equiv_sigma_prod' `(Q : A -> B -> Type)
  : {a : A & {b : B & Q a b}} <~> sig (fun ab => Q (fst ab) (snd ab)).
A, B: Type
Q: A -> B -> Type
{a : A & {b : B & Q a b}} <~>
{ab : A * B & Q (fst ab) (snd ab)}
Proof.
A, B: Type
Q: A -> B -> Type
{a : A & {b : B & Q a b}} <~>
{ab : A * B & Q (fst ab) (snd ab)}
  make_equiv.
Defined.

Definition equiv_sigma_prod0 (A B : Type)
  : {a : A & B} <~> A * B.
A, B: Type
{_ : A & B} <~> A * B
Proof.
A, B: Type
{_ : A & B} <~> A * B
  make_equiv.
Defined.

Definition equiv_sigma_prod1 (A B C : Type)
  : {a : A & {b : B & C}} <~> A * B * C
  := ltac:(make_equiv).

Definition equiv_sigma_prod_prod {X Y : Type} (P : X -> Type) (Q : Y -> Type)
  : {z : X * Y & (P (fst z)) * (Q (snd z))} <~> (sig P) * (sig Q)
  := ltac:(make_equiv).

(** ** Symmetry *)

Definition equiv_sigma_symm `(P : A -> B -> Type)
  : {a : A & {b : B & P a b}} <~> {b : B & {a : A & P a b}}.
A, B: Type
P: A -> B -> Type
{a : A & {b : B & P a b}} <~>
{b : B & {a : A & P a b}}
Proof.
A, B: Type
P: A -> B -> Type
{a : A & {b : B & P a b}} <~>
{b : B & {a : A & P a b}}
  make_equiv.
Defined.

Definition equiv_sigma_symm' {A : Type} `(P : A -> Type) `(Q : A -> Type)
  : { ap : { a : A & P a } & Q ap.1 } <~> { aq : { a : A & Q a } & P aq.1 }.
A: Type
P, Q: A -> Type
{ap : {a : A & P a} & Q ap.1} <~>
{aq : {a : A & Q a} & P aq.1}
Proof.
A: Type
P, Q: A -> Type
{ap : {a : A & P a} & Q ap.1} <~>
{aq : {a : A & Q a} & P aq.1}
  make_equiv.
Defined.

Definition equiv_sigma_symm0 (A B : Type)
: {a : A & B} <~> {b : B & A}.
A, B: Type
{_ : A & B} <~> {_ : B & A}
Proof.
A, B: Type
{_ : A & B} <~> {_ : B & A}
  make_equiv.
Defined.

(** ** Universal mapping properties *)

(** *** The positive universal property. *)
Global Instance isequiv_sig_ind `{P : A -> Type}
         (Q : sig P -> Type)
: IsEquiv (sig_ind Q) | 0
  := Build_IsEquiv
       _ _
       (sig_ind Q)
       (fun f x y => f (x;y))
       (fun _ => 1)
       (fun _ => 1)
       (fun _ => 1).

Definition equiv_sig_ind `{P : A -> Type}
           (Q : sig P -> Type)
: (forall (x:A) (y:P x), Q (x;y)) <~> (forall xy, Q xy)
  := Build_Equiv _ _ (sig_ind Q) _.

(** And a curried version *)
Definition equiv_sig_ind' `{P : A -> Type}
           (Q : forall a, P a -> Type)
: (forall (x:A) (y:P x), Q x y) <~> (forall xy, Q xy.1 xy.2)
  := equiv_sig_ind (fun xy => Q xy.1 xy.2).

(** *** The negative universal property. *)

Definition sig_coind_uncurried
           `{A : X -> Type} (P : forall x, A x -> Type)
: { f : forall x, A x & forall x, P x (f x) }
  -> (forall x, sig (P x))
  := fun fg => fun x => (fg.1 x ; fg.2 x).

Definition sig_coind
           `{A : X -> Type} (P : forall x, A x -> Type)
           (f : forall x, A x) (g : forall x, P x (f x))
: (forall x, sig (P x))
  := sig_coind_uncurried P (f;g).

Global Instance isequiv_sig_coind
         `{A : X -> Type} {P : forall x, A x -> Type}
: IsEquiv (sig_coind_uncurried P) | 0
  := Build_IsEquiv
       _ _
       (sig_coind_uncurried P)
       (fun h => exist (fun f => forall x, P x (f x))
                        (fun x => (h x).1)
                        (fun x => (h x).2))
       (fun _ => 1)
       (fun _ => 1)
       (fun _ => 1).

Definition equiv_sig_coind
           `(A : X -> Type) (P : forall x, A x -> Type)
: { f : forall x, A x & forall x, P x (f x) }
    <~> (forall x, sig (P x))
  := Build_Equiv _ _ (sig_coind_uncurried P) _.

(** ** Sigmas preserve truncation *)

Global Instance istrunc_sigma `{P : A -> Type}
         `{IsTrunc n A} `{forall a, IsTrunc n (P a)}
: IsTrunc n (sig P) | 100.
A: Type
P: A -> Type
n: trunc_index
IsTrunc0: IsTrunc n A
H: forall a : A, IsTrunc n (P a)
IsTrunc n {x : _ & P x}
Proof.
A: Type
P: A -> Type
n: trunc_index
IsTrunc0: IsTrunc n A
H: forall a : A, IsTrunc n (P a)
IsTrunc n {x : _ & P x}
  generalize dependent A.
n: trunc_index
forall (A : Type) (P : A -> Type),
IsTrunc n A ->
(forall a : A, IsTrunc n (P a)) ->
IsTrunc n {x : _ & P x}
  induction n; simpl; intros A P ac Pc.
A: Type
P: A -> Type
ac: Contr A
Pc: forall a : A, Contr (P a)
Contr {x : _ & P x}
n: trunc_index
IHn: forall (A : Type) (P : A -> Type),
IsTrunc n A ->
(forall a : A, IsTrunc n (P a)) ->
IsTrunc n {x : _ & P x}
A: Type
P: A -> Type
ac: IsTrunc n.+1 A
Pc: forall a : A, IsTrunc n.+1 (P a)
IsTrunc n.+1 {x : _ & P x}
  {
A: Type
P: A -> Type
ac: Contr A
Pc: forall a : A, Contr (P a)
Contr {x : _ & P x} apply (Build_Contr _ (center A; center (P (center A)))).
A: Type
P: A -> Type
ac: Contr A
Pc: forall a : A, Contr (P a)
forall y : {x : _ & P x},
(center A; center (P (center A))) = y
    intros [a ?].
A: Type
P: A -> Type
ac: Contr A
Pc: forall a : A, Contr (P a)
a: A
proj2: P a
(center A; center (P (center A))) = (a; proj2)
    refine (path_sigma' P (contr a) (path_contr _ _)). }
n: trunc_index
IHn: forall (A : Type) (P : A -> Type),
IsTrunc n A ->
(forall a : A, IsTrunc n (P a)) ->
IsTrunc n {x : _ & P x}
A: Type
P: A -> Type
ac: IsTrunc n.+1 A
Pc: forall a : A, IsTrunc n.+1 (P a)
IsTrunc n.+1 {x : _ & P x}
  apply istrunc_S.
n: trunc_index
IHn: forall (A : Type) (P : A -> Type),
IsTrunc n A ->
(forall a : A, IsTrunc n (P a)) ->
IsTrunc n {x : _ & P x}
A: Type
P: A -> Type
ac: IsTrunc n.+1 A
Pc: forall a : A, IsTrunc n.+1 (P a)
forall (x : {x : _ & P x}) 
(y : {x : _ & P x}), IsTrunc n (x = y)
  intros u v.
n: trunc_index
IHn: forall (A : Type) (P : A -> Type),
IsTrunc n A ->
(forall a : A, IsTrunc n (P a)) ->
IsTrunc n {x : _ & P x}
A: Type
P: A -> Type
ac: IsTrunc n.+1 A
Pc: forall a : A, IsTrunc n.+1 (P a)
u, v: {x : _ & P x}
IsTrunc n (u = v)
  refine (istrunc_isequiv_istrunc _ (path_sigma_uncurried P u v)).
Defined.

(** The sigma of an arbitrary family of *disjoint* hprops is an hprop. *)
Definition ishprop_sigma_disjoint
           `{P : A -> Type} `{forall a, IsHProp (P a)}
: (forall x y, P x -> P y -> x = y) -> IsHProp { x : A & P x }.
A: Type
P: A -> Type
H: forall a : A, IsHProp (P a)
(forall x y : A, P x -> P y -> x = y) ->
IsHProp {x : A & P x}
Proof.
A: Type
P: A -> Type
H: forall a : A, IsHProp (P a)
(forall x y : A, P x -> P y -> x = y) ->
IsHProp {x : A & P x}
  intros dj; apply hprop_allpath; intros [x px] [y py].
A: Type
P: A -> Type
H: forall a : A, IsHProp (P a)
dj: forall x y : A, P x -> P y -> x = y
x: A
px: P x
y: A
py: P y
(x; px) = (y; py)
  refine (path_sigma' P (dj x y px py) _).
A: Type
P: A -> Type
H: forall a : A, IsHProp (P a)
dj: forall x y : A, P x -> P y -> x = y
x: A
px: P x
y: A
py: P y
transport P (dj x y px py) px = py
  apply path_ishprop.
Defined.

(** ** Subtypes (sigma types whose second components are hprops) *)

(** To prove equality in a subtype, we only need equality of the first component. *)
Definition path_sigma_hprop {A : Type} {P : A -> Type}
           `{forall x, IsHProp (P x)}
           (u v : sig P)
: u.1 = v.1 -> u = v
  := path_sigma_uncurried P u v o pr1^-1.

Global Instance isequiv_path_sigma_hprop {A P} `{forall x : A, IsHProp (P x)} {u v : sig P}
: IsEquiv (@path_sigma_hprop A P _ u v) | 100
  := isequiv_compose.

#[export]
Hint Immediate isequiv_path_sigma_hprop : typeclass_instances.

Definition equiv_path_sigma_hprop {A : Type} {P : A -> Type}
           {HP : forall a, IsHProp (P a)} (u v : sig P)
: (u.1 = v.1) <~> (u = v)
  := Build_Equiv _ _ (path_sigma_hprop _ _) _.

Definition isequiv_pr1_path_hprop {A} {P : A -> Type}
         `{forall a, IsHProp (P a)}
         x y
: IsEquiv (@pr1_path A P x y)
  := _ : IsEquiv (path_sigma_hprop x y)^-1.

#[export]
Hint Immediate isequiv_pr1_path_hprop : typeclass_instances.

(** We define this for ease of [SearchAbout IsEquiv ap pr1] *)
Definition isequiv_ap_pr1_hprop {A} {P : A -> Type}
           `{forall a, IsHProp (P a)}
           x y
: IsEquiv (@ap _ _ (@pr1 A P) x y)
  := _.


(** [path_sigma_hprop] is functorial *)
Definition path_sigma_hprop_1 {A : Type} {P : A -> Type}
           `{forall x, IsHProp (P x)} (u : sig P)
: path_sigma_hprop u u 1 = 1.
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
u: {x : _ & P x}
path_sigma_hprop u u 1 = 1
Proof.
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
u: {x : _ & P x}
path_sigma_hprop u u 1 = 1
  unfold path_sigma_hprop.
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
u: {x : _ & P x}
path_sigma_uncurried P u u (pr1^-1 1) = 1
  unfold isequiv_pr1_contr; simpl.
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
u: {x : _ & P x}
match
  center (u.2 = u.2) in (_ = v2)
  return (u = (u.1; v2))
with
| 1 => 1
end = 1
  (** Ugh *)
  refine (ap (fun p => match p in (_ = v2) return (u = (u.1; v2)) with 1 => 1 end)
             (contr (idpath u.2))).
Defined.

Definition path_sigma_hprop_V {A : Type} {P : A -> Type}
           `{forall x, IsHProp (P x)} {a b : A} (p : a = b)
           (x : P a) (y : P b)
: path_sigma_hprop (b;y) (a;x) p^ = (path_sigma_hprop (a;x) (b;y) p)^.
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
a, b: A
p: a = b
x: P a
y: P b
path_sigma_hprop (b; y) (a; x) p^ =
(path_sigma_hprop (a; x) (b; y) p)^
Proof.
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
a, b: A
p: a = b
x: P a
y: P b
path_sigma_hprop (b; y) (a; x) p^ =
(path_sigma_hprop (a; x) (b; y) p)^
  destruct p; simpl.
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
a: A
x, y: P a
path_sigma_hprop (a; y) (a; x) 1 =
(path_sigma_hprop (a; x) (a; y) 1)^
  rewrite (path_ishprop x y).
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
a: A
x, y: P a
path_sigma_hprop (a; y) (a; y) 1 =
(path_sigma_hprop (a; y) (a; y) 1)^
  refine (path_sigma_hprop_1 _ @ (ap inverse (path_sigma_hprop_1 _))^).
Qed.

Definition path_sigma_hprop_pp
           {A : Type}
           {P : A -> Type}
           `{forall x, IsHProp (P x)}
           {a b c : A}
           (p : a = b) (q : b = c)
           (x : P a) (y : P b) (z : P c)
: path_sigma_hprop (a;x) (c;z) (p @ q)
    =
  path_sigma_hprop (a;x) (b;y) p @ path_sigma_hprop (b;y) (c;z) q.
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
a, b, c: A
p: a = b
q: b = c
x: P a
y: P b
z: P c
path_sigma_hprop (a; x) (c; z) (p @ q) =
path_sigma_hprop (a; x) (b; y) p @
path_sigma_hprop (b; y) (c; z) q
Proof.
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
a, b, c: A
p: a = b
q: b = c
x: P a
y: P b
z: P c
path_sigma_hprop (a; x) (c; z) (p @ q) =
path_sigma_hprop (a; x) (b; y) p @
path_sigma_hprop (b; y) (c; z) q
  destruct p, q.
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
a: A
x, y, z: P a
path_sigma_hprop (a; x) (a; z) (1 @ 1) =
path_sigma_hprop (a; x) (a; y) 1 @
path_sigma_hprop (a; y) (a; z) 1
  rewrite (path_ishprop y x).
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
a: A
x, y, z: P a
path_sigma_hprop (a; x) (a; z) (1 @ 1) =
path_sigma_hprop (a; x) (a; x) 1 @
path_sigma_hprop (a; x) (a; z) 1
  rewrite (path_ishprop z x).
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
a: A
x, y, z: P a
path_sigma_hprop (a; x) (a; x) (1 @ 1) =
path_sigma_hprop (a; x) (a; x) 1 @
path_sigma_hprop (a; x) (a; x) 1
  refine (_ @ (ap (fun z => z @ _) (path_sigma_hprop_1 _))^).
A: Type
P: A -> Type
H: forall x : A, IsHProp (P x)
a: A
x, y, z: P a
path_sigma_hprop (a; x) (a; x) (1 @ 1) =
1 @ path_sigma_hprop (a; x) (a; x) 1
  apply (concat_1p _)^.
Qed.

(** The inverse of [path_sigma_hprop] has its own name, so we give special names to the section and retraction homotopies to help [rewrite] out. *)
Definition path_sigma_hprop_ap_pr1 {A : Type} {P : A -> Type}
           `{forall x, IsHProp (P x)} (u v : sig P) (p : u = v)
: path_sigma_hprop u v (ap pr1 p) = p
  := eisretr (path_sigma_hprop u v) p.
Definition path_sigma_hprop_pr1_path {A : Type} {P : A -> Type}
           `{forall x, IsHProp (P x)} (u v : sig P) (p : u = v)
: path_sigma_hprop u v p..1 = p
  := eisretr (path_sigma_hprop u v) p.
Definition ap_pr1_path_sigma_hprop {A : Type} {P : A -> Type}
           `{forall x, IsHProp (P x)} (u v : sig P) (p : u.1 = v.1)
: ap pr1 (path_sigma_hprop u v p) = p
  := eissect (path_sigma_hprop u v) p.
Definition pr1_path_path_sigma_hprop {A : Type} {P : A -> Type}
           `{forall x, IsHProp (P x)} (u v : sig P) (p : u.1 = v.1)
: (path_sigma_hprop u v p)..1 = p
  := eissect (path_sigma_hprop u v) p.

(** ** Fibers of [functor_sigma] *)
Definition hfiber_functor_sigma {A B} (P : A -> Type) (Q : B -> Type)
           (f : A -> B) (g : forall a, P a -> Q (f a))
           (b : B) (v : Q b)
: (hfiber (functor_sigma f g) (b; v)) <~>
  {w : hfiber f b & hfiber (g w.1) ((w.2)^ # v)}.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
b: B
v: Q b
hfiber (functor_sigma f g) (b; v) <~>
{w : hfiber f b &
hfiber (g w.1) (transport Q (w.2)^ v)}
Proof.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
b: B
v: Q b
hfiber (functor_sigma f g) (b; v) <~>
{w : hfiber f b &
hfiber (g w.1) (transport Q (w.2)^ v)}
  unfold hfiber, functor_sigma.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
b: B
v: Q b
{x : {x : _ & P x} & (f x.1; g x.1 x.2) = (b; v)} <~>
{w : {x : A & f x = b} &
{x : P w.1 & g w.1 x = transport Q (w.2)^ v}}
  refine (_ oE equiv_functor_sigma_id _).
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
b: B
v: Q b
{x : _ & ?Goal0 x} <~>
{w : {x : A & f x = b} &
{x : P w.1 & g w.1 x = transport Q (w.2)^ v}}
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
b: B
v: Q b
forall a : {x : _ & P x},
(f a.1; g a.1 a.2) = (b; v) <~> ?Goal0 a
  2:intros; symmetry; apply equiv_path_sigma.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
b: B
v: Q b
{a : {x : _ & P x} &
{p : (f a.1; g a.1 a.2).1 = (b; v).1 &
transport Q p (f a.1; g a.1 a.2).2 = (b; v).2}} <~>
{w : {x : A & f x = b} &
{x : P w.1 & g w.1 x = transport Q (w.2)^ v}}
  transitivity {w : {x : A & f x = b} & {x : P w.1 & (w.2) # (g w.1 x) = v}}.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
b: B
v: Q b
{a : {x : _ & P x} &
{p : (f a.1; g a.1 a.2).1 = (b; v).1 &
transport Q p (f a.1; g a.1 a.2).2 = (b; v).2}} <~>
{w : {x : A & f x = b} &
{x : P w.1 & transport Q w.2 (g w.1 x) = v}}
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
b: B
v: Q b
{w : {x : A & f x = b} &
{x : P w.1 & transport Q w.2 (g w.1 x) = v}} <~>
{w : {x : A & f x = b} &
{x : P w.1 & g w.1 x = transport Q (w.2)^ v}}
  1:make_equiv.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
b: B
v: Q b
{w : {x : A & f x = b} &
{x : P w.1 & transport Q w.2 (g w.1 x) = v}} <~>
{w : {x : A & f x = b} &
{x : P w.1 & g w.1 x = transport Q (w.2)^ v}}
  apply equiv_functor_sigma_id; intros [a p]; simpl.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
b: B
v: Q b
a: A
p: f a = b
{x : P a & transport Q p (g a x) = v} <~>
{x : P a & g a x = transport Q p^ v}
  apply equiv_functor_sigma_id; intros u; simpl.
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
b: B
v: Q b
a: A
p: f a = b
u: P a
transport Q p (g a u) = v <~> g a u = transport Q p^ v
  apply equiv_moveL_transport_V.
Defined.

Global Instance istruncmap_functor_sigma n {A B P Q}
       (f : A -> B) (g : forall a, P a -> Q (f a))
       {Hf : IsTruncMap n f} {Hg : forall a, IsTruncMap n (g a)}
  : IsTruncMap n (functor_sigma f g).
n: trunc_index
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
Hf: IsTruncMap n f
Hg: forall a : A, IsTruncMap n (g a)
IsTruncMap n (functor_sigma f g)
Proof.
n: trunc_index
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
Hf: IsTruncMap n f
Hg: forall a : A, IsTruncMap n (g a)
IsTruncMap n (functor_sigma f g)
  intros [a b].
n: trunc_index
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
Hf: IsTruncMap n f
Hg: forall a : A, IsTruncMap n (g a)
a: B
b: Q a
IsTrunc n (hfiber (functor_sigma f g) (a; b))
  exact (istrunc_equiv_istrunc _ (hfiber_functor_sigma _ _ _ _ _ _)^-1).
Defined.

(** Theorem 4.7.6 *)
Definition hfiber_functor_sigma_idmap {A} (P Q : A -> Type)
           (g : forall a, P a -> Q a)
           (b : A) (v : Q b)
: (hfiber (functor_sigma idmap g) (b; v)) <~>
   hfiber (g b) v.
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
b: A
v: Q b
hfiber (functor_sigma idmap g) (b; v) <~>
hfiber (g b) v
Proof.
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
b: A
v: Q b
hfiber (functor_sigma idmap g) (b; v) <~>
hfiber (g b) v
  refine (_ oE hfiber_functor_sigma P Q idmap g b v).
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
b: A
v: Q b
{w : hfiber idmap b &
hfiber (g w.1) (transport Q (w.2)^ v)} <~>
hfiber (g b) v
  exact (equiv_contr_sigma
           (fun (w:hfiber idmap b) => hfiber (g w.1) (transport Q (w.2)^ v))).
Defined.

(** The converse and Theorem 4.7.7 can be found in Types/Equiv.v *)
Definition istruncmap_from_functor_sigma n {A P Q}
           (g : forall a : A, P a -> Q a)
           `{!IsTruncMap n (functor_sigma idmap g)}
  : forall a, IsTruncMap n (g a).
n: trunc_index
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
IsTruncMap0: IsTruncMap n (functor_sigma idmap g)
forall a : A, IsTruncMap n (g a)
Proof.
n: trunc_index
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
IsTruncMap0: IsTruncMap n (functor_sigma idmap g)
forall a : A, IsTruncMap n (g a)
  intros a v.
n: trunc_index
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
IsTruncMap0: IsTruncMap n (functor_sigma idmap g)
a: A
v: Q a
IsTrunc n (hfiber (g a) v)
  exact (istrunc_equiv_istrunc _ (hfiber_functor_sigma_idmap _ _ _ _ _)).
Defined.