{"action":"created","issue":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/757","labels_url":"https://api.github.com/repos/HoTT/HoTT/issues/757/labels{/name}","comments_url":"https://api.github.com/repos/HoTT/HoTT/issues/757/comments","events_url":"https://api.github.com/repos/HoTT/HoTT/issues/757/events","html_url":"https://github.com/HoTT/HoTT/issues/757","id":76140493,"number":757,"title":"Including a simpler proof that NaiveFunext -> Funext?","user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-05-13T22:11:10Z","updated_at":"2015-05-13T22:25:49Z","closed_at":null,"body":"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:\r\n```coq\r\ndec_to_UIP : forall {A} {x : A},\r\n  (forall y, (x = y) + (x <> y)) -> (forall y (p q : x = y), p = q)\r\n\r\nUIP_bump : forall {A} {x : A},\r\n  (forall y, x = y) -> (forall y (p q : x = y), p = q)\r\n```\r\nThis 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\".\r\n\r\nWhen 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`:\r\n\r\n```coq\r\nDefinition NaiveFunext_implies_Funext : NaiveFunext -> Funext_type.\r\nProof.\r\n  intros path_forall A P f g; hnf in path_forall.\r\n  refine (isequiv_adjointify _ _ _ _).\r\n  { exact (fun H => (path_forall _ _ f f (fun _ => idpath))^ @ path_forall _ _ f g H). }\r\n  { intro H.\r\n    set (H' := fun x => (g x; H x)).\r\n    change H with (fun x => (H' x).2).\r\n    change g with (fun x => (H' x).1).\r\n    clearbody H'; clear H g.\r\n    assert (H'' : forall x, (f x; 1) = H' x).\r\n    { intro x.\r\n      change (H' x) with ((H' x).1; (H' x).2).\r\n      destruct (H' x).2; reflexivity. }\r\n    apply path_forall in H''.\r\n    destruct H''; simpl.\r\n    rewrite concat_Vp; reflexivity. }\r\n  { intro H.\r\n    destruct H.\r\n    unfold apD10; simpl.\r\n    rewrite concat_Vp.\r\n    reflexivity. }\r\nDefined.\r\n```\r\n\r\nThe 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:\r\n\r\n```coq\r\nLemma forall_path_induction\r\n      (path_forall : NaiveFunext)\r\n      {A B} (f : forall a : A, B a)\r\n      (P : { g : _ & (forall a, f a = g a) } -> Type)\r\n      (k : P (f; (fun a => idpath)))\r\n      g\r\n: P g.\r\nProof.\r\n  set (g' := fun x => (g.1 x; g.2 x)).\r\n  change g with (existT (fun g => forall a, f a = g a) (fun x => (g' x).1) (fun x => (g' x).2)).\r\n  clearbody g'; clear g.\r\n  cut (forall x, (f x; 1) = g' x).\r\n  { intro H'.\r\n    apply path_forall in H'.\r\n    destruct H'.\r\n    exact k. }\r\n  { intro x.\r\n    change (g' x) with ((g' x).1; (g' x).2).\r\n    destruct (g' x).2.\r\n    reflexivity. }\r\nDefined.\r\n```\r\nwhere 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).\r\n\r\nIs this worth including in the library, somewhere?  Has anyone made this decomposition before?  Is it a helpful decomposition to make?"},"comment":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/comments/101837327","html_url":"https://github.com/HoTT/HoTT/issues/757#issuecomment-101837327","issue_url":"https://api.github.com/repos/HoTT/HoTT/issues/757","id":101837327,"user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"created_at":"2015-05-13T22:25:49Z","updated_at":"2015-05-13T22:25:49Z","body":"Here's another proof, using a generalization of the trick that I mentioned above:\r\n\r\n```coq\r\nSection gen.\r\n  Context {A : Type} (x : A) (code : A -> Type)\r\n          (encode : forall y, x = y -> code y)\r\n          (encode_contr : forall yH, (x; encode x 1) = yH)\r\n          (decode' : forall y, code y -> x = y).\r\n\r\n  Definition decode y (H : code y) : x = y\r\n    := (decode' x (encode x 1))^ @ (decode' y H).\r\n\r\n  Definition deencode y (H : x = y) : decode y (encode y H) = H.\r\n  Proof.\r\n    destruct H.\r\n    unfold decode.\r\n    edestruct decode'.\r\n    reflexivity.\r\n  Defined.\r\n\r\n  Lemma isequiv_encode y : IsEquiv (encode y).\r\n  Proof.\r\n    refine (isequiv_adjointify _ _ _ _).\r\n    { exact (@decode y). }\r\n    { intro H.\r\n      unfold decode.\r\n      set (yH := (y; H)).\r\n      change H with yH.2.\r\n      change y with yH.1.\r\n      clearbody yH; clear y H.\r\n      destruct (encode_contr yH); simpl.\r\n      abstract (rewrite concat_Vp; reflexivity). }\r\n    { intro p.\r\n      apply deencode. }\r\n  Defined.\r\nEnd gen.\r\n\r\nDefinition NaiveFunext_implies_Funext' : NaiveFunext -> Funext_type.\r\nProof.\r\n  intros path_forall A P f.\r\n  refine (isequiv_encode _ _ _ _ (path_forall A P f)).\r\n  pose (@contr_basedhtpy (NaiveFunext_implies_WeakFunext path_forall) A P f) as C.\r\n  exact (@contr _ C).\r\nDefined.\r\n```"}}