Isabelle-HoTT/spartan/theories, branch master trying to make Isabelle/HoTT work with Isabelle 2021-1 https://stuebinm.eu/git/Isabelle-HoTT/atom/spartan/theories?h=master 2020-05-25T15:09:54Z Reorganize theory structure. In particular, the identity type moves out from under Spartan to HoTT. Spartan now only has Pi and Sigma. 2020-05-25T15:09:54Z Josh Chen 2020-05-25T15:09:54Z urn:sha1:80edbd08e13200d2c080ac281d19948bbbcd92e0 slightly nicer homotopy proofs with calculations 2020-05-25T14:27:37Z Josh Chen 2020-05-25T14:27:37Z urn:sha1:2f63e165d696688f0fcc721289889a8baa00cc02 `refl` and `this` methods 2020-05-25T14:26:53Z Josh Chen 2020-05-25T14:26:53Z urn:sha1:5e18f1964efca8e73c3bda1967803b6b85feb27c use existing calculation infrastructure for sym and trans 2020-05-25T14:01:18Z Josh Chen 2020-05-25T14:01:18Z urn:sha1:575e98cac4871f0fdeefa0f5ac75bbba8103e82e 1. equality method now uses general elimination tactic. 2. New constant `` refers to rhs of equalities. 2020-05-25T13:24:20Z Josh Chen 2020-05-25T13:24:20Z urn:sha1:8f47d9f3ca38a3fc2c3c462d1157866081102ce1 new elimination tactic 2020-05-25T13:21:02Z Josh Chen 2020-05-25T13:21:02Z urn:sha1:3de65af4b59e6d3cc8e74acecf704beccd54b774 new work on elimination tactic 2020-05-24T18:44:33Z Josh Chen 2020-05-24T18:44:33Z urn:sha1:3ad2f03f7dbc922e2c711241146db091d193003d some tweaks and comments, in preparation for general inductive type elimination 2020-05-22T13:43:14Z Josh Chen 2020-05-22T13:43:14Z urn:sha1:720da0f918118388d114e09664b129d2b29be2b1 1. make id function an abbrev. 2. fix reduce method 2020-04-02T21:27:06Z Josh Chen 2020-04-02T21:27:06Z urn:sha1:2781c68f0fdb435827097efc497c2172d6050e50 better lambda notation 2020-04-02T17:31:33Z Josh Chen 2020-04-02T17:31:33Z urn:sha1:0ddab0fe11c33fc559fc8fb58528618efdbc93a4