Formalize Lemma 3.8.5

contrib/HoTTBook.v

@@ -449,7 +449,62 @@ Definition Book_3_6_2 `{Funext} (A : Type) (B : A -> Type)
 (* ================================================== thm:no-higher-ac *)
 (** Lemma 3.8.5 *)
 
-
+Lemma Book_3_8_5 `{Univalence} : exists X (Y : X -> Type),
+    ~ forall X Y, (forall x : X, merely (Y x)) -> merely (forall x : X, Y x).
+Proof.
+  set (X := { A : Type0 & merely (Bool = A)}).
+  exists X.
+  set (x0 := (Bool; tr idpath) : X).
+  assert (Fact_equiv : forall (x y : X), x = y <~> (pr1 x <~> pr1 y)).
+  { intros [A p] [B q]. etransitivity.
+    1: apply equiv_inverse.
+    1: eapply equiv_path_sigma_hprop.
+    apply equiv_equiv_path.
+  }
+  pose (Fact := Fact_equiv x0 x0).
+  simpl in Fact.
+  assert (XnotSet: ~ IsHSet X).
+  {
+    intro setX. apply true_ne_false. set (Hprop_x0_eq_x0 := (hprop_allpath _ (@hset_path2 _ setX x0 x0))).
+    pose (bool_hprop := (@istrunc_equiv_istrunc _ _ Fact _ Hprop_x0_eq_x0)).
+    pose (r := @path_ishprop _ bool_hprop equiv_negb (equiv_idmap Bool)).
+    replace false with (1%equiv false) by reflexivity.
+    rewrite <- r. reflexivity.
+  }
+  assert (AisSet : forall x : X, IsHSet x.1).
+  {
+    intros [A p].
+    refine (Trunc_rec _ p).
+    intro I. rewrite <- I. typeclasses eauto.
+  }
+  assert (set_equiv_set : forall x y : X, IsHSet (x.1 <~> y.1)) by (intros; apply istrunc_equiv).
+  assert (x_eq_y_set : forall x y : X, IsHSet (x = y)).
+  {
+    intros x y. pose (e := Fact_equiv x y). apply equiv_inverse in e.
+    exact (istrunc_equiv_istrunc (x.1 <~> y.1) e).
+  }
+  set (Y := fun x => x0 = x).
+  exists Y.
+  assert (YisSet : forall x, IsHSet (Y x)) by (intro x; exact (x_eq_y_set x0 x)).
+  assert (premise : forall x, merely (Y x)).
+  {
+    intros [A p].
+    refine (Trunc_rec _ p).
+    intro boolA. unfold Y.
+    apply tr. refine (equiv_inverse (Fact_equiv x0 (A; p)) _).
+    simpl. exact (equiv_path _ _ boolA).
+  }
+  intro AC.
+  specialize (AC _ Y premise).
+  refine (Trunc_rec _ AC).
+  unfold Y.
+  intro proof_of_merely. apply XnotSet.
+  apply Book_3_3_4.
+  apply hprop_allpath.
+  intros x y.
+  rewrite <- (proof_of_merely x), <- (proof_of_merely y).
+  reflexivity.
+Qed.
 
 (* ================================================== thm:prop-equiv-trunc *)
 (** Lemma 3.9.1 *)