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

Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids
               Basics.Tactics Basics.Contractible.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Require Export Basics.Trunc (istrunc_forall).

Local Open Scope path_scope.


Generalizable Variables A B C f g e n.

Section AssumeFunext.
Context `{Funext}.

(** ** Paths *)

(** Paths [p : f = g] in a function type [forall x:X, P x] are equivalent to functions taking values in path types, [H : forall x:X, f x = g x], or concisely, [H : f == g].

This equivalence, however, is just the combination of [apD10] and function extensionality [funext], and as such, [path_forall], et seq. are given in the [Overture]:  *)

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

Definition apD10_path_forall `{P : A -> Type}
  (f g : forall x, P x) (h : f == g)
  : apD10 (path_forall _ _ h) == h
  := apD10 (eisretr apD10 h).

Definition eta_path_forall `{P : A -> Type}
  (f g : forall x, P x) (p : f = g)
  : path_forall _ _ (apD10 p) = p
  := eissect apD10 p.

Definition path_forall_1 `{P : A -> Type} (f : forall x, P x)
  : (path_forall f f (fun x => 1)) = 1
  := eta_path_forall f f 1.

(** The identification of the path space of a dependent function space, up to equivalence, is of course just funext. *)

Definition equiv_apD10 {A : Type} (P : A -> Type) f g
: (f = g) <~> (f == g)
  := Build_Equiv _ _ (@apD10 A P f g) _.

Global Instance isequiv_path_forall `{P : A -> Type} (f g : forall x, P x)
  : IsEquiv (path_forall f g) | 0
  := @isequiv_inverse _ _ (@apD10 A P f g) _.

Definition equiv_path_forall `{P : A -> Type} (f g : forall x, P x)
  : (f == g)  <~>  (f = g)
  := Build_Equiv _ _ (path_forall f g) _.

Global Arguments equiv_path_forall {A%type_scope P} (f g)%function_scope.

(** ** Path algebra *)

Definition path_forall_pp `{P : A -> Type} (f g h : forall x, P x)
           (p : f == g) (q : g == h)
: path_forall f h (fun x => p x @ q x) = path_forall f g p @ path_forall g h q.
H: Funext
A: Type
P: A -> Type
f, g, h: forall x : A, P x
p: f == g
q: g == h
path_forall f h (fun x : A => p x @ q x) =
path_forall f g p @ path_forall g h q
Proof.
H: Funext
A: Type
P: A -> Type
f, g, h: forall x : A, P x
p: f == g
q: g == h
path_forall f h (fun x : A => p x @ q x) =
path_forall f g p @ path_forall g h q
  revert p q.
H: Funext
A: Type
P: A -> Type
f, g, h: forall x : A, P x
forall (p : f == g) (q : g == h),
path_forall f h (fun x : A => p x @ q x) =
path_forall f g p @ path_forall g h q
  equiv_intro (@apD10 A P f g) p.
H: Funext
A: Type
P: A -> Type
f, g, h: forall x : A, P x
p: f = g
forall q : g == h,
path_forall f h (fun x : A => apD10 p x @ q x) =
path_forall f g (apD10 p) @ path_forall g h q
  equiv_intro (@apD10 A P g h) q.
H: Funext
A: Type
P: A -> Type
f, g, h: forall x : A, P x
p: f = g
q: g = h
path_forall f h (fun x : A => apD10 p x @ apD10 q x) =
path_forall f g (apD10 p) @ path_forall g h (apD10 q)
  transitivity (path_forall f h (apD10 (p @ q))).
H: Funext
A: Type
P: A -> Type
f, g, h: forall x : A, P x
p: f = g
q: g = h
path_forall f h (fun x : A => apD10 p x @ apD10 q x) =
path_forall f h (apD10 (p @ q))
H: Funext
A: Type
P: A -> Type
f, g, h: forall x : A, P x
p: f = g
q: g = h
path_forall f h (apD10 (p @ q)) =
path_forall f g (apD10 p) @ path_forall g h (apD10 q)
  -
H: Funext
A: Type
P: A -> Type
f, g, h: forall x : A, P x
p: f = g
q: g = h
path_forall f h (fun x : A => apD10 p x @ apD10 q x) =
path_forall f h (apD10 (p @ q)) apply ap, path_forall; intros x.
H: Funext
A: Type
P: A -> Type
f, g, h: forall x : A, P x
p: f = g
q: g = h
x: A
apD10 p x @ apD10 q x = apD10 (p @ q) x
    symmetry; apply apD10_pp.
  -
H: Funext
A: Type
P: A -> Type
f, g, h: forall x : A, P x
p: f = g
q: g = h
path_forall f h (apD10 (p @ q)) =
path_forall f g (apD10 p) @ path_forall g h (apD10 q) refine (eta_path_forall _ _ _ @ _).
H: Funext
A: Type
P: A -> Type
f, g, h: forall x : A, P x
p: f = g
q: g = h
p @ q =
path_forall f g (apD10 p) @ path_forall g h (apD10 q)
    apply concat2; symmetry; apply eta_path_forall.
Defined.


Definition path_forall_V `{P : A -> Type} (f g : forall x, P x)
           (p : f == g)
  : path_forall _ _ (fun x => (p x)^) = (path_forall _ _ p)^.
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
path_forall g f (fun x : A => (p x)^) =
(path_forall f g p)^
Proof.
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
path_forall g f (fun x : A => (p x)^) =
(path_forall f g p)^
  transitivity (path_forall _ _ (fun x => (apD10 (path_forall _ _ p) x)^)).
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
path_forall g f (fun x : A => (p x)^) =
path_forall g f
  (fun x : A => (apD10 (path_forall f g p) x)^)
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
path_forall g f
  (fun x : A => (apD10 (path_forall f g p) x)^) =
