Leonardo de Moura
74b28f6ad9
feat(library,hott): new notation for typeof
2015-03-24 18:35:21 -07:00
Leonardo de Moura
c0b4a47f63
refactor(hott/algebra/precategory/functor): remove unnecessary annotation
2015-03-24 12:06:16 -07:00
Leonardo de Moura
4817f2a18b
refactor(hott/algebra/precategory/basic): improve basic.hlean compilation time
2015-03-24 12:06:16 -07:00
Leonardo de Moura
30e3049c56
feat(hott/algebra/precategory/nat_trans): reduce compilation time using rewrite tactic
2015-03-23 19:55:01 -07:00
Leonardo de Moura
5bf46d1226
fix(library/tactic/inversion_tactic): improve 'cases' tactic for HoTT mode
...
closes #481
2015-03-23 18:06:11 -07:00
Leonardo de Moura
227de07758
fix(hott/algebra/category/constructions): avoid type class resolution loop
2015-03-23 11:32:20 -07:00
Jakob von Raumer
024ce8012f
fix(hott/algebra) make previously added lemma more applicable to groupoids
2015-03-23 11:17:57 -07:00
Jakob von Raumer
97a1cc8edb
feat(hott/algebra) show that functors preserve inverses and isos
2015-03-23 11:17:56 -07:00
Jakob von Raumer
74824078a8
fix(hott/algebra) fix previous commit by importing 'arity'
2015-03-23 11:17:56 -07:00
Jakob von Raumer
36a102bad2
feat(hott/algebra) add another equality lemma for precategories
2015-03-23 11:17:56 -07:00
Jakob von Raumer
4e790057b3
feat(hott/algebra) add structure for strict precategories
2015-03-23 11:17:56 -07:00
Jakob von Raumer
10c0b3a3ca
feat(hott/algebra) add characterization of paths between precategories
2015-03-23 11:17:56 -07:00
Jakob von Raumer
f480d67881
chore(hott/algebra) make carrier hset witness an instance
2015-03-23 11:17:56 -07:00
Floris van Doorn
8948926a07
style(hott/algebra/precategory): some cleanup
2015-03-16 17:15:51 -07:00
Floris van Doorn
57514244b1
feat(hott/algebra/precategory): add todo-file for adjoint functors, equivalences and isomorphisms
2015-03-16 17:15:51 -07:00
Floris van Doorn
c914b79341
feat(hott/algebra/category): show that functor category is univalent if codomain is
2015-03-16 17:15:51 -07:00
Floris van Doorn
ebba33057c
feat(hott): add arity.hlean, about multivariate functions
2015-03-16 17:15:51 -07:00
Floris van Doorn
71f9a5d1d2
feat(hott/algebra/precategory): do lots of stuff with categories
2015-03-16 17:15:51 -07:00
Jakob von Raumer
7083f2fccd
fix(hott/algebra) correct the name of a groupoid constructor
2015-03-13 15:45:46 -07:00
Jakob von Raumer
25abecaa26
chore(hott/algebra) cmall changes in category files
2015-03-13 15:45:02 -07:00
Leonardo de Moura
a24f8dce67
refactor(hott/algebra/precategory): minor cleanup
2015-03-12 20:52:00 -07:00
Leonardo de Moura
14aeac180a
refactor(library/algebra/category/constructions): more rewrite tactic tests
2015-03-12 20:27:11 -07:00
Leonardo de Moura
adae95cf68
refactor(hott/algebra/precategory/functor): remove unnecessary annotations
2015-03-12 20:13:40 -07:00
Leonardo de Moura
265316a9f5
refactor(hott/algebra/precategory/basic): remove unnecessary set_option commands
2015-03-12 20:10:47 -07:00
Leonardo de Moura
0118ecf3cd
refactor(hott/algebra/precategory/yoneda): remove unnecessary annotations
2015-03-12 20:06:25 -07:00
Leonardo de Moura
7accd0f1e6
feat(library/tactic/rewrite_tactic): allow rewrite with terms that contains binders
...
see discussion at #470
2015-03-12 18:07:55 -07:00
Leonardo de Moura
d7c6028a3e
refactor(hott,library): use/test the rewrite tactic in more places
...
The performance also improved.
2015-03-12 17:25:31 -07:00
Leonardo de Moura
55586dcb2d
refactor(hott/algebra/precategory/yoneda): reduce compilation time to 1sec using rewrite tactic
...
After the latest improvements, the rewrite tactic "works" more often
at yoneda.hlean
2015-03-12 17:07:27 -07:00
Leonardo de Moura
1490bdad49
feat(frontends/lean): add version of 'exact' tactic (sexact) that enforces goal type during term elaboration
2015-03-06 17:34:45 -08:00
Leonardo de Moura
368f9d347e
refactor(frontends/lean): approach used to parse tactics
...
The previous approach was too fragile
TODO: we should add separate parsing tables for tactics
2015-03-05 18:11:21 -08:00
Leonardo de Moura
039afb4578
feat(frontends/lean): treat "proof t qed" as alias for "by exact t"
2015-03-05 11:12:39 -08:00
Leonardo de Moura
8295ef4e57
fix(library/tactic/class_instance_synth): constraint execution order at type class resolution
...
We could not fix this problem before because we did not have the
[quasireducible] annotation.
Without this annotation, the fixed TC would loop in some HoTT files.
2015-03-04 22:20:20 -08:00
Jeremy Avigad
c09f1c4eaf
feat(*.md): create markdown files for HoTT library, update ones in standard library
2015-03-04 18:33:18 -08:00
Floris van Doorn
3d7656078d
feat(hott/types): prove that 'is_equiv f' is an hprop
2015-03-04 00:22:51 -05:00
Floris van Doorn
704f2b2697
feat(hott/algebra/category): prove that set is a univalent category assuming is_equiv is an hprop
2015-03-04 00:22:41 -05:00
Floris van Doorn
5b922aad5c
feat(init): add 'do' tactic
2015-03-04 00:17:41 -05:00
Floris van Doorn
da9b134dd8
feat(hott/types): start with proof that is_equiv is an hprop
2015-03-04 00:14:18 -05:00
Leonardo de Moura
e40e2f0677
feat(hott/init): define num.sub in the HoTT library
2015-03-03 16:22:59 -08:00
Leonardo de Moura
ca57b43698
feat(library/tactic): add 'change' tactic
2015-03-01 14:15:39 -08:00
Floris van Doorn
1559e0e58c
feat(hott): some more renaming in category library
2015-02-28 01:16:23 -05:00
Floris van Doorn
326eaffafb
style(hott/algebra): rename theorems in the HoTT category libraries
2015-02-28 01:16:23 -05:00
Floris van Doorn
23a248ab28
style(hott): let inverse notation have higher binding power than application
2015-02-28 01:16:23 -05:00
Floris van Doorn
219f7ae11a
feat(hott/algebra/precategory): general cleanup in precategories, define uncurrying functor
2015-02-28 01:16:23 -05:00
Floris van Doorn
f513538631
feat(hott): more cleanup of HoTT library
...
remove funext class,
remove a couple of sorry's,
add characterization of equality in trunctypes,
use Jeremy's format for headers everywhere in the HoTT library,
continue working on Yoneda embedding
2015-02-26 13:19:54 -05:00
Floris van Doorn
c091acc55b
feat(hott): remove funext as type class, add theorems to prove equalities between functors and natural transformations
2015-02-26 12:52:33 -05:00
Floris van Doorn
9201bd7ca6
feat (hott/init): move nat.of_num to init.num and make it reducible outside namespace nat
...
This is so that init.trunc can already use nat.of_num.
Also make nat.of_num reducible in the standard library
Also make gt and ge abbreviations
2015-02-26 12:28:57 -05:00
Leonardo de Moura
68110faa4d
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
2015-02-25 17:00:10 -08:00
Leonardo de Moura
5ca52d81ec
feat(frontends/lean): ML-like notation for match and recursive equations
2015-02-25 16:20:44 -08:00
Leonardo de Moura
3c24461e51
refactor(*): modify '|' binding power, use 'abs a' instead of '|a|', and '(a | b)' instead of 'a | b'
2015-02-25 15:18:21 -08:00
Leonardo de Moura
c04c610b7b
feat(frontends/lean): add 'assert H : A, ...' as notation for 'have H [visible] : A, ...'
2015-02-25 14:30:42 -08:00
