First beta release

First beta release of the Isabelle HoTT object logic.
This release removes the "well-formedness" rules of the alpha release, provides new proof methods, and streamlines many proofs.

Important functionality that is still missing is the ability to concatenate paths in proofs; this is ongoing work.