trunc_iff_isequiv_truncation via modalities
comments about the reason for repleteness
identity modality

Conflicts:

	theories/Modality.v
	theories/ReflectiveSubuniverse.v
	theories/hit/Truncations.v
eliminate funext (mostly) in ReflectiveSubuniverse.v
eliminate funext (mostly) in Modality.v
update Truncations.v and PropositionalFracture.v for no funext
comments
add unicode notation for identity_modality
simpl rewrite
Use -2 and -1 rather than minus_two and minus_one
Merge pull request #511 from JasonGross/neg-trunc-notation

Use -2 and -1 rather than minus_two and minus_one
Merge pull request #507 from mikeshulman/rsu-without-funext

Merging as per @mikeshulman 's suggestion.

eliminate funext (mostly) from reflective subuniverses
Prove that O preserves products without funext
Delete minus1Trunc.v, close #434
Work around bug 3638

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3638, "Anomaly: Bad
recursive type. Please report." on [set]ting an evar involving
primitive projections
Remove dead code
Exercises 3.4 and 3.5
Better solution to Exc. 3.4
named pose in Exc. 3.4
make "happly" a parsing notation for "ap10"