some of the changes are backported from the hott3 library
pi_pathover and pi_pathover' are interchanged (same for variants and for sigma)
various definitions received explicit arguments: pinverse and eq_equiv_homotopy and ***.sigma_char
eq_of_fn_eq_fn is renamed to inj
in definitions about higher loop spaces and homotopy groups, the natural number arguments are now consistently before the type arguments
All HITs which automatically have a point are pointed without a 'p' in front. HITs which do not automatically have a point do still have a p (e.g. pushout/ppushout).
There were a lot of annoyances with spheres being indexed by N_{-1} with almost no extra generality. We now index the spheres by nat, making sphere 0 = pbool.
This commit adds truncated 2-quotients, groupoid quotients, Eilenberg MacLane spaces, chain complexes, the long exact sequence of homotopy groups, the Freudenthal Suspension Theorem, Whitehead's principle, and the computation of homotopy groups of almost all spheres which are known in HoTT.
Add more theorems about mapping cylinders, fibers, truncated 2-quotient, truncated univalence, pre/postcomposition with an iso in a precategory.
renamings: equiv.refl -> equiv.rfl and equiv_eq <-> equiv_eq'
other changes:
- move result about connectedness of susp to homotopy.susp
- improved definition of circle multiplication
- improved the interface to join
Most notably:
Give le.refl the attribute [refl]. This simplifies tactic proofs in various places.
Redefine the order of trunc_index, and instantiate it as weak order.
Add more about pointed equivalences.
quasireducible are also known as lazyreducible.
There is a lot of work to be done.
We still need to revise blast, and add a normalizer for type class
instances. This commit worksaround that by eagerly unfolding
quasireducible.
