Isabelle-HoTT/spartan/theories, branch master trying to make Isabelle/HoTT work with Isabelle 2021-1 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:54+00:00 Josh Chen 2020-05-25T15:09:54+00:00 80edbd08e13200d2c080ac281d19948bbbcd92e0 






slightly nicer homotopy proofs with calculations
2020-05-25T14:27:37+00:00

Josh Chen

2020-05-25T14:27:37+00:00

2f63e165d696688f0fcc721289889a8baa00cc02












`refl` and `this` methods
2020-05-25T14:26:53+00:00

Josh Chen

2020-05-25T14:26:53+00:00

5e18f1964efca8e73c3bda1967803b6b85feb27c












use existing calculation infrastructure for sym and trans
2020-05-25T14:01:18+00:00

Josh Chen

2020-05-25T14:01:18+00:00

575e98cac4871f0fdeefa0f5ac75bbba8103e82e












1. equality method now uses general elimination tactic. 2. New constant `` refers to rhs of equalities.
2020-05-25T13:24:20+00:00

Josh Chen

2020-05-25T13:24:20+00:00

8f47d9f3ca38a3fc2c3c462d1157866081102ce1












new elimination tactic
2020-05-25T13:21:02+00:00

Josh Chen

2020-05-25T13:21:02+00:00

3de65af4b59e6d3cc8e74acecf704beccd54b774












new work on elimination tactic
2020-05-24T18:44:33+00:00

Josh Chen

2020-05-24T18:44:33+00:00

3ad2f03f7dbc922e2c711241146db091d193003d












some tweaks and comments, in preparation for general inductive type elimination
2020-05-22T13:43:14+00:00

Josh Chen

2020-05-22T13:43:14+00:00

720da0f918118388d114e09664b129d2b29be2b1












1. make id function an abbrev. 2. fix reduce method
2020-04-02T21:27:06+00:00

Josh Chen

2020-04-02T21:27:06+00:00

2781c68f0fdb435827097efc497c2172d6050e50












better lambda notation
2020-04-02T17:31:33+00:00

Josh Chen

2020-04-02T17:31:33+00:00

0ddab0fe11c33fc559fc8fb58528618efdbc93a4