Formalizations of 3.2.2 and 3.2.7

[ezyang]

In preparation of doing exercise 3.11, I did a direct transcription of theorem 3.2.2 and corollary 3.2.7 into Coq. However, I was not sure if this should just go in contrib/HoTTBook.v, or into the library proper.

Definition thm3_2_2_e : Bool <~> Bool.
  apply (equiv_adjointify negb negb); unfold Sect; destruct x; trivial.
Defined.

Theorem thm3_2_2 `{Univalence} `{Funext} : ~ (forall A, ~~A -> A).
  intro f.
  (* NB: happly is called apD10 *)
  (* to work around universe inconsistency, you cannot path_universe in a Definition *)
  pose proof (fun u => apD10 (apD f (path_universe thm3_2_2_e)) u) as h.
  (* NB: lemma 2.9.4 is transport_arrow *)
  pose proof (fun u => @transport_arrow _ (fun A => ~~A) (fun A => A) _ _ (path_universe thm3_2_2_e) (f Bool) u) as g.
  assert (forall (u v : ~~Bool), u = v) as eq.
    intros; apply path_forall; intro x; contradiction (u x).
  assert (forall (u : ~~Bool), transport (fun A => ~~A) (path_universe thm3_2_2_e)^ u = u) as i.
    intros; apply eq.
  pose proof (fun u => (h u)^ @ g u @ ap (fun z => transport idmap (path_universe thm3_2_2_e) (f Bool z)) (i u)) as j.
  (* NB: 2.10 discussion is transport_path_universe *)
  pose proof (fun u => j u @ transport_path_universe thm3_2_2_e (f Bool u)) as k.
  assert (forall x : Bool, ~(thm3_2_2_e x = x)) as X.
    destruct x; unfold thm3_2_2_e; simpl. apply false_ne_true. apply true_ne_false.
  apply (X (f Bool (fun k => k true)) (k (fun k => k true))^).
Qed.

Corollary thm3_2_7 `{Univalence} `{Funext} : ~ (forall A, A + ~A).
  intro g.
  refine (thm3_2_2 (fun A => _)).
  intro u.
  destruct (g A). trivial. contradiction (u n).
Qed.

[andrejbauer]

A smallish chunk of code can be stuck in contrib/HoTTBook.v initially (Bot of course you shouldn't be calling things thmX_Y_Z) and then someone will port them to the library. Or you could just try to guess where in the library this should go.

[JasonGross]

Note: your thm3_2_2_e is now HoTT.types.Bool.isequiv_negb.

[JasonGross]

I would suggest the following decomposition and locations: prove (maybe in types.Universe) that there is a path without a fixed point (Univalence -> { p : Bool = Bool & forall b, b <> transport idmap p b }), and then prove in HoTTBook (or make a Classical.v file or something) that (assuming Funext, double negation elimination implies that all paths @paths Type A A for non-empty A (i.e., given ~~A) have a fixed point (it's essentially the same as a chunk of the proof you gave). And then infer the contradiction as a separate lemma. If you can break down the "double-negation elimination implies all paths have a fixed point" even more, that'd be nice.

Also, you can do assert (forall (u v : ~~Bool), u = v) as eq by apply allpath_hprop. rather than the slightly longer proof you use.

Anyway, you should submit a pull request! (Sorry for the long delay in feedback.)