Floris van Doorn
9a17a244c9
move more results and make arguments explicit
...
More results from the Spectral repository are moved to this library
Also make various type-class arguments of truncatedness and equivalences which were hard to synthesize explicit
2018-09-11 17:06:08 +02:00
Floris van Doorn
5eafb1f6b2
feat(algebra): use infinity groups
2017-02-02 21:38:48 -05:00
Floris van Doorn
25ab404781
feat(algebra): define the infinity-version of algebraic structures with one binary operator
2017-02-02 17:23:23 -05:00
Floris van Doorn
e87a27cb4b
fix(hott/init/path): reorder arguments of whisker_right
2016-12-02 16:55:23 -08:00
Floris van Doorn
9342fe2716
feat(hott) move many lemmas to library, and cleanup various parts
2016-12-02 16:55:23 -08:00
Floris van Doorn
ecbe4af3c7
fix(hott:group): use only reducible definitions in instances
2016-12-02 16:55:23 -08:00
Floris van Doorn
c884e7bbb9
feat(hott/algebra): define additive structures to be multiplicative structures
2016-09-19 22:13:35 -04:00
Floris van Doorn
c68e013fcb
refactor(fin+nat): move is_succ to nat
2016-09-18 02:14:25 -04:00
Floris van Doorn
d70334d100
feat(hott/algebra/bundled): add a parameter to Group to specify whether it's an additive or multiplicative group
2016-09-18 02:13:30 -04:00
Leonardo de Moura
5e14b4ebe8
fix(library,hott): avoid rewrite with patterns of the form (?M ...)
2016-03-09 15:39:17 -08:00
Leonardo de Moura
cc8d9bc7ff
refactor(hott): replace 'assert'-expr with 'have'-expr
2016-02-29 12:11:17 -08:00
Leonardo de Moura
768ba1c363
refactor(library/hott): remove more unnecessary annotations
2016-02-25 14:30:00 -08:00
Leonardo de Moura
510168a387
refactor(library,hott): remove unnecessary annotations
2016-02-25 12:26:20 -08:00
Floris van Doorn
4e2cc66061
style(*): rename is_hprop/is_hset to is_prop/is_set
2016-02-22 11:15:38 -08:00
Floris van Doorn
da5f10ce63
feat(hott): minor fixes. allow the usage of numerals for trunc_index
2015-12-17 12:46:16 -08:00
Floris van Doorn
4ef58f1ba5
chore(hott): more cleanup.
...
Make zero and one reducible (see algebra/port.md)
Change some theorems which need to compute into definitions
2015-12-10 10:42:16 -08:00
Floris van Doorn
2325d23f68
feat(hott): port nat and int from the standard library
2015-12-09 12:36:11 -08:00
Floris van Doorn
46739c8b70
feat(hott/algebra): port abstract structures
2015-12-09 12:34:06 -08:00
Floris van Doorn
74aff044ef
feat(group): port three more theorems from the standard library
2015-11-22 14:21:26 -08:00
Leonardo de Moura
9bedbbb739
refactor(library,hott): remove coercions between algebraic structures
...
They are classes, and mixing coercion with type class resolution is a
recipe for disaster (aka counterintuitive behavior).
2015-11-11 11:57:44 -08:00
Leonardo de Moura
d1e111fd6c
fix(hott,frontends/lean,library,library/tactic): make sure we can still compile the HoTT library
2015-11-08 14:04:55 -08:00
Leonardo de Moura
744d1cba3d
feat(library,hott,frontends/lean): avoid keywords with hyphen
2015-11-08 14:04:54 -08:00
Floris van Doorn
115dedbd1c
fix(hott): notation spacing and markdown files
2015-10-02 16:26:10 -07:00
Leonardo de Moura
cfafc90cc0
refactor(hott,library): make sure files compile even without using "projection macros"
2015-06-22 12:22:11 -07:00
Jeremy Avigad
3b010b8c92
feat({library,hott}/algebra/group): add abbreviations e.g. for mul.cancel_left
2015-06-15 22:53:11 +10:00
Jeremy Avigad
33214f0895
refactor(hott/*): remove 'Module:' lines
2015-05-23 20:52:58 +10:00
Jeremy Avigad
d33c91d7b9
fix({hott,library}/algebra/*): fix names
2015-05-23 14:05:06 +10:00
Floris van Doorn
2144036cdb
feat(hott.circle): prove that the fundamental group of the circle is equal to the integers, as groups
...
Also many minor fixes at various places
2015-05-18 15:59:55 -07:00
Leonardo de Moura
19361f0196
feat(library/unifier): do not fire type class resolution as last resort when type contains metavariables
...
see discussion at #604
2015-05-18 15:45:23 -07:00
Floris van Doorn
7cfac38eda
feat(hott): port parts of natural numbers and integers from standard library to HoTT
...
This also involves:
- adding definitions about logic and natural numbers existing in the standard library to init
- porting the current algebraic hierarchy
2015-05-07 16:39:03 -07:00
Floris van Doorn
90f1a691fd
feat(hott): change notation of transport to correspond with standard library
2015-05-07 16:39:03 -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
23a248ab28
style(hott): let inverse notation have higher binding power than application
2015-02-28 01:16:23 -05:00
Floris van Doorn
61901cff81
feat(hott): rename definition and cleanup in HoTT library
...
also add more definitions in types.pi, types.path, algebra.precategory
the (pre)category library still needs cleanup
authors of this commit: @avigad, @javra, @fpvandoorn
2015-02-20 21:40:42 -05:00
Leonardo de Moura
b4d6f6e3ed
feat(frontends/lean): 'attribute' command is persistent by default
2015-01-26 11:51:17 -08:00
Leonardo de Moura
4f2e0c6d7f
refactor(frontends/lean): add 'attribute' command
...
The new command provides a uniform way to set declaration attributes.
It replaces the commands: class, instance, coercion, multiple_instances,
reducible, irreducible
2015-01-24 20:23:21 -08:00
Leonardo de Moura
abc64fbab8
refactor(library/algebra/group): remove unnecessary symm
2015-01-20 16:20:47 -08:00
Leonardo de Moura
2e4a2451e6
refactor(library/reducible): simplify reducible/irreducible semantics
2015-01-08 18:52:18 -08:00
Jakob von Raumer
503048226e
chore(hott) fix the types and algebra
2014-12-16 13:11:32 -08:00
Jakob von Raumer
dae2aeb605
chore(hott) fix file endings
2014-12-16 13:11:32 -08:00
