Floris van Doorn
3d0d0947d6
various cleanup changes in library
...
some of the changes are backported from the hott3 library
pi_pathover and pi_pathover' are interchanged (same for variants and for sigma)
various definitions received explicit arguments: pinverse and eq_equiv_homotopy and ***.sigma_char
eq_of_fn_eq_fn is renamed to inj
in definitions about higher loop spaces and homotopy groups, the natural number arguments are now consistently before the type arguments
2018-09-10 17:59:11 +02:00
Floris van Doorn
afdcf7cb71
backport some changes from lean 3
...
ap_compose' is reversed, and is_trunc_equiv_closed and variants don't have a type class argument anymore
2018-09-10 17:05:29 +02:00
Floris van Doorn
9e3611fe3e
move naturality of loop-susp-adjunction to standard library
2017-07-21 15:53:34 +01:00
Floris van Doorn
ddef24223b
make pointed suspensions, wedges and spheres the default (in contrast to the unpointed ones), remove sphere_index
...
All HITs which automatically have a point are pointed without a 'p' in front. HITs which do not automatically have a point do still have a p (e.g. pushout/ppushout).
There were a lot of annoyances with spheres being indexed by N_{-1} with almost no extra generality. We now index the spheres by nat, making sphere 0 = pbool.
2017-07-20 15:02:09 +01:00
Floris van Doorn
914addc66c
feat(homotopy): introduce notation for topological type constructors
...
Also change the alternative induction/recursion principle for the smash product
2017-01-18 22:24:59 +01: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
17ccc283a9
feat(hott): move basic theorems from colimit development to library.
...
Most notable changes:
rename apo011 -> apd011 and apd011 -> apdt011
make an argument of pathover_of_eq explicit
2016-07-09 10:20:22 -07:00
Floris van Doorn
54da5bcbda
feat(hott): add some [constructor] attributes
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
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
Sebastian Ullrich
2185ee7e95
feat(library/tactic): make let tactic transparent, introduce new opaque note tactic
...
The new let tactic is semantically equivalent to let terms, while `note`
preserves its old opaque behavior.
2015-12-14 10:14:02 -08:00
Jakob von Raumer
68901c7788
feat(hott/homotopy): complete join associativity proof, helper lemmas for squares
2015-12-02 23:13:21 -08:00
Jakob von Raumer
bd064ef9c8
feat(hott/homotopy): prove missing helper lemmas up to cube massaging
2015-12-02 23:13:17 -08:00
Jakob von Raumer
811f3067ff
feat(hott): join associativity proof done up to small auxiliary lemmas, add transposition, inversion of cubes
2015-12-02 23:13:12 -08:00
Jakob von Raumer
e481e541a2
feat(hott/homotopy): more progress on join associativity
2015-12-02 23:13:03 -08:00
Jakob von Raumer
6c6dde7e48
feat(hott/homotopy): progress on join associativity, many coherence lemmas about square operations needed
2015-12-02 23:12:59 -08:00
Jakob von Raumer
54b1d1a9fe
feat(hott/homotopy): more steps towards join associativity, cube composition
2015-12-02 23:12:46 -08:00
Jakob von Raumer
e1e8680474
feat(hott/homotopy): continue defining squares for join associativity
2015-12-02 23:12:41 -08:00
Jakob von Raumer
12a498d411
feat(hott/homotopy): add join switch and derive associativity from switch
2015-12-02 23:12:29 -08:00
Jakob von Raumer
149e5fff9f
feat(hott/homotopy): add commutativity proof for join
2015-12-02 23:12:24 -08:00
Jakob von Raumer
eea219e33f
feat(hott/homotopy): start associativity proof for join
2015-12-02 23:12:19 -08:00
Jakob von Raumer
d508ceccec
feat(hott/homotpy) add join operator, and prove two basic lemmas
2015-10-13 09:59:24 -07:00
