Jakob von Raumer
651df51cb7
chore(hott) the coercion doesn't seem to be the problem
2016-04-11 09:45:59 -07:00
Jakob von Raumer
7a9e1c7f4f
chore(hott) fix sum proof by adding manual coercions
2016-04-11 09:45:59 -07:00
Floris van Doorn
a6319118e3
feat(types.pointed): small additions
2016-04-11 09:45:59 -07:00
Floris van Doorn
f983724cf6
feat(pointed): merge pointed2 into pointed
...
We move the basic notions of pointed types into init.pointed, to avoid cycles in the import graph. Also adds pointed versions of pi and sigma, with corresponding notation
2016-04-11 09:45:59 -07:00
Floris van Doorn
4895726c54
feat(connectedness): show that if f is n-connected, then trunc_functor k f is so, too
2016-04-11 09:45:59 -07:00
Floris van Doorn
54da5bcbda
feat(hott): add some [constructor] attributes
2016-04-11 09:45:59 -07:00
Floris van Doorn
3887efa7c1
feat(hott): some renamings in init.path
2016-04-11 09:45:59 -07:00
Floris van Doorn
3240df6020
feat(book): add comments about chapter 10
2016-04-11 09:45:59 -07:00
Floris van Doorn
dc37ec954d
refactor(hott): rename apdo to apd
2016-04-11 09:45:59 -07:00
Floris van Doorn
80a2e285cb
feat(init/ua): add ua_symm and ua_trans
2016-04-11 09:45:59 -07:00
Floris van Doorn
05b59aecf8
refactor(hott): rename apd to apdt
2016-04-11 09:45:59 -07:00
Floris van Doorn
b1ed69f621
feat(hott): small changes, mostly in pointed2
2016-04-11 09:45:59 -07:00
Leonardo de Moura
226f8bafeb
fix(library/tactic/rewrite_tactic): do not allow projections to be unfolded
...
fixes #1032
This is just a workaround. A better fix has been implemented in the
lean3 branch.
2016-03-28 13:02:57 -07:00
Ulrik Buchholtz
1c52062f1e
chore(hott): standardize names of homotopy_of_inv_homotopy_post and friends
2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
5257e282aa
feat(hott/homotopy): additions to sphere and susp, improve quaternionc_hopf
2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
7e8ba1440f
feat(hott): update book.md and homotopy.md to reflect additions
2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
f11169b8f2
feat(hott): the quaternionic hopf fibration
2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
89296ec52a
feat(hott): the complex hopf fibration S3 to S2
2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
d53320cb0f
feat(hott): the imaginaroid version of the cayley dickson construction
2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
0b9084c7d2
feat(hott): hopf construction and delooping of K(G,1)s
2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
bb64913e50
feat(hott): flattening lemma for susp
2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
bd9e47c82c
feat(hott): functoriality of pushout; connectedness in is_conn namespace
...
other changes:
- move result about connectedness of susp to homotopy.susp
- improved definition of circle multiplication
- improved the interface to join
2016-03-23 09:22:55 -07:00
Leonardo de Moura
5e14b4ebe8
fix(library,hott): avoid rewrite with patterns of the form (?M ...)
2016-03-09 15:39:17 -08:00
Floris van Doorn
003c11c917
feat(connectedness): is_conn_map -> is_conn_fun, and unbundle the P in elimination principles
2016-03-06 13:03:31 -05:00
Floris van Doorn
1e10810a1e
feat(init/funext): add function extensionality as an axiom.
...
This allows us to keep track of theorems which use function extensionality, but not full univalence
2016-03-06 13:03:31 -05:00
Floris van Doorn
2d9c3985c9
feat(square): add variants of eq_pathover
2016-03-06 13:03:31 -05:00
Floris van Doorn
671ef077b9
feat(hott): additions, mostly to types.trunc
2016-03-06 13:03:31 -05:00
Floris van Doorn
5cacebcf86
feat(hott): replace assert by have and merge namespace equiv.ops into equiv
...
The coercion A ≃ B -> (A -> B) is now in namespace equiv. The notation ⁻¹ for symmetry of equivalences is not supported anymore. Use ⁻¹ᵉ
2016-03-03 10:13:21 -08:00
Floris van Doorn
058000f61d
feat(homotopy/homotopy_group): add theorems in section 8.3 of the HoTT book
2016-03-03 10:13:21 -08:00
Floris van Doorn
1903601ba5
refactor(trunc): rename namespace is_trunc.trunc_index to trunc_index
2016-03-03 10:13:20 -08:00
Floris van Doorn
e2b31a9b33
feat(hott): remove multiple_instances attribute
2016-03-03 10:13:20 -08:00
Floris van Doorn
af4ba3d2fb
feat(hott): prove that the (n+1)-sphere is n-connected
2016-03-03 10:13:20 -08:00
Floris van Doorn
e515875464
feat(hott): various additions
2016-03-03 10:13:20 -08:00
Floris van Doorn
c6e628da12
feat(hott): more computation rules for trunc_index and use nats for Lemma 8.6.2
2016-03-03 10:13:20 -08:00
Floris van Doorn
e5d5ef9d55
feat(hott/library): various changes and additions.
...
Most notably:
Give le.refl the attribute [refl]. This simplifies tactic proofs in various places.
Redefine the order of trunc_index, and instantiate it as weak order.
Add more about pointed equivalences.
2016-03-03 10:13:20 -08:00
Floris van Doorn
65b367ddff
feat(fin): port more parts of fin from the standard library
2016-03-03 10:13:20 -08:00
Floris van Doorn
bf403e124a
feat(nat/div): port to HoTT library
2016-03-03 10:13:20 -08:00
Floris van Doorn
4238fdd3d8
fix(hott): add missing links to markdown files
2016-03-03 10:13:20 -08:00
Jakob von Raumer
1104537d02
chore(hott) adjust to new naming for pointed types and truncated types
2016-03-01 13:52:53 -08:00
Jakob von Raumer
2b13777bbe
feat(hott) add type functors, maybe they should be changed to be un-funexted.
2016-03-01 13:52:53 -08:00
Jakob von Raumer
11458f64fe
feat(hott/algebra) add order categories
2016-03-01 13:52:53 -08:00
Leonardo de Moura
fbe5188480
refactor(frontends/lean): remove 'by+' and 'begin+' tokens
2016-02-29 13:45:43 -08:00
Leonardo de Moura
faa0031d4e
refactor(library,hott): remove 'by+' and 'begin+'
2016-02-29 13:15:48 -08:00
Leonardo de Moura
b41c65f549
feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking
2016-02-29 12:31:23 -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
101cf1ec4c
feat(frontends/lean): remove difference between 'have' and 'assert'
2016-02-29 11:28:20 -08:00
Leonardo de Moura
5a4dd3f237
feat(library/reducible): remove [quasireducible] annotation
2016-02-25 17:42:44 -08:00
Leonardo de Moura
d501295ec1
refactor(algebra/binary): remove unnecessary annotations
2016-02-25 15:11:52 -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
