# Theorems about the universe, including the Univalence Axiom.

Require Import HoTT.Basics.
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

Global Instance isequiv_path {A B : Type} (p : A = B)
: IsEquiv (transport (fun X:TypeX) p) | 0
:= Build_IsEquiv _ _ _ (transport (fun X:TypeX) p^)
(transport_pV idmap p)
(transport_Vp idmap p)
(fun amatch p in _ = C return
(transport_pp idmap p^ p (transport idmap p a))^ @
transport2 idmap (concat_Vp p) (transport idmap p a) =
ap (transport idmap p) ((transport_pp idmap p p^ a) ^ @
transport2 idmap (concat_pV p) a) with idpath ⇒ 1 end).

Definition equiv_path (A B : Type) (p : A = B) : A <~> B
:= Build_Equiv _ _ (transport (fun X:TypeX) p) _.

Definition equiv_path_V `{Funext} (A B : Type) (p : A = B) :
equiv_path B A (p^) = (equiv_path A B p)^-1%equiv.
Proof.
destruct p. simpl. unfold equiv_path, equiv_inverse. simpl. apply ap.
refine (@path_ishprop _ (hprop_isequiv _) _ _).
Defined.

See the note by Funext in Overture.v
Monomorphic Axiom Univalence : Type0.
Existing Class Univalence.
Axiom isequiv_equiv_path : `{Univalence} (A B : Type), 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.

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.

## Behavior on path operations

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.
Proof.
destruct p, q. simpl.
apply path_equiv, path_arrow.
intros x; reflexivity.
Defined.

Definition path_universe_compose_uncurried `{Funext} {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.
revert f. equiv_intro (equiv_path A B) f.
revert g. equiv_intro (equiv_path B C) g.
refine ((ap path_universe_uncurried (equiv_path_pp f g))^ @ _).
refine (eta_path_universe (f @ g) @ _).
apply concat2; symmetry; apply eta_path_universe.
Defined.

Definition path_universe_compose `{Funext} {A B C : Type}
(f : A <~> B) (g : B <~> C)
: path_universe (g o f) = path_universe f @ path_universe g.
Proof.
revert f. equiv_intro (equiv_path A B) f.
revert g. equiv_intro (equiv_path B C) g.
refine ((ap path_universe_uncurried (equiv_path_pp f g))^ @ _).
refine (eta_path_universe (f @ g) @ _).
apply concat2; symmetry; apply eta_path_universe.
Defined.

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

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

Definition path_universe_V `{Funext} `(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 A) behaves like postcomposition.
Definition ap_equiv_path_universe `{Funext} 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.
Proof.
revert f. equiv_intro (equiv_path B C) f.
rewrite (eissect (equiv_path B C) f : path_universe (equiv_path B C f) = f).
destruct f; simpl.
apply path_equiv, path_forall; intros g.
apply path_equiv, path_forall; intros a.
reflexivity.
Defined.

ap (prod A) behaves like equiv_functor_prod_l.
Definition ap_prod_l_path_universe `{Funext} A {B C} (f : B <~> C)
: equiv_path (A × B) (A × C) (ap (prod A) (path_universe f))
= equiv_functor_prod_l f.
Proof.
revert f. equiv_intro (equiv_path B C) f.
rewrite (eissect (equiv_path B C) f : path_universe (equiv_path B C f) = f).
destruct f.
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 `{Funext} A {B C} (f : B <~> C)
: equiv_path (B × A) (C × A) (ap (fun ZZ × A) (path_universe f))
= equiv_functor_prod_r f.
Proof.
revert f. equiv_intro (equiv_path B C) f.
rewrite (eissect (equiv_path B C) f : path_universe (equiv_path B C f) = f).
destruct f.
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:TypeX) (path_universe_uncurried f) z = f z.
Proof.
revert f. equiv_intro (equiv_path A B) p.
exact (ap (fun stransport idmap s z) (eissect _ p)).
Defined.

Definition transport_path_universe
{A B : Type} (f : A B) {feq : IsEquiv f} (z : A)
: transport (fun X:TypeX) (path_universe f) z = f z
:= transport_path_universe_uncurried (Build_Equiv A B 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 stransport idmap s z) (eissect _ p))
:= equiv_ind_comp _ _ _.

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 `{Funext}
{A B : Type} (f : A <~> B) (z : B)
: transport (fun X:TypeX) (path_universe_uncurried f)^ z = f^-1 z.
Proof.
revert f. equiv_intro (equiv_path A B) p.
exact (ap (fun stransport idmap s z) (inverse2 (eissect _ p))).
Defined.

