Isabelle-HoTT/ex, branch master trying to make Isabelle/HoTT work with Isabelle 2021-1 Brand-spanking new version using Spartan infrastructure 2020-04-02T15:57:48+00:00 Josh Chen 2020-04-02T15:57:48+00:00 c2dfffffb7586662c67e44a2d255a1a97ab0398b 






add ROOT file
2018-09-18T14:52:08+00:00

Lars Hupel

2018-09-18T14:52:08+00:00

f07e0e2349a222130209ada9c029eea3d1fe8144












Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0!
2018-09-18T09:38:54+00:00

Josh Chen

2018-09-18T09:38:54+00:00

6857e783fa5cb91f058be322a18fb9ea583f2aad












Should write the correct rule for Ord_leq_min. Another exercise.
2018-08-29T22:51:48+00:00

Josh Chen

2018-08-29T22:51:48+00:00

2a2e8e46e0de6f99154a9421f75ae802557f22c7












Reorganize methods
2018-08-18T21:27:25+00:00

Josh Chen

2018-08-18T21:27:25+00:00

8833cdf99d3128466d85eb88aeb8e340e07e937c












Regrouping type rules
2018-08-18T19:28:21+00:00

Josh Chen

2018-08-18T19:28:21+00:00

e1be5f97bb2a42b3179bc24b118d69af137f8e5d












Misc formatting
2018-08-18T12:34:08+00:00

Josh Chen

2018-08-18T12:34:08+00:00

41f13f91d023e497d9b35e7a958a961aa0c7a5e5












Some comments and reorganization
2018-08-16T14:28:50+00:00

Josh Chen

2018-08-16T14:28:50+00:00

d8699451025a3bd5e8955e07fa879ed248418949












Prod.thy now has the correct definitional equality structure rule. Definition of function composition and properties.
2018-08-16T14:13:33+00:00

Josh Chen

2018-08-16T14:11:42+00:00

8ed9cf8682c07fc47b86c2d0aaeb8b4628aeaa31












Basic compute method
2018-08-15T10:42:52+00:00

Josh Chen

2018-08-15T10:42:52+00:00

257561ff4036d0eb5b51e649f2590b61e08d6fc5