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.

Initial release

Initial release of the Isabelle/HoTT object logic, coinciding with the submission of my MS thesis.
There is still lots of work to be done, and it is quite likely that future versions will not look very much like the current state.
In particular, polymorphism is a pain.
Also proof methods.