(path_forall f g p)^
  -
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
path_forall g f (fun x : A => (p x)^) =
path_forall g f
  (fun x : A => (apD10 (path_forall f g p) x)^) f_ap.
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
(fun x : A => (p x)^) =
(fun x : A => (apD10 (path_forall f g p) x)^) symmetry.
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
(fun x : A => (apD10 (path_forall f g p) x)^) =
(fun x : A => (p x)^) apply (@ap _ _ (fun h x => (h x)^)).
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
apD10 (path_forall f g p) = p apply eisretr.
  -
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
path_forall g f
  (fun x : A => (apD10 (path_forall f g p) x)^) =
(path_forall f g p)^ transitivity (path_forall _ _ (apD10 (path_forall _ _ p)^)).
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
path_forall g f
  (fun x : A => (apD10 (path_forall f g p) x)^) =
path_forall g f (apD10 (path_forall f g p)^)
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
path_forall g f (apD10 (path_forall f g p)^) =
(path_forall f g p)^
    +
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
path_forall g f
  (fun x : A => (apD10 (path_forall f g p) x)^) =
path_forall g f (apD10 (path_forall f g p)^) apply ap, inverse.
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
apD10 (path_forall f g p)^ =
(fun x : A => (apD10 (path_forall f g p) x)^) apply path_forall; intros x.
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
x: A
apD10 (path_forall f g p)^ x =
(apD10 (path_forall f g p) x)^ apply apD10_V.
    +
H: Funext
A: Type
P: A -> Type
f, g: forall x : A, P x
p: f == g
path_forall g f (apD10 (path_forall f g p)^) =
(path_forall f g p)^ apply eissect.
Defined.

(** ** Transport *)

