(* -*- mode: coq; mode: visual-line -*- *)
(** * Theorems about cartesian products *)

Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids
               Basics.Tactics Basics.Trunc Basics.Decidable.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Empty.
Local Open Scope path_scope.

Generalizable Variables X A B f g n.

Scheme prod_ind := Induction for prod Sort Type.
Arguments prod_ind {A B} P f p.

(** ** Unpacking *)

(** Sometimes we would like to prove [Q u] where [u : A * B] by writing [u] as a pair [(fst u ; snd u)]. This is accomplished by [unpack_prod]. We want tight control over the proof, so we just write it down even though is looks a bit scary. *)

Definition unpack_prod `{P : A * B -> Type} (u : A * B) :
  P (fst u, snd u) -> P u
  := idmap.

Arguments unpack_prod / .

(** Now we write down the reverse. *)
Definition pack_prod `{P : A * B -> Type} (u : A * B) :
  P u -> P (fst u, snd u)
  := idmap.

Arguments pack_prod / .

(** ** Eta conversion *)

Definition eta_prod `(z : A * B) : (fst z, snd z) = z
  := 1.

Arguments eta_prod / .

(** ** Paths *)

(** With this version of the function, we often have to give [z] and [z'] explicitly, so we make them explicit arguments. *)
Definition path_prod_uncurried {A B : Type} (z z' : A * B)
  (pq : (fst z = fst z') * (snd z = snd z'))
  : (z = z').
A, B: Type
z, z': A * B
pq: (fst z = fst z') * (snd z = snd z')
z = z'
Proof.
A, B: Type
z, z': A * B
pq: (fst z = fst z') * (snd z = snd z')
z = z'
  change ((fst z, snd z) = (fst z', snd z')).
A, B: Type
z, z': A * B
pq: (fst z = fst z') * (snd z = snd z')
(fst z, snd z) = (fst z', snd z')
  case (fst pq).
A, B: Type
z, z': A * B
pq: (fst z = fst z') * (snd z = snd z')
(fst z, snd z) = (fst z, snd z') case (snd pq).
A, B: Type
z, z': A * B
pq: (fst z = fst z') * (snd z = snd z')
(fst z, snd z) = (fst z, snd z)
  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_prod {A B : Type} (z z' : A * B) :
  (fst z = fst z') -> (snd z = snd z') -> (z = z')
  := fun p q => path_prod_uncurried z z' (p,q).

(** This version produces only paths between pairs, as opposed to paths between arbitrary inhabitants of product types.  But it has the advantage that the components of those pairs can more often be inferred. *)
Definition path_prod' {A B : Type} {x x' : A} {y y' : B}
  : (x = x') -> (y = y') -> ((x,y) = (x',y'))
  := fun p q => path_prod (x,y) (x',y') p q.

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

Definition ap_fst_path_prod {A B : Type} {z z' : A * B}
  (p : fst z = fst z') (q : snd z = snd z') :
  ap fst (path_prod _ _ p q) = p.
A, B: Type
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap fst (path_prod z z' p q) = p
Proof.
A, B: Type
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap fst (path_prod z z' p q) = p
  change z with (fst z, snd z).
A, B: Type
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap fst (path_prod (fst z, snd z) z' p q) = p
  change z' with (fst z', snd z').
A, B: Type
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap fst (path_prod (fst z, snd z) (fst z', snd z') p q) =
p
  destruct p, q.
A, B: Type
z, z': A * B
ap fst (path_prod (fst z, snd z) (fst z, snd z) 1 1) =
1
  reflexivity.
Defined.

Definition ap_fst_path_prod' {A B : Type} {x x' : A} {y y' : B}
  (p : x = x') (q : y = y')
  : ap fst (path_prod' p q) = p.
A, B: Type
x, x': A
y, y': B
p: x = x'
q: y = y'
ap fst (path_prod' p q) = p
Proof.
A, B: Type
x, x': A
y, y': B
p: x = x'
q: y = y'
ap fst (path_prod' p q) = p
  apply ap_fst_path_prod.
Defined.

Definition ap_snd_path_prod {A B : Type} {z z' : A * B}
  (p : fst z = fst z') (q : snd z = snd z') :
  ap snd (path_prod _ _ p q) = q.
A, B: Type
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap snd (path_prod z z' p q) = q
Proof.
A, B: Type
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap snd (path_prod z z' p q) = q
  change z with (fst z, snd z).
A, B: Type
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap snd (path_prod (fst z, snd z) z' p q) = q
  change z' with (fst z', snd z').
A, B: Type
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap snd (path_prod (fst z, snd z) (fst z', snd z') p q) =
q
  destruct p, q.
A, B: Type
z, z': A * B
ap snd (path_prod (fst z, snd z) (fst z, snd z) 1 1) =
1
  reflexivity.
Defined.

Definition ap_snd_path_prod' {A B : Type} {x x' : A} {y y' : B}
  (p : x = x') (q : y = y')
  : ap snd (path_prod' p q) = q.
A, B: Type
x, x': A
y, y': B
p: x = x'
q: y = y'
ap snd (path_prod' p q) = q
Proof.
A, B: Type
x, x': A
y, y': B
p: x = x'
q: y = y'
ap snd (path_prod' p q) = q
  apply ap_snd_path_prod.
Defined.

Definition eta_path_prod {A B : Type} {z z' : A * B} (p : z = z') :
  path_prod _ _(ap fst p) (ap snd p) = p.
A, B: Type
z, z': A * B
p: z = z'
path_prod z z' (ap fst p) (ap snd p) = p
Proof.
A, B: Type
z, z': A * B
p: z = z'
path_prod z z' (ap fst p) (ap snd p) = p
  destruct p.
A, B: Type
z: A * B
path_prod z z (ap fst 1) (ap snd 1) = 1 reflexivity.
Defined.

Definition ap_path_prod {A B C : Type} (f : A -> B -> C)
           {z z' : A * B} (p : fst z = fst z') (q : snd z = snd z')
: ap (fun z => f (fst z) (snd z)) (path_prod _ _ p q)
  = ap011 f p q.
A, B, C: Type
f: A -> B -> C
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap (fun z : A * B => f (fst z) (snd z))
  (path_prod z z' p q) = ap011 f p q
Proof.
A, B, C: Type
f: A -> B -> C
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap (fun z : A * B => f (fst z) (snd z))
  (path_prod z z' p q) = ap011 f p q
  destruct z, z'; simpl in *; destruct p, q; reflexivity.
Defined.

(** Now we show how these compute with transport. *)

Lemma transport_path_prod_uncurried {A B} (P : A * B -> Type) {x y : A * B}
      (H : (fst x = fst y) * (snd x = snd y))
      (Px : P x)
: transport P (path_prod_uncurried _ _ H) Px
  = transport (fun x => P (x, snd y))
              (fst H)
              (transport (fun y => P (fst x, y))
                         (snd H)
                         Px).
A, B: Type
P: A * B -> Type
x, y: A * B
H: (fst x = fst y) * (snd x = snd y)
Px: P x
transport P (path_prod_uncurried x y H) Px =
transport (fun x : A => P (x, snd y)) (fst H)
  (transport (fun y : B => P (fst x, y)) (snd H) Px)
Proof.
A, B: Type
P: A * B -> Type
x, y: A * B
H: (fst x = fst y) * (snd x = snd y)
Px: P x
transport P (path_prod_uncurried x y H) Px =
transport (fun x : A => P (x, snd y)) (fst H)
  (transport (fun y : B => P (fst x, y)) (snd H) Px)
  destruct x, y, H; simpl in *.
A, B: Type
P: A * B -> Type
fst: A
snd: B
fst0: A
snd0: B
fst1: fst = fst0
snd1: snd = snd0
Px: P (fst, snd)
transport P
  match
    fst1 in (_ = a) return ((fst, snd) = (a, snd0))
  with
  | 1 =>
      match
        snd1 in (_ = b) return ((fst, snd) = (fst, b))
      with
      | 1 => 1
      end
  end Px =
transport (fun x : A => P (x, snd0)) fst1
  (transport (fun y : B => P (fst, y)) snd1 Px)
  path_induction.
A, B: Type
P: A * B -> Type
fst: A
snd: B
Px: P (fst, snd)
transport P 1 Px =
transport (fun x : A => P (x, snd)) 1
  (transport (fun y : B => P (fst, y)) 1 Px)
  reflexivity.
Defined.

Definition transport_path_prod {A B} (P : A * B -> Type) {x y : A * B}
           (HA : fst x = fst y)
           (HB : snd x = snd y)
           (Px : P x)
: transport P (path_prod _ _ HA HB) Px
  = transport (fun x => P (x, snd y))
              HA
              (transport (fun y => P (fst x, y))
                         HB
                         Px)
  := transport_path_prod_uncurried P (HA, HB) Px.

Definition transport_path_prod'
           {A B} (P : A * B -> Type)
           {x y : A}
           {x' y' : B}
           (HA : x = y)
           (HB : x' = y')
           (Px : P (x,x'))
: transport P (path_prod' HA HB) Px
  = transport (fun x => P (x, y'))
              HA
              (transport (fun y => P (x, y))
                         HB
                         Px)
  := @transport_path_prod _ _ P (x, x') (y, y') HA HB Px.

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

Global Instance isequiv_path_prod {A B : Type} {z z' : A * B}
: IsEquiv (path_prod_uncurried z z') | 0.
A, B: Type
z, z': A * B
IsEquiv (path_prod_uncurried z z')
Proof.
A, B: Type
z, z': A * B
IsEquiv (path_prod_uncurried z z')
  refine (Build_IsEquiv _ _ _
            (fun r => (ap fst r, ap snd r))
            eta_path_prod
            (fun pq => path_prod'
                         (ap_fst_path_prod (fst pq) (snd pq))
                         (ap_snd_path_prod (fst pq) (snd pq)))
            _).
A, B: Type
z, z': A * B
forall x : (fst z = fst z') * (snd z = snd z'),
eta_path_prod (path_prod_uncurried z z' x) =
ap (path_prod_uncurried z z')
  (path_prod' (ap_fst_path_prod (fst x) (snd x))
     (ap_snd_path_prod (fst x) (snd x)))
  destruct z as [x y], z' as [x' y'].
A, B: Type
x: A
y: B
x': A
y': B
forall
x0 : (fst (x, y) = fst (x', y')) *
     (snd (x, y) = snd (x', y')),
eta_path_prod (path_prod_uncurried (x, y) (x', y') x0) =
ap (path_prod_uncurried (x, y) (x', y'))
  (path_prod' (ap_fst_path_prod (fst x0) (snd x0))
     (ap_snd_path_prod (fst x0) (snd x0)))
  intros [p q]; simpl in p, q.
A, B: Type
x: A
y: B
x': A
y': B
p: x = x'
q: y = y'
eta_path_prod
  (path_prod_uncurried (x, y) (x', y') (p, q)) =
ap (path_prod_uncurried (x, y) (x', y'))
  (path_prod'
     (ap_fst_path_prod (fst (p, q)) (snd (p, q)))
     (ap_snd_path_prod (fst (p, q)) (snd (p, q))))
  destruct p, q; reflexivity.
Defined.

Definition equiv_path_prod {A B : Type} (z z' : A * B)
  : (fst z = fst z') * (snd z = snd z')  <~>  (z = z')
  := Build_Equiv _ _ (path_prod_uncurried z z') _.

(** Path algebra *)

(** Composition.  The next three lemma are displayed equations in section 2.6 of the book, but they have no numbers so we can't put them into [HoTTBook.v]. *)
Definition path_prod_pp {A B : Type} (z z' z'' : A * B)
           (p : fst z = fst z') (p' : fst z' = fst z'')
           (q : snd z = snd z') (q' : snd z' = snd z'')
: path_prod z z'' (p @ p') (q @ q') = path_prod z z' p q @ path_prod z' z'' p' q'.
A, B: Type
z, z', z'': A * B
p: fst z = fst z'
p': fst z' = fst z''
q: snd z = snd z'
q': snd z' = snd z''
path_prod z z'' (p @ p') (q @ q') =
path_prod z z' p q @ path_prod z' z'' p' q'
Proof.
A, B: Type
z, z', z'': A * B
p: fst z = fst z'
p': fst z' = fst z''
q: snd z = snd z'
q': snd z' = snd z''
path_prod z z'' (p @ p') (q @ q') =
path_prod z z' p q @ path_prod z' z'' p' q'
  destruct z, z', z''; simpl in *; destruct p, p', q, q'.
A, B: Type
fst: A
snd: B
path_prod (fst, snd) (fst, snd) (1 @ 1) (1 @ 1) =
path_prod (fst, snd) (fst, snd) 1 1 @
path_prod (fst, snd) (fst, snd) 1 1
  reflexivity.
Defined.

(** Associativity *)
Definition path_prod_pp_p  {A B : Type} (u v z w : A * B)
           (p : fst u = fst v) (q : fst v = fst z) (r : fst z = fst w)
           (p' : snd u = snd v) (q' : snd v = snd z) (r' : snd z = snd w)
: path_prod_pp u z w (p @ q) r (p' @ q') r'
  @ whiskerR (path_prod_pp u v z p q p' q') (path_prod z w r r')
  @ concat_pp_p (path_prod u v p p') (path_prod v z q q') (path_prod z w r r')
  = ap011 (path_prod u w) (concat_pp_p p q r) (concat_pp_p p' q' r')
    @ path_prod_pp u v w p (q @ r) p' (q' @ r')
    @ whiskerL (path_prod u v p p') (path_prod_pp v z w q r q' r').
A, B: Type
u, v, z, w: A * B
p: fst u = fst v
q: fst v = fst z
r: fst z = fst w
p': snd u = snd v
q': snd v = snd z
r': snd z = snd w
(path_prod_pp u z w (p @ q) r (p' @ q') r' @
 whiskerR (path_prod_pp u v z p q p' q')
   (path_prod z w r r')) @
concat_pp_p (path_prod u v p p') (path_prod v z q q')
  (path_prod z w r r') =
(ap011 (path_prod u w) (concat_pp_p p q r)
   (concat_pp_p p' q' r') @
 path_prod_pp u v w p (q @ r) p' (q' @ r')) @
whiskerL (path_prod u v p p')
  (path_prod_pp v z w q r q' r')
Proof.
A, B: Type
u, v, z, w: A * B
p: fst u = fst v
q: fst v = fst z
r: fst z = fst w
p': snd u = snd v
q': snd v = snd z
r': snd z = snd w
(path_prod_pp u z w (p @ q) r (p' @ q') r' @
 whiskerR (path_prod_pp u v z p q p' q')
   (path_prod z w r r')) @
concat_pp_p (path_prod u v p p') (path_prod v z q q')
  (path_prod z w r r') =
(ap011 (path_prod u w) (concat_pp_p p q r)
   (concat_pp_p p' q' r') @
 path_prod_pp u v w p (q @ r) p' (q' @ r')) @
whiskerL (path_prod u v p p')
  (path_prod_pp v z w q r q' r')
  destruct u, v, z, w; simpl in *; destruct p, p', q, q', r, r'.
A, B: Type
fst: A
snd: B
(path_prod_pp (fst, snd) (fst, snd) (fst, snd) (1 @ 1)
   1 (1 @ 1) 1 @
 whiskerR
   (path_prod_pp (fst, snd) (fst, snd) (fst, snd) 1 1
      1 1) (path_prod (fst, snd) (fst, snd) 1 1)) @
concat_pp_p (path_prod (fst, snd) (fst, snd) 1 1)
  (path_prod (fst, snd) (fst, snd) 1 1)
  (path_prod (fst, snd) (fst, snd) 1 1) =
(ap011 (path_prod (fst, snd) (fst, snd))
   (concat_pp_p 1 1 1) (concat_pp_p 1 1 1) @
 path_prod_pp (fst, snd) (fst, snd) (fst, snd) 1
   (1 @ 1) 1 (1 @ 1)) @
whiskerL (path_prod (fst, snd) (fst, snd) 1 1)
  (path_prod_pp (fst, snd) (fst, snd) (fst, snd) 1 1 1
     1)
  reflexivity.
Defined.

(** Inversion *)
Definition path_prod_V {A B : Type} (u v: A * B)
           (p : fst u = fst v)
           (q : snd u = snd v)
  : path_prod v u p^ q^ = (path_prod u v p q)^.
A, B: Type
u, v: A * B
p: fst u = fst v
q: snd u = snd v
path_prod v u p^ q^ = (path_prod u v p q)^
Proof.
A, B: Type
u, v: A * B
p: fst u = fst v
q: snd u = snd v
path_prod v u p^ q^ = (path_prod u v p q)^
  destruct u, v; simpl in *; destruct p, q.
A, B: Type
fst: A
snd: B
path_prod (fst, snd) (fst, snd) 1^ 1^ =
(path_prod (fst, snd) (fst, snd) 1 1)^
  reflexivity.
Defined.

(** ** Transport *)

Definition transport_prod {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
  (z : P a * Q a)
  : transport (fun a => P a * Q a) p z  =  (p # (fst z), p # (snd z))
  := match p with idpath => 1 end.

(** ** Functorial action *)

Definition functor_prod {A A' B B' : Type} (f:A->A') (g:B->B')
  : A * B -> A' * B'
  := fun z => (f (fst z), g (snd z)).

Definition ap_functor_prod {A A' B B' : Type} (f:A->A') (g:B->B')
  (z z' : A * B) (p : fst z = fst z') (q : snd z = snd z')
  : ap (functor_prod f g) (path_prod _ _ p q)
  = path_prod (functor_prod f g z) (functor_prod f g z') (ap f p) (ap g q).
A, A', B, B': Type
f: A -> A'
g: B -> B'
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap (functor_prod f g) (path_prod z z' p q) =
path_prod (functor_prod f g z) (functor_prod f g z')
  (ap f p) (ap g q)
Proof.
A, A', B, B': Type
f: A -> A'
g: B -> B'
z, z': A * B
p: fst z = fst z'
q: snd z = snd z'
ap (functor_prod f g) (path_prod z z' p q) =
path_prod (functor_prod f g z) (functor_prod f g z')
  (ap f p) (ap g q)
  destruct z as [a b]; destruct z' as [a' b'].
A, A', B, B': Type
f: A -> A'
g: B -> B'
a: A
b: B
a': A
b': B
p: fst (a, b) = fst (a', b')
q: snd (a, b) = snd (a', b')
ap (functor_prod f g) (path_prod (a, b) (a', b') p q) =
path_prod (functor_prod f g (a, b))
  (functor_prod f g (a', b')) (ap f p) (ap g q)
  simpl in p, q.
A, A', B, B': Type
f: A -> A'
g: B -> B'
a: A
b: B
a': A
b': B
p: a = a'
q: b = b'
ap (functor_prod f g) (path_prod (a, b) (a', b') p q) =
path_prod (functor_prod f g (a, b))
  (functor_prod f g (a', b')) (ap f p) (ap g q) destruct p, q.
A, A', B, B': Type
f: A -> A'
g: B -> B'
a: A
b: B
ap (functor_prod f g) (path_prod (a, b) (a, b) 1 1) =
path_prod (functor_prod f g (a, b))
  (functor_prod f g (a, b)) (ap f 1) (ap g 1) reflexivity.
Defined.

(** ** Equivalences *)

Global Instance isequiv_functor_prod `{IsEquiv A A' f} `{IsEquiv B B' g}
: IsEquiv (functor_prod f g) | 1000.
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
IsEquiv (functor_prod f g)
Proof.
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
IsEquiv (functor_prod f g)
  refine (Build_IsEquiv
            _ _ (functor_prod f g) (functor_prod f^-1 g^-1)
            (fun z => path_prod' (eisretr f (fst z)) (eisretr g (snd z))
                      @ eta_prod z)
            (fun w => path_prod' (eissect f (fst w)) (eissect g (snd w))
                      @ eta_prod w)
            _).
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
forall x : A * B,
path_prod' (eisretr f (fst (functor_prod f g x)))
  (eisretr g (snd (functor_prod f g x))) @
