(* -*- mode: coq; mode: visual-line -*- *)
(** * Theorems about the universe, including the Univalence Axiom. *)

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 Types.Equiv Types.Bool Types.Prod.

Local Open Scope path_scope.

Generalizable Variables A B f.

(** ** Paths *)

Definition equiv_path (A B : Type@{u}) (p : A = B) : A <~> B
  := equiv_transport (fun X => X) p.

Definition equiv_path_V `{Funext} (A B : Type) (p : A = B) :
  equiv_path B A (p^) = (equiv_path A B p)^-1%equiv.
H: Funext
A, B: Type
p: A = B
equiv_path B A p^ = ((equiv_path A B p)^-1)%equiv
Proof.
H: Funext
A, B: Type
p: A = B
equiv_path B A p^ = ((equiv_path A B p)^-1)%equiv
  apply path_equiv.
H: Funext
A, B: Type
p: A = B
equiv_path B A p^ = ((equiv_path A B p)^-1)%equiv
  reflexivity.
Defined.

(** See the note by [Funext] in Overture.v *)
Monomorphic Axiom Univalence : Type0.
Existing Class Univalence.

(** Mark this axiom as a "global axiom", which some of our tactics will automatically handle. *)
Global Instance is_global_axiom_univalence : IsGlobalAxiom Univalence := {}.

Axiom isequiv_equiv_path : forall `{Univalence} (A B : Type@{u}), IsEquiv (equiv_path A B).
Global Existing Instance isequiv_equiv_path.

(** A proof that univalence implies function extensionality can be found in the metatheory file [UnivalenceImpliesFunext], but that actual proof can't be used on our dummy typeclasses.  So we assert the following axiomatic instance.  *)
Global Instance Univalence_implies_Funext `{Univalence} : Funext.
H: Univalence
Funext
Admitted.

Section Univalence.
Context `{Univalence}.

Definition path_universe_uncurried {A B : Type} (f : A <~> B) : A = B
  := (equiv_path A B)^-1 f.

Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B)
  := path_universe_uncurried (Build_Equiv _ _ f feq).

Global Arguments path_universe {A B}%type_scope f%function_scope {feq}.

Definition eta_path_universe {A B : Type} (p : A = B)
  : path_universe (equiv_path A B p) = p
  := eissect (equiv_path A B) p.

Definition eta_path_universe_uncurried {A B : Type} (p : A = B)
  : path_universe_uncurried (equiv_path A B p) = p
  := eissect (equiv_path A B) p.

Definition isequiv_path_universe {A B : Type}
  : IsEquiv (@path_universe_uncurried A B)
 := _.

Definition equiv_path_universe (A B : Type) : (A <~> B) <~> (A = B)
  := Build_Equiv _ _ (@path_universe_uncurried A B) isequiv_path_universe.


Definition equiv_equiv_path  (A B : Type) : (A = B) <~> (A <~> B)
  := (equiv_path_universe A B)^-1%equiv.

(** These operations have too many names, making [rewrite] a pain.  So we give lots of names to the computation laws. *)
Definition path_universe_equiv_path {A B : Type} (p : A = B)
  : path_universe (equiv_path A B p) = p
  := eissect (equiv_path A B) p.
Definition path_universe_uncurried_equiv_path {A B : Type} (p : A = B)
  : path_universe_uncurried (equiv_path A B p) = p
  := eissect (equiv_path A B) p.
Definition path_universe_transport_idmap {A B : Type} (p : A = B)
  : path_universe (transport idmap p) = p
  := eissect (equiv_path A B) p.
Definition path_universe_uncurried_transport_idmap {A B : Type} (p : A = B)
  : path_universe_uncurried (equiv_transport idmap p) = p
  := eissect (equiv_path A B) p.
Definition equiv_path_path_universe {A B : Type} (f : A <~> B)
  : equiv_path A B (path_universe f) = f
  := eisretr (equiv_path A B) f.
Definition equiv_path_path_universe_uncurried {A B : Type} (f : A <~> B)
  : equiv_path A B (path_universe_uncurried f) = f
  := eisretr (equiv_path A B) f.
Definition transport_idmap_path_universe {A B : Type} (f : A <~> B)
  : transport idmap (path_universe f) = f
  := ap equiv_fun (eisretr (equiv_path A B) f).
Definition transport_idmap_path_universe_uncurried {A B : Type} (f : A <~> B)
  : transport idmap (path_universe_uncurried f) = f
  := ap equiv_fun (eisretr (equiv_path A B) f).

(** ** Behavior on path operations *)