(** The concrete description of transport in sigmas and 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 the full Id-elim rule by way of "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_forall
  {A : Type} {P : A -> Type} {C : forall x, P x -> Type}
  {x1 x2 : A} (p : x1 = x2) (f : forall y : P x1, C x1 y)
  : (transport (fun x => forall y : P x, C x y) p f)
    == (fun y =>
       transport (C x2) (transport_pV _ _ _) (transportD _ _ p _ (f (p^ # y))))
  := match p with idpath => fun _ => 1 end.

(** A special case of [transport_forall] where the type [P] does not depend on [A],
    and so it is just a fixed type [B]. *)
Definition transport_forall_constant
  {A B : Type} {C : A -> B -> Type}
  {x1 x2 : A} (p : x1 = x2) (f : forall y : B, C x1 y)
  : (transport (fun x => forall y : B, C x y) p f)
    == (fun y => transport (fun x => C x y) p (f y))
  := match p with idpath => fun _ => 1 end.

Definition apD_transport_forall_constant
  {A B : Type} (C : A -> B -> Type)
  {x1 x2 : A} (p : x1 = x2) (f : forall y : B, C x1 y)
  {y1 y2 : B} (q : y1 = y2)
: apD (transport (fun x => forall y : B, C x y) p f) q
  = ap (transport (C x2) q) (transport_forall_constant p f y1)
    @ transport_transport C p q (f y1)
    @ ap (transport (fun x : A => C x y2) p) (apD f q)
    @ (transport_forall_constant p f y2)^.
H: Funext
A, B: Type
C: A -> B -> Type
x1, x2: A
p: x1 = x2
f: forall y : B, C x1 y
y1, y2: B
q: y1 = y2
apD (transport (fun x : A => forall y : B, C x y) p f)
  q =
((ap (transport (C x2) q)
    (transport_forall_constant p f y1) @
  transport_transport C p q (f y1)) @
 ap (transport (fun x : A => C x y2) p) (apD f q)) @
(transport_forall_constant p f y2)^
Proof.
H: Funext
A, B: Type
C: A -> B -> Type
x1, x2: A
p: x1 = x2
f: forall y : B, C x1 y
y1, y2: B
q: y1 = y2
apD (transport (fun x : A => forall y : B, C x y) p f)
  q =
((ap (transport (C x2) q)
    (transport_forall_constant p f y1) @
  transport_transport C p q (f y1)) @
 ap (transport (fun x : A => C x y2) p) (apD f q)) @
(transport_forall_constant p f y2)^
  destruct p, q; reflexivity.
Defined.

(** ** Maps on paths *)

(** The action of maps given by application. *)
Definition ap_apply_lD {A} {B : A -> Type} {f g : forall x, B x} (p : f = g) (z : A)
  : ap (fun f => f z) p = apD10 p z
:= 1.

Definition ap_apply_lD2 {A} {B : A -> Type} { C : forall x, B x -> Type}
           {f g : forall x y, C x y} (p : f = g) (z1 : A) (z2 : B z1)
  : ap (fun f => f z1 z2) p = apD10 (apD10 p z1) z2.
H: Funext
A: Type
B: A -> Type
C: forall x : A, B x -> Type
f, g: forall (x : A) (y : B x), C x y
p: f = g
z1: A
z2: B z1
ap
  (fun f : forall (x : A) (x0 : B x), C x x0 =>
   f z1 z2) p = apD10 (apD10 p z1) z2
Proof.
H: Funext
A: Type
B: A -> Type
C: forall x : A, B x -> Type
f, g: forall (x : A) (y : B x), C x y
p: f = g
z1: A
z2: B z1
ap
  (fun f : forall (x : A) (x0 : B x), C x x0 =>
   f z1 z2) p = apD10 (apD10 p z1) z2
    by path_induction.
Defined.


(** The action of maps given by lambda. *)
Definition ap_lambdaD {A B : Type} {C : B -> Type} {x y : A} (p : x = y) (M : forall a b, C b) :
  ap (fun a b => M a b) p =
  path_forall _ _ (fun b => ap (fun a => M a b) p).
H: Funext
A, B: Type
C: B -> Type
x, y: A
p: x = y
M: A -> forall b : B, C b
ap (fun (a : A) (b : B) => M a b) p =
path_forall (fun b : B => (fun a : A => M a b) x)
  (fun b : B => (fun a : A => M a b) y)
  (fun b : B => ap (fun a : A => M a b) p)
Proof.
H: Funext
A, B: Type
C: B -> Type
x, y: A
p: x = y
M: A -> forall b : B, C b
ap (fun (a : A) (b : B) => M a b) p =
path_forall (fun b : B => (fun a : A => M a b) x)
  (fun b : B => (fun a : A => M a b) y)
  (fun b : B => ap (fun a : A => M a b) p)
  destruct p;
  symmetry;
  simpl; apply path_forall_1.
Defined.

(** ** Dependent paths *)

(** Usually, a dependent path over [p:x1=x2] in [P:A->Type] between [y1:P x1] and [y2:P x2] is a path [transport P p y1 = y2] in [P x2].  However, when [P] is a function space, these dependent paths have a more convenient description: rather than transporting the argument of [y1] forwards and backwards, we transport only forwards but on both sides of the equation, yielding a "naturality square". *)

Definition dpath_forall
  {A:Type} (B:A -> Type) (C:forall a, B a -> Type) (x1 x2:A) (p:x1=x2)
  (f:forall y1:B x1, C x1 y1) (g:forall (y2:B x2), C x2 y2)
  : (forall (y1:B x1), transportD B C p y1 (f y1) = g (transport B p y1))
  <~>
  (transport (fun x => forall y:B x, C x y) p f = g).
H: Funext
A: Type
B: A -> Type
C: forall a : A, B a -> Type
x1, x2: A
p: x1 = x2
f: forall y1 : B x1, C x1 y1
g: forall y2 : B x2, C x2 y2
(forall y1 : B x1,
 transportD B C p y1 (f y1) = g (transport B p y1)) <~>
transport (fun x : A => forall y : B x, C x y) p f = g
Proof.
H: Funext
A: Type
B: A -> Type
C: forall a : A, B a -> Type
x1, x2: A
p: x1 = x2
f: forall y1 : B x1, C x1 y1
g: forall y2 : B x2, C x2 y2
(forall y1 : B x1,
 transportD B C p y1 (f y1) = g (transport B p y1)) <~>
transport (fun x : A => forall y : B x, C x y) p f = g
  destruct p.
H: Funext
A: Type
B: A -> Type
C: forall a : A, B a -> Type
x1: A
f, g: forall y2 : B x1, C x1 y2
(forall y1 : B x1,
 transportD B C 1 y1 (f y1) = g (transport B 1 y1)) <~>
transport (fun x : A => forall y : B x, C x y) 1 f = g
  apply equiv_path_forall.
Defined.

Definition dpath_forall_constant
  {A B:Type} (C : A -> B -> Type) (x1 x2:A) (p:x1=x2)
  (f:forall (y1:B), C x1 y1) (g:forall (y2:B), C x2 y2)
  : (forall (y1:B), transport (fun x => C x y1) p (f y1) = g y1)
  <~>
  (transport (fun x => forall y:B, C x y) p f = g).
H: Funext
A, B: Type
C: A -> B -> Type
x1, x2: A
p: x1 = x2
f: forall y1 : B, C x1 y1
g: forall y2 : B, C x2 y2
(forall y1 : B,
 transport (fun x : A => C x y1) p (f y1) = g y1) <~>
transport (fun x : A => forall y : B, C x y) p f = g
Proof.
H: Funext
A, B: Type
C: A -> B -> Type
x1, x2: A
p: x1 = x2
f: forall y1 : B, C x1 y1
g: forall y2 : B, C x2 y2
(forall y1 : B,
 transport (fun x : A => C x y1) p (f y1) = g y1) <~>
transport (fun x : A => forall y : B, C x y) p f = g
  destruct p.
H: Funext
A, B: Type
C: A -> B -> Type
x1: A
f, g: forall y2 : B, C x1 y2
(forall y1 : B,
 transport (fun x : A => C x y1) 1 (f y1) = g y1) <~>
transport (fun x : A => forall y : B, C x y) 1 f = g
  apply equiv_path_forall.
Defined.

(** ** Functorial action *)

(** The functoriality of [forall] is slightly subtle: it is contravariant in the domain type and covariant in the codomain, but the codomain is dependent on the domain. *)

Definition functor_forall `{P : A -> Type} `{Q : B -> Type}
    (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b)
  : (forall a:A, P a) -> (forall b:B, Q b)
  := (fun g b => f1 _ (g (f0 b))).

Definition ap_functor_forall `{P : A -> Type} `{Q : B -> Type}
    (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b)
    (g g' : forall a:A, P a) (h : g == g')
  : ap (functor_forall f0 f1) (path_forall _ _ h)
    = path_forall _ _ (fun b:B => (ap (f1 b) (h (f0 b)))).
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: B -> A
f1: forall b : B, P (f0 b) -> Q b
g, g': forall a : A, P a
h: g == g'
ap (functor_forall f0 f1) (path_forall g g' h) =
path_forall (fun b : B => f1 b (g (f0 b)))
  (fun b : B => f1 b (g' (f0 b)))
  (fun b : B => ap (f1 b) (h (f0 b)))
Proof.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: B -> A
f1: forall b : B, P (f0 b) -> Q b
g, g': forall a : A, P a
h: g == g'
ap (functor_forall f0 f1) (path_forall g g' h) =
path_forall (fun b : B => f1 b (g (f0 b)))
  (fun b : B => f1 b (g' (f0 b)))
  (fun b : B => ap (f1 b) (h (f0 b)))
  revert h.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: B -> A
f1: forall b : B, P (f0 b) -> Q b
g, g': forall a : A, P a
forall h : g == g',
ap (functor_forall f0 f1) (path_forall g g' h) =
path_forall (fun b : B => f1 b (g (f0 b)))
  (fun b : B => f1 b (g' (f0 b)))
  (fun b : B => ap (f1 b) (h (f0 b)))  equiv_intro (@apD10 A P g g') h.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: B -> A
f1: forall b : B, P (f0 b) -> Q b
g, g': forall a : A, P a
h: g = g'
ap (functor_forall f0 f1) (path_forall g g' (apD10 h)) =
path_forall (fun b : B => f1 b (g (f0 b)))
  (fun b : B => f1 b (g' (f0 b)))
  (fun b : B => ap (f1 b) (apD10 h (f0 b)))
  destruct h.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: B -> A
f1: forall b : B, P (f0 b) -> Q b
g: forall a : A, P a
ap (functor_forall f0 f1) (path_forall g g (apD10 1)) =
path_forall (fun b : B => f1 b (g (f0 b)))
  (fun b : B => f1 b (g (f0 b)))
  (fun b : B => ap (f1 b) (apD10 1 (f0 b)))  simpl.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: B -> A
f1: forall b : B, P (f0 b) -> Q b
g: forall a : A, P a
ap (functor_forall f0 f1) (path_forall g g (apD10 1)) =
path_forall (fun b : B => f1 b (g (f0 b)))
  (fun b : B => f1 b (g (f0 b))) (fun b : B => 1)
  transitivity (idpath (functor_forall f0 f1 g)).
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: B -> A
f1: forall b : B, P (f0 b) -> Q b
g: forall a : A, P a
ap (functor_forall f0 f1) (path_forall g g (apD10 1)) =
1
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: B -> A
f1: forall b : B, P (f0 b) -> Q b
g: forall a : A, P a
1 =
path_forall (fun b : B => f1 b (g (f0 b)))
  (fun b : B => f1 b (g (f0 b))) (fun b : B => 1)
  -
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: B -> A
f1: forall b : B, P (f0 b) -> Q b
g: forall a : A, P a
ap (functor_forall f0 f1) (path_forall g g (apD10 1)) =
1 exact (ap (ap (functor_forall f0 f1)) (path_forall_1 g)).
  -
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: B -> A
f1: forall b : B, P (f0 b) -> Q b
g: forall a : A, P a
1 =
path_forall (fun b : B => f1 b (g (f0 b)))
  (fun b : B => f1 b (g (f0 b))) (fun b : B => 1) symmetry.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: B -> A
f1: forall b : B, P (f0 b) -> Q b
g: forall a : A, P a
path_forall (fun b : B => f1 b (g (f0 b)))
  (fun b : B => f1 b (g (f0 b))) (fun b : B => 1) = 1  apply path_forall_1.
Defined.

Definition functor_forall_compose
           `{P : A -> Type} `{Q : B -> Type} `{R : C -> Type}
           (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b)
           (g0 : C -> B) (g1 : forall c:C, Q (g0 c) -> R c)
           (k : forall a, P a)
  : functor_forall g0 g1 (functor_forall f0 f1 k) == functor_forall (f0 o g0) (fun c => g1 c o f1 (g0 c)) k
  := fun a => 1.

(** Some special cases appear when one or the other of the maps are equivalences. *)

Definition functor_forall_id `{P : A -> Type} `{Q : A -> Type}
    (f1 : forall a:A, P a -> Q a)
  : (forall a:A, P a) -> (forall a:A, Q a)
  := functor_forall idmap f1.

Definition functor_forall_pb {A B : Type} `{P : A -> Type}
    (f0 : B -> A)
  : (forall a:A, P a) -> (forall b:B, P (f0 b))
  := functor_forall f0 (fun _ => idmap).

(** If [f0] is an equivalence, then we can simply apply [functor_forall] to its inverse.  However, in this case it is sometimes more convenient to place the substitution on the other side of [f1]. *)

Definition functor_forall_equiv `{P : A -> Type} `{Q : B -> Type}
    (f0 : A -> B) `{!IsEquiv f0} (f1 : forall a:A, P a -> Q (f0 a))
  : (forall a:A, P a) -> (forall b:B, Q b).
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: A -> B
IsEquiv0: IsEquiv f0
f1: forall a : A, P a -> Q (f0 a)
(forall a : A, P a) -> forall b : B, Q b
Proof.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: A -> B
IsEquiv0: IsEquiv f0
f1: forall a : A, P a -> Q (f0 a)
(forall a : A, P a) -> forall b : B, Q b
  nrapply (functor_forall f0^-1).
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: A -> B
IsEquiv0: IsEquiv f0
f1: forall a : A, P a -> Q (f0 a)
forall b : B, P (f0^-1 b) -> Q b
  intros b u.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: A -> B
IsEquiv0: IsEquiv f0
f1: forall a : A, P a -> Q (f0 a)
b: B
u: P (f0^-1 b)
Q b
  refine ((eisretr f0 b) # _).
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f0: A -> B
IsEquiv0: IsEquiv f0
f1: forall a : A, P a -> Q (f0 a)
b: B
u: P (f0^-1 b)
Q (f0 (f0^-1 b))
  exact (f1 _ u).
Defined.

Definition functor_forall_equiv_pb {A B : Type} `{Q : B -> Type}
    (f0 : A -> B) `{!IsEquiv f0}
  : (forall a:A, Q (f0 a)) -> (forall b:B, Q b)
  := functor_forall_equiv f0 (fun _ => idmap).

(** Since there's a nontrivial transport here, it's useful to have a computation lemma. *)
Definition functor_forall_equiv_pb_beta {A B : Type} {P : B -> Type} (f : A -> B)
  `{!IsEquiv f} (h : forall a, P (f a))
  : forall a, functor_forall_equiv_pb f h (f a) = h a.
H: Funext
A, B: Type
P: B -> Type
f: A -> B
IsEquiv0: IsEquiv f
h: forall a : A, P (f a)
forall a : A, functor_forall_equiv_pb f h (f a) = h a
Proof.
H: Funext
A, B: Type
P: B -> Type
f: A -> B
IsEquiv0: IsEquiv f
h: forall a : A, P (f a)
forall a : A, functor_forall_equiv_pb f h (f a) = h a
  intro a; srapply (_ @ apD h (eissect f a)); srapply (_ @ (transport_compose _ _ _ _)^).
H: Funext
A, B: Type
P: B -> Type
f: A -> B
IsEquiv0: IsEquiv f
h: forall a : A, P (f a)
a: A
functor_forall_equiv_pb f h (f a) =
transport P (ap f (eissect f a)) (h (f^-1 (f a)))
  srapply ap10; apply ap; apply eisadj.
Defined.

(** ** Equivalences *)

(** If *both* maps in [functor_forall] are equivalences, then so is the output. *)
Global Instance isequiv_functor_forall `{P : A -> Type} `{Q : B -> Type}
  `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)}
  : IsEquiv (functor_forall f g) | 1000.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: B -> A
H0: IsEquiv f
g: forall x : B, P (f x) -> Q x
H1: forall b : B, IsEquiv (g b)
IsEquiv (functor_forall f g)
Proof.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: B -> A
H0: IsEquiv f
g: forall x : B, P (f x) -> Q x
H1: forall b : B, IsEquiv (g b)
IsEquiv (functor_forall f g)
  simple refine (isequiv_adjointify (functor_forall f g)
    (functor_forall (f^-1)
      (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y
      )) _ _);
  intros h.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: B -> A
H0: IsEquiv f
g: forall x : B, P (f x) -> Q x
H1: forall b : B, IsEquiv (g b)
h: forall b : B, Q b
functor_forall f g
  (functor_forall f^-1
     (fun (x : A) (y : Q (f^-1 x)) =>
      transport P (eisretr f x) ((g (f^-1 x))^-1 y)) h) =
h
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: B -> A
H0: IsEquiv f
g: forall x : B, P (f x) -> Q x
H1: forall b : B, IsEquiv (g b)
h: forall a : A, P a
functor_forall f^-1
  (fun (x : A) (y : Q (f^-1 x)) =>
   transport P (eisretr f x) ((g (f^-1 x))^-1 y))
  (functor_forall f g h) = h
  -
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: B -> A
H0: IsEquiv f
g: forall x : B, P (f x) -> Q x
H1: forall b : B, IsEquiv (g b)
h: forall b : B, Q b
functor_forall f g
  (functor_forall f^-1
     (fun (x : A) (y : Q (f^-1 x)) =>
      transport P (eisretr f x) ((g (f^-1 x))^-1 y)) h) =
h abstract (
        apply path_forall; intros b; unfold functor_forall;
        rewrite eisadj;
        rewrite <- transport_compose;
        rewrite ap_transport;
        rewrite eisretr;
        apply apD
      ).
  -
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
f: B -> A
H0: IsEquiv f
g: forall x : B, P (f x) -> Q x
H1: forall b : B, IsEquiv (g b)
h: forall a : A, P a
functor_forall f^-1
  (fun (x : A) (y : Q (f^-1 x)) =>
   transport P (eisretr f x) ((g (f^-1 x))^-1 y))
  (functor_forall f g h) = h abstract (
        apply path_forall; intros a; unfold functor_forall;
        rewrite eissect;
        apply apD
      ).
Defined.

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

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

Definition equiv_functor_forall_id `{P : A -> Type} `{Q : A -> Type}
  (g : forall a, P a <~> Q a)
  : (forall a, P a) <~> (forall a, Q a)
  := equiv_functor_forall (equiv_idmap A) g.

Definition equiv_functor_forall_pb {A B : Type} {P : A -> Type}
  (f : B <~> A)
  : (forall a, P a) <~> (forall b, P (f b))
  := equiv_functor_forall' (Q := P o f) f (fun b => equiv_idmap).

(** Similarly, we have a version of [functor_forall_equiv] that acts on on equivalences both upstairs and downstairs. *)

Definition equiv_functor_forall_covariant
           `{P : A -> Type} `{Q : B -> Type}
           (f : A <~> B) (g : forall a, P a <~> Q (f a))
  : (forall a, P a) <~> (forall b, Q b)
  := (equiv_functor_forall' f (fun a => (g a)^-1%equiv))^-1.

Definition equiv_functor_forall_covariant_compose
           `{P : A -> Type} `{Q : B -> Type} `{R : C -> Type}
           (f0 : A <~> B) (f1 : forall a, P a <~> Q (f0 a))
           (g0 : B <~> C) (g1 : forall b, Q b <~> R (g0 b))
           (h : forall a, P a)
  : equiv_functor_forall_covariant g0 g1 (equiv_functor_forall_covariant f0 f1 h)
    == equiv_functor_forall_covariant (g0 oE f0) (fun a => g1 (f0 a) oE f1 a) h.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
C: Type
R: C -> Type
f0: A <~> B
f1: forall a : A, P a <~> Q (f0 a)
g0: B <~> C
g1: forall b : B, Q b <~> R (g0 b)
h: forall a : A, P a
equiv_functor_forall_covariant g0 g1
  (equiv_functor_forall_covariant f0 f1 h) ==
equiv_functor_forall_covariant (g0 oE f0)
  (fun a : A => g1 (f0 a) oE f1 a) h
Proof.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
C: Type
R: C -> Type
f0: A <~> B
f1: forall a : A, P a <~> Q (f0 a)
g0: B <~> C
g1: forall b : B, Q b <~> R (g0 b)
h: forall a : A, P a
equiv_functor_forall_covariant g0 g1
  (equiv_functor_forall_covariant f0 f1 h) ==
equiv_functor_forall_covariant (g0 oE f0)
  (fun a : A => g1 (f0 a) oE f1 a) h
  apply apD10.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
C: Type
R: C -> Type
f0: A <~> B
f1: forall a : A, P a <~> Q (f0 a)
g0: B <~> C
g1: forall b : B, Q b <~> R (g0 b)
h: forall a : A, P a
equiv_functor_forall_covariant g0 g1
  (equiv_functor_forall_covariant f0 f1 h) =
equiv_functor_forall_covariant (g0 oE f0)
  (fun a : A => g1 (f0 a) oE f1 a) h
  refine ((equiv_inverse_compose
             (equiv_functor_forall' g0 (fun a : B => (g1 a)^-1%equiv))
             (equiv_functor_forall' f0 (fun a : A => (f1 a)^-1%equiv))
             h)^ @ _).
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
C: Type
R: C -> Type
f0: A <~> B
f1: forall a : A, P a <~> Q (f0 a)
g0: B <~> C
g1: forall b : B, Q b <~> R (g0 b)
h: forall a : A, P a
(equiv_functor_forall' f0 (fun a : A => (f1 a)^-1)
 oE equiv_functor_forall' g0 (fun a : B => (g1 a)^-1))^-1
  h =
equiv_functor_forall_covariant (g0 oE f0)
  (fun a : A => g1 (f0 a) oE f1 a) h
  revert h; apply equiv_inverse_homotopy; intros h.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
C: Type
R: C -> Type
f0: A <~> B
f1: forall a : A, P a <~> Q (f0 a)
g0: B <~> C
g1: forall b : B, Q b <~> R (g0 b)
h: forall a : C, R a
equiv_functor_forall' (g0 oE f0)
  (fun a : A => ((g1 (f0 a) oE f1 a)^-1)%equiv) h =
(equiv_functor_forall' f0 (fun a : A => (f1 a)^-1)
 oE equiv_functor_forall' g0 (fun a : B => (g1 a)^-1))
  h
  apply path_forall; intros c.
H: Funext
A: Type
P: A -> Type
B: Type
Q: B -> Type
C: Type
R: C -> Type
f0: A <~> B
f1: forall a : A, P a <~> Q (f0 a)
g0: B <~> C
g1: forall b : B, Q b <~> R (g0 b)
h: forall a : C, R a
c: A
equiv_functor_forall' (g0 oE f0)
  (fun a : A => ((g1 (f0 a) oE f1 a)^-1)%equiv) h c =
(equiv_functor_forall' f0 (fun a : A => (f1 a)^-1)
 oE equiv_functor_forall' g0 (fun a : B => (g1 a)^-1))
  h c
  symmetry; rapply functor_forall_compose.
Defined.

(** ** Functoriality on logical equivalences *)

(** At least over a fixed base *)
Definition iff_functor_forall {A : Type} {P Q : A -> Type}
           (f : forall a, P a <-> Q a)
  : (forall a, P a) <-> (forall a, Q a).
H: Funext
A: Type
P, Q: A -> Type
f: forall a : A, P a <-> Q a
(forall a : A, P a) <-> (forall a : A, Q a)
Proof.
H: Funext
A: Type
P, Q: A -> Type
f: forall a : A, P a <-> Q a
(forall a : A, P a) <-> (forall a : A, Q a)
  split.
H: Funext
A: Type
P, Q: A -> Type
f: forall a : A, P a <-> Q a
(forall a : A, P a) -> forall a : A, Q a
H: Funext
A: Type
P, Q: A -> Type
f: forall a : A, P a <-> Q a
(forall a : A, Q a) -> forall a : A, P a
  -
H: Funext
A: Type
P, Q: A -> Type
f: forall a : A, P a <-> Q a
(forall a : A, P a) -> forall a : A, Q a intros g a; exact (fst (f a) (g a)).
  -
H: Funext
A: Type
P, Q: A -> Type
f: forall a : A, P a <-> Q a
(forall a : A, Q a) -> forall a : A, P a intros h a; exact (snd (f a) (h a)).
Defined.

(** ** Two variable versions for function extensionality. *)

Definition equiv_path_forall11 {A : Type} {B : A -> Type} {P : forall a : A, B a -> Type} (f g : forall a b, P a b)
  : (forall (a : A) (b : B a), f a b = g a b) <~> f = g
  := (equiv_path_forall f g) oE (equiv_functor_forall_id (fun a => equiv_path_forall (f a) (g a))).

Definition path_forall11 {A : Type} {B : A -> Type} {P : forall a : A, B a -> Type} (f g : forall a b, P a b)
  : (forall x y, f x y = g x y) -> f = g
  := equiv_path_forall11 f g.

Global Instance isequiv_path_forall11 {A : Type} {B : A -> Type} `{P : forall a : A, B a -> Type} (f g : forall a b, P a b)
  : IsEquiv (path_forall11 f g) | 0
  := _.

Global Arguments equiv_path_forall11 {A B}%type_scope {P} (f g)%function_scope.

Global Arguments path_forall11 {A B}%type_scope {P} (f g)%function_scope _.

(** ** Truncatedness: any dependent product of n-types is an n-type: see [contr_forall] and [istrunc_forall] in Basics.Trunc. *)

(** ** Contractibility: A product over a contractible type is equivalent to the fiber over the center. *)

Definition equiv_contr_forall `{Contr A} `(P : A -> Type)
: (forall a, P a) <~> P (center A).
H: Funext
A: Type
Contr0: Contr A
P: A -> Type
(forall a : A, P a) <~> P (center A)
Proof.
H: Funext
A: Type
Contr0: Contr A
P: A -> Type
(forall a : A, P a) <~> P (center A)
  simple refine (equiv_adjointify (fun (f:forall a, P a) => f (center A)) _ _ _).
H: Funext
A: Type
Contr0: Contr A
P: A -> Type
P (center A) -> forall a : A, P a
H: Funext
A: Type
Contr0: Contr A
P: A -> Type
(fun f : forall a : A, P a => f (center A)) o ?g ==
idmap
H: Funext
A: Type
Contr0: Contr A
P: A -> Type
?g o (fun f : forall a : A, P a => f (center A)) ==
idmap
  -
H: Funext
A: Type
Contr0: Contr A
P: A -> Type
P (center A) -> forall a : A, P a intros p a; exact (transport P (path_contr _ _) p).
  -
H: Funext
A: Type
Contr0: Contr A
P: A -> Type
(fun f : forall a : A, P a => f (center A))
o (fun (p : P (center A)) (a : A) =>
   transport P (path_contr (center A) a) p) == idmap intros p.
H: Funext
A: Type
Contr0: Contr A
P: A -> Type
p: P (center A)
transport P (path_contr (center A) (center A)) p = p
    refine (transport2 P (q := 1) _ p).
H: Funext
A: Type
Contr0: Contr A
P: A -> Type
p: P (center A)
path_contr (center A) (center A) = 1
    apply path_contr.
  -
H: Funext
A: Type
Contr0: Contr A
P: A -> Type
(fun (p : P (center A)) (a : A) =>
 transport P (path_contr (center A) a) p)
o (fun f : forall a : A, P a => f (center A)) == idmap intros f; apply path_forall; intros a.
H: Funext
A: Type
Contr0: Contr A
P: A -> Type
f: forall a : A, P a
a: A
transport P (path_contr (center A) a) (f (center A)) =
f a
    apply apD.
Defined.

End AssumeFunext.

(** ** Symmetry of curried arguments *)

(** Using the standard Haskell name for this, as it’s a handy utility function.

Note: not sure if [P] will usually be deducible, or whether it would be better explicit. *)
Definition flip `{P : A -> B -> Type}
  : (forall a b, P a b) -> (forall b a, P a b)
  := fun f b a => f a b.

Global Instance isequiv_flip `{P : A -> B -> Type}
  : IsEquiv (@flip _ _ P) | 0.
A, B: Type
P: A -> B -> Type
IsEquiv flip
Proof.
A, B: Type
P: A -> B -> Type
IsEquiv flip
  set (flip_P := @flip _ _ P).
A, B: Type
P: A -> B -> Type
flip_P:= flip: (forall (a : A) (b : B), P a b) ->
forall (b : B) (a : A), P a b
IsEquiv flip_P
  set (flip_P_inv := @flip _ _ (flip P)).
A, B: Type
P: A -> B -> Type
flip_P:= flip: (forall (a : A) (b : B), P a b) ->
forall (b : B) (a : A), P a b
flip_P_inv:= flip: (forall (a : B) (b : A), flip P a b) ->
forall (b : A) (a : B), flip P a b
IsEquiv flip_P
  set (flip_P_is_sect := (fun f => 1) : flip_P_inv o flip_P == idmap).
A, B: Type
P: A -> B -> Type
flip_P:= flip: (forall (a : A) (b : B), P a b) ->
forall (b : B) (a : A), P a b
flip_P_inv:= flip: (forall (a : B) (b : A), flip P a b) ->
forall (b : A) (a : B), flip P a b
flip_P_is_sect:= (fun f : forall (a : A) (b : B), P a b
 => 1)
:
flip_P_inv o flip_P == idmap: flip_P_inv o flip_P == idmap
IsEquiv flip_P
  set (flip_P_is_retr := (fun g => 1) : flip_P o flip_P_inv == idmap).
A, B: Type
P: A -> B -> Type
flip_P:= flip: (forall (a : A) (b : B), P a b) ->
forall (b : B) (a : A), P a b
flip_P_inv:= flip: (forall (a : B) (b : A), flip P a b) ->
forall (b : A) (a : B), flip P a b
flip_P_is_sect:= (fun f : forall (a : A) (b : B), P a b
 => 1)
:
flip_P_inv o flip_P == idmap: flip_P_inv o flip_P == idmap
flip_P_is_retr:= (fun
   g : forall (a : B) (b : A),
       flip P a b => 1)
:
flip_P o flip_P_inv == idmap: flip_P o flip_P_inv == idmap
IsEquiv flip_P
  exists flip_P_inv flip_P_is_retr flip_P_is_sect.
A, B: Type
P: A -> B -> Type
flip_P:= flip: (forall (a : A) (b : B), P a b) ->
forall (b : B) (a : A), P a b
flip_P_inv:= flip: (forall (a : B) (b : A), flip P a b) ->
forall (b : A) (a : B), flip P a b
flip_P_is_sect:= (fun f : forall (a : A) (b : B), P a b
 => 1)
:
flip_P_inv o flip_P == idmap: flip_P_inv o flip_P == idmap
flip_P_is_retr:= (fun
   g : forall (a : B) (b : A),
       flip P a b => 1)
:
flip_P o flip_P_inv == idmap: flip_P o flip_P_inv == idmap
forall x : forall (b : A) (a : B), flip P a b,
flip_P_is_retr (flip_P x) =
ap flip_P (flip_P_is_sect x)
  intro g.
A, B: Type
P: A -> B -> Type
flip_P:= flip: (forall (a : A) (b : B), P a b) ->
forall (b : B) (a : A), P a b
flip_P_inv:= flip: (forall (a : B) (b : A), flip P a b) ->
forall (b : A) (a : B), flip P a b
flip_P_is_sect:= (fun f : forall (a : A) (b : B), P a b
 => 1)
:
flip_P_inv o flip_P == idmap: flip_P_inv o flip_P == idmap
flip_P_is_retr:= (fun
   g : forall (a : B) (b : A),
       flip P a b => 1)
:
flip_P o flip_P_inv == idmap: flip_P o flip_P_inv == idmap
g: forall (b : A) (a : B), flip P a b
flip_P_is_retr (flip_P g) =
ap flip_P (flip_P_is_sect g)  exact 1.
Defined.

Definition equiv_flip `(P : A -> B -> Type)
  : (forall a b, P a b) <~> (forall b a, P a b)
  := Build_Equiv _ _ (@flip _ _ P) _.