(* -*- mode: coq; mode: visual-line -*- *)

Require Import HoTT.Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.

Local Open Scope path_scope.

(** * Equivalences *)

Section AssumeFunext.
  Context `{Funext}.

  Global Instance contr_map_isequiv {A B} (f : A -> B) `{IsEquiv _ _ f}
    : IsTruncMap (-2) f.
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
IsTruncMap (-2) f
  Proof.
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
IsTruncMap (-2) f
    intros b; refine (contr_equiv' {a : A & a = f^-1 b} _).
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
b: B
{a : A & a = f^-1 b} <~> hfiber f b
    apply equiv_functor_sigma_id; intros a.
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
b: B
a: A
a = f^-1 b <~> f a = b
    apply equiv_moveR_equiv_M.
  Defined.

  Definition isequiv_contr_map {A B} (f : A -> B) `{IsTruncMap (-2) A B f}
    : IsEquiv f.
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
IsEquiv f
  Proof.
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
IsEquiv f
    srapply Build_IsEquiv.
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
B -> A
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
f o ?equiv_inv == idmap
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
?equiv_inv o f == idmap
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
forall x : A, ?eisretr (f x) = ap f (?eissect x)
    -
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
B -> A intros b; exact (center {a : A & f a = b}).1.
    -
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
f o (fun b : B => (center {a : A & f a = b}).1) ==
idmap intros b.
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
b: B
f (center {a : A & f a = b}).1 = b exact (center {a : A & f a = b}).2.
    -
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
(fun b : B => (center {a : A & f a = b}).1) o f ==
idmap intros a.
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
a: A
(center {a0 : A & f a0 = f a}).1 = a exact (@contr {x : A & f x = f a} _ (a;1))..1.
    -
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
forall x : A,
((fun b : B => (center {a : A & f a = b}).2)
 :
 f o (fun b : B => (center {a : A & f a = b}).1) ==
 idmap) (f x) =
ap f
  (((fun a : A => (contr (a; 1)) ..1)
    :
    (fun b : B => (center {a : A & f a = b}).1) o f ==
    idmap) x) intros a; cbn.
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
a: A
(center {a0 : A & f a0 = f a}).2 =
ap f (contr (a; 1)) ..1 apply moveL_M1.
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
a: A
(ap f (contr (a; 1)) ..1)^ @
(center {a0 : A & f a0 = f a}).2 = 1
      rewrite <- transport_paths_l, <- transport_compose.
H: Funext
A, B: Type
f: A -> B
H0: IsTruncMap (-2) f
a: A
transport (fun x : A => f x = f a) (contr (a; 1)) ..1
  (center {a0 : A & f a0 = f a}).2 = 1
      exact ((@contr {x : A & f x = f a} _ (a;1))..2).
  Defined.

  (** As usual, we can't make both of these [Instances]. *)
  #[local]
  Hint Immediate isequiv_contr_map : typeclass_instances.

  (** It follows that when proving a map is an equivalence, we may assume its codomain is inhabited. *)
  Definition isequiv_inhab_codomain {A B} (f : A -> B) (feq : B -> IsEquiv f)
    : IsEquiv f.
H: Funext
A, B: Type
f: A -> B
feq: B -> IsEquiv f
IsEquiv f
  Proof.
H: Funext
A, B: Type
f: A -> B
feq: B -> IsEquiv f
IsEquiv f
    apply isequiv_contr_map.
H: Funext
A, B: Type
f: A -> B
feq: B -> IsEquiv f
IsTruncMap (-2) f
    intros b.
H: Funext
A, B: Type
f: A -> B
feq: B -> IsEquiv f
b: B
Contr (hfiber f b)
    pose (feq b); exact _.
  Defined.

  Global Instance contr_sect_equiv {A B} (f : A -> B) `{IsEquiv A B f}
    : Contr {g : B -> A & f o g == idmap}.
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
Contr {g : B -> A & f o g == idmap}
  Proof.
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
Contr {g : B -> A & f o g == idmap}
    refine (contr_change_center (f^-1 ; eisretr f)).
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
Contr {g : B -> A & (fun x : B => f (g x)) == idmap}
    refine (contr_equiv' { g : B -> A & f o g = idmap } _).
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
{g : B -> A & (fun x : B => f (g x)) = idmap} <~>
{g : B -> A & (fun x : B => f (g x)) == idmap}
    (* Typeclass inference finds this contractible instance: it's the fiber over [idmap] of postcomposition with [f], and the latter is an equivalence since [f] is. *)
    apply equiv_functor_sigma_id; intros g.
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
g: B -> A
(fun x : B => f (g x)) = idmap <~>
(fun x : B => f (g x)) == idmap
    apply equiv_ap10.
  Defined.

  Global Instance contr_retr_equiv {A B} (f : A -> B) `{IsEquiv A B f}
    : Contr {g : B -> A & g o f == idmap}.
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
Contr {g : B -> A & g o f == idmap}
  Proof.
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
Contr {g : B -> A & g o f == idmap}
    refine (contr_change_center (f^-1 ; eissect f)).
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
Contr {g : B -> A & (fun x : A => g (f x)) == idmap}
    refine (contr_equiv' { g : B -> A & g o f = idmap } _).
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
{g : B -> A & (fun x : A => g (f x)) = idmap} <~>
{g : B -> A & (fun x : A => g (f x)) == idmap}
    apply equiv_functor_sigma_id; intros g.
H: Funext
A, B: Type
f: A -> B
H0: IsEquiv f
g: B -> A
(fun x : A => g (f x)) = idmap <~>
(fun x : A => g (f x)) == idmap
    apply equiv_ap10.
  Defined.

  (** We begin by showing that, assuming function extensionality, [IsEquiv f] is an hprop. *)
  Global Instance hprop_isequiv {A B} (f : A -> B)
  : IsHProp (IsEquiv f).
H: Funext
A, B: Type
f: A -> B
IsHProp (IsEquiv f)
  Proof.
H: Funext
A, B: Type
f: A -> B
IsHProp (IsEquiv f)
    (** We will show that assuming [f] is an equivalence, [IsEquiv f] decomposes into a sigma of two contractible types. *)
    apply hprop_inhabited_contr; intros feq.
H: Funext
A, B: Type
f: A -> B
feq: IsEquiv f
Contr (IsEquiv f)
    nrefine (contr_equiv' _ (issig_isequiv f oE (equiv_sigma_assoc' _ _)^-1)).
H: Funext
A, B: Type
f: A -> B
feq: IsEquiv f
Contr
  {ap0
  : {a : B -> A & (fun x : B => f (a x)) == idmap} &
  {s : (fun x : A => ap0.1 (f x)) == idmap &
  forall x : A, ap0.2 (f x) = ap f (s x)}}
    srefine (contr_equiv' _ (equiv_contr_sigma _)^-1).
H: Funext
A, B: Type
f: A -> B
feq: IsEquiv f
Contr {a : B -> A & (fun x : B => f (a x)) == idmap}
H: Funext
A, B: Type
f: A -> B
feq: IsEquiv f
Contr
  ((fun
      x : {a : B -> A &
          (fun x : B => f (a x)) == idmap} =>
    {s : (fun x0 : A => x.1 (f x0)) == idmap &
    forall x0 : A, x.2 (f x0) = ap f (s x0)})
     (center
        {a : B -> A & (fun x : B => f (a x)) == idmap}))
    (** Each of these types is equivalent to a based homotopy space.  The first is exactly [contr_sect_equiv]. *)
    1: rapply contr_sect_equiv.
H: Funext
A, B: Type
f: A -> B
feq: IsEquiv f
Contr
  ((fun
      x : {a : B -> A &
          (fun x : B => f (a x)) == idmap} =>
    {s : (fun x0 : A => x.1 (f x0)) == idmap &
    forall x0 : A, x.2 (f x0) = ap f (s x0)})
     (center
        {a : B -> A & (fun x : B => f (a x)) == idmap}))
    (** The second requires a bit more work. *)
    cbn.
H: Funext
A, B: Type
f: A -> B
feq: IsEquiv f
Contr
  {s : (fun x : A => f^-1 (f x)) == idmap &
  forall x : A, eisretr f (f x) = ap f (s x)}
    refine (contr_equiv' { s : f^-1 o f == idmap & eissect f == s } _).
H: Funext
A, B: Type
f: A -> B
feq: IsEquiv f
{s : (fun x : A => f^-1 (f x)) == idmap &
eissect f == s} <~>
{s : (fun x : A => f^-1 (f x)) == idmap &
forall x : A, eisretr f (f x) = ap f (s x)}
    apply equiv_functor_sigma_id; intros s; cbn.
H: Funext
A, B: Type
f: A -> B
feq: IsEquiv f
s: (fun x : A => f^-1 (f x)) == idmap
eissect f == s <~>
(forall x : A, eisretr f (f x) = ap f (s x))
    apply equiv_functor_forall_id; intros a.
H: Funext
A, B: Type
f: A -> B
feq: IsEquiv f
s: (fun x : A => f^-1 (f x)) == idmap
a: A
eissect f a = s a <~> eisretr f (f a) = ap f (s a)
    refine (equiv_concat_l (eisadj f a) _ oE _).
H: Funext
A, B: Type
f: A -> B
feq: IsEquiv f
s: (fun x : A => f^-1 (f x)) == idmap
a: A
eissect f a = s a <~> ap f (eissect f a) = ap f (s a)
    rapply equiv_ap.
  Qed.

  (** Now since [IsEquiv f] and the assertion that its fibers are contractible are both HProps, logical equivalence implies equivalence. *)
  Definition equiv_contr_map_isequiv {A B} (f : A -> B)
    : IsTruncMap (-2) f <~> IsEquiv f.
H: Funext
A, B: Type
f: A -> B
IsTruncMap (-2) f <~> IsEquiv f
  Proof.
H: Funext
A, B: Type
f: A -> B
IsTruncMap (-2) f <~> IsEquiv f
    rapply equiv_iff_hprop.
    (** Both directions are found by typeclass inference! *)
  Defined.

  (** Thus, paths of equivalences are equivalent to paths of functions. *)
  Lemma equiv_path_equiv {A B : Type} (e1 e2 : A <~> B)
  : (e1 = e2 :> (A -> B)) <~> (e1 = e2 :> (A <~> B)).
H: Funext
A, B: Type
e1, e2: A <~> B
e1 = e2 <~> e1 = e2
  Proof.
H: Funext
A, B: Type
e1, e2: A <~> B
e1 = e2 <~> e1 = e2
    equiv_via ((issig_equiv A B) ^-1 e1 = (issig_equiv A B) ^-1 e2).
H: Funext
A, B: Type
e1, e2: A <~> B
e1 = e2 <~>
(issig_equiv A B)^-1 e1 = (issig_equiv A B)^-1 e2
H: Funext
A, B: Type
e1, e2: A <~> B
(issig_equiv A B)^-1 e1 = (issig_equiv A B)^-1 e2 <~>
e1 = e2
    2: symmetry; apply equiv_ap; refine _.
H: Funext
A, B: Type
e1, e2: A <~> B
e1 = e2 <~>
(issig_equiv A B)^-1 e1 = (issig_equiv A B)^-1 e2
    exact (equiv_path_sigma_hprop ((issig_equiv A B)^-1 e1) ((issig_equiv A B)^-1 e2)).
  Defined.

  Definition path_equiv {A B : Type} {e1 e2 : A <~> B}
  : (e1 = e2 :> (A -> B)) -> (e1 = e2 :> (A <~> B))
    := equiv_path_equiv e1 e2.

  Global Instance isequiv_path_equiv {A B : Type} {e1 e2 : A <~> B}
  : IsEquiv (@path_equiv _ _ e1 e2)
    (* Coq can find this instance by itself, but it's slow. *)
    := equiv_isequiv (equiv_path_equiv e1 e2).

  (** The inverse equivalence is homotopic to [ap equiv_fun], so that is also an equivalence. *)
  Global Instance isequiv_ap_equiv_fun {A B : Type} (e1 e2 : A <~> B)
    : IsEquiv (ap (x:=e1) (y:=e2) (@equiv_fun A B)).
H: Funext
A, B: Type
e1, e2: A <~> B
IsEquiv (ap equiv_fun)
  Proof.
H: Funext
A, B: Type
e1, e2: A <~> B
IsEquiv (ap equiv_fun)
    snrapply isequiv_homotopic.
H: Funext
A, B: Type
e1, e2: A <~> B
e1 = e2 -> e1 = e2
H: Funext
A, B: Type
e1, e2: A <~> B
IsEquiv ?f
H: Funext
A, B: Type
e1, e2: A <~> B
?f == ap equiv_fun
    -
H: Funext
A, B: Type
e1, e2: A <~> B
e1 = e2 -> e1 = e2 exact (equiv_path_equiv e1 e2)^-1%equiv.
    -
H: Funext
A, B: Type
e1, e2: A <~> B
IsEquiv ((equiv_path_equiv e1 e2)^-1)%equiv exact _.
    -
H: Funext
A, B: Type
e1, e2: A <~> B
((equiv_path_equiv e1 e2)^-1)%equiv == ap equiv_fun intro p.
H: Funext
A, B: Type
e1, e2: A <~> B
p: e1 = e2
((equiv_path_equiv e1 e2)^-1)%equiv p = ap equiv_fun p exact (ap_compose (fun v => (equiv_fun v; equiv_isequiv v)) pr1 p)^.
  Defined.

  (** This implies that types of equivalences inherit truncation.  Note that we only state the theorem for [n.+1]-truncatedness, since it is not true for contractibility: if [B] is contractible but [A] is not, then [A <~> B] is not contractible because it is not inhabited.

   Don't confuse this lemma with [trunc_equiv], which says that if [A] is truncated and [A] is equivalent to [B], then [B] is truncated.  It would be nice to find a better pair of names for them. *)
  Global Instance istrunc_equiv {n : trunc_index} {A B : Type} `{IsTrunc n.+1 B}
  : IsTrunc n.+1 (A <~> B).
H: Funext
n: trunc_index
A, B: Type
IsTrunc0: IsTrunc n.+1 B
IsTrunc n.+1 (A <~> B)
  Proof.
H: Funext
n: trunc_index
A, B: Type
IsTrunc0: IsTrunc n.+1 B
IsTrunc n.+1 (A <~> B)
    simpl.
H: Funext
n: trunc_index
A, B: Type
IsTrunc0: IsTrunc n.+1 B
IsTrunc n.+1 (A <~> B)
    apply istrunc_S.
H: Funext
n: trunc_index
A, B: Type
IsTrunc0: IsTrunc n.+1 B
forall x y : A <~> B, IsTrunc n (x = y)
    intros e1 e2.
H: Funext
n: trunc_index
A, B: Type
IsTrunc0: IsTrunc n.+1 B
e1, e2: A <~> B
IsTrunc n (e1 = e2)
    apply (istrunc_equiv_istrunc _ (equiv_path_equiv e1 e2)).
  Defined.

  (** In the contractible case, we have to assume that *both* types are contractible to get a contractible type of equivalences. *)
  Global Instance contr_equiv_contr_contr {A B : Type} `{Contr A} `{Contr B}
  : Contr (A <~> B).
H: Funext
A, B: Type
Contr0: Contr A
Contr1: Contr B
Contr (A <~> B)
  Proof.
H: Funext
A, B: Type
Contr0: Contr A
Contr1: Contr B
Contr (A <~> B)
    apply (Build_Contr _ equiv_contr_contr).
H: Funext
A, B: Type
Contr0: Contr A
Contr1: Contr B
forall y : A <~> B, equiv_contr_contr = y
    intros e.
H: Funext
A, B: Type
Contr0: Contr A
Contr1: Contr B
e: A <~> B
equiv_contr_contr = e apply path_equiv, path_forall.
H: Funext
A, B: Type
Contr0: Contr A
Contr1: Contr B
e: A <~> B
equiv_contr_contr == e intros ?; apply contr.
  Defined.

  (** The type of *automorphisms* of an hprop is always contractible *)
  Global Instance contr_aut_hprop A `{IsHProp A}
  : Contr (A <~> A).
H: Funext
A: Type
IsHProp0: IsHProp A
Contr (A <~> A)
  Proof.
H: Funext
A: Type
IsHProp0: IsHProp A
Contr (A <~> A)
    apply (Build_Contr _ 1%equiv).
H: Funext
A: Type
IsHProp0: IsHProp A
forall y : A <~> A, 1%equiv = y
    intros e; apply path_equiv, path_forall.
H: Funext
A: Type
IsHProp0: IsHProp A
e: A <~> A
1%equiv == e intros ?; apply path_ishprop.
  Defined.

  (** Equivalences are functorial under equivalences. *)
  Definition functor_equiv {A B C D} (h : A <~> C) (k : B <~> D)
  : (A <~> B) -> (C <~> D)
  := fun f => ((k oE f) oE h^-1).

  Global Instance isequiv_functor_equiv {A B C D} (h : A <~> C) (k : B <~> D)
  : IsEquiv (functor_equiv h k).
H: Funext
A, B, C, D: Type
h: A <~> C
k: B <~> D
IsEquiv (functor_equiv h k)
  Proof.
H: Funext
A, B, C, D: Type
h: A <~> C
k: B <~> D
IsEquiv (functor_equiv h k)
    refine (isequiv_adjointify _
              (functor_equiv (equiv_inverse h) (equiv_inverse k)) _ _).
H: Funext
A, B, C, D: Type
h: A <~> C
k: B <~> D
(fun x : C <~> D =>
 functor_equiv h k (functor_equiv h^-1 k^-1 x)) ==
idmap
H: Funext
A, B, C, D: Type
h: A <~> C
k: B <~> D
(fun x : A <~> B =>
 functor_equiv h^-1 k^-1 (functor_equiv h k x)) ==
idmap
    -
H: Funext
A, B, C, D: Type
h: A <~> C
k: B <~> D
(fun x : C <~> D =>
 functor_equiv h k (functor_equiv h^-1 k^-1 x)) ==
idmap intros f; apply path_equiv, path_arrow; intros x; simpl.
H: Funext
A, B, C, D: Type
h: A <~> C
k: B <~> D
f: C <~> D
x: C
k (k^-1 (f (h (h^-1 x)))) = f x
      exact (eisretr k _ @ ap f (eisretr h x)).
    -
H: Funext
A, B, C, D: Type
h: A <~> C
k: B <~> D
(fun x : A <~> B =>
 functor_equiv h^-1 k^-1 (functor_equiv h k x)) ==
idmap intros g; apply path_equiv, path_arrow; intros x; simpl.
H: Funext
A, B, C, D: Type
h: A <~> C
k: B <~> D
g: A <~> B
x: A
k^-1 (k (g (h^-1 (h x)))) = g x
      exact (eissect k _ @ ap g (eissect h x)).
  Defined.

  Definition equiv_functor_equiv {A B C D} (h : A <~> C) (k : B <~> D)
  : (A <~> B) <~> (C <~> D)
  := Build_Equiv _ _ (functor_equiv h k) _.

  (** Reversing equivalences is an equivalence *)
  Global Instance isequiv_equiv_inverse {A B}
  : IsEquiv (@equiv_inverse A B).
H: Funext
A, B: Type
IsEquiv equiv_inverse
  Proof.
H: Funext
A, B: Type
IsEquiv equiv_inverse
    refine (isequiv_adjointify _ equiv_inverse _ _);
      intros e; apply path_equiv; reflexivity.
  Defined.

  Definition equiv_equiv_inverse A B
  : (A <~> B) <~> (B <~> A)
    := Build_Equiv _ _ (@equiv_inverse A B) _.

  (** If [functor_sigma idmap g] is an equivalence then so is g *)
  Definition isequiv_from_functor_sigma {A} (P Q : A -> Type)
    (g : forall a, P a -> Q a) `{!IsEquiv (functor_sigma idmap g)}
    : forall (a : A), IsEquiv (g a).
H: Funext
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
IsEquiv0: IsEquiv (functor_sigma idmap g)
forall a : A, IsEquiv (g a)
  Proof.
H: Funext
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
IsEquiv0: IsEquiv (functor_sigma idmap g)
forall a : A, IsEquiv (g a)
    intros a; apply isequiv_contr_map.
H: Funext
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
IsEquiv0: IsEquiv (functor_sigma idmap g)
a: A
IsTruncMap (-2) (g a)
    apply istruncmap_from_functor_sigma.
H: Funext
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
IsEquiv0: IsEquiv (functor_sigma idmap g)
a: A
IsTruncMap (-2) (functor_sigma idmap g)
    exact _.
  Defined.

  (** Theorem 4.7.7 *)
  (** [functor_sigma idmap g] is an equivalence if and only if g is *)
  Definition equiv_total_iff_equiv_fiberwise {A} (P Q : A -> Type)
           (g : forall a, P a -> Q a)
    : IsEquiv (functor_sigma idmap g) <-> forall a, IsEquiv (g a).
H: Funext
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
IsEquiv (functor_sigma idmap g) <->
(forall a : A, IsEquiv (g a))
  Proof.
H: Funext
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
IsEquiv (functor_sigma idmap g) <->
(forall a : A, IsEquiv (g a))
    split.
H: Funext
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
IsEquiv (functor_sigma idmap g) ->
forall a : A, IsEquiv (g a)
H: Funext
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
(forall a : A, IsEquiv (g a)) ->
IsEquiv (functor_sigma idmap g)
    -
H: Funext
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
IsEquiv (functor_sigma idmap g) ->
forall a : A, IsEquiv (g a) apply isequiv_from_functor_sigma.
    -
H: Funext
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
(forall a : A, IsEquiv (g a)) ->
IsEquiv (functor_sigma idmap g) intro K.
H: Funext
A: Type
P, Q: A -> Type
g: forall a : A, P a -> Q a
K: forall a : A, IsEquiv (g a)
IsEquiv (functor_sigma idmap g) apply isequiv_functor_sigma.
  Defined.

End AssumeFunext.

(** We make this a global hint outside of the section. *)
#[export] Hint Immediate isequiv_contr_map : typeclass_instances.

(** 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)).
A: Type
B, C: A -> Type
x1, x2: A
p: x1 = x2
f: B x1 <~> C x1
y: B x2
transport (fun x : A => B x <~> C x) p f y =
transport C p (f (transport B p^ y))
Proof.
A: Type
B, C: A -> Type
x1, x2: A
p: x1 = x2
f: B x1 <~> C x1
y: B x2
transport (fun x : A => B x <~> C x) p f y =
transport C p (f (transport B p^ y))
  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).
A: Type
B, C: A -> Type
x1, x2: A
p: x1 = x2
f: B x1 <~> C x1
transport (fun x : A => B x <~> C x) p f =
equiv_transport C p oE f oE equiv_transport B p^
Proof.
A: Type
B, C: A -> Type
x1, x2: A
p: x1 = x2
f: B x1 <~> C x1
transport (fun x : A => B x <~> C x) p f =
equiv_transport C p oE f oE equiv_transport B p^
  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^).
H: Funext
A: Type
B, C: A -> Type
x1, x2: A
p: x1 = x2
f: B x1 <~> C x1
transport (fun x : A => B x <~> C x) p f =
equiv_transport C p oE f oE equiv_transport B p^
Proof.
H: Funext
A: Type
B, C: A -> Type
x1, x2: A
p: x1 = x2
f: B x1 <~> C x1
transport (fun x : A => B x <~> C x) p f =
equiv_transport C p oE f oE equiv_transport B p^
  apply path_equiv.
H: Funext
A: Type
B, C: A -> Type
x1, x2: A
p: x1 = x2
f: B x1 <~> C x1
transport (fun x : A => B x <~> C x) p f =
equiv_transport C p oE f oE equiv_transport B p^
  destruct p; auto.
Defined.