Require Import HoTT.Basics.Require Import HoTT.Basics.
Require Import Types.Universe.
Require Import Metatheory.Core Metatheory.FunextVarieties.

Generalizable All Variables.

(** * Univalence Implies Functional Extensionality *)

Section UnivalenceImpliesFunext.
  Context `{ua : Univalence_type}.

  (** Exponentiation preserves equivalences, i.e., if [e] is an equivalence then so is post-composition by [e]. *)

  (* Should this go somewhere else? *)

  Theorem univalence_isequiv_postcompose `{H0 : IsEquiv A B w} C : IsEquiv (fun (g:C->A) => w o g).
ua: Univalence_type
A, B: Type
w: A -> B
H0: IsEquiv w
C: Type
IsEquiv (fun g : C -> A => w o g)
  Proof.
ua: Univalence_type
A, B: Type
w: A -> B
H0: IsEquiv w
C: Type
IsEquiv (fun g : C -> A => w o g)
    unfold Univalence_type in *.
ua: forall A0 B0 : Type, IsEquiv (equiv_path A0 B0)
A, B: Type
w: A -> B
H0: IsEquiv w
C: Type
IsEquiv (fun (g : C -> A) (x : C) => w (g x))
    refine (isequiv_adjointify
              (fun (g:C->A) => w o g)
              (fun (g:C->B) => w^-1 o g)
              _
              _);
    intro;
    pose (Build_Equiv _ _ w _) as w';
    change H0 with (@equiv_isequiv _ _ w');
    change w with (@equiv_fun _ _ w');
    clearbody w'; clear H0 w;
    rewrite <- (@eisretr _ _ (@equiv_path A B) (ua A B) w');
    generalize ((@equiv_inv _ _ (equiv_path A B) (ua A B)) w');
    intro p;
    clear w';
    destruct p;
    reflexivity.
  Defined.

  (** We are ready to prove functional extensionality, starting with the naive non-dependent version. *)

  Local Instance isequiv_src_compose A B
  : @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
             (A -> B)
             (fun g => (fst o pr1) o g).
ua: Univalence_type
A, B: Type
IsEquiv (fun g : A -> {xy : B * B & fst xy = snd xy} => fst o pr1 o g)
  Proof.
ua: Univalence_type
A, B: Type
IsEquiv (fun g : A -> {xy : B * B & fst xy = snd xy} => fst o pr1 o g)
    rapply @univalence_isequiv_postcompose.
ua: Univalence_type
A, B: Type
IsEquiv (fun x : {xy : B * B & fst xy = snd xy} => fst x.1)
    refine (isequiv_adjointify
              (fst o pr1) (fun x => ((x, x); idpath))
              (fun _ => idpath)
              _);
      let p := fresh in
      intros [[? ?] p];
        simpl in p; destruct p;
        reflexivity.
  Defined.


  Local Instance isequiv_tgt_compose A B
  : @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
             (A -> B)
             (fun g => (snd o pr1) o g).
ua: Univalence_type
A, B: Type
IsEquiv (fun g : A -> {xy : B * B & fst xy = snd xy} => snd o pr1 o g)
  Proof.
ua: Univalence_type
A, B: Type
IsEquiv (fun g : A -> {xy : B * B & fst xy = snd xy} => snd o pr1 o g)
    rapply @univalence_isequiv_postcompose.
ua: Univalence_type
A, B: Type
IsEquiv (fun x : {xy : B * B & fst xy = snd xy} => snd x.1)
    refine (isequiv_adjointify
              (snd o pr1) (fun x => ((x, x); idpath))
              (fun _ => idpath)
              _);
      let p := fresh in
      intros [[? ?] p];
        simpl in p; destruct p;
        reflexivity.
  Defined.

  Theorem Univalence_implies_FunextNondep : NaiveNondepFunext.
ua: Univalence_type
NaiveNondepFunext
  Proof.
ua: Univalence_type
NaiveNondepFunext
    intros A B f g p.
ua: Univalence_type
A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
f = g
    (** Consider the following maps. *)
    pose (d := fun x : A => exist (fun xy => fst xy = snd xy) (f x, f x) (idpath (f x))).
ua: Univalence_type
A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
d:= fun x : A => ((f x, f x); 1): A -> {xy : B * B & fst xy = snd xy}
f = g
    pose (e := fun x : A => exist (fun xy => fst xy = snd xy) (f x, g x) (p x)).
ua: Univalence_type
A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
d:= fun x : A => ((f x, f x); 1): A -> {xy : B * B & fst xy = snd xy}
e:= fun x : A => ((f x, g x); p x): A -> {xy : B * B & fst xy = snd xy}
f = g
    (** If we compose [d] and [e] with [free_path_target], we get [f] and [g], respectively. So, if we had a path from [d] to [e], we would get one from [f] to [g]. *)
    change f with ((snd o pr1) o d).
ua: Univalence_type
A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
d:= fun x : A => ((f x, f x); 1): A -> {xy : B * B & fst xy = snd xy}
e:= fun x : A => ((f x, g x); p x): A -> {xy : B * B & fst xy = snd xy}
snd o pr1 o d = g
    change g with ((snd o pr1) o e).
ua: Univalence_type
A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
d:= fun x : A => ((f x, f x); 1): A -> {xy : B * B & fst xy = snd xy}
e:= fun x : A => ((f x, g x); p x): A -> {xy : B * B & fst xy = snd xy}
snd o pr1 o d = snd o pr1 o e
    rapply (ap (fun g => snd o pr1 o g)).
ua: Univalence_type
A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
d:= fun x : A => ((f x, f x); 1): A -> {xy : B * B & fst xy = snd xy}
e:= fun x : A => ((f x, g x); p x): A -> {xy : B * B & fst xy = snd xy}
d = e
    (** Since composition with [src] is an equivalence, we can freely compose with [src]. *)
    pose (fun A B x y=> @equiv_inv _ _ _ (@isequiv_ap _ _ _ (@isequiv_src_compose A B) x y)) as H'.
ua: Univalence_type
A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
d:= fun x : A => ((f x, f x); 1): A -> {xy : B * B & fst xy = snd xy}
e:= fun x : A => ((f x, g x); p x): A -> {xy : B * B & fst xy = snd xy}
H':= fun (A0 B0 : Type) (x y : A0 -> {xy : B0 * B0 & fst xy = snd xy}) =>
(ap (fun g0 : A0 -> {xy : B0 * B0 & fst xy = snd xy} => fst o pr1 o g0))^-1: forall (A0 B0 : Type) (x y : A0 -> {xy : B0 * B0 & fst xy = snd xy}),
(fun g0 : A0 -> {xy : B0 * B0 & fst xy = snd xy} => fst o pr1 o g0) x =
(fun g0 : A0 -> {xy : B0 * B0 & fst xy = snd xy} => fst o pr1 o g0) y ->
x = y
d = e
    apply H'.
ua: Univalence_type
A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
d:= fun x : A => ((f x, f x); 1): A -> {xy : B * B & fst xy = snd xy}
e:= fun x : A => ((f x, g x); p x): A -> {xy : B * B & fst xy = snd xy}
H':= fun (A0 B0 : Type) (x y : A0 -> {xy : B0 * B0 & fst xy = snd xy}) =>
(ap (fun g0 : A0 -> {xy : B0 * B0 & fst xy = snd xy} => fst o pr1 o g0))^-1: forall (A0 B0 : Type) (x y : A0 -> {xy : B0 * B0 & fst xy = snd xy}),
(fun g0 : A0 -> {xy : B0 * B0 & fst xy = snd xy} => fst o pr1 o g0) x =
(fun g0 : A0 -> {xy : B0 * B0 & fst xy = snd xy} => fst o pr1 o g0) y ->
x = y
(fun x : A => fst (d x).1) = (fun x : A => fst (e x).1)
    reflexivity.
  Defined.

End UnivalenceImpliesFunext.

(** Now we use this to prove strong dependent funext.  Again only the codomain universe must be univalent, but the domain universe must be no larger than it is.  Thus practically speaking this means that a univalent universe satisfies funext only for functions between two types in that same universe. *)

Definition Univalence_implies_WeakFunext : Univalence_type -> WeakFunext
  := NaiveNondepFunext_implies_WeakFunext o @Univalence_implies_FunextNondep.

Definition Univalence_type_implies_Funext_type
           `{ua : Univalence_type@{j jplusone} }
  : Funext_type@{i j j}
  := NaiveNondepFunext_implies_Funext
       (@Univalence_implies_FunextNondep ua).

(** The above proof justifies assuming [Univalence -> Funext], which we did axiomatically in [Types/Universe.v]. *)