Formalize Lemma 3.8.5

[HyunggyuJang]

No description provided.

[jdchristensen]

The statement of this result has two mistakes. First, it does not state that each Y x is a set. Second, the first forall should not be there (and the X and Y in it shadow the X and Y earlier in the statement). I believe a correct statement is

Lemma Book_3_8_5 `{Univalence} : exists X (Y : X -> Type),
  (forall x : X, IsHSet (Y x)) * ~ ((forall x : X, merely (Y x)) -> merely (forall x : X, Y x)).

I think that it shouldn't be too hard to adapt the proof to this set-up.

[jdchristensen]

The X in this proof is called BAut Bool in the library, and is studied in Spaces/BAut/Bool.v. Some results there might simplify the proof. Also, Spaces/BAut.v contains trunc_baut which shows that BAut Bool is a 1-type, from which it follows that each Y x is a set. In fact, Coq can infer this using typeclasses:

Lemma Book_3_8_5 `{Univalence} : exists X (Y : X -> Type),
  (forall x : X, IsHSet (Y x)) * ~ ((forall x : X, merely (Y x)) -> merely (forall x : X, Y x)).
Proof.
  set (X := BAut Bool).
  exists X.
  set (x0 := point X).
  set (Y := fun x : X => x0 = x).
  exists Y.
  split.
  1: exact _.
  ...

[jdchristensen]

@HyunggyuJang Would you like to try updating this PR with the corrected statement of 3.8.5 and using some of the material already in the library? It would be nice to have this! Maybe it should go in Spaces/BAut/Bool.v or somewhere nearby?