Library HoTT.Metatheory.UnivalenceImpliesFunext

Require Import HoTT.Basics.
Require Import Types.Universe Types.Paths Types.Unit.
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.


  Theorem univalence_isequiv_postcompose `{H0 : IsEquiv A B w} C : IsEquiv (fun (g:CA) ⇒ w o g).
  Proof.
    unfold Univalence_type in ×.
    refine (isequiv_adjointify
              (fun (g:CA) ⇒ w o g)
              (fun (g:CB) ⇒ 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).
  Proof.
    rapply @univalence_isequiv_postcompose.
    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).
  Proof.
    rapply @univalence_isequiv_postcompose.
    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.
  Proof.
    intros A B f g p.
Consider the following maps.
    pose (d := fun x : AexistT (fun xyfst xy = snd xy) (f x, f x) (idpath (f x))).
    pose (e := fun x : AexistT (fun xyfst xy = snd xy) (f x, g x) (p x)).
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).
    change g with ((snd o pr1) o e).
    rapply (ap (fun gsnd o pr1 o g)).
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'.
    apply H'.
    reflexivity.
  Defined.

End UnivalenceImpliesFunext.

Note that only the codomain universe of NaiveNondepFunext is required to be univalent.
Check @Univalence_implies_FunextNondep@{j jplusone i max j max}
  : Univalence_type@{j jplusone} NaiveNondepFunext@{i j max}.

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.
The above proof justifies assuming Univalence Funext, which we did axiomatically in Types/Universe.v.