| e6b5a8f | Josh Chen | 26 May 2020, 14:38:33 UTC | add Maybe | 26 May 2020, 14:38:33 UTC |
| eee7d97 | Josh Chen | 25 May 2020, 17:37:57 UTC | more reorganizing | 25 May 2020, 17:37:57 UTC |
| c19533a | Josh Chen | 25 May 2020, 17:36:30 UTC | notation | 25 May 2020, 17:36:30 UTC |
| f97d715 | Josh Chen | 25 May 2020, 17:33:23 UTC | fix implicits table merge mistake | 25 May 2020, 17:33:49 UTC |
| 60f3240 | Josh Chen | 25 May 2020, 16:50:59 UTC | Lists + more reorganizing | 25 May 2020, 16:50:59 UTC |
| 80edbd0 | Josh Chen | 25 May 2020, 15:09:54 UTC | Reorganize theory structure. In particular, the identity type moves out from under Spartan to HoTT. Spartan now only has Pi and Sigma. | 25 May 2020, 15:09:54 UTC |
| 22c5b89 | Josh Chen | 25 May 2020, 14:27:53 UTC | minor | 25 May 2020, 14:27:53 UTC |
| 2f63e16 | Josh Chen | 25 May 2020, 14:27:37 UTC | slightly nicer homotopy proofs with calculations | 25 May 2020, 14:27:37 UTC |
| 5e18f19 | Josh Chen | 25 May 2020, 14:26:53 UTC | `refl` and `this` methods | 25 May 2020, 14:26:53 UTC |
| 0d80505 | Josh Chen | 25 May 2020, 14:01:38 UTC | some arithmetic | 25 May 2020, 14:01:38 UTC |
| 575e98c | Josh Chen | 25 May 2020, 14:01:18 UTC | use existing calculation infrastructure for sym and trans | 25 May 2020, 14:01:18 UTC |
| 8f47d9f | Josh Chen | 25 May 2020, 13:24:20 UTC | 1. equality method now uses general elimination tactic. 2. New constant `` refers to rhs of equalities. | 25 May 2020, 13:24:20 UTC |
| 3de65af | Josh Chen | 25 May 2020, 13:21:02 UTC | new elimination tactic | 25 May 2020, 13:21:02 UTC |
| 3ad2f03 | Josh Chen | 24 May 2020, 18:44:33 UTC | new work on elimination tactic | 24 May 2020, 18:44:33 UTC |
| 6f37e6b | Josh Chen | 24 May 2020, 18:44:12 UTC | small comment | 24 May 2020, 18:44:12 UTC |
| 720da0f | Josh Chen | 22 May 2020, 13:43:14 UTC | some tweaks and comments, in preparation for general inductive type elimination | 22 May 2020, 13:43:14 UTC |
| 1571e03 | Josh Chen | 16 April 2020, 13:41:53 UTC | Update README.md | 16 April 2020, 13:41:53 UTC |
| 0b52ba4 | Josh Chen | 16 April 2020, 13:39:41 UTC | Merge branch 'master' of https://github.com/jaycech3n/Isabelle-HoTT | 16 April 2020, 13:39:41 UTC |
| 1885667 | Josh Chen | 16 April 2020, 13:37:43 UTC | update for Isabelle2020 | 16 April 2020, 13:37:43 UTC |
| 88df851 | Josh Chen | 16 April 2020, 13:03:23 UTC | minor naming | 16 April 2020, 13:03:23 UTC |
| ad27e7a | Josh Chen | 06 April 2020, 11:40:42 UTC | Update README.md | 06 April 2020, 11:40:42 UTC |
| 01a4d1f | Josh Chen | 02 April 2020, 23:30:02 UTC | 1. change var names. 2. add and mul | 02 April 2020, 23:30:02 UTC |
| bc2bc24 | Josh Chen | 02 April 2020, 23:15:43 UTC | fix ROOT | 02 April 2020, 23:15:43 UTC |
| 97f3c05 | Josh Chen | 02 April 2020, 23:13:29 UTC | 1. Base theory. 2. Fix Nat axioms, addition. | 02 April 2020, 23:13:34 UTC |
| 2781c68 | Josh Chen | 02 April 2020, 21:27:06 UTC | 1. make id function an abbrev. 2. fix reduce method | 02 April 2020, 21:27:06 UTC |
| 0ddab0f | Josh Chen | 02 April 2020, 17:31:33 UTC | better lambda notation | 02 April 2020, 17:31:33 UTC |
| 6e88bda | Josh Chen | 02 April 2020, 16:02:49 UTC | Merge branch 'master' of https://github.com/jaycech3n/Isabelle-HoTT | 02 April 2020, 16:02:49 UTC |
| c2dffff | Josh Chen | 02 April 2020, 15:57:48 UTC | Brand-spanking new version using Spartan infrastructure | 02 April 2020, 15:57:48 UTC |
| 045fc39 | Josh Chen | 24 January 2020, 16:01:12 UTC | make development shift really obvious | 24 January 2020, 16:01:12 UTC |
| 438e210 | Josh Chen | 24 January 2020, 15:58:02 UTC | Update README.md | 24 January 2020, 15:58:02 UTC |
| fc2a739 | Josh Chen | 24 January 2020, 15:52:45 UTC | Update README.md | 24 January 2020, 15:52:45 UTC |
| 1d99fa1 | Josh Chen | 24 January 2020, 15:52:09 UTC | Update README.md | 24 January 2020, 15:52:09 UTC |
| b4faf76 | Josh Chen | 29 November 2019, 15:52:10 UTC | Change link | 29 November 2019, 15:52:10 UTC |
| 326475c | Josh Chen | 29 October 2019, 13:58:58 UTC | Update README.md | 29 October 2019, 13:58:58 UTC |
| d7ae804 | Josh Chen | 29 October 2019, 10:52:02 UTC | Update README.md | 29 October 2019, 10:52:02 UTC |
| 32dc5b9 | Josh Chen | 29 October 2019, 10:51:26 UTC | Update README.md | 29 October 2019, 10:51:26 UTC |
| b815a89 | Josh Chen | 15 October 2019, 21:13:00 UTC | Update README.md | 15 October 2019, 21:13:00 UTC |
| b01b8ee | Josh Chen | 27 March 2019, 13:41:16 UTC | More progress. I think we are reaching the limit of what can be conveniently proved with the current implementation. | 27 March 2019, 13:41:16 UTC |
| 45c3879 | Josh Chen | 26 March 2019, 16:04:01 UTC | working towards biinv_imp_qinv | 26 March 2019, 16:04:01 UTC |
| 6dd1b27 | Josh Chen | 08 March 2019, 18:33:24 UTC | prune import lists | 08 March 2019, 18:33:24 UTC |
| 22c4bbc | Josh Chen | 08 March 2019, 16:26:25 UTC | type lemmas for derived functions should type the functions themselves | 08 March 2019, 16:26:25 UTC |
| ad0c275 | Josh Chen | 08 March 2019, 16:24:57 UTC | some options, renaming | 08 March 2019, 16:24:57 UTC |
| 8f71649 | Josh Chen | 06 March 2019, 10:42:19 UTC | Make functions object-level | 06 March 2019, 10:42:19 UTC |
| fa4c19c | Josh Chen | 03 March 2019, 21:54:13 UTC | Removed transport section from Eq.thy | 03 March 2019, 21:54:13 UTC |
| 3f7a827 | Josh Chen | 03 March 2019, 21:53:45 UTC | Move definition of transport to Type_Families.thy, and change it to use meta-functions for type families again. This together with the previous commit simplifies the definitions and proofs for idtoeqv greatly. | 03 March 2019, 21:53:45 UTC |
| 38dd685 | Josh Chen | 03 March 2019, 21:47:03 UTC | Improve automated handling of universes. derive now can automatically handle more proofs requiring the use of "U i: U (Suc i)", and shouldn't loop as much. | 03 March 2019, 21:48:25 UTC |
| de6672d | Josh Chen | 03 March 2019, 11:38:54 UTC | Defined idtoeqv. Should next state univalence in terms of an explicit inverse equivalence. | 03 March 2019, 11:38:54 UTC |
| fa413a9 | Josh Chen | 01 March 2019, 19:44:02 UTC | finished proof of transport_biinv | 01 March 2019, 19:44:02 UTC |
| c33f290 | Josh Chen | 01 March 2019, 19:17:53 UTC | Proving transport is bi-invertible is harder than expected | 01 March 2019, 19:17:53 UTC |
| 9ba4720 | Josh Chen | 01 March 2019, 19:05:00 UTC | change id precedence | 01 March 2019, 19:05:00 UTC |
| 85fc133 | Josh Chen | 01 March 2019, 14:45:10 UTC | transport and homotopy | 01 March 2019, 14:45:10 UTC |
| 7a58970 | Josh Chen | 28 February 2019, 23:45:40 UTC | Working on univalence | 28 February 2019, 23:45:40 UTC |
| 39b22fe | Josh Chen | 28 February 2019, 23:44:58 UTC | Syntax changes. Transport inverse lemmas. | 28 February 2019, 23:44:58 UTC |
| 73e7023 | Josh Chen | 28 February 2019, 17:42:59 UTC | tweak mixfix priorities | 28 February 2019, 17:42:59 UTC |
| 2116cee | Josh Chen | 28 February 2019, 13:15:31 UTC | more convenient syntax | 28 February 2019, 13:15:31 UTC |
| 0d4faf2 | Josh Chen | 27 February 2019, 23:05:23 UTC | 1. Remove all type inference functionality (feature development moving to another branch). 2. Eq.thy complete. | 27 February 2019, 23:05:23 UTC |
| 76a0095 | Josh Chen | 23 February 2019, 17:58:20 UTC | touchups | 23 February 2019, 17:58:20 UTC |
| 232856f | Josh Chen | 23 February 2019, 17:57:15 UTC | compute method solves subgoals arising from subst | 23 February 2019, 17:57:15 UTC |
| 0c96ce5 | Josh Chen | 23 February 2019, 17:50:37 UTC | readme | 23 February 2019, 17:50:37 UTC |
| e9df793 | Josh Chen | 23 February 2019, 17:14:09 UTC | more proofs involving equality | 23 February 2019, 17:14:09 UTC |
| ad48f91 | Josh Chen | 23 February 2019, 00:42:34 UTC | change mixfix pretty-printing indentation | 23 February 2019, 00:42:59 UTC |
| ce2f78d | Josh Chen | 23 February 2019, 00:42:18 UTC | rewrite associativity proof | 23 February 2019, 00:42:18 UTC |
| 57d183c | Josh Chen | 22 February 2019, 22:45:50 UTC | Cleanups and reorganization | 22 February 2019, 22:45:50 UTC |
| 0036345 | Josh Chen | 22 February 2019, 18:43:53 UTC | Proof of pathcomp associativity done. Some comments | 22 February 2019, 18:43:53 UTC |
| f39f927 | Josh Chen | 18 February 2019, 10:38:59 UTC | Partway through associativity proof. Lots to work on to make this more usable. | 18 February 2019, 10:38:59 UTC |
| 7f93280 | Josh Chen | 17 February 2019, 22:15:02 UTC | Dependent elimator for Eq now has the correct form. Cleaned up theorems | 17 February 2019, 22:15:02 UTC |
| ff95b7b | Josh Chen | 17 February 2019, 22:13:57 UTC | finalize quantify methods | 17 February 2019, 22:13:57 UTC |
| 68aa069 | Josh Chen | 17 February 2019, 17:34:38 UTC | Method "quantify" converts product inhabitation into Pure universal statements. Also misc. cleanups. | 17 February 2019, 17:34:38 UTC |
| 76b5731 | Josh Chen | 11 February 2019, 21:44:21 UTC | Organize this commit as a backup of the work on type inference done so far; learnt that I probably need to take a different approach. In particular, should first make the constants completely monomorphic, and then work on full proper type inference, rather than the heuristic approach taken here. | 11 February 2019, 21:44:21 UTC |
| a5692e0 | Josh Chen | 11 February 2019, 14:37:18 UTC | Put typing functionality into a .thy and clean up antiquotations, which results in some reorganization of the theory import structure. | 11 February 2019, 14:37:18 UTC |
| da8edcc | Josh Chen | 11 February 2019, 09:46:16 UTC | get_this more robust. Functions to convert ML terms and types to strings. | 11 February 2019, 09:46:16 UTC |
| 91dc479 | Josh Chen | 10 February 2019, 09:55:37 UTC | restructure library | 10 February 2019, 09:55:37 UTC |
| 923cfee | Josh Chen | 10 February 2019, 02:17:12 UTC | Fix antiquotation situation | 10 February 2019, 02:17:12 UTC |
| 29068d3 | Josh Chen | 10 February 2019, 02:16:51 UTC | Explicit references in antiquotations in typing.ML. Move trace switch definition to HoTT_Base. | 10 February 2019, 02:16:51 UTC |
| afef9e6 | Josh Chen | 10 February 2019, 01:59:30 UTC | Type information storage functionality (assume_type, assume_types keywords) done! Inference and pretty-printing for function composition done. | 10 February 2019, 01:59:30 UTC |
| 964aa49 | Josh Chen | 05 February 2019, 17:34:48 UTC | Merge branch '2019': beginning type inference automation. | 05 February 2019, 17:34:48 UTC |
| 64d2a5c | Josh Chen | 05 February 2019, 17:32:43 UTC | Add cong named theorem for congruence rules | 05 February 2019, 17:32:43 UTC |
| 9d21e7e | Josh Chen | 05 February 2019, 17:29:37 UTC | Basic type inference for composed lambda terms! | 05 February 2019, 17:29:37 UTC |
| 8759a6f | Josh Chen | 05 February 2019, 17:29:10 UTC | Decided to keep terms eta-expanded | 05 February 2019, 17:29:10 UTC |
| d70da13 | Josh Chen | 05 February 2019, 17:15:58 UTC | Type inference setup begun - first use-case for function composition. | 05 February 2019, 17:15:58 UTC |
| 7a7e27f | Josh Chen | 04 February 2019, 10:53:47 UTC | 1. Change syntax to rely less on unicode/control symbols. 2. Begin work on object-level type inference and input syntax help. | 04 February 2019, 10:53:47 UTC |
| 07d312b | Josh Chen | 31 January 2019, 14:51:24 UTC | Text remarks | 31 January 2019, 14:51:24 UTC |
| def15c3 | Josh Chen | 30 January 2019, 15:38:38 UTC | Clean and comment methods file | 30 January 2019, 15:38:38 UTC |
| 843d53d | Josh Chen | 30 January 2019, 15:09:50 UTC | Remove "constrained" notation for type families. Clean and document. | 30 January 2019, 15:09:50 UTC |
| a245a3e | Josh Chen | 30 January 2019, 14:43:47 UTC | Begin refactor | 30 January 2019, 14:43:47 UTC |
| 36c7898 | Josh Chen | 20 September 2018, 19:38:14 UTC | Update README.md Remove DOI badge | 20 September 2018, 19:38:14 UTC |
| 55c1480 | Josh Chen | 20 September 2018, 19:35:51 UTC | Derive can prove pathcomp_comp. Fix typo. | 20 September 2018, 19:35:51 UTC |
| 0bceaa9 | Josh Chen | 20 September 2018, 12:14:17 UTC | Application should bind tighter than composition | 20 September 2018, 12:14:17 UTC |
| 19eb191 | Josh Chen | 20 September 2018, 12:03:33 UTC | Rename properties of equality + more properties. Output formatting for ` | 20 September 2018, 12:03:33 UTC |
| 24a0d9c | Josh Chen | 19 September 2018, 13:07:05 UTC | Renaming | 19 September 2018, 13:07:05 UTC |
| 150f7eb | Josh Chen | 19 September 2018, 13:06:44 UTC | Renaming | 19 September 2018, 13:06:44 UTC |
| 1305c6b | Josh Chen | 19 September 2018, 09:57:22 UTC | Not sure what advantage is provided by having eta-expanded forms in the rules. Removing for now. | 19 September 2018, 09:57:22 UTC |
| f602cb5 | Josh Chen | 19 September 2018, 09:55:45 UTC | proof of associativity of path composition | 19 September 2018, 09:55:45 UTC |
| 59a1409 | Josh Chen | 18 September 2018, 19:20:08 UTC | Merge branch 'larsrh-topic/root' | 18 September 2018, 19:20:08 UTC |
| f9bbcff | Josh Chen | 18 September 2018, 19:18:33 UTC | Add ROOT. No eta-contraction | 18 September 2018, 19:18:33 UTC |
| f07e0e2 | Lars Hupel | 18 September 2018, 14:52:08 UTC | add ROOT file | 18 September 2018, 14:52:08 UTC |
| c93932c | Josh Chen | 18 September 2018, 09:46:04 UTC | Load Univalence by default | 18 September 2018, 09:46:07 UTC |
| 78f5c8e | Josh Chen | 18 September 2018, 09:45:22 UTC | Update README.md | 18 September 2018, 09:45:22 UTC |
| 8295956 | Josh Chen | 18 September 2018, 09:41:39 UTC | Update README.md | 18 September 2018, 09:41:39 UTC |
| a9588df | Josh Chen | 18 September 2018, 09:39:40 UTC | Merge branch 'develop', ready for release 0.1.0 | 18 September 2018, 09:39:40 UTC |
