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

34 commits

Author SHA1 Message Date
Floris van Doorn
2b722b3e34 use psquare for naturality squares consistently 
this commit renames some definitions and swaps some arguments around for consistency
 2018-09-10 17:59:11 +02:00
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
1a26d405ef define pmap in terms of ppi 2017-07-21 15:53:34 +01: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
39a8c7fef4 feat(pointed): define phomotopy as a dependent pointed function 
this also requires dependent pointed functions to be generalized to the case where the type family only has a point over the basepoint of the basetype
 2017-06-17 17:20:04 -04:00
Floris van Doorn
5ad4443237 feat(pointed): rename pequiv.MK2 to pequiv.MK, it is the more natural constructor 
also move some definitions from pointed or equiv to pointed2 and define transitivity so that it computes
 2017-06-14 22:47:55 -04:00
Floris van Doorn
7d0eecc449 feat(hott): move basic lemmas from the spectral repository to the main repository 2017-06-02 12:13:20 -04:00
Floris van Doorn
c268731093 fix(hott): small changes to pointed and susp and book.md 2017-03-30 16:51:51 -04:00
Floris van Doorn
8e2adaa5ba feat(pointed): generalize the definition of ap1 so that we can use path induction to prove properties about it 2017-03-30 16:51:20 -04:00
Floris van Doorn
2d918bafaa feat(pointed): some definition changes to make reasoning about them easier 2017-01-18 22:25:26 +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
55bdf2764b feat(homotopy/red_susp): prove that reduced suspension is equivalent to suspension, and some small things 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
341a53b880 feat(pointed): make the naming in the pointed library more consistent. 
Also start on a naming conventions file
 2016-09-22 16:00:27 -04:00
Floris van Doorn
fd5adb831b feat(category.pushout): finish universal property of pushout 
In the previous commit there was still one step missing: that the natural isomorphisms are also unique.
 2016-09-17 17:05:46 -04: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
dd5dcb1dd1 feat(hott): prove something without using ua and update book.md 2016-07-09 10:20:21 -07:00
Floris van Doorn
52dd6cf90b feat(hott): Port files from other repositories to the HoTT library. 
This commit adds truncated 2-quotients, groupoid quotients, Eilenberg MacLane spaces, chain complexes, the long exact sequence of homotopy groups, the Freudenthal Suspension Theorem, Whitehead's principle, and the computation of homotopy groups of almost all spheres which are known in HoTT.
 2016-05-06 14:27:27 -07:00
Floris van Doorn
8db4676c46 feat(hott): various changes and additions in the HoTT library 
Add more theorems about mapping cylinders, fibers, truncated 2-quotient, truncated univalence, pre/postcomposition with an iso in a precategory.

renamings: equiv.refl -> equiv.rfl and equiv_eq <-> equiv_eq'
 2016-05-06 14:27:27 -07:00
Floris van Doorn
a6b5191be6 feat(pushout/susp): change definition of elim_type, so that flattening is easier to prove 2016-05-06 14:26:46 -07:00
Floris van Doorn
dc37ec954d refactor(hott): rename apdo to apd 2016-04-11 09:45:59 -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
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
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
087c44d614 style(hott): rename instances of pType using pfoo instead of Foo 
For example, the pointed suspension operation was called Susp before this commit, but now is called psusp
 2016-02-22 11:15:38 -08:00
Floris van Doorn
bac6d99cc7 style(hott): rename Pointed to pType 
also rename sigma_equiv_sigma_id to sigma_equiv_sigma_right and similarly for pi
 2016-02-22 11:15:38 -08:00
Floris van Doorn
ecc141779a feat(init.path): update init.path to use tactics, also some additions 
Now the file hardly uses eq.rec explicitly anymore.
Also add the fact that horizontal and vertical inverses of paths are equal
Make one more argument explicit in eq.cancel_left and eq.cancel_right (to make it nicer to write 'apply cancel_right p')
 2016-02-22 11:15:38 -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
3c4c722afd feat(hott): port more from chapters 4 and 6 of the book 2015-09-28 09:09:21 -07:00
Ulrik Buchholtz
384a366e0f refactor(hott): move homotopy hits to new homotopy folder 2015-09-24 22:52:33 -04:00
Renamed from hott/hit/susp.hlean (Browse further)