Add transport lemmas for families of equivalences

[Alizter]

          > I'm thinking about `transport (fun x => A x <~> B x) p y`.

Various results of that form can be proved just using path induction. Only one of them uses Funext. I was surprised about the first one, which proves that two functions are equal without using Funext.

(** This is an improvement to [transport_arrow].  That result only shows that the functions are homotopic, but even without funext, we can prove that these functions are equal. *)
Definition transport_arrow' {A : Type} {B C : A -> Type}
  {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C x1)
  : transport (fun x => B x -> C x) p f = transport _ p o f o transport _ p^.
Proof.
  destruct p; auto.
Defined.

(** This is like [transport_arrow], but for a family of equivalence types. It just shows that the functions are homotopic. *)
Definition transport_equiv {A : Type} {B C : A -> Type}
  {x1 x2 : A} (p : x1 = x2) (f : B x1 <~> C x1) (y : B x2)
  : (transport (fun x => B x <~> C x) p f) y  =  p # (f (p^ # y)).
Proof.
  destruct p; auto.
Defined.

(** A version that shows that the underlying functions are equal. *)
Definition transport_equiv' {A : Type} {B C : A -> Type}
  {x1 x2 : A} (p : x1 = x2) (f : B x1 <~> C x1)
  : transport (fun x => B x <~> C x) p f = (equiv_transport _ p) oE f oE (equiv_transport _ p^) :> (B x2 -> C x2).
Proof.
  destruct p; auto.
Defined.

(** A version that shows that the equivalences are equal.  Here we do need [Funext], for [path_equiv]. *)
Definition transport_equiv'' `{Funext} {A : Type} {B C : A -> Type}
  {x1 x2 : A} (p : x1 = x2) (f : B x1 <~> C x1)
  : transport (fun x => B x <~> C x) p f = (equiv_transport _ p) oE f oE (equiv_transport _ p^).
Proof.
  apply path_equiv.
  destruct p; auto.
Defined.

Originally posted by @jdchristensen in #1840 (comment)