Including a simpler proof that NaiveFunext -> Funext?

[JasonGross]

I'm designing a week-long class on homotopy type theory for Mathcamp, and in trying to simplify the material, noticed that the essential insight to the proofs of the following two types is exactly the same:

dec_to_UIP : forall {A} {x : A},
  (forall y, (x = y) + (x <> y)) -> (forall y (p q : x = y), p = q)

UIP_bump : forall {A} {x : A},
  (forall y, x = y) -> (forall y (p q : x = y), p = q)

This is, in some sense, because the proof that IsTrunc n A -> IsTrunc n.+1 A (which is another way of phrasing UIP_bump, I believe) is proved by instantiating an equality decider with the function that always returns "yes, they're equal".

When looking through the HoTT book for exercises, I noticed 2.16, that NaiveFunext -> Funext. And the adjustment to the function given by NaiveFunext is exactly analogous to the adjustment in the proofs of the above two theorems (I guessed that this might be the case, and checked by reducing the term given by NaiveFunext_implies_Funext). Inspired by this, I wrote a relatively short, fairly direct proof that NaiveFunext -> Funext:

Definition NaiveFunext_implies_Funext : NaiveFunext -> Funext_type.
Proof.
  intros path_forall A P f g; hnf in path_forall.
  refine (isequiv_adjointify _ _ _ _).
  { exact (fun H => (path_forall _ _ f f (fun _ => idpath))^ @ path_forall _ _ f g H). }
  { intro H.
    set (H' := fun x => (g x; H x)).
    change H with (fun x => (H' x).2).
    change g with (fun x => (H' x).1).
    clearbody H'; clear H g.
    assert (H'' : forall x, (f x; 1) = H' x).
    { intro x.
      change (H' x) with ((H' x).1; (H' x).2).
      destruct (H' x).2; reflexivity. }
    apply path_forall in H''.
    destruct H''; simpl.
    rewrite concat_Vp; reflexivity. }
  { intro H.
    destruct H.
    unfold apD10; simpl.
    rewrite concat_Vp.
    reflexivity. }
Defined.

The only other key insight in this proof (which I gleaned after staring at FunextVarieties for long enough) is that the key to "destructing" a "path" of type forall x, f x = g x is to go via based path induction (which seems obvious in hindsight, because all path induction is fundamentally about { x : A & x = y } (or { x : A & y = x }), and not about individual paths). This insight can be extracted into its own theorem:

Lemma forall_path_induction
      (path_forall : NaiveFunext)
      {A B} (f : forall a : A, B a)
      (P : { g : _ & (forall a, f a = g a) } -> Type)
      (k : P (f; (fun a => idpath)))
      g
: P g.
Proof.
  set (g' := fun x => (g.1 x; g.2 x)).
  change g with (existT (fun g => forall a, f a = g a) (fun x => (g' x).1) (fun x => (g' x).2)).
  clearbody g'; clear g.
  cut (forall x, (f x; 1) = g' x).
  { intro H'.
    apply path_forall in H'.
    destruct H'.
    exact k. }
  { intro x.
    change (g' x) with ((g' x).1; (g' x).2).
    destruct (g' x).2.
    reflexivity. }
Defined.

where the only two non-obvious lines are the insight that you want to be talking about forall a : A, { ga : B a & f a = ga } rather than the type { g : forall a : A, B a & forall a : A, f a = g a } (this is the set line at the beginning of the proof), and the fact that naive functional extensionality is enough to turn induction on each { ga : B a & f a = ga } into induction on the entire function (this is the cut line).

Is this worth including in the library, somewhere? Has anyone made this decomposition before? Is it a helpful decomposition to make?

[JasonGross]

Here's another proof, using a generalization of the trick that I mentioned above:

Section gen.
  Context {A : Type} (x : A) (code : A -> Type)
          (encode : forall y, x = y -> code y)
          (encode_contr : forall yH, (x; encode x 1) = yH)
          (decode' : forall y, code y -> x = y).

  Definition decode y (H : code y) : x = y
    := (decode' x (encode x 1))^ @ (decode' y H).

  Definition deencode y (H : x = y) : decode y (encode y H) = H.
  Proof.
    destruct H.
    unfold decode.
    edestruct decode'.
    reflexivity.
  Defined.

  Lemma isequiv_encode y : IsEquiv (encode y).
  Proof.
    refine (isequiv_adjointify _ _ _ _).
    { exact (@decode y). }
    { intro H.
      unfold decode.
      set (yH := (y; H)).
      change H with yH.2.
      change y with yH.1.
      clearbody yH; clear y H.
      destruct (encode_contr yH); simpl.
      abstract (rewrite concat_Vp; reflexivity). }
    { intro p.
      apply deencode. }
  Defined.
End gen.

Definition NaiveFunext_implies_Funext' : NaiveFunext -> Funext_type.
Proof.
  intros path_forall A P f.
  refine (isequiv_encode _ _ _ _ (path_forall A P f)).
  pose (@contr_basedhtpy (NaiveFunext_implies_WeakFunext path_forall) A P f) as C.
  exact (@contr _ C).
Defined.

[mikeshulman]

This is cute; I can't quite remember seeing the proof beta-reduced like that before, but maybe someone else has? @peterlefanulumsdaine, maybe? It would probably be worth including somewhere.

Your forall_path_induction looks about the same as htpy_ind in FunextVarieties, only with the type family uncurried.

[JasonGross]

For reference, because I spent the time coding them up, here's the way to use isequiv_code to prove dec_to_UIP and UIP_bump. (It can probably be stripped of all the stuff it draws from Basics.Trunc and Types.Sigma, but I didn't get a chance to do that.)

Require Import HoTT.Basics.Trunc.
Require Import HoTT.Types.Sigma.

Section dec_to_UIP.
  Context {A : Type} (x : A) (dec : forall y, (x = y) + (x <> y)).

  Let code (y : A) := if dec y then Unit else Empty.
  Let encode {y} (H : x = y) : code y
    := match dec y as dy return if dy then Unit else Empty with
         | inl _ => tt
         | inr n => n H
       end.
  Let decode' {y} : code y -> x = y
    := match dec y as dy return (if dy then Unit else Empty) -> x = y with
         | inl pf => fun _ => pf
         | inr _ => fun e => match e with end
       end.

  Local Instance code_hprop y : IsHProp (code y).
  Proof.
    unfold code; destruct (dec y); exact _.
  Qed.

  Let encode_contr yH : (x; encode idpath) = yH.
  Proof.
    destruct yH as [y H].
    unfold code in *.
    apply path_sigma_hprop; simpl.
    destruct (dec y), H; assumption.
  Qed.

  Local Instance isequiv_encode' y : IsEquiv (@encode y)
    := @isequiv_encode A x code (@encode) encode_contr (@decode') y.

  Lemma dec_to_UIP y (p q : x = y) : p = q.
  Proof.
    apply (ap (@encode y))^-1.
    apply path_ishprop.
  Qed.
End dec_to_UIP.

Definition UIP_bump {A} {x : A} (allpaths : forall y, x = y) {y : A} (p q : x = y)
: p = q
  := @dec_to_UIP A x (fun y => inl (allpaths y)) y p q.

[JasonGross]

Note that this can be pushed a bit further, to show that the following axiom is enough to prove univalence:

Axiom weak_univalence : forall A (p q : { B : Type | A <~> B }), p = q.

(or, equivalently,

Axiom weak_univalence' : forall A B (e : A <~> B), { p : A = B | p # equiv_idmap = e }.

)

Here is the proof:

Section gen.
  Context {A : Type} (x : A) (code : A -> Type)
          (encode : forall y, x = y -> code y)
          (code_hprop : forall x y : { a : A | code a }, x = y).

  Definition decode' y (p : code y) : x = y
    := ap pr1 (code_hprop (x; encode x 1) (y; p)).

  Definition decode y (H : code y) : x = y
    := (decode' x (encode x 1))^ @ (decode' y H).

  Definition deencode y (H : x = y) : decode y (encode y H) = H.
  Proof.
    destruct H.
    unfold decode.
    edestruct decode'.
    reflexivity.
  Defined.

  Lemma isequiv_encode y : IsEquiv (encode y).
  Proof.
    refine (isequiv_adjointify _ _ _ _).
    { exact (@decode y). }
    { intro H.
      unfold decode.
      set (yH := (y; H)).
      change H with yH.2.
      change y with yH.1.
      clearbody yH; clear y H.
      destruct (code_hprop (x; encode x 1) yH); simpl.
      abstract (rewrite concat_Vp; reflexivity). }
    { intro p.
      apply deencode. }
  Defined.
End gen.

Axiom weak_univalence : forall A (p q : { B : Type | Equiv A B }), p = q.

Require Import HoTT.Types.Universe.

Lemma isequiv_equiv_path : forall (A B : Type), IsEquiv (equiv_path A B).
Proof.
  intro A.
  apply isequiv_encode.
  apply weak_univalence.
Qed.

Print Assumptions isequiv_equiv_path.

Was this formulation of univalence previously known?

[vladimirias]

This is not very surprising. In general, given P: A -> A -> Type such that forall a : A , iscontr ( { a’ : A | P a a’ } ) you can show that forall a a’ , isweq ( P a a’ ) ( paths a a’ ).

Here you apply it to A = Type and P X Y = X <~> Y . Then you assert forall X ( isaprop { Y | X <~>Y } ) but since { Y | X <~> Y } is inhabited by X <~> X this is equivalent to asserting iscontr ( { Y | X <~> Y} ).

Vladimir.

On May 14, 2015, at 8:28 PM, Jason Gross notifications@github.com wrote:

Note that this can be pushed a bit further, to show that the following axiom is enough to prove univalence:

Axiom weak_univalence : forall A (p q : { B : Type | A <~> B }), p = q. (or, equivalently,

Axiom weak_univalence' : forall A B (e : A <~> B), { p : A = B | p # equiv_idmap = e }. )

Here is the proof:

Section gen. Context {A : Type} (x : A) (code : A -> Type) (encode : forall y, x = y -> code y) (code_hprop : forall x y : { a : A | code a }, x = y).

Definition decode' y (p : code y) : x = y := ap pr1 (code_hprop (x; encode x 1) (y; p)).

Definition decode y (H : code y) : x = y := (decode' x (encode x 1))^ @ (decode' y H).

Definition deencode y (H : x = y) : decode y (encode y H) = H. Proof. destruct H. unfold decode. edestruct decode'. reflexivity. Defined.

Lemma isequiv_encode y : IsEquiv (encode y). Proof. refine (isequivadjointify _). { exact (@decode y). } { intro H. unfold decode. set (yH := (y; H)). change H with yH.2. change y with yH.1. clearbody yH; clear y H. destruct (code_hprop (x; encode x 1) yH); simpl. abstract (rewrite concat_Vp; reflexivity). } { intro p. apply deencode. } Defined. End gen.

Axiom weak_univalence : forall A (p q : { B : Type | Equiv A B }), p = q.

Require Import HoTT.Types.Universe.

Lemma isequiv_equiv_path : forall (A B : Type), IsEquiv (equiv_path A B). Proof. intro A. apply isequiv_encode. apply weak_univalence. Qed.

Print Assumptions isequiv_equiv_path. Was this formulation of univalence previously known?

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/757#issuecomment-102128029.

[mikeshulman]

I think we noticed this on the list a while ago, but I don't have time to track down the reference right now.

[awodey]

it was a comment by Martin Escardo.

On May 14, 2015, at 3:56 PM, Mike Shulman notifications@github.com wrote:

I think we noticed this on the list a while ago, but I don't have time to track down the reference right now.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/757#issuecomment-102150317.

[mikeshulman]

The thread I was thinking of was this one, where I said, as part of a proof that large elims imply univalence:

Thus, Equiv(A,B) is a retract of Id_U(A,B). But then Sum(B:U) Equiv(A,B) is also a retract of Sum(B:U) Id_U(A,B), and the latter is contractible, hence so is the former; so by Martin's observation last week, U is univalent.

Roughly the same thing was discussed here, here, and here.

[andrejbauer]

Did we change notation in the HoTT library, or should those { ... | ... } be { ... & ... }?

[Alizter]

@andrejbauer AFAIK both currently work.