Definition transport_path_universe_V `{Funext}
{A B : Type} (f : A B) {feq : IsEquiv f} (z : B)
: transport (fun X:TypeX) (path_universe f)^ z = f^-1 z
:= transport_path_universe_V_uncurried (Build_Equiv _ _ f feq) z.

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

And some coherence for it.

Definition transport_path_universe_Vp_uncurried `{Funext}
{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.
pattern f.
refine (equiv_ind (equiv_path A B) _ _ _); intros p.
refine (_ @ ap_transport_Vp_idmap p (path_universe (equiv_path A B p))
(eissect (equiv_path A B) p) z).
apply whiskerR. apply concat2.
- apply ap. apply transport_path_universe_equiv_path.
- apply transport_path_universe_V_equiv_path.
Defined.

Definition transport_path_universe_Vp `{Funext}
{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.

## 2-paths

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

Definition path2_universe `{Funext}
{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 `{Funext}
{A B : Type} (f : A <~> B)
: equiv_path2_universe f f (fun x ⇒ 1) = 1.
Proof.
simpl.
rewrite concat_1p, concat_p1, path_forall_1, path_sigma_hprop_1.
reflexivity.
Qed.

Definition path2_universe_1 `{Funext}
{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 `{Funext}
{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 `{Funext}
{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 `{Funext}
{A C : Type} (p : a:A, a = a)
(g : A <~> C)
: equiv_path2_universe g g (fun aap 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 _.
Proof.
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 aap (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 aap g' (p a)))
(eisretr (equiv_path A C) g))^ @ _).
refine (transport_paths_FlFr (eisretr (equiv_path A C) g) _ @ _).
apply concat2.
+ apply whiskerR.
apply inverse2, symmetry.
refine (eisadj (equiv_path A C)^-1 g).
+ symmetry; refine (eisadj (equiv_path A C)^-1 g).
- generalize (path_universe g).
intros h. destruct h. cbn.
rewrite !concat_1p, !concat_p1.
refine (_ @ whiskerR (whiskerR_pp 1 path_universe_1^ _) _).
refine (_ @ whiskerR_pp 1 _ path_universe_1).
refine (_ @ (whiskerR_p1_1 _)^).
apply whiskerR, whiskerL, ap, ap, ap.
apply path_forall; intros x; apply ap_idmap.
Defined.

Definition path2_universe_precompose_idmap `{Funext}
{A B : Type} (p : 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 _.
Proof.
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 ap (equiv_path A B (path_universe g) a))
@ eta_path_universe (path_universe g)).
- refine ((apD (fun g'equiv_path2_universe g' g'
(fun ap (g' a)))
(eisretr (equiv_path A B) g))^ @ _).
refine (transport_paths_FlFr (eisretr (equiv_path A B) g) _ @ _).
apply concat2.
+ apply whiskerR.
apply inverse2, symmetry.
refine (eisadj (equiv_path A B)^-1 g).
+ symmetry; refine (eisadj (equiv_path A B)^-1 g).
- generalize (path_universe g).
intros h. destruct h. cbn.
rewrite !concat_p1.
refine (_ @ (((concat_1p (whiskerL 1 path_universe_1^))^ @@ 1) @@ 1)).
refine (_ @ whiskerR (whiskerL_pp 1 path_universe_1^ _) _).
refine (_ @ whiskerL_pp 1 _ path_universe_1).
exact ((whiskerL_1p_1 _)^).
Defined.

End PathEquivSimplNever.

## 3-paths

Definition equiv_path3_universe `{Funext}
{A B : Type} {f g : A <~> B} (p q : f == g)
: (p == q) <~> (path2_universe p = path2_universe q).
Proof.
refine (_ oE equiv_path_forall p q).
refine (_ oE equiv_ap (equiv_path_arrow f g) p q).
refine (_ oE equiv_ap (equiv_path_equiv f g) _ _).
unfold path2_universe, equiv_path2_universe.
simpl. refine (equiv_ap (ap (equiv_path A B)^-1) _ _).
Defined.

Definition path3_universe `{Funext}
{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 `{Funext}
{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.
pattern f.
refine (equiv_ind (equiv_path A B) _ _ _); intros p.
refine (_ @ ap_transport_pV_idmap p (path_universe (equiv_path A B p))
(eissect (equiv_path A B) p) z).
apply whiskerR.
refine ((concat_Ap _ _)^ @ _).
apply concat2.
- apply ap.
refine (transport_path_universe_V_equiv_path _ _ @ _).
unfold inverse2. symmetry; apply (ap_compose inverse (fun stransport idmap s z)).
- apply transport_path_universe_equiv_path.
Defined.

Definition transport_path_universe_pV `{Funext}
{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 : V, U <~> V Type) :
(P U (equiv_idmap U)) ( V (w : U <~> V), P V w).
Proof.
intros H0 V.
apply (equiv_ind (equiv_path U V)).
intro p; induction p; exact H0.
Defined.

Definition equiv_induction_comp {U : Type} (P : 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 : U V, U <~> V Type) :
( T, P T T (equiv_idmap T)) ( U V (w : U <~> V), P U V w).
Proof.
intros H0 U V w.
apply (equiv_ind (equiv_path U V)).
intro p; induction p; apply H0.
Defined.

Definition equiv_induction'_comp (P : U V, U <~> V Type)
(didmap : 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 : V, V <~> U Type) :
(P U (equiv_idmap U)) ( V (w : V <~> U), P V w).
Proof.
intros H0 V.
apply (equiv_ind (equiv_path V U)).
intro p; induction p; apply H0.
Defined.

Definition equiv_induction_inv_comp {U : Type} (P : 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 {X : Type}
: Contr {Y : Type & X <~> Y}.
Proof.
(X; equiv_idmap).
intros [Y f]; revert Y f.
exact (equiv_induction _ idpath).
Defined.

Global Instance contr_basedequiv' {X : Type}
: Contr {Y : Type & Y <~> X}.
Proof.
srapply Build_Contr.
- exact (X; equiv_idmap).
- intros [Y f]; revert 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 `{Funext}
{n : trunc_index} {A B : Type} `{IsTrunc n.+1 B}
: IsTrunc n.+1 (A = B).
Proof.
refine (trunc_equiv _ path_universe_uncurried).
Defined.

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

End Univalence.