michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
7270 commits 3 branches 0 tags 28 MiB
Commit graph

319 commits

Author SHA1 Message Date
Floris van Doorn
115dedbd1c fix(hott): notation spacing and markdown files 2015-10-02 16:26:10 -07:00
Leonardo de Moura
ede23a3267 feat(hott,library): add additional spacing hints 2015-09-30 17:41:44 -07:00
Floris van Doorn
aac13a2ee7 fix(hott): minor changes to merge ulrik and my commits 2015-09-28 09:09:22 -07:00
Floris van Doorn
2264759060 feat(category): define colimits as dual of limits 2015-09-28 09:09:22 -07:00
Floris van Doorn
df73931a6d feat(category.opposite): prove that the opposite of a univalent category is univalent 2015-09-28 09:09:22 -07:00
Floris van Doorn
099bd95ebd feat(category.limits): prove that being complete is a mere proposition for categories 2015-09-28 09:09:22 -07:00
Floris van Doorn
51edd0ad1d feat(category.constructions.hset): prove that the category of sets is complete 2015-09-28 09:09:22 -07:00
Floris van Doorn
f82d1bd566 feat(category): add limits in a category 2015-09-28 09:09:22 -07:00
Floris van Doorn
6e23305c5d feat(category): define terminal, initial, indiscrete and sum category 2015-09-28 09:09:21 -07:00
Floris van Doorn
3c4c722afd feat(hott): port more from chapters 4 and 6 of the book 2015-09-28 09:09:21 -07:00
Ulrik Buchholtz
c6f3f6f3f4 feat(hott): prove HoTT book 7.5.4 and 7.5.5 2015-09-28 09:09:21 -07:00
Ulrik Buchholtz
25ed9d6e5a feat(hott): prove HoTT book Theorem 4.7.7 2015-09-28 09:09:21 -07:00
Ulrik Buchholtz
ed1029641a fix(hott/*): update book.md and clean up homotopy.connectedness 2015-09-28 09:09:21 -07:00
Ulrik Buchholtz
2c22501084 feat(hott): prove HoTT book Theorem 4.7.6 2015-09-28 09:09:21 -07:00
Leonardo de Moura
33f46fd137 feat(library/blast): parse blast tactic and invoke stub 2015-09-25 12:45:16 -07:00
Leonardo de Moura
4a6ff8058d fix(hott): import commands (some files have been moved to different directories) 2015-09-25 09:39:45 -07:00
Ulrik Buchholtz
384a366e0f refactor(hott): move homotopy hits to new homotopy folder 2015-09-24 22:52:33 -04:00
Floris van Doorn
732897340d fix(types): change some definitions to theorems 2015-09-11 23:35:21 -07:00
Floris van Doorn
fb364f8bc7 feat(types): add more equivalences between combinations of type constructors 2015-09-11 23:35:21 -07:00
Floris van Doorn
e84b22864f feat(hott): various changes in the HoTT library 2015-09-11 23:35:21 -07:00
Floris van Doorn
bd3aa9cf54 feat(category): prove Theorem 9.5.9 from the HoTT book 2015-09-11 23:35:21 -07:00
Floris van Doorn
1a3b363467 feat(category): prove that the yoneda embedding is an embedding 2015-09-11 23:35:21 -07:00
Floris van Doorn
fd89aa77a3 feat(hott): prove Yoneda lemma 2015-09-11 23:35:21 -07:00
Floris van Doorn
817d691237 fix(hott/init/nat): also define ℕ in the top-level in HoTT 2015-09-11 23:35:21 -07:00
Leonardo de Moura
cae2271818 refactor(hott/algebra/category/adjoint): rewrite expensive proof 
see #815
 2015-09-01 16:59:14 -07:00
Floris van Doorn
a8964adb9c fix(hott): make sure there are no sorry's visible 2015-09-01 15:17:46 -07:00
Floris van Doorn
7e52c49dce feat(hott): many changes is the HoTT library 
Prove that 'is_left_adjoint F' is a mere proposition, although this proof is commented out because it takes ~10 seconds
 2015-09-01 15:17:46 -07:00
Floris van Doorn
f555120428 feat(types/eq): add general encode-decode method 2015-09-01 15:17:46 -07:00
Floris van Doorn
f4892db432 feat(types.trunc): prove the principle of unique choice 2015-09-01 15:17:46 -07:00
Floris van Doorn
c24fd508b6 feat(hott/types): add more about pathovers in type constructors, prove that double negation elimination doesn't hold universally 2015-09-01 15:17:46 -07:00
Floris van Doorn
cfddfdfa84 feat(hott/types): add characterization of lift, prove that Type.{u} is not an hset 2015-09-01 15:17:46 -07:00
Leonardo de Moura
582dbecfd0 feat(library,hott): add notation T1 : T2 as syntax sugar for (focus (T1; all_goals T2)) 
closes #775
 2015-08-08 10:16:25 -07:00
Floris van Doorn
ad5cda48a8 refactor(hott): move cubical folder and files eq2, function and hprop_trunc from types/ to the root HoTT directory 2015-08-07 13:34:41 -07:00
Floris van Doorn
e51ba09a27 feat(hott): add types.sum, greatly expand types.prod, minor changes in types.sigma and types.pi 2015-08-07 13:34:41 -07:00
Floris van Doorn
3d2a6a08a4 feat(hott/nat): add characterization of equality in nat 2015-08-07 13:34:41 -07:00
Floris van Doorn
189293b5d4 fix(init.path): rename transport_compose to tr_compose 2015-08-07 13:34:41 -07:00
Floris van Doorn
d111607890 feat(hott): add file which maps sections of the HoTT book to the HoTT library 2015-08-07 13:34:41 -07:00
Floris van Doorn
f3ba81a19d fix(init.path): a couple of small simplifications 2015-08-07 13:34:40 -07:00
Floris van Doorn
0ec525a8ee feat(two_quotient): finish proof of elim_incl2 2015-08-07 13:34:40 -07:00
Floris van Doorn
11b1f416f6 feat(nat): add unfold attributes to add, mul, sub and of_num in namespace nat_esimp in both libraries 2015-08-04 13:23:20 +02:00
Floris van Doorn
747d12a385 feat(hott): prove characterization of a pathover in a pathover-type 2015-08-04 13:01:12 +02:00
Floris van Doorn
e198be318f feat(circle): show that x = x in the circle is always Z 2015-08-04 13:01:11 +02:00
Floris van Doorn
7a780b1b60 feat(hott): various minor changes in the HoTT library 2015-08-04 13:01:11 +02:00
Leonardo de Moura
b3cd3efbb4 refactor(hott): fix "sorry"s at int/basic.hlean, and comment the remaining "sorry"s 2015-07-27 08:34:11 -07:00
Leonardo de Moura
e969c7a8d6 refactor(library): remove 'simp' hack 2015-07-22 10:13:19 -07:00
Leonardo de Moura
267545ca0c feat(frontends/lean): parse 'with_options' tactical 
see issue #492
 2015-07-13 19:13:41 -04:00
Leonardo de Moura
6ab5cf214c feat(library,hott): add simp tactic reference 2015-07-13 18:01:40 -04:00
Leonardo de Moura
38d5c361df refactor(hott/types/trunc): remove unnecessary fold 
The new unfold tactic performs the fold automatically for us.

see issue #692
 2015-07-12 13:07:18 -04:00
Leonardo de Moura
584f9e3f49 fix(library/tactic/unfold_rec): support indexed families at unfold_rec 
This commit also removes many (now unnecessary) folds from the HoTT
library.

See issue #692

We still have to implement support for recursive definitions based on
brec_on that recurse over inductive families.
 2015-07-12 12:32:58 -04:00
Leonardo de Moura
a9515ac7a4 feat(library/tactic/rewrite_tactic): try to fold nested recursive applications after unfolding a recursive function 
See issue #692.
The implementation still has some rough spots.
It is not clear what the right semantic is.
Moreover, the folds in e_closure could not be eliminated automatically.
 2015-07-08 21:19:18 -04:00