(* We explicitly assume [Funext] here, since this result doesn't use [Univalence]. *)
Definition equiv_path_pp `{Funext} {A B C : Type} (p : A = B) (q : B = C)
: equiv_path A C (p @ q) = equiv_path B C q oE equiv_path A B p.
H: Univalence
H0: Funext
A, B, C: Type
p: A = B
q: B = C
equiv_path A C (p @ q) =
equiv_path B C q oE equiv_path A B p
Proof.
H: Univalence
H0: Funext
A, B, C: Type
p: A = B
q: B = C
equiv_path A C (p @ q) =
equiv_path B C q oE equiv_path A B p
  apply path_equiv, path_arrow.
H: Univalence
H0: Funext
A, B, C: Type
p: A = B
q: B = C
equiv_path A C (p @ q) ==
equiv_path B C q oE equiv_path A B p
  nrapply transport_pp.
Defined.

Definition path_universe_compose_uncurried {A B C : Type}
           (f : A <~> B) (g : B <~> C)
: path_universe_uncurried (equiv_compose g f)
= path_universe_uncurried f @ path_universe_uncurried g.
H: Univalence
A, B, C: Type
f: A <~> B
g: B <~> C
path_universe_uncurried (equiv_compose g f) =
path_universe_uncurried f @ path_universe_uncurried g
Proof.
H: Univalence
A, B, C: Type
f: A <~> B
g: B <~> C
path_universe_uncurried (equiv_compose g f) =
path_universe_uncurried f @ path_universe_uncurried g
  revert f.
H: Univalence
A, B, C: Type
g: B <~> C
forall f : A <~> B,
path_universe_uncurried (equiv_compose g f) =
path_universe_uncurried f @ path_universe_uncurried g equiv_intro (equiv_path A B) f.
H: Univalence
A, B, C: Type
g: B <~> C
f: A = B
path_universe_uncurried
  (equiv_compose g (equiv_path A B f)) =
path_universe_uncurried (equiv_path A B f) @
path_universe_uncurried g
  revert g.
H: Univalence
A, B, C: Type
f: A = B
forall g : B <~> C,
path_universe_uncurried
  (equiv_compose g (equiv_path A B f)) =
path_universe_uncurried (equiv_path A B f) @
path_universe_uncurried g equiv_intro (equiv_path B C) g.
H: Univalence
A, B, C: Type
f: A = B
g: B = C
path_universe_uncurried
  (equiv_compose (equiv_path B C g) (equiv_path A B f)) =
path_universe_uncurried (equiv_path A B f) @
path_universe_uncurried (equiv_path B C g)
  refine ((ap path_universe_uncurried (equiv_path_pp f g))^ @ _).
H: Univalence
A, B, C: Type
f: A = B
g: B = C
path_universe_uncurried (equiv_path A C (f @ g)) =
path_universe_uncurried (equiv_path A B f) @
path_universe_uncurried (equiv_path B C g)
  refine (eta_path_universe (f @ g) @ _).
H: Univalence
A, B, C: Type
f: A = B
g: B = C
f @ g =
path_universe_uncurried (equiv_path A B f) @
path_universe_uncurried (equiv_path B C g)
  apply concat2; symmetry; apply eta_path_universe.
Defined.

Definition path_universe_compose {A B C : Type}
           (f : A <~> B) (g : B <~> C)
  : path_universe (g o f) = path_universe f @ path_universe g
  := path_universe_compose_uncurried f g.

Definition path_universe_1 {A : Type}
  : path_universe (equiv_idmap A) = 1
  := eta_path_universe 1.

Definition path_universe_V_uncurried {A B : Type} (f : A <~> B)
  : path_universe_uncurried f^-1 = (path_universe_uncurried f)^.
H: Univalence
A, B: Type
f: A <~> B
path_universe_uncurried f^-1 =
(path_universe_uncurried f)^
Proof.
H: Univalence
A, B: Type
f: A <~> B
path_universe_uncurried f^-1 =
(path_universe_uncurried f)^
  revert f.
H: Univalence
A, B: Type
forall f : A <~> B,
path_universe_uncurried f^-1 =
(path_universe_uncurried f)^ equiv_intro ((equiv_path_universe A B)^-1) p.
H: Univalence
A, B: Type
p: A = B
path_universe_uncurried
  (((equiv_path_universe A B)^-1)%function p)^-1 =
(path_universe_uncurried
   (((equiv_path_universe A B)^-1)%function p))^ simpl.
H: Univalence
A, B: Type
p: A = B
path_universe_uncurried (equiv_path A B p)^-1 =
(path_universe_uncurried (equiv_path A B p))^
  transitivity (p^).
H: Univalence
A, B: Type
p: A = B
path_universe_uncurried (equiv_path A B p)^-1 = p^
H: Univalence
A, B: Type
p: A = B
p^ = (path_universe_uncurried (equiv_path A B p))^
    2: exact (inverse2 (eisretr (equiv_path_universe A B) p)^).
H: Univalence
A, B: Type
p: A = B
path_universe_uncurried (equiv_path A B p)^-1 = p^
  transitivity (path_universe_uncurried (equiv_path B A p^)).
H: Univalence
A, B: Type
p: A = B
path_universe_uncurried (equiv_path A B p)^-1 =
path_universe_uncurried (equiv_path B A p^)
H: Univalence
A, B: Type
p: A = B
path_universe_uncurried (equiv_path B A p^) = p^
  -
H: Univalence
A, B: Type
p: A = B
path_universe_uncurried (equiv_path A B p)^-1 =
path_universe_uncurried (equiv_path B A p^) by refine (ap _ (equiv_path_V A B p)^).
  -
H: Univalence
A, B: Type
p: A = B
path_universe_uncurried (equiv_path B A p^) = p^ by refine (eissect (equiv_path B A) p^).
Defined.

Definition path_universe_V `(f : A -> B) `{IsEquiv A B f}
  : path_universe (f^-1) = (path_universe f)^
  := path_universe_V_uncurried (Build_Equiv A B f _).

(** ** Path operations vs Type operations *)

(** [ap (Equiv A)] behaves like postcomposition. *)
Definition ap_equiv_path_universe A {B C} (f : B <~> C)
: equiv_path (A <~> B) (A <~> C) (ap (Equiv A) (path_universe f))
  = equiv_functor_equiv (equiv_idmap A) f.
H: Univalence
A, B, C: Type
f: B <~> C
equiv_path (A <~> B) (A <~> C)
  (ap (Equiv A) (path_universe f)) =
equiv_functor_equiv 1 f
Proof.
H: Univalence
A, B, C: Type
f: B <~> C
equiv_path (A <~> B) (A <~> C)
  (ap (Equiv A) (path_universe f)) =
equiv_functor_equiv 1 f
  revert f.
H: Univalence
A, B, C: Type
forall f : B <~> C,
equiv_path (A <~> B) (A <~> C)
  (ap (Equiv A) (path_universe f)) =
equiv_functor_equiv 1 f equiv_intro (equiv_path B C) f.
H: Univalence
A, B, C: Type
f: B = C
equiv_path (A <~> B) (A <~> C)
  (ap (Equiv A) (path_universe (equiv_path B C f))) =
equiv_functor_equiv 1 (equiv_path B C f)
  rewrite (eissect (equiv_path B C) f : path_universe (equiv_path B C f) = f).
H: Univalence
A, B, C: Type
f: B = C
equiv_path (A <~> B) (A <~> C) (ap (Equiv A) f) =
equiv_functor_equiv 1 (equiv_path B C f)
  destruct f; simpl.
H: Univalence
A, B: Type
equiv_path (A <~> B) (A <~> B) 1 =
equiv_functor_equiv 1 (equiv_path B B 1)
  apply path_equiv, path_forall; intros g.
H: Univalence
A, B: Type
g: A <~> B
equiv_path (A <~> B) (A <~> B) 1 g =
equiv_functor_equiv 1 (equiv_path B B 1) g
  apply path_equiv, path_forall; intros a.
H: Univalence
A, B: Type
g: A <~> B
a: A
equiv_path (A <~> B) (A <~> B) 1 g a =
equiv_functor_equiv 1 (equiv_path B B 1) g a
  reflexivity.
Defined.

(** [ap (prod A)] behaves like [equiv_functor_prod_l]. *)
Definition ap_prod_l_path_universe A {B C} (f : B <~> C)
  : equiv_path (A * B) (A * C) (ap (prod A) (path_universe f))
    = equiv_functor_prod_l f.
H: Univalence
A, B, C: Type
f: B <~> C
equiv_path (A * B) (A * C)
  (ap (prod A) (path_universe f)) =
equiv_functor_prod_l f
Proof.
H: Univalence
A, B, C: Type
f: B <~> C
equiv_path (A * B) (A * C)
  (ap (prod A) (path_universe f)) =
equiv_functor_prod_l f
  revert f.
H: Univalence
A, B, C: Type
forall f : B <~> C,
equiv_path (A * B) (A * C)
  (ap (prod A) (path_universe f)) =
equiv_functor_prod_l f equiv_intro (equiv_path B C) f.
H: Univalence
A, B, C: Type
f: B = C
equiv_path (A * B) (A * C)
  (ap (prod A) (path_universe (equiv_path B C f))) =
equiv_functor_prod_l (equiv_path B C f)
  rewrite (eissect (equiv_path B C) f : path_universe (equiv_path B C f) = f).
H: Univalence
A, B, C: Type
f: B = C
equiv_path (A * B) (A * C) (ap (prod A) f) =
equiv_functor_prod_l (equiv_path B C f)
  destruct f.
H: Univalence
A, B: Type
equiv_path (A * B) (A * B) (ap (prod A) 1) =
equiv_functor_prod_l (equiv_path B B 1)
  apply path_equiv, path_arrow; intros x; reflexivity.
Defined.

(** [ap (fun Z => Z * A)] behaves like [equiv_functor_prod_r]. *)
Definition ap_prod_r_path_universe A {B C} (f : B <~> C)
  : equiv_path (B * A) (C * A) (ap (fun Z => Z * A) (path_universe f))
    = equiv_functor_prod_r f.
H: Univalence
A, B, C: Type
f: B <~> C
equiv_path (B * A) (C * A)
  (ap (fun Z : Type => Z * A) (path_universe f)) =
equiv_functor_prod_r f
Proof.
H: Univalence
A, B, C: Type
f: B <~> C
equiv_path (B * A) (C * A)
  (ap (fun Z : Type => Z * A) (path_universe f)) =
equiv_functor_prod_r f
  revert f.
H: Univalence
A, B, C: Type
forall f : B <~> C,
equiv_path (B * A) (C * A)
  (ap (fun Z : Type => Z * A) (path_universe f)) =
equiv_functor_prod_r f equiv_intro (equiv_path B C) f.
H: Univalence
A, B, C: Type
f: B = C
equiv_path (B * A) (C * A)
  (ap (fun Z : Type => Z * A)
     (path_universe (equiv_path B C f))) =
equiv_functor_prod_r (equiv_path B C f)
  rewrite (eissect (equiv_path B C) f : path_universe (equiv_path B C f) = f).
H: Univalence
A, B, C: Type
f: B = C
equiv_path (B * A) (C * A)
  (ap (fun Z : Type => Z * A) f) =
equiv_functor_prod_r (equiv_path B C f)
  destruct f.
H: Univalence
A, B: Type
equiv_path (B * A) (B * A)
  (ap (fun Z : Type => Z * A) 1) =
equiv_functor_prod_r (equiv_path B B 1)
  apply path_equiv, path_arrow; intros x; reflexivity.
Defined.

(** ** Transport *)

(** There are two ways we could define [transport_path_universe]: we could give an explicit definition, or we could reduce it to paths by [equiv_ind] and give an explicit definition there.  The two should be equivalent, but we choose the second for now as it makes the currently needed coherence lemmas easier to prove. *)
Definition transport_path_universe_uncurried
           {A B : Type} (f : A <~> B) (z : A)
  : transport (fun X:Type => X) (path_universe_uncurried f) z = f z.
H: Univalence
A, B: Type
f: A <~> B
z: A
transport idmap (path_universe_uncurried f) z = f z
Proof.
H: Univalence
A, B: Type
f: A <~> B
z: A
transport idmap (path_universe_uncurried f) z = f z
  revert f.
H: Univalence
A, B: Type
z: A
forall f : A <~> B,
transport idmap (path_universe_uncurried f) z = f z  equiv_intro (equiv_path A B) p.
H: Univalence
A, B: Type
z: A
p: A = B
transport idmap
  (path_universe_uncurried (equiv_path A B p)) z =
equiv_path A B p z
  exact (ap (fun s => transport idmap s z) (eissect _ p)).
Defined.
(* Alternatively, [apply ap10, transport_idmap_path_universe_uncurried.], but then some later proofs would have to change. *)

Definition transport_path_universe
           {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A)
  : transport (fun X:Type => X) (path_universe f) z = f z
  := transport_path_universe_uncurried (Build_Equiv A B f feq) z.
(* Alternatively, [ap10_equiv (eisretr (equiv_path A B) (Build_Equiv _ _ f feq)) z]. *)

Definition transport_path_universe_equiv_path
           {A B : Type} (p : A = B) (z : A)
  : transport_path_universe (equiv_path A B p) z =
    (ap (fun s => transport idmap s z) (eissect _ p))
  := equiv_ind_comp _ _ _.

(* This somewhat fancier version is useful when working with HITs. *)
Definition transport_path_universe'
  {A : Type} (P : A -> Type) {x y : A} (p : x = y)
  (f : P x <~> P y) (q : ap P p = path_universe f) (u : P x)
  : transport P p u = f u
  := transport_compose idmap P p u
   @ ap10 (ap (transport idmap) q) u
   @ transport_path_universe f u.

(** And a version for transporting backwards. *)

Definition transport_path_universe_V_uncurried
           {A B : Type} (f : A <~> B) (z : B)
  : transport (fun X:Type => X) (path_universe_uncurried f)^ z = f^-1 z.
H: Univalence
A, B: Type
f: A <~> B
z: B
transport idmap (path_universe_uncurried f)^ z =
f^-1 z
Proof.
H: Univalence
A, B: Type
f: A <~> B
z: B
transport idmap (path_universe_uncurried f)^ z =
f^-1 z
  revert f.
H: Univalence
A, B: Type
z: B
forall f : A <~> B,
transport idmap (path_universe_uncurried f)^ z =
f^-1 z equiv_intro (equiv_path A B) p.
H: Univalence
A, B: Type
z: B
p: A = B
transport idmap
  (path_universe_uncurried (equiv_path A B p))^ z =
(equiv_path A B p)^-1 z
  exact (ap (fun s => transport idmap s z) (inverse2 (eissect _ p))).
Defined.

Definition transport_path_universe_V
           {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : B)
  : transport (fun X:Type => X) (path_universe f)^ z = f^-1 z
  := transport_path_universe_V_uncurried (Build_Equiv _ _ f feq) z.
(* Alternatively, [(transport2 idmap (path_universe_V f) z)^ @ (transport_path_universe (f^-1) z)]. *)

Definition transport_path_universe_V_equiv_path
           {A B : Type} (p : A = B) (z : B)
  : transport_path_universe_V (equiv_path A B p) z =
    ap (fun s => transport idmap s z) (inverse2 (eissect _ p))
  := equiv_ind_comp _ _ _.

(** And some coherence for it. *)

Definition transport_path_universe_Vp_uncurried
           {A B : Type} (f : A <~> B) (z : A)
: ap (transport idmap (path_universe f)^) (transport_path_universe f z)
  @ transport_path_universe_V f (f z)
  @ eissect f z
  = transport_Vp idmap (path_universe f) z.
H: Univalence
A, B: Type
f: A <~> B
z: A
(ap (transport idmap (path_universe f)^)
   (transport_path_universe f z) @
 transport_path_universe_V f (f z)) @ eissect f z =
transport_Vp idmap (path_universe f) z
Proof.
H: Univalence
A, B: Type
f: A <~> B
z: A
(ap (transport idmap (path_universe f)^)
   (transport_path_universe f z) @
 transport_path_universe_V f (f z)) @ eissect f z =
transport_Vp idmap (path_universe f) z
  pattern f.
H: Univalence
A, B: Type
f: A <~> B
z: A
(fun e : A <~> B =>
 (ap (transport idmap (path_universe e)^)
    (transport_path_universe e z) @
  transport_path_universe_V e (e z)) @ eissect e z =
 transport_Vp idmap (path_universe e) z) f
  refine (equiv_ind (equiv_path A B) _ _ _); intros p.
H: Univalence
A, B: Type
f: A <~> B
z: A
p: A = B
(ap
   (transport idmap
      (path_universe (equiv_path A B p))^)
   (transport_path_universe (equiv_path A B p) z) @
 transport_path_universe_V (equiv_path A B p)
   (equiv_path A B p z)) @
eissect (equiv_path A B p) z =
transport_Vp idmap (path_universe (equiv_path A B p))
  z
  (* Something slightly sneaky happens here: by definition of [equiv_path], [eissect (equiv_path A B p)] is judgmentally equal to [transport_Vp idmap p].  Thus, we can apply [ap_transport_Vp_idmap]. *)
  refine (_ @ ap_transport_Vp_idmap p (path_universe (equiv_path A B p))
            (eissect (equiv_path A B) p) z).
H: Univalence
A, B: Type
f: A <~> B
z: A
p: A = B
(ap
   (transport idmap
      (path_universe (equiv_path A B p))^)
   (transport_path_universe (equiv_path A B p) z) @
 transport_path_universe_V (equiv_path A B p)
   (equiv_path A B p z)) @
eissect (equiv_path A B p) z =
(ap
   (transport idmap
      (path_universe (equiv_path A B p))^)
   (ap (fun s : A = B => transport idmap s z)
      (eissect (equiv_path A B) p)) @
 ap
   (fun s : B = A =>
    transport idmap s (transport idmap p z))
   (inverse2 (eissect (equiv_path A B) p))) @
transport_Vp idmap p z
  apply whiskerR.
H: Univalence
A, B: Type
f: A <~> B
z: A
p: A = B
ap
  (transport idmap (path_universe (equiv_path A B p))^)
  (transport_path_universe (equiv_path A B p) z) @
transport_path_universe_V (equiv_path A B p)
  (equiv_path A B p z) =
ap
  (transport idmap (path_universe (equiv_path A B p))^)
  (ap (fun s : A = B => transport idmap s z)
     (eissect (equiv_path A B) p)) @
ap
  (fun s : B = A =>
   transport idmap s (transport idmap p z))
  (inverse2 (eissect (equiv_path A B) p)) apply concat2.
H: Univalence
A, B: Type
f: A <~> B
z: A
p: A = B
ap
  (transport idmap (path_universe (equiv_path A B p))^)
  (transport_path_universe (equiv_path A B p) z) =
ap
  (transport idmap (path_universe (equiv_path A B p))^)
  (ap (fun s : A = B => transport idmap s z)
     (eissect (equiv_path A B) p))
H: Univalence
A, B: Type
f: A <~> B
z: A
p: A = B
transport_path_universe_V (equiv_path A B p)
  (equiv_path A B p z) =
ap
  (fun s : B = A =>
   transport idmap s (transport idmap p z))
  (inverse2 (eissect (equiv_path A B) p))
  -
H: Univalence
A, B: Type
f: A <~> B
z: A
p: A = B
ap
  (transport idmap (path_universe (equiv_path A B p))^)
  (transport_path_universe (equiv_path A B p) z) =
ap
  (transport idmap (path_universe (equiv_path A B p))^)
  (ap (fun s : A = B => transport idmap s z)
     (eissect (equiv_path A B) p)) apply ap.
H: Univalence
A, B: Type
f: A <~> B
z: A
p: A = B
transport_path_universe (equiv_path A B p) z =
ap (fun s : A = B => transport idmap s z)
  (eissect (equiv_path A B) p) apply transport_path_universe_equiv_path.
  -
H: Univalence
A, B: Type
f: A <~> B
z: A
p: A = B
transport_path_universe_V (equiv_path A B p)
  (equiv_path A B p z) =
ap
  (fun s : B = A =>
   transport idmap s (transport idmap p z))
  (inverse2 (eissect (equiv_path A B) p)) apply transport_path_universe_V_equiv_path.
Defined.

Definition transport_path_universe_Vp
           {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A)
: ap (transport idmap (path_universe f)^) (transport_path_universe f z)
  @ transport_path_universe_V f (f z)
  @ eissect f z
  = transport_Vp idmap (path_universe f) z
  := transport_path_universe_Vp_uncurried (Build_Equiv A B f feq) z.

(** *** Transporting in particular type families *)

Theorem transport_arrow_toconst_path_universe {A U V : Type} (w : U <~> V)
  : forall f : U -> A, transport (fun E : Type => E -> A) (path_universe w) f = (f o w^-1).
H: Univalence
A, U, V: Type
w: U <~> V
forall f : U -> A,
transport (fun E : Type => E -> A) (path_universe w) f =
f o w^-1
Proof.
H: Univalence
A, U, V: Type
w: U <~> V
forall f : U -> A,
transport (fun E : Type => E -> A) (path_universe w) f =
f o w^-1
  intros f.
H: Univalence
A, U, V: Type
w: U <~> V
f: U -> A
transport (fun E : Type => E -> A) (path_universe w) f =
f o w^-1 funext y.
H: Univalence
A, U, V: Type
w: U <~> V
f: U -> A
y: V
transport (fun E : Type => E -> A) (path_universe w) f
  y = f (w^-1 y)
  refine (transport_arrow_toconst _ _ _ @ _).
H: Univalence
A, U, V: Type
w: U <~> V
f: U -> A
y: V
f (transport idmap (path_universe w)^ y) = f (w^-1 y)
  apply ap.
H: Univalence
A, U, V: Type
w: U <~> V
f: U -> A
y: V
transport idmap (path_universe w)^ y = w^-1 y
  apply transport_path_universe_V.
Defined.

(** ** 2-paths *)

Definition equiv_path2_universe
           {A B : Type} (f g : A <~> B)
: (f == g) <~> (path_universe f = path_universe g).
H: Univalence
A, B: Type
f, g: A <~> B
f == g <~> path_universe f = path_universe g
Proof.
H: Univalence
A, B: Type
f, g: A <~> B
f == g <~> path_universe f = path_universe g
  refine (_ oE equiv_path_arrow f g).
H: Univalence
A, B: Type
f, g: A <~> B
f = g <~> path_universe f = path_universe g
  refine (_ oE equiv_path_equiv f g).
H: Univalence
A, B: Type
f, g: A <~> B
f = g <~> path_universe f = path_universe g
  exact (equiv_ap (equiv_path A B)^-1 _ _).
Defined.

Definition path2_universe
           {A B : Type} {f g : A <~> B}
: (f == g) -> (path_universe f = path_universe g)
  := equiv_path2_universe f g.

Definition equiv_path2_universe_1
           {A B : Type} (f : A <~> B)
: equiv_path2_universe f f (fun x => 1) = 1.
H: Univalence
A, B: Type
f: A <~> B
equiv_path2_universe f f (fun x : A => 1) = 1
Proof.
H: Univalence
A, B: Type
f: A <~> B
equiv_path2_universe f f (fun x : A => 1) = 1
  simpl.
H: Univalence
A, B: Type
f: A <~> B
ap (equiv_path A B)^-1
  ((1 @
    ap
      (fun u : {f : A -> B & IsEquiv f} =>
       {| equiv_fun := u.1; equiv_isequiv := u.2 |})
      (path_sigma_hprop (f; equiv_isequiv f)
         (f; equiv_isequiv f)
         (path_forall f f (fun x : A => 1)))) @ 1) = 1
  rewrite concat_1p, concat_p1, path_forall_1, path_sigma_hprop_1.
H: Univalence
A, B: Type
f: A <~> B
ap (equiv_path A B)^-1
  (ap
     (fun u : {f : A -> B & IsEquiv f} =>
      {| equiv_fun := u.1; equiv_isequiv := u.2 |}) 1) =
1
  reflexivity.
Qed.

Definition path2_universe_1
           {A B : Type} (f : A <~> B)
: @path2_universe _ _ f f (fun x => 1) = 1
  := equiv_path2_universe_1 f.

(** There ought to be a lemma which says something like this:

<<
Definition path2_universe_postcompose
           {A B C : Type} {f1 f2 : A <~> B} (p : f1 == f2)
           (g : B <~> C)
: equiv_path2_universe (g o f1)
                       (g o f2)
                       (fun a => ap g (p a))
  = path_universe_compose f1 g
    @ whiskerR (path2_universe p) (path_universe g)
    @ (path_universe_compose f2 g)^.
>>

and similarly

<<
Definition path2_universe_precompose
           {A B C : Type} {f1 f2 : B <~> C} (p : f1 == f2)
           (g : A <~> B)
: equiv_path2_universe (f1 o g)
                       (f2 o g)
                       (fun a => (p (g a)))
  = path_universe_compose g f1
    @ whiskerL (path_universe g) (path2_universe p)
    @ (path_universe_compose g f2)^.
>>

but I haven't managed to prove them yet.  Fortunately, for existing applications what we actually need is the following rather different-looking version that applies only when [f1] and [f2] are identities. *)

(** Coq is too eager about unfolding [equiv_path_equiv] in the following proofs, so we tell it not to.  We go into a section in order to limit the scope of the [simpl never] command. *)
Section PathEquivSimplNever.
  Local Arguments equiv_path_equiv : simpl never.

  Definition path2_universe_postcompose_idmap
             {A C : Type} (p : forall a:A, a = a)
             (g : A <~> C)
  : equiv_path2_universe g g (fun a => ap g (p a))
    = (concat_1p _)^
      @ whiskerR (path_universe_1)^ (path_universe g)
      @ whiskerR (equiv_path2_universe (equiv_idmap A) (equiv_idmap A) p)
        (path_universe g)
      @ whiskerR path_universe_1 (path_universe g)
      @ concat_1p _.
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
equiv_path2_universe g g (fun a : A => ap g (p a)) =
((((concat_1p (path_universe g))^ @
   whiskerR path_universe_1^ (path_universe g)) @
  whiskerR (equiv_path2_universe 1 1 p)
    (path_universe g)) @
 whiskerR path_universe_1 (path_universe g)) @
concat_1p (path_universe g)
  Proof.
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
equiv_path2_universe g g (fun a : A => ap g (p a)) =
((((concat_1p (path_universe g))^ @
   whiskerR path_universe_1^ (path_universe g)) @
  whiskerR (equiv_path2_universe 1 1 p)
    (path_universe g)) @
 whiskerR path_universe_1 (path_universe g)) @
concat_1p (path_universe g)
    transitivity ((eta_path_universe (path_universe g))^
                  @ equiv_path2_universe
                    (equiv_path A C (path_universe g))
                    (equiv_path A C (path_universe g))
                    (fun a => ap (equiv_path A C (path_universe g)) (p a))
                    @ eta_path_universe (path_universe g)).
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
equiv_path2_universe g g (fun a : A => ap g (p a)) =
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A C (path_universe g))
   (equiv_path A C (path_universe g))
   (fun a : A =>
    ap (equiv_path A C (path_universe g)) (p a))) @
eta_path_universe (path_universe g)
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A C (path_universe g))
   (equiv_path A C (path_universe g))
   (fun a : A =>
    ap (equiv_path A C (path_universe g)) (p a))) @
eta_path_universe (path_universe g) =
((((concat_1p (path_universe g))^ @
   whiskerR path_universe_1^ (path_universe g)) @
  whiskerR (equiv_path2_universe 1 1 p)
    (path_universe g)) @
 whiskerR path_universe_1 (path_universe g)) @
concat_1p (path_universe g)
    -
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
equiv_path2_universe g g (fun a : A => ap g (p a)) =
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A C (path_universe g))
   (equiv_path A C (path_universe g))
   (fun a : A =>
    ap (equiv_path A C (path_universe g)) (p a))) @
eta_path_universe (path_universe g) refine ((apD (fun g' => equiv_path2_universe g' g'
                                (fun a => ap g' (p a)))
                   (eisretr (equiv_path A C) g))^ @ _).
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
transport
  (fun g' : A <~> C =>
   path_universe g' = path_universe g')
  (eisretr (equiv_path A C) g)
  (equiv_path2_universe
     (equiv_path A C ((equiv_path A C)^-1 g))
     (equiv_path A C ((equiv_path A C)^-1 g))
     (fun a : A =>
      ap (equiv_path A C ((equiv_path A C)^-1 g))
        (p a))) =
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A C (path_universe g))
   (equiv_path A C (path_universe g))
   (fun a : A =>
    ap (equiv_path A C (path_universe g)) (p a))) @
eta_path_universe (path_universe g)
      refine (transport_paths_FlFr (eisretr (equiv_path A C) g) _ @ _).
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
((ap path_universe_uncurried
    (eisretr (equiv_path A C) g))^ @
 equiv_path2_universe
   (equiv_path A C ((equiv_path A C)^-1 g))
   (equiv_path A C ((equiv_path A C)^-1 g))
   (fun a : A =>
    ap (equiv_path A C ((equiv_path A C)^-1 g)) (p a))) @
ap path_universe_uncurried
  (eisretr (equiv_path A C) g) =
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A C (path_universe g))
   (equiv_path A C (path_universe g))
   (fun a : A =>
    ap (equiv_path A C (path_universe g)) (p a))) @
eta_path_universe (path_universe g)
      apply concat2.
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
(ap path_universe_uncurried
   (eisretr (equiv_path A C) g))^ @
equiv_path2_universe
  (equiv_path A C ((equiv_path A C)^-1 g))
  (equiv_path A C ((equiv_path A C)^-1 g))
  (fun a : A =>
   ap (equiv_path A C ((equiv_path A C)^-1 g)) (p a)) =
(eta_path_universe (path_universe g))^ @
equiv_path2_universe
  (equiv_path A C (path_universe g))
  (equiv_path A C (path_universe g))
  (fun a : A =>
   ap (equiv_path A C (path_universe g)) (p a))
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
ap path_universe_uncurried
  (eisretr (equiv_path A C) g) =
eta_path_universe (path_universe g)
      +
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
(ap path_universe_uncurried
   (eisretr (equiv_path A C) g))^ @
equiv_path2_universe
  (equiv_path A C ((equiv_path A C)^-1 g))
  (equiv_path A C ((equiv_path A C)^-1 g))
  (fun a : A =>
   ap (equiv_path A C ((equiv_path A C)^-1 g)) (p a)) =
(eta_path_universe (path_universe g))^ @
equiv_path2_universe
  (equiv_path A C (path_universe g))
  (equiv_path A C (path_universe g))
  (fun a : A =>
   ap (equiv_path A C (path_universe g)) (p a)) apply whiskerR.
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
(ap path_universe_uncurried
   (eisretr (equiv_path A C) g))^ =
(eta_path_universe (path_universe g))^
        apply inverse2, symmetry.
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
eta_path_universe (path_universe g) =
ap path_universe_uncurried
  (eisretr (equiv_path A C) g)
        refine (eisadj (equiv_path A C)^-1 g).
      +
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
ap path_universe_uncurried
  (eisretr (equiv_path A C) g) =
eta_path_universe (path_universe g) symmetry; refine (eisadj (equiv_path A C)^-1 g).
    -
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A C (path_universe g))
   (equiv_path A C (path_universe g))
   (fun a : A =>
    ap (equiv_path A C (path_universe g)) (p a))) @
eta_path_universe (path_universe g) =
((((concat_1p (path_universe g))^ @
   whiskerR path_universe_1^ (path_universe g)) @
  whiskerR (equiv_path2_universe 1 1 p)
    (path_universe g)) @
 whiskerR path_universe_1 (path_universe g)) @
concat_1p (path_universe g) generalize (path_universe g).
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
forall p0 : A = C,
((eta_path_universe p0)^ @
 equiv_path2_universe (equiv_path A C p0)
   (equiv_path A C p0)
   (fun a : A => ap (equiv_path A C p0) (p a))) @
eta_path_universe p0 =
((((concat_1p p0)^ @ whiskerR path_universe_1^ p0) @
  whiskerR (equiv_path2_universe 1 1 p) p0) @
 whiskerR path_universe_1 p0) @ concat_1p p0
      intros h.
H: Univalence
A, C: Type
p: forall a : A, a = a
g: A <~> C
h: A = C
((eta_path_universe h)^ @
 equiv_path2_universe (equiv_path A C h)
   (equiv_path A C h)
   (fun a : A => ap (equiv_path A C h) (p a))) @
eta_path_universe h =
((((concat_1p h)^ @ whiskerR path_universe_1^ h) @
  whiskerR (equiv_path2_universe 1 1 p) h) @
 whiskerR path_universe_1 h) @ concat_1p h destruct h.
H: Univalence
A: Type
p: forall a : A, a = a
g: A <~> A
((eta_path_universe 1)^ @
 equiv_path2_universe (equiv_path A A 1)
   (equiv_path A A 1)
   (fun a : A => ap (equiv_path A A 1) (p a))) @
eta_path_universe 1 =
((((concat_1p 1)^ @ whiskerR path_universe_1^ 1) @
  whiskerR (equiv_path2_universe 1 1 p) 1) @
 whiskerR path_universe_1 1) @ concat_1p 1 cbn.
H: Univalence
A: Type
p: forall a : A, a = a
g: A <~> A
((eta_path_universe 1)^ @
 ap (equiv_path A A)^-1
   (equiv_path_equiv (equiv_path A A 1)
      (equiv_path A A 1)
      (path_forall (transport idmap 1)
         (transport idmap 1)
         (fun a : A => ap (transport idmap 1) (p a))))) @
eta_path_universe 1 =
(((1 @ whiskerR path_universe_1^ 1) @
  whiskerR
    (ap (equiv_path A A)^-1
       (equiv_path_equiv 1 1
          (path_forall idmap idmap p))) 1) @
 whiskerR path_universe_1 1) @ 1
      rewrite !concat_1p, !concat_p1.
H: Univalence
A: Type
p: forall a : A, a = a
g: A <~> A
((eta_path_universe 1)^ @
 ap (equiv_path A A)^-1
   (equiv_path_equiv (equiv_path A A 1)
      (equiv_path A A 1)
      (path_forall (transport idmap 1)
         (transport idmap 1)
         (fun a : A => ap (transport idmap 1) (p a))))) @
eta_path_universe 1 =
(whiskerR path_universe_1^ 1 @
 whiskerR
   (ap (equiv_path A A)^-1
      (equiv_path_equiv 1 1
         (path_forall idmap idmap p))) 1) @
whiskerR path_universe_1 1
      refine (_ @ whiskerR (whiskerR_pp 1 path_universe_1^ _) _).
H: Univalence
A: Type
p: forall a : A, a = a
g: A <~> A
((eta_path_universe 1)^ @
 ap (equiv_path A A)^-1
   (equiv_path_equiv (equiv_path A A 1)
      (equiv_path A A 1)
      (path_forall (transport idmap 1)
         (transport idmap 1)
         (fun a : A => ap (transport idmap 1) (p a))))) @
eta_path_universe 1 =
whiskerR
  (path_universe_1^ @
   ap (equiv_path A A)^-1
     (equiv_path_equiv 1 1 (path_forall idmap idmap p)))
  1 @ whiskerR path_universe_1 1
      refine (_ @ whiskerR_pp 1 _ path_universe_1).
H: Univalence
A: Type
p: forall a : A, a = a
g: A <~> A
((eta_path_universe 1)^ @
 ap (equiv_path A A)^-1
   (equiv_path_equiv (equiv_path A A 1)
      (equiv_path A A 1)
      (path_forall (transport idmap 1)
         (transport idmap 1)
         (fun a : A => ap (transport idmap 1) (p a))))) @
eta_path_universe 1 =
whiskerR
  ((path_universe_1^ @
    ap (equiv_path A A)^-1
      (equiv_path_equiv 1 1
         (path_forall idmap idmap p))) @
   path_universe_1) 1
      refine (_ @ (whiskerR_p1_1 _)^).
H: Univalence
A: Type
p: forall a : A, a = a
g: A <~> A
((eta_path_universe 1)^ @
 ap (equiv_path A A)^-1
   (equiv_path_equiv (equiv_path A A 1)
      (equiv_path A A 1)
      (path_forall (transport idmap 1)
         (transport idmap 1)
         (fun a : A => ap (transport idmap 1) (p a))))) @
eta_path_universe 1 =
(path_universe_1^ @
 ap (equiv_path A A)^-1
   (equiv_path_equiv 1 1 (path_forall idmap idmap p))) @
path_universe_1
      apply whiskerR, whiskerL, ap, ap, ap.
H: Univalence
A: Type
p: forall a : A, a = a
g: A <~> A
(fun a : A => ap (transport idmap 1) (p a)) = p
      apply path_forall; intros x; apply ap_idmap.
  Defined.

  Definition path2_universe_precompose_idmap
             {A B : Type} (p : forall b:B, b = b)
             (g : A <~> B)
  : equiv_path2_universe g g (fun a => (p (g a)))
    = (concat_p1 _)^
      @ whiskerL (path_universe g) (path_universe_1)^
      @ whiskerL (path_universe g)
          (equiv_path2_universe (equiv_idmap B) (equiv_idmap B) p)
      @ whiskerL (path_universe g) (path_universe_1)
      @ concat_p1 _.
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
equiv_path2_universe g g (fun a : A => p (g a)) =
((((concat_p1 (path_universe g))^ @
   whiskerL (path_universe g) path_universe_1^) @
  whiskerL (path_universe g)
    (equiv_path2_universe 1 1 p)) @
 whiskerL (path_universe g) path_universe_1) @
concat_p1 (path_universe g)
  Proof.
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
equiv_path2_universe g g (fun a : A => p (g a)) =
((((concat_p1 (path_universe g))^ @
   whiskerL (path_universe g) path_universe_1^) @
  whiskerL (path_universe g)
    (equiv_path2_universe 1 1 p)) @
 whiskerL (path_universe g) path_universe_1) @
concat_p1 (path_universe g)
  transitivity ((eta_path_universe (path_universe g))^
                @ equiv_path2_universe
                  (equiv_path A B (path_universe g))
                  (equiv_path A B (path_universe g))
                  (fun a => p (equiv_path A B (path_universe g) a))
                @ eta_path_universe (path_universe g)).
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
equiv_path2_universe g g (fun a : A => p (g a)) =
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A B (path_universe g))
   (equiv_path A B (path_universe g))
   (fun a : A =>
    p (equiv_path A B (path_universe g) a))) @
eta_path_universe (path_universe g)
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A B (path_universe g))
   (equiv_path A B (path_universe g))
   (fun a : A =>
    p (equiv_path A B (path_universe g) a))) @
eta_path_universe (path_universe g) =
((((concat_p1 (path_universe g))^ @
   whiskerL (path_universe g) path_universe_1^) @
  whiskerL (path_universe g)
    (equiv_path2_universe 1 1 p)) @
 whiskerL (path_universe g) path_universe_1) @
concat_p1 (path_universe g)
  -
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
equiv_path2_universe g g (fun a : A => p (g a)) =
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A B (path_universe g))
   (equiv_path A B (path_universe g))
   (fun a : A =>
    p (equiv_path A B (path_universe g) a))) @
eta_path_universe (path_universe g) refine ((apD (fun g' => equiv_path2_universe g' g'
                              (fun a => p (g' a)))
              (eisretr (equiv_path A B) g))^ @ _).
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
transport
  (fun g' : A <~> B =>
   path_universe g' = path_universe g')
  (eisretr (equiv_path A B) g)
  (equiv_path2_universe
     (equiv_path A B ((equiv_path A B)^-1 g))
     (equiv_path A B ((equiv_path A B)^-1 g))
     (fun a : A =>
      p (equiv_path A B ((equiv_path A B)^-1 g) a))) =
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A B (path_universe g))
   (equiv_path A B (path_universe g))
   (fun a : A =>
    p (equiv_path A B (path_universe g) a))) @
eta_path_universe (path_universe g)
    refine (transport_paths_FlFr (eisretr (equiv_path A B) g) _ @ _).
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
((ap path_universe_uncurried
    (eisretr (equiv_path A B) g))^ @
 equiv_path2_universe
   (equiv_path A B ((equiv_path A B)^-1 g))
   (equiv_path A B ((equiv_path A B)^-1 g))
   (fun a : A =>
    p (equiv_path A B ((equiv_path A B)^-1 g) a))) @
ap path_universe_uncurried
  (eisretr (equiv_path A B) g) =
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A B (path_universe g))
   (equiv_path A B (path_universe g))
   (fun a : A =>
    p (equiv_path A B (path_universe g) a))) @
eta_path_universe (path_universe g)
    apply concat2.
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
(ap path_universe_uncurried
   (eisretr (equiv_path A B) g))^ @
equiv_path2_universe
  (equiv_path A B ((equiv_path A B)^-1 g))
  (equiv_path A B ((equiv_path A B)^-1 g))
  (fun a : A =>
   p (equiv_path A B ((equiv_path A B)^-1 g) a)) =
(eta_path_universe (path_universe g))^ @
equiv_path2_universe
  (equiv_path A B (path_universe g))
  (equiv_path A B (path_universe g))
  (fun a : A => p (equiv_path A B (path_universe g) a))
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
ap path_universe_uncurried
  (eisretr (equiv_path A B) g) =
eta_path_universe (path_universe g)
    +
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
(ap path_universe_uncurried
   (eisretr (equiv_path A B) g))^ @
equiv_path2_universe
  (equiv_path A B ((equiv_path A B)^-1 g))
  (equiv_path A B ((equiv_path A B)^-1 g))
  (fun a : A =>
   p (equiv_path A B ((equiv_path A B)^-1 g) a)) =
(eta_path_universe (path_universe g))^ @
equiv_path2_universe
  (equiv_path A B (path_universe g))
  (equiv_path A B (path_universe g))
  (fun a : A => p (equiv_path A B (path_universe g) a)) apply whiskerR.
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
(ap path_universe_uncurried
   (eisretr (equiv_path A B) g))^ =
(eta_path_universe (path_universe g))^
      apply inverse2, symmetry.
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
eta_path_universe (path_universe g) =
ap path_universe_uncurried
  (eisretr (equiv_path A B) g)
      refine (eisadj (equiv_path A B)^-1 g).
    +
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
ap path_universe_uncurried
  (eisretr (equiv_path A B) g) =
eta_path_universe (path_universe g) symmetry; refine (eisadj (equiv_path A B)^-1 g).
  -
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
((eta_path_universe (path_universe g))^ @
 equiv_path2_universe
   (equiv_path A B (path_universe g))
   (equiv_path A B (path_universe g))
   (fun a : A =>
    p (equiv_path A B (path_universe g) a))) @
eta_path_universe (path_universe g) =
((((concat_p1 (path_universe g))^ @
   whiskerL (path_universe g) path_universe_1^) @
  whiskerL (path_universe g)
    (equiv_path2_universe 1 1 p)) @
 whiskerL (path_universe g) path_universe_1) @
concat_p1 (path_universe g) generalize (path_universe g).
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
forall p0 : A = B,
((eta_path_universe p0)^ @
 equiv_path2_universe (equiv_path A B p0)
   (equiv_path A B p0)
   (fun a : A => p (equiv_path A B p0 a))) @
eta_path_universe p0 =
((((concat_p1 p0)^ @ whiskerL p0 path_universe_1^) @
  whiskerL p0 (equiv_path2_universe 1 1 p)) @
 whiskerL p0 path_universe_1) @ concat_p1 p0
    intros h.
H: Univalence
A, B: Type
p: forall b : B, b = b
g: A <~> B
h: A = B
((eta_path_universe h)^ @
 equiv_path2_universe (equiv_path A B h)
   (equiv_path A B h)
   (fun a : A => p (equiv_path A B h a))) @
eta_path_universe h =
((((concat_p1 h)^ @ whiskerL h path_universe_1^) @
  whiskerL h (equiv_path2_universe 1 1 p)) @
 whiskerL h path_universe_1) @ concat_p1 h destruct h.
H: Univalence
A: Type
p: forall b : A, b = b
g: A <~> A
((eta_path_universe 1)^ @
 equiv_path2_universe (equiv_path A A 1)
   (equiv_path A A 1)
   (fun a : A => p (equiv_path A A 1 a))) @
eta_path_universe 1 =
((((concat_p1 1)^ @ whiskerL 1 path_universe_1^) @
  whiskerL 1 (equiv_path2_universe 1 1 p)) @
 whiskerL 1 path_universe_1) @ concat_p1 1 cbn.
H: Univalence
A: Type
p: forall b : A, b = b
g: A <~> A
((eta_path_universe 1)^ @
 ap (equiv_path A A)^-1
   (equiv_path_equiv (equiv_path A A 1)
      (equiv_path A A 1)
      (path_forall (transport idmap 1)
         (transport idmap 1) (fun a : A => p a)))) @
eta_path_universe 1 =
(((1 @ whiskerL 1 path_universe_1^) @
  whiskerL 1
    (ap (equiv_path A A)^-1
       (equiv_path_equiv 1 1
          (path_forall idmap idmap p)))) @
 whiskerL 1 path_universe_1) @ 1
    rewrite !concat_p1.
H: Univalence
A: Type
p: forall b : A, b = b
g: A <~> A
((eta_path_universe 1)^ @
 ap (equiv_path A A)^-1
   (equiv_path_equiv (equiv_path A A 1)
      (equiv_path A A 1)
      (path_forall (transport idmap 1)
         (transport idmap 1) (fun a : A => p a)))) @
eta_path_universe 1 =
((1 @ whiskerL 1 path_universe_1^) @
 whiskerL 1
   (ap (equiv_path A A)^-1
      (equiv_path_equiv 1 1
         (path_forall idmap idmap p)))) @
whiskerL 1 path_universe_1
    refine (_ @ (((concat_1p (whiskerL 1 path_universe_1^))^ @@ 1) @@ 1)).
H: Univalence
A: Type
p: forall b : A, b = b
g: A <~> A
((eta_path_universe 1)^ @
 ap (equiv_path A A)^-1
   (equiv_path_equiv (equiv_path A A 1)
      (equiv_path A A 1)
      (path_forall (transport idmap 1)
         (transport idmap 1) (fun a : A => p a)))) @
eta_path_universe 1 =
(whiskerL 1 path_universe_1^ @
 whiskerL 1
   (ap (equiv_path A A)^-1
      (equiv_path_equiv 1 1
         (path_forall idmap idmap p)))) @
whiskerL 1 path_universe_1
    refine (_ @ whiskerR (whiskerL_pp 1 path_universe_1^ _) _).
H: Univalence
A: Type
p: forall b : A, b = b
g: A <~> A
((eta_path_universe 1)^ @
 ap (equiv_path A A)^-1
   (equiv_path_equiv (equiv_path A A 1)
      (equiv_path A A 1)
      (path_forall (transport idmap 1)
         (transport idmap 1) (fun a : A => p a)))) @
eta_path_universe 1 =
whiskerL 1
  (path_universe_1^ @
   ap (equiv_path A A)^-1
     (equiv_path_equiv 1 1 (path_forall idmap idmap p))) @
whiskerL 1 path_universe_1
    refine (_ @ whiskerL_pp 1 _ path_universe_1).
H: Univalence
A: Type
p: forall b : A, b = b
g: A <~> A
((eta_path_universe 1)^ @
 ap (equiv_path A A)^-1
   (equiv_path_equiv (equiv_path A A 1)
      (equiv_path A A 1)
      (path_forall (transport idmap 1)
         (transport idmap 1) (fun a : A => p a)))) @
eta_path_universe 1 =
whiskerL 1
  ((path_universe_1^ @
    ap (equiv_path A A)^-1
      (equiv_path_equiv 1 1
         (path_forall idmap idmap p))) @
   path_universe_1)
    exact ((whiskerL_1p_1 _)^).
  Defined.

End PathEquivSimplNever.

(** ** 3-paths *)

Definition equiv_path3_universe
           {A B : Type} {f g : A <~> B} (p q : f == g)
: (p == q) <~> (path2_universe p = path2_universe q).
H: Univalence
A, B: Type
f, g: A <~> B
p, q: f == g
p == q <~> path2_universe p = path2_universe q
Proof.
H: Univalence
A, B: Type
f, g: A <~> B
p, q: f == g
p == q <~> path2_universe p = path2_universe q
  refine (_ oE equiv_path_forall p q).
H: Univalence
A, B: Type
f, g: A <~> B
p, q: f == g
p = q <~> path2_universe p = path2_universe q
  refine (_ oE equiv_ap (equiv_path_arrow f g) p q).
H: Univalence
A, B: Type
f, g: A <~> B
p, q: f == g
equiv_path_arrow f g p = equiv_path_arrow f g q <~>
path2_universe p = path2_universe q
  refine (_ oE equiv_ap (equiv_path_equiv f g) _ _).
H: Univalence
A, B: Type
f, g: A <~> B
p, q: f == g
equiv_path_equiv f g (equiv_path_arrow f g p) =
equiv_path_equiv f g (equiv_path_arrow f g q) <~>
path2_universe p = path2_universe q
  unfold path2_universe, equiv_path2_universe.
H: Univalence
A, B: Type
f, g: A <~> B
p, q: f == g
equiv_path_equiv f g (equiv_path_arrow f g p) =
equiv_path_equiv f g (equiv_path_arrow f g q) <~>
(equiv_ap (equiv_path A B)^-1 f g
 oE equiv_path_equiv f g oE equiv_path_arrow f g) p =
(equiv_ap (equiv_path A B)^-1 f g
 oE equiv_path_equiv f g oE equiv_path_arrow f g) q
  simpl.
H: Univalence
A, B: Type
f, g: A <~> B
p, q: f == g
(1 @
 ap
   (fun u : {f : A -> B & IsEquiv f} =>
    {| equiv_fun := u.1; equiv_isequiv := u.2 |})
   (path_sigma_hprop (f; equiv_isequiv f)
      (g; equiv_isequiv g) (path_forall f g p))) @ 1 =
(1 @
 ap
   (fun u : {f : A -> B & IsEquiv f} =>
    {| equiv_fun := u.1; equiv_isequiv := u.2 |})
   (path_sigma_hprop (f; equiv_isequiv f)
      (g; equiv_isequiv g) (path_forall f g q))) @ 1 <~>
ap (equiv_path A B)^-1
  ((1 @
    ap
      (fun u : {f : A -> B & IsEquiv f} =>
       {| equiv_fun := u.1; equiv_isequiv := u.2 |})
      (path_sigma_hprop (f; equiv_isequiv f)
         (g; equiv_isequiv g) (path_forall f g p))) @
   1) =
ap (equiv_path A B)^-1
  ((1 @
    ap
      (fun u : {f : A -> B & IsEquiv f} =>
       {| equiv_fun := u.1; equiv_isequiv := u.2 |})
      (path_sigma_hprop (f; equiv_isequiv f)
         (g; equiv_isequiv g) (path_forall f g q))) @
   1) refine (equiv_ap (ap (equiv_path A B)^-1) _ _).
Defined.

Definition path3_universe
           {A B : Type} {f g : A <~> B} {p q : f == g}
: (p == q) -> (path2_universe p = path2_universe q)
  := equiv_path3_universe p q.

Definition transport_path_universe_pV_uncurried
           {A B : Type} (f : A <~> B) (z : B)
: transport_path_universe f (transport idmap (path_universe f)^ z)
  @ ap f (transport_path_universe_V f z)
  @ eisretr f z
  = transport_pV idmap (path_universe f) z.
H: Univalence
A, B: Type
f: A <~> B
z: B
(transport_path_universe f
   (transport idmap (path_universe f)^ z) @
 ap f (transport_path_universe_V f z)) @ eisretr f z =
transport_pV idmap (path_universe f) z
Proof.
H: Univalence
A, B: Type
f: A <~> B
z: B
(transport_path_universe f
   (transport idmap (path_universe f)^ z) @
 ap f (transport_path_universe_V f z)) @ eisretr f z =
transport_pV idmap (path_universe f) z
  pattern f.
H: Univalence
A, B: Type
f: A <~> B
z: B
(fun e : A <~> B =>
 (transport_path_universe e
    (transport idmap (path_universe e)^ z) @
  ap e (transport_path_universe_V e z)) @ eisretr e z =
 transport_pV idmap (path_universe e) z) f
  refine (equiv_ind (equiv_path A B) _ _ _); intros p.
H: Univalence
A, B: Type
f: A <~> B
z: B
p: A = B
(transport_path_universe (equiv_path A B p)
   (transport idmap
      (path_universe (equiv_path A B p))^ z) @
 ap (equiv_path A B p)
   (transport_path_universe_V (equiv_path A B p) z)) @
eisretr (equiv_path A B p) z =
transport_pV idmap (path_universe (equiv_path A B p))
  z
  refine (_ @ ap_transport_pV_idmap p (path_universe (equiv_path A B p))
            (eissect (equiv_path A B) p) z).
H: Univalence
A, B: Type
f: A <~> B
z: B
p: A = B
(transport_path_universe (equiv_path A B p)
   (transport idmap
      (path_universe (equiv_path A B p))^ z) @
 ap (equiv_path A B p)
   (transport_path_universe_V (equiv_path A B p) z)) @
eisretr (equiv_path A B p) z =
(ap
   (transport idmap (path_universe (equiv_path A B p)))
   (ap (fun s : A = B => transport idmap s^ z)
      (eissect (equiv_path A B) p)) @
 ap
   (fun s : A = B =>
    transport idmap s (transport idmap p^ z))
   (eissect (equiv_path A B) p)) @
transport_pV idmap p z
  apply whiskerR.
H: Univalence
A, B: Type
f: A <~> B
z: B
p: A = B
transport_path_universe (equiv_path A B p)
  (transport idmap (path_universe (equiv_path A B p))^
     z) @
ap (equiv_path A B p)
  (transport_path_universe_V (equiv_path A B p) z) =
ap
  (transport idmap (path_universe (equiv_path A B p)))
  (ap (fun s : A = B => transport idmap s^ z)
     (eissect (equiv_path A B) p)) @
ap
  (fun s : A = B =>
   transport idmap s (transport idmap p^ z))
  (eissect (equiv_path A B) p)
  refine ((concat_Ap _ _)^ @ _).
H: Univalence
A, B: Type
f: A <~> B
z: B
p: A = B
ap
  (transport idmap (path_universe (equiv_path A B p)))
  (transport_path_universe_V (equiv_path A B p) z) @
transport_path_universe (equiv_path A B p)
  ((equiv_path A B p)^-1 z) =
ap
  (transport idmap (path_universe (equiv_path A B p)))
  (ap (fun s : A = B => transport idmap s^ z)
     (eissect (equiv_path A B) p)) @
ap
  (fun s : A = B =>
   transport idmap s (transport idmap p^ z))
  (eissect (equiv_path A B) p)
  apply concat2.
H: Univalence
A, B: Type
f: A <~> B
z: B
p: A = B
ap
  (transport idmap (path_universe (equiv_path A B p)))
  (transport_path_universe_V (equiv_path A B p) z) =
ap
  (transport idmap (path_universe (equiv_path A B p)))
  (ap (fun s : A = B => transport idmap s^ z)
     (eissect (equiv_path A B) p))
H: Univalence
A, B: Type
f: A <~> B
z: B
p: A = B
transport_path_universe (equiv_path A B p)
  ((equiv_path A B p)^-1 z) =
ap
  (fun s : A = B =>
   transport idmap s (transport idmap p^ z))
  (eissect (equiv_path A B) p)
  -
H: Univalence
A, B: Type
f: A <~> B
z: B
p: A = B
ap
  (transport idmap (path_universe (equiv_path A B p)))
  (transport_path_universe_V (equiv_path A B p) z) =
ap
  (transport idmap (path_universe (equiv_path A B p)))
  (ap (fun s : A = B => transport idmap s^ z)
     (eissect (equiv_path A B) p)) apply ap.
H: Univalence
A, B: Type
f: A <~> B
z: B
p: A = B
transport_path_universe_V (equiv_path A B p) z =
ap (fun s : A = B => transport idmap s^ z)
  (eissect (equiv_path A B) p)
    refine (transport_path_universe_V_equiv_path _ _ @ _).
H: Univalence
A, B: Type
f: A <~> B
z: B
p: A = B
ap (fun s : B = A => transport idmap s z)
  (inverse2 (eissect (equiv_path A B) p)) =
ap (fun s : A = B => transport idmap s^ z)
  (eissect (equiv_path A B) p)
    unfold inverse2.
H: Univalence
A, B: Type
f: A <~> B
z: B
p: A = B
ap (fun s : B = A => transport idmap s z)
  (ap inverse (eissect (equiv_path A B) p)) =
ap (fun s : A = B => transport idmap s^ z)
  (eissect (equiv_path A B) p) symmetry; apply (ap_compose inverse (fun s => transport idmap s z)).
  -
H: Univalence
A, B: Type
f: A <~> B
z: B
p: A = B
transport_path_universe (equiv_path A B p)
  ((equiv_path A B p)^-1 z) =
ap
  (fun s : A = B =>
   transport idmap s (transport idmap p^ z))
  (eissect (equiv_path A B) p) apply transport_path_universe_equiv_path.
Defined.

Definition transport_path_universe_pV
           {A B : Type} (f : A -> B) {feq : IsEquiv f } (z : B)
: transport_path_universe f (transport idmap (path_universe f)^ z)
  @ ap f (transport_path_universe_V f z)
  @ eisretr f z
  = transport_pV idmap (path_universe f) z
:= transport_path_universe_pV_uncurried (Build_Equiv A B f feq) z.

(** ** Equivalence induction *)

(** Paulin-Mohring style *)
Theorem equiv_induction {U : Type} (P : forall V, U <~> V -> Type) :
  (P U (equiv_idmap U)) -> (forall V (w : U <~> V), P V w).
H: Univalence
U: Type
P: forall V : Type, U <~> V -> Type
P U 1%equiv -> forall (V : Type) (w : U <~> V), P V w
Proof.
H: Univalence
U: Type
P: forall V : Type, U <~> V -> Type
P U 1%equiv -> forall (V : Type) (w : U <~> V), P V w
  intros H0 V.
H: Univalence
U: Type
P: forall V : Type, U <~> V -> Type
H0: P U 1%equiv
V: Type
forall w : U <~> V, P V w
  apply (equiv_ind (equiv_path U V)).
H: Univalence
U: Type
P: forall V : Type, U <~> V -> Type
H0: P U 1%equiv
V: Type
forall x : U = V, P V (equiv_path U V x)
  intro p; induction p; exact H0.
Defined.

Definition equiv_induction_comp {U : Type} (P : forall V, U <~> V -> Type)
  (didmap : P U (equiv_idmap U))
  : equiv_induction P didmap U (equiv_idmap U) = didmap
  := (equiv_ind_comp (P U) _ 1).

(** Martin-Lof style *)
Theorem equiv_induction' (P : forall U V, U <~> V -> Type) :
  (forall T, P T T (equiv_idmap T)) -> (forall U V (w : U <~> V), P U V w).
H: Univalence
P: forall U V : Type, U <~> V -> Type
(forall T : Type, P T T 1%equiv) ->
forall (U V : Type) (w : U <~> V), P U V w
Proof.
H: Univalence
P: forall U V : Type, U <~> V -> Type
(forall T : Type, P T T 1%equiv) ->
forall (U V : Type) (w : U <~> V), P U V w
  intros H0 U V w.
H: Univalence
P: forall U V : Type, U <~> V -> Type
H0: forall T : Type, P T T 1%equiv
U, V: Type
w: U <~> V
P U V w
  apply (equiv_ind (equiv_path U V)).
H: Univalence
P: forall U V : Type, U <~> V -> Type
H0: forall T : Type, P T T 1%equiv
U, V: Type
w: U <~> V
forall x : U = V, P U V (equiv_path U V x)
  intro p; induction p; apply H0.
Defined.

Definition equiv_induction'_comp (P : forall U V, U <~> V -> Type)
  (didmap : forall T, P T T (equiv_idmap T)) (U : Type)
  : equiv_induction' P didmap U U (equiv_idmap U) = didmap U
  := (equiv_ind_comp (P U U) _ 1).

Theorem equiv_induction_inv {U : Type} (P : forall V, V <~> U -> Type) :
  (P U (equiv_idmap U)) -> (forall V (w : V <~> U), P V w).
H: Univalence
U: Type
P: forall V : Type, V <~> U -> Type
P U 1%equiv -> forall (V : Type) (w : V <~> U), P V w
Proof.
H: Univalence
U: Type
P: forall V : Type, V <~> U -> Type
P U 1%equiv -> forall (V : Type) (w : V <~> U), P V w
  intros H0 V.
H: Univalence
U: Type
P: forall V : Type, V <~> U -> Type
H0: P U 1%equiv
V: Type
forall w : V <~> U, P V w
  apply (equiv_ind (equiv_path V U)).
H: Univalence
U: Type
P: forall V : Type, V <~> U -> Type
H0: P U 1%equiv
V: Type
forall x : V = U, P V (equiv_path V U x)
  (* We manually apply [paths_ind_r] to reduce universe levels. *)
  revert V; rapply paths_ind_r; apply H0.
Defined.

Definition equiv_induction_inv_comp {U : Type} (P : forall V, V <~> U -> Type)
  (didmap : P U (equiv_idmap U))
  : equiv_induction_inv P didmap U (equiv_idmap U) = didmap
  := (equiv_ind_comp (P U) _ 1).

(** ** Based equivalence types *)

Global Instance contr_basedequiv@{u +} {X : Type@{u}}
: Contr {Y : Type@{u} & X <~> Y}.
H: Univalence
X: Type
Contr {Y : Type & X <~> Y}
Proof.
H: Univalence
X: Type
Contr {Y : Type & X <~> Y}
  apply (Build_Contr _ (X; equiv_idmap)).
H: Univalence
X: Type
forall y : {x : _ & X <~> x}, (X; 1%equiv) = y
  intros [Y f]; revert Y f.
H: Univalence
X: Type
forall (Y : Type) (f : X <~> Y), (X; 1%equiv) = (Y; f)
  exact (equiv_induction _ idpath).
Defined.

Global Instance contr_basedequiv'@{u +} {X : Type@{u}}
: Contr {Y : Type@{u} & Y <~> X}.
H: Univalence
X: Type
Contr {Y : Type & Y <~> X}
Proof.
H: Univalence
X: Type
Contr {Y : Type & Y <~> X}
  (* The next line is used so that Coq can figure out the type of (X; equiv_idmap). *)
  srapply Build_Contr.
H: Univalence
X: Type
{Y : Type & Y <~> X}
H: Univalence
X: Type
forall y : {Y : Type & Y <~> X}, ?center = y
  -
H: Univalence
X: Type
{Y : Type & Y <~> X} exact (X; equiv_idmap).
  -
H: Univalence
X: Type
forall y : {Y : Type & Y <~> X}, (X; 1%equiv) = y intros [Y f]; revert Y f.
H: Univalence
X: Type
forall (Y : Type) (f : Y <~> X), (X; 1%equiv) = (Y; f)
    refine (equiv_induction_inv _ idpath).
Defined.

(** ** Truncations *)

(** Truncatedness of the universe is a subtle question, but with univalence we can conclude things about truncations of certain of its path-spaces. *)
Global Instance istrunc_paths_Type
       {n : trunc_index} {A B : Type} `{IsTrunc n.+1 B}
: IsTrunc n.+1 (A = B).
H: Univalence
n: trunc_index
A, B: Type
IsTrunc0: IsTrunc n.+1 B
IsTrunc n.+1 (A = B)
Proof.
H: Univalence
n: trunc_index
A, B: Type
IsTrunc0: IsTrunc n.+1 B
IsTrunc n.+1 (A = B)
  refine (istrunc_isequiv_istrunc _ path_universe_uncurried).
Defined.

(** We can also say easily that the universe is not a set. *)
Definition not_hset_Type : ~ (IsHSet Type).
H: Univalence
~ IsHSet Type
Proof.
H: Univalence
~ IsHSet Type
  intro HT.
H: Univalence
HT: IsHSet Type
Empty
  apply true_ne_false.
H: Univalence
HT: IsHSet Type
true = false
  pose (r := path_ishprop (path_universe equiv_negb) 1).
H: Univalence
HT: IsHSet Type
r:= path_ishprop (path_universe equiv_negb) 1: path_universe equiv_negb = 1
true = false
  refine (_ @ (ap (fun q => transport idmap q false) r)).
H: Univalence
HT: IsHSet Type
r:= path_ishprop (path_universe equiv_negb) 1: path_universe equiv_negb = 1
true =
transport idmap (path_universe equiv_negb) false
  symmetry; apply transport_path_universe.
Defined.

End Univalence.