Coq-HoTT icon indicating copy to clipboard operation
Coq-HoTT copied to clipboard

Including a simpler proof that NaiveFunext -> Funext?

Open JasonGross opened this issue 9 years ago • 10 comments

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 avatar May 13 '15 22:05 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.

JasonGross avatar May 13 '15 22:05 JasonGross

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.

mikeshulman avatar May 14 '15 06:05 mikeshulman

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 avatar May 14 '15 15:05 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?

JasonGross avatar May 14 '15 18:05 JasonGross

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 [email protected] 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 (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?

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

vladimirias avatar May 14 '15 19:05 vladimirias

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

mikeshulman avatar May 14 '15 19:05 mikeshulman

it was a comment by Martin Escardo.

On May 14, 2015, at 3:56 PM, Mike Shulman [email protected] 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.

awodey avatar May 14 '15 20:05 awodey

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.

mikeshulman avatar May 15 '15 04:05 mikeshulman

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

andrejbauer avatar May 15 '15 08:05 andrejbauer

@andrejbauer AFAIK both currently work.

Alizter avatar Nov 20 '19 12:11 Alizter