Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | fix ROOT | Josh Chen | 2020-04-03 | 1 | -1/+1 | |
| | ||||||
* | 1. Base theory. 2. Fix Nat axioms, addition. | Josh Chen | 2020-04-03 | 2 | -11/+21 | |
| | ||||||
* | 1. make id function an abbrev. 2. fix reduce method | Josh Chen | 2020-04-02 | 2 | -8/+6 | |
| | ||||||
* | better lambda notation | Josh Chen | 2020-04-02 | 1 | -4/+7 | |
| | ||||||
* | Merge branch 'master' of https://github.com/jaycech3n/Isabelle-HoTT | Josh Chen | 2020-04-02 | 0 | -0/+0 | |
|\ | ||||||
| * | make development shift really obvious | Josh Chen | 2020-01-24 | 1 | -2/+2 | |
| | | ||||||
| * | Update README.md | Josh Chen | 2020-01-24 | 1 | -1/+1 | |
| | | ||||||
| * | Update README.md | Josh Chen | 2020-01-24 | 1 | -1/+1 | |
| | | ||||||
| * | Update README.md | Josh Chen | 2020-01-24 | 1 | -3/+3 | |
| | | ||||||
| * | Change link | Josh Chen | 2019-11-29 | 1 | -1/+1 | |
| | | ||||||
| * | Update README.md | Josh Chen | 2019-10-29 | 1 | -3/+3 | |
| | | ||||||
| * | Update README.md | Josh Chen | 2019-10-29 | 1 | -1/+2 | |
| | | ||||||
| * | Update README.md | Josh Chen | 2019-10-29 | 1 | -1/+5 | |
| | | ||||||
| * | Update README.md | Josh Chen | 2019-10-15 | 1 | -0/+1 | |
| | | ||||||
* | | Brand-spanking new version using Spartan infrastructure | Josh Chen | 2020-04-02 | 35 | -1829/+3291 | |
|/ | ||||||
* | More progress. I think we are reaching the limit of what can be conveniently ↵ | Josh Chen | 2019-03-27 | 2 | -24/+83 | |
| | | | | proved with the current implementation. | |||||
* | working towards biinv_imp_qinv | Josh Chen | 2019-03-26 | 4 | -5/+202 | |
| | ||||||
* | prune import lists | Josh Chen | 2019-03-08 | 3 | -153/+10 | |
| | ||||||
* | type lemmas for derived functions should type the functions themselves | Josh Chen | 2019-03-08 | 2 | -29/+102 | |
| | ||||||
* | some options, renaming | Josh Chen | 2019-03-08 | 3 | -2/+3 | |
| | ||||||
* | Make functions object-level | Josh Chen | 2019-03-06 | 4 | -146/+173 | |
| | ||||||
* | Removed transport section from Eq.thy | Josh Chen | 2019-03-03 | 1 | -99/+1 | |
| | ||||||
* | Move definition of transport to Type_Families.thy, and change it to use ↵ | Josh Chen | 2019-03-03 | 2 | -79/+147 | |
| | | | | meta-functions for type families again. This together with the previous commit simplifies the definitions and proofs for idtoeqv greatly. | |||||
* | Improve automated handling of universes. derive now can automatically handle ↵ | Josh Chen | 2019-03-03 | 2 | -2/+13 | |
| | | | | more proofs requiring the use of "U i: U (Suc i)", and shouldn't loop as much. | |||||
* | Defined idtoeqv. Should next state univalence in terms of an explicit ↵ | Josh Chen | 2019-03-03 | 1 | -13/+50 | |
| | | | | inverse equivalence. | |||||
* | finished proof of transport_biinv | Josh Chen | 2019-03-01 | 2 | -17/+21 | |
| | ||||||
* | Proving transport is bi-invertible is harder than expected | Josh Chen | 2019-03-01 | 1 | -83/+87 | |
| | ||||||
* | change id precedence | Josh Chen | 2019-03-01 | 2 | -14/+16 | |
| | ||||||
* | transport and homotopy | Josh Chen | 2019-03-01 | 2 | -22/+81 | |
| | ||||||
* | Working on univalence | Josh Chen | 2019-03-01 | 1 | -46/+115 | |
| | ||||||
* | Syntax changes. Transport inverse lemmas. | Josh Chen | 2019-03-01 | 1 | -18/+70 | |
| | ||||||
* | tweak mixfix priorities | Josh Chen | 2019-02-28 | 2 | -7/+16 | |
| | ||||||
* | more convenient syntax | Josh Chen | 2019-02-28 | 2 | -72/+100 | |
| | ||||||
* | 1. Remove all type inference functionality (feature development moving to ↵ | Josh Chen | 2019-02-28 | 6 | -577/+178 | |
| | | | | | | another branch). 2. Eq.thy complete. | |||||
* | touchups | Josh Chen | 2019-02-23 | 2 | -2/+2 | |
| | ||||||
* | compute method solves subgoals arising from subst | Josh Chen | 2019-02-23 | 1 | -6/+8 | |
| | ||||||
* | readme | Josh Chen | 2019-02-23 | 1 | -3/+12 | |
| | ||||||
* | more proofs involving equality | Josh Chen | 2019-02-23 | 1 | -44/+97 | |
| | ||||||
* | change mixfix pretty-printing indentation | Josh Chen | 2019-02-23 | 2 | -8/+8 | |
| | ||||||
* | rewrite associativity proof | Josh Chen | 2019-02-23 | 1 | -17/+16 | |
| | ||||||
* | Cleanups and reorganization | Josh Chen | 2019-02-22 | 10 | -397/+153 | |
| | ||||||
* | Proof of pathcomp associativity done. Some comments | Josh Chen | 2019-02-22 | 3 | -23/+249 | |
| | ||||||
* | Partway through associativity proof. Lots to work on to make this more usable. | Josh Chen | 2019-02-18 | 1 | -28/+58 | |
| | ||||||
* | Dependent elimator for Eq now has the correct form. Cleaned up theorems | Josh Chen | 2019-02-17 | 1 | -20/+104 | |
| | ||||||
* | finalize quantify methods | Josh Chen | 2019-02-17 | 1 | -3/+2 | |
| | ||||||
* | Method "quantify" converts product inhabitation into Pure universal ↵ | Josh Chen | 2019-02-17 | 6 | -41/+132 | |
| | | | | statements. Also misc. cleanups. | |||||
* | Organize this commit as a backup of the work on type inference done so far; ↵ | Josh Chen | 2019-02-11 | 3 | -61/+60 | |
| | | | | 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. | |||||
* | Put typing functionality into a .thy and clean up antiquotations, which ↵ | Josh Chen | 2019-02-11 | 4 | -109/+125 | |
| | | | | results in some reorganization of the theory import structure. | |||||
* | get_this more robust. Functions to convert ML terms and types to strings. | Josh Chen | 2019-02-11 | 1 | -3/+23 | |
| | ||||||
* | restructure library | Josh Chen | 2019-02-10 | 4 | -104/+108 | |
| |