eta_prod (functor_prod f g x) =
ap (functor_prod f g)
  (path_prod' (eissect f (fst x)) (eissect g (snd x)) @
   eta_prod x)
  intros [a b]; simpl.
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
a: A
b: B
path_prod' (eisretr f (f a)) (eisretr g (g b)) @ 1 =
ap (functor_prod f g)
  (path_prod' (eissect f a) (eissect g b) @ 1)
  unfold path_prod'.
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
a: A
b: B
path_prod (f (f^-1 (f a)), g (g^-1 (g b))) (f a, g b)
  (eisretr f (f a)) (eisretr g (g b)) @ 1 =
ap (functor_prod f g)
  (path_prod (f^-1 (f a), g^-1 (g b)) (a, b)
     (eissect f a) (eissect g b) @ 1)
  rewrite !concat_p1.
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
a: A
b: B
path_prod (f (f^-1 (f a)), g (g^-1 (g b))) (f a, g b)
  (eisretr f (f a)) (eisretr g (g b)) =
ap (functor_prod f g)
  (path_prod (f^-1 (f a), g^-1 (g b)) (a, b)
     (eissect f a) (eissect g b))
  rewrite ap_functor_prod.
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
a: A
b: B
path_prod (f (f^-1 (f a)), g (g^-1 (g b))) (f a, g b)
  (eisretr f (f a)) (eisretr g (g b)) =
path_prod (functor_prod f g (f^-1 (f a), g^-1 (g b)))
  (functor_prod f g (a, b)) (ap f (eissect f a))
  (ap g (eissect g b))
  rewrite !eisadj.
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
a: A
b: B
path_prod (f (f^-1 (f a)), g (g^-1 (g b))) (f a, g b)
  (ap f (eissect f a)) (ap g (eissect g b)) =
path_prod (functor_prod f g (f^-1 (f a), g^-1 (g b)))
  (functor_prod f g (a, b)) (ap f (eissect f a))
  (ap g (eissect g b))
  reflexivity.
Defined.

Definition equiv_functor_prod `{IsEquiv A A' f} `{IsEquiv B B' g}
  : A * B <~> A' * B'.
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
A * B <~> A' * B'
Proof.
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
A * B <~> A' * B'
  exists (functor_prod f g).
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
IsEquiv (functor_prod f g)
  exact _. (* i.e., search the context for instances *)
Defined.

Definition equiv_functor_prod' {A A' B B' : Type} (f : A <~> A') (g : B <~> B')
  : A * B <~> A' * B'.
A, A', B, B': Type
f: A <~> A'
g: B <~> B'
A * B <~> A' * B'
Proof.
A, A', B, B': Type
f: A <~> A'
g: B <~> B'
A * B <~> A' * B'
  exists (functor_prod f g).
A, A', B, B': Type
f: A <~> A'
g: B <~> B'
IsEquiv (functor_prod f g)
  exact _.
Defined.

Notation "f *E g" := (equiv_functor_prod' f g) : equiv_scope.

Definition equiv_functor_prod_l {A B B' : Type} (g : B <~> B')
  : A * B <~> A * B'
  := 1 *E g.

Definition equiv_functor_prod_r {A A' B : Type} (f : A <~> A')
  : A * B <~> A' * B
  := f *E 1.

(** ** Logical equivalences *)

Definition iff_functor_prod {A A' B B' : Type} (f : A <-> A') (g : B <-> B')
  : A * B <-> A' * B'
  := (functor_prod (fst f) (fst g) , functor_prod (snd f) (snd g)).

(** ** Symmetry *)

(** This is a special property of [prod], of course, not an instance of a general family of facts about types. *)

Definition equiv_prod_symm (A B : Type) : A * B <~> B * A.
A, B: Type
A * B <~> B * A
Proof.
A, B: Type
A * B <~> B * A
  make_equiv.
Defined.

(** ** Associativity *)

(** This, too, is a special property of [prod], of course, not an instance of a general family of facts about types. *)
Definition equiv_prod_assoc (A B C : Type) : A * (B * C) <~> (A * B) * C.
A, B, C: Type
A * (B * C) <~> A * B * C
Proof.
A, B, C: Type
A * (B * C) <~> A * B * C
  make_equiv.
Defined.

(** ** Unit and annihilation *)

Definition prod_empty_r X : X * Empty <~> Empty
  := (Build_Equiv _ _ snd _).

Definition prod_empty_l X : Empty * X <~> Empty
  := (Build_Equiv _ _ fst _).

Definition prod_unit_r X : X * Unit <~> X.
X: Type
X * Unit <~> X
Proof.
X: Type
X * Unit <~> X
  refine (Build_Equiv _ _ fst _).
X: Type
IsEquiv fst
  simple refine (Build_IsEquiv _ _ _ (fun x => (x,tt)) _ _ _).
X: Type
fst o (fun x : X => (x, tt)) == idmap
X: Type
(fun x : X => (x, tt)) o fst == idmap
X: Type
forall x : X * Unit,
?eisretr (fst x) = ap fst (?eissect x)
  -
X: Type
fst o (fun x : X => (x, tt)) == idmap intros x; reflexivity.
  -
X: Type
(fun x : X => (x, tt)) o fst == idmap intros [x []]; reflexivity.
  -
X: Type
forall x : X * Unit,
((fun x0 : X => 1)
 :
 fst o (fun x0 : X => (x0, tt)) == idmap) (fst x) =
ap fst
  (((fun x0 : X * Unit =>
     (fun (x1 : X) (snd : Unit) =>
      match
        snd as u return ((fst (x1, u), tt) = (x1, u))
      with
      | tt => 1
      end) (fst x0) (snd x0))
    :
    (fun x0 : X => (x0, tt)) o fst == idmap) x) intros [x []]; reflexivity.
Defined.

Definition prod_unit_l X : Unit * X <~> X.
X: Type
Unit * X <~> X
Proof.
X: Type
Unit * X <~> X
  refine (Build_Equiv _ _ snd _).
X: Type
IsEquiv snd
  simple refine (Build_IsEquiv _ _ _ (fun x => (tt,x)) _ _ _).
X: Type
snd o (fun x : X => (tt, x)) == idmap
X: Type
(fun x : X => (tt, x)) o snd == idmap
X: Type
forall x : Unit * X,
?eisretr (snd x) = ap snd (?eissect x)
  -
X: Type
snd o (fun x : X => (tt, x)) == idmap intros x; reflexivity.
  -
X: Type
(fun x : X => (tt, x)) o snd == idmap intros [[] x]; reflexivity.
  -
X: Type
forall x : Unit * X,
((fun x0 : X => 1)
 :
 snd o (fun x0 : X => (tt, x0)) == idmap) (snd x) =
ap snd
  (((fun x0 : Unit * X =>
     (fun fst : Unit =>
      match
        fst as u
        return
          (forall snd0 : X,
           (tt, snd (u, snd0)) = (u, snd0))
      with
      | tt => fun x1 : X => 1
      end) (fst x0) (snd x0))
    :
    (fun x0 : X => (tt, x0)) o snd == idmap) x) intros [[] x]; reflexivity.
Defined.

(** ** Universal mapping properties *)

(** Ordinary universal mapping properties are expressed as equivalences of sets or spaces of functions.  In type theory, we can go beyond this and express an equivalence of types of *dependent* functions.  Moreover, because the product type can expressed both positively and negatively, it has both a left universal property and a right one. *)

(* First the positive universal property. *)
Global Instance isequiv_prod_ind `(P : A * B -> Type)
: IsEquiv (prod_ind P) | 0
  := Build_IsEquiv
       _ _
       (prod_ind P)
       (fun f x y => f (x, y))
       (fun _ => 1)
       (fun _ => 1)
       (fun _ => 1).

Definition equiv_prod_ind `(P : A * B -> Type)
  : (forall (a : A) (b : B), P (a, b)) <~> (forall p : A * B, P p)
  := Build_Equiv _ _ (prod_ind P) _.

(* The non-dependent version, which is a special case, is the currying equivalence. *)
Definition equiv_uncurry (A B C : Type)
  : (A -> B -> C) <~> (A * B -> C)
  := equiv_prod_ind (fun _ => C).

(* Now the negative universal property. *)
Definition prod_coind_uncurried `{A : X -> Type} `{B : X -> Type}
  : (forall x, A x) * (forall x, B x) -> (forall x, A x * B x)
  := fun fg x => (fst fg x, snd fg x).

Definition prod_coind `(f : forall x:X, A x) `(g : forall x:X, B x)
  : forall x, A x * B x
  := prod_coind_uncurried (f, g).

Global Instance isequiv_prod_coind `(A : X -> Type) (B : X -> Type)
: IsEquiv (@prod_coind_uncurried X A B) | 0
  := Build_IsEquiv
       _ _
       (@prod_coind_uncurried X A B)
       (fun h => (fun x => fst (h x), fun x => snd (h x)))
       (fun _ => 1)
       (fun _ => 1)
       (fun _ => 1).

Definition equiv_prod_coind `(A : X -> Type) (B : X -> Type)
  : ((forall x, A x) * (forall x, B x)) <~> (forall x, A x * B x)
  := Build_Equiv _ _ (@prod_coind_uncurried X A B) _.

(** ** Products preserve truncation *)

Global Instance istrunc_prod `{IsTrunc n A} `{IsTrunc n B} : IsTrunc n (A * B) | 100.
A: Type
n: trunc_index
IsTrunc0: IsTrunc n A
B: Type
IsTrunc1: IsTrunc n B
IsTrunc n (A * B)
Proof.
A: Type
n: trunc_index
IsTrunc0: IsTrunc n A
B: Type
IsTrunc1: IsTrunc n B
IsTrunc n (A * B)
  generalize dependent B; generalize dependent A.
n: trunc_index
forall A : Type,
IsTrunc n A ->
forall B : Type, IsTrunc n B -> IsTrunc n (A * B)
  simple_induction n n IH; simpl; (intros A ? B ?).
A: Type
IsTrunc0: Contr A
B: Type
IsTrunc1: Contr B
Contr (A * B)
n: trunc_index
IH: forall A : Type,
IsTrunc n A ->
forall B : Type, IsTrunc n B -> IsTrunc n (A * B)
A: Type
IsTrunc0: IsTrunc n.+1 A
B: Type
IsTrunc1: IsTrunc n.+1 B
IsTrunc n.+1 (A * B)
  {
A: Type
IsTrunc0: Contr A
B: Type
IsTrunc1: Contr B
Contr (A * B) apply (Build_Contr _ (center A, center B)).
A: Type
IsTrunc0: Contr A
B: Type
IsTrunc1: Contr B
forall y : A * B, (center A, center B) = y
    intros z; apply path_prod; apply contr. }
n: trunc_index
IH: forall A : Type,
IsTrunc n A ->
forall B : Type, IsTrunc n B -> IsTrunc n (A * B)
A: Type
IsTrunc0: IsTrunc n.+1 A
B: Type
IsTrunc1: IsTrunc n.+1 B
IsTrunc n.+1 (A * B)
  apply istrunc_S.
n: trunc_index
IH: forall A : Type,
IsTrunc n A ->
forall B : Type, IsTrunc n B -> IsTrunc n (A * B)
A: Type
IsTrunc0: IsTrunc n.+1 A
B: Type
IsTrunc1: IsTrunc n.+1 B
forall x y : A * B, IsTrunc n (x = y)
  intros x y.
n: trunc_index
IH: forall A : Type,
IsTrunc n A ->
forall B : Type, IsTrunc n B -> IsTrunc n (A * B)
A: Type
IsTrunc0: IsTrunc n.+1 A
B: Type
IsTrunc1: IsTrunc n.+1 B
x, y: A * B
IsTrunc n (x = y)
  exact (istrunc_equiv_istrunc _ (equiv_path_prod x y)).
Defined.

Global Instance contr_prod `{CA : Contr A} `{CB : Contr B} : Contr (A * B) | 100
  := istrunc_prod.

(** ** Decidability *)

Global Instance decidable_prod {A B : Type}
       `{Decidable A} `{Decidable B}
: Decidable (A * B).
A, B: Type
H: Decidable A
H0: Decidable B
Decidable (A * B)
Proof.
A, B: Type
H: Decidable A
H0: Decidable B
Decidable (A * B)
  destruct (dec A) as [x1|y1]; destruct (dec B) as [x2|y2].
A, B: Type
H: Decidable A
H0: Decidable B
x1: A
x2: B
Decidable (A * B)
A, B: Type
H: Decidable A
H0: Decidable B
x1: A
y2: ~ B
Decidable (A * B)
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
x2: B
Decidable (A * B)
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
y2: ~ B
Decidable (A * B)
  -
A, B: Type
H: Decidable A
H0: Decidable B
x1: A
x2: B
Decidable (A * B) exact (inl (x1,x2)).
  -
A, B: Type
H: Decidable A
H0: Decidable B
x1: A
y2: ~ B
Decidable (A * B) apply inr; intros [_ x2]; exact (y2 x2).
  -
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
x2: B
Decidable (A * B) apply inr; intros [x1 _]; exact (y1 x1).
  -
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
y2: ~ B
Decidable (A * B) apply inr; intros [x1 _]; exact (y1 x1).
Defined.

(** Interaction of ap and uncurry *)

(* The function in ap011 can be uncurried *)
Definition ap_uncurry {A B C} (f : A -> B -> C) {a a' : A} (p : a = a')
  {b b' : B} (q : b = b')
  : ap (uncurry f) (path_prod' p q) = ap011 f p q.
A, B, C: Type
f: A -> B -> C
a, a': A
p: a = a'
b, b': B
q: b = b'
ap (uncurry f) (path_prod' p q) = ap011 f p q
Proof.
A, B, C: Type
f: A -> B -> C
a, a': A
p: a = a'
b, b': B
q: b = b'
ap (uncurry f) (path_prod' p q) = ap011 f p q
  by destruct q, p.
Defined.

(** Fibers *)

(** ** Fibers of [functor_prod] *)
Definition hfiber_functor_prod {A B C D : Type} (f : A -> B) (g : C -> D) y
  : hfiber (functor_prod f g) y <~> (hfiber f (fst y) * hfiber g (snd y)).
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
hfiber (functor_prod f g) y <~>
hfiber f (fst y) * hfiber g (snd y)
Proof.
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
hfiber (functor_prod f g) y <~>
hfiber f (fst y) * hfiber g (snd y)
  unfold functor_prod.
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
hfiber (fun z : A * C => (f (fst z), g (snd z))) y <~>
hfiber f (fst y) * hfiber g (snd y)
  snrefine (equiv_adjointify _ _ _ _).
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
hfiber (fun z : A * C => (f (fst z), g (snd z))) y ->
hfiber f (fst y) * hfiber g (snd y)
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
hfiber f (fst y) * hfiber g (snd y) ->
hfiber (fun z : A * C => (f (fst z), g (snd z))) y
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
?f o ?g == idmap
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
?g o ?f == idmap
  -
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
hfiber (fun z : A * C => (f (fst z), g (snd z))) y ->
hfiber f (fst y) * hfiber g (snd y) exact (fun x => ((fst x.1; ap fst x.2), (snd x.1; ap snd x.2))).
  -
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
hfiber f (fst y) * hfiber g (snd y) ->
hfiber (fun z : A * C => (f (fst z), g (snd z))) y refine (fun xs => (((fst xs).1, (snd xs).1); _)).
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
xs: hfiber f (fst y) * hfiber g (snd y)
(f (fst ((fst xs).1, (snd xs).1)),
g (snd ((fst xs).1, (snd xs).1))) = y
    apply Prod.path_prod;simpl.
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
xs: hfiber f (fst y) * hfiber g (snd y)
f (fst xs).1 = fst y
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
xs: hfiber f (fst y) * hfiber g (snd y)
g (snd xs).1 = snd y
    +
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
xs: hfiber f (fst y) * hfiber g (snd y)
f (fst xs).1 = fst y exact (fst xs).2.
    +
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
xs: hfiber f (fst y) * hfiber g (snd y)
g (snd xs).1 = snd y exact (snd xs).2.
  -
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
(fun
   x : hfiber
         (fun z : A * C => (f (fst z), g (snd z))) y
 => ((fst x.1; ap fst x.2), (snd x.1; ap snd x.2)))
o (fun xs : hfiber f (fst y) * hfiber g (snd y) =>
   (((fst xs).1, (snd xs).1);
   path_prod
     (f (fst ((fst xs).1, (snd xs).1)),
     g (snd ((fst xs).1, (snd xs).1))) y
     ((fst xs).2
      :
      fst
        (f (fst ((fst xs).1, (snd xs).1)),
        g (snd ((fst xs).1, (snd xs).1))) = fst y)
     ((snd xs).2
      :
      snd
        (f (fst ((fst xs).1, (snd xs).1)),
        g (snd ((fst xs).1, (snd xs).1))) = snd y))) ==
idmap destruct y as [y1 y2]; intros [[x1 p1] [x2 p2]].
A, B, C, D: Type
f: A -> B
g: C -> D
y1: B
y2: D
x1: A
p1: f x1 = fst (y1, y2)
x2: C
p2: g x2 = snd (y1, y2)
((fst
    (((fst ((x1; p1), (x2; p2))).1,
     (snd ((x1; p1), (x2; p2))).1);
    path_prod
      (f
         (fst
            ((fst ((x1; p1), (x2; p2))).1,
            (snd ((x1; p1), (x2; p2))).1)),
      g
        (snd
           ((fst ((x1; p1), (x2; p2))).1,
           (snd ((x1; p1), (x2; p2))).1))) (y1, y2)
      (fst ((x1; p1), (x2; p2))).2
      (snd ((x1; p1), (x2; p2))).2).1;
 ap fst
   (((fst ((x1; p1), (x2; p2))).1,
    (snd ((x1; p1), (x2; p2))).1);
   path_prod
     (f
        (fst
           ((fst ((x1; p1), (x2; p2))).1,
           (snd ((x1; p1), (x2; p2))).1)),
     g
       (snd
          ((fst ((x1; p1), (x2; p2))).1,
          (snd ((x1; p1), (x2; p2))).1))) (y1, y2)
     (fst ((x1; p1), (x2; p2))).2
     (snd ((x1; p1), (x2; p2))).2).2),
(snd
   (((fst ((x1; p1), (x2; p2))).1,
    (snd ((x1; p1), (x2; p2))).1);
   path_prod
     (f
        (fst
           ((fst ((x1; p1), (x2; p2))).1,
           (snd ((x1; p1), (x2; p2))).1)),
     g
       (snd
          ((fst ((x1; p1), (x2; p2))).1,
          (snd ((x1; p1), (x2; p2))).1))) (y1, y2)
     (fst ((x1; p1), (x2; p2))).2
     (snd ((x1; p1), (x2; p2))).2).1;
ap snd
  (((fst ((x1; p1), (x2; p2))).1,
   (snd ((x1; p1), (x2; p2))).1);
  path_prod
    (f
       (fst
          ((fst ((x1; p1), (x2; p2))).1,
          (snd ((x1; p1), (x2; p2))).1)),
    g
      (snd
         ((fst ((x1; p1), (x2; p2))).1,
         (snd ((x1; p1), (x2; p2))).1))) (y1, y2)
    (fst ((x1; p1), (x2; p2))).2
    (snd ((x1; p1), (x2; p2))).2).2)) =
((x1; p1), (x2; p2))
    simpl in *.
A, B, C, D: Type
f: A -> B
g: C -> D
y1: B
y2: D
x1: A
p1: f x1 = y1
x2: C
p2: g x2 = y2
((x1; ap fst (path_prod (f x1, g x2) (y1, y2) p1 p2)),
(x2; ap snd (path_prod (f x1, g x2) (y1, y2) p1 p2))) =
((x1; p1), (x2; p2)) destruct p1,p2.
A, B, C, D: Type
f: A -> B
g: C -> D
x1: A
x2: C
((x1;
 ap fst (path_prod (f x1, g x2) (f x1, g x2) 1 1)),
(x2; ap snd (path_prod (f x1, g x2) (f x1, g x2) 1 1))) =
((x1; 1), (x2; 1)) reflexivity.
  -
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
(fun xs : hfiber f (fst y) * hfiber g (snd y) =>
 (((fst xs).1, (snd xs).1);
 path_prod
   (f (fst ((fst xs).1, (snd xs).1)),
   g (snd ((fst xs).1, (snd xs).1))) y
   ((fst xs).2
    :
    fst
      (f (fst ((fst xs).1, (snd xs).1)),
      g (snd ((fst xs).1, (snd xs).1))) = fst y)
   ((snd xs).2
    :
    snd
      (f (fst ((fst xs).1, (snd xs).1)),
      g (snd ((fst xs).1, (snd xs).1))) = snd y)))
o (fun
     x : hfiber
           (fun z : A * C => (f (fst z), g (snd z))) y
   => ((fst x.1; ap fst x.2), (snd x.1; ap snd x.2))) ==
idmap intros [[x1 x2] p].
A, B, C, D: Type
f: A -> B
g: C -> D
y: B * D
x1: A
x2: C
p: (f (fst (x1, x2)), g (snd (x1, x2))) = y
(((fst
     ((fst ((x1, x2); p).1; ap fst ((x1, x2); p).2),
     (snd ((x1, x2); p).1; ap snd ((x1, x2); p).2))).1,
 (snd
    ((fst ((x1, x2); p).1; ap fst ((x1, x2); p).2),
    (snd ((x1, x2); p).1; ap snd ((x1, x2); p).2))).1);
path_prod
  (f
     (fst
        ((fst
            ((fst ((x1, x2); p).1;
             ap fst ((x1, x2); p).2),
            (snd ((x1, x2); p).1;
            ap snd ((x1, x2); p).2))).1,
        (snd
           ((fst ((x1, x2); p).1;
            ap fst ((x1, x2); p).2),
           (snd ((x1, x2); p).1;
           ap snd ((x1, x2); p).2))).1)),
  g
    (snd
       ((fst
           ((fst ((x1, x2); p).1;
            ap fst ((x1, x2); p).2),
           (snd ((x1, x2); p).1;
           ap snd ((x1, x2); p).2))).1,
       (snd
          ((fst ((x1, x2); p).1;
           ap fst ((x1, x2); p).2),
          (snd ((x1, x2); p).1;
          ap snd ((x1, x2); p).2))).1))) y
  (fst
     ((fst ((x1, x2); p).1; ap fst ((x1, x2); p).2),
     (snd ((x1, x2); p).1; ap snd ((x1, x2); p).2))).2
  (snd
     ((fst ((x1, x2); p).1; ap fst ((x1, x2); p).2),
     (snd ((x1, x2); p).1; ap snd ((x1, x2); p).2))).2) =
((x1, x2); p) destruct p;cbn.
A, B, C, D: Type
f: A -> B
g: C -> D
x1: A
x2: C
((x1, x2); 1) = ((x1, x2); 1) reflexivity.
Defined.

Global Instance istruncmap_functor_prod (n : trunc_index) {A B C D : Type}
  (f : A -> B) (g : C -> D) `{!IsTruncMap n f} `{!IsTruncMap n g}
  : IsTruncMap n (Prod.functor_prod f g)
  := fun y => istrunc_equiv_istrunc _ (hfiber_functor_prod _ _ _)^-1.