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

120 commits

Author SHA1 Message Date
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
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
227fcad22a feat(hott): various small changes 
move total_image.rec, redefine hvconcat/hvinverse and change precedence of transporto notation
 2017-09-07 14:37:07 -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
540d451e01 fix(hott): small fixes 2017-03-07 22:56:47 -05: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
217035b06c feat(hott): minor changes 2017-01-18 22:24:59 +01: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
467001c0a9 feat(hott): minor changes 2016-09-18 02:13:21 -04:00
Floris van Doorn
3213b1b3b0 feat(EM): Prove some corollaries of Whitehead's principle, and prove that K(G,1) is unique. 
Also reorder the arguments of is_equiv_compose
 2016-07-09 10:20:22 -07: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
ae1b2e854c feat(hott): various minor changes 2016-07-09 10:20:21 -07:00
Floris van Doorn
fcf06ae2f5 feat(vankampen): prove the van Kampen theorem with basepoints 2016-07-09 10:20:21 -07:00
Floris van Doorn
41de1a8271 feat(hit): add construction of propositional truncation to the library 2016-07-09 10:20:21 -07:00
Floris van Doorn
e96e4a677d feat(homotopy): prove the naive Seifert-Van Kampen theorem 
Also define the pushout of categories and the pushout of groupoids
 2016-07-09 10:20:21 -07:00
Floris van Doorn
61848c4a2e feat(hott): define pushout of groupoids 2016-07-09 10:20:21 -07:00
Floris van Doorn
9f13527c25 chore(hott): update default files and some markdown files 2016-07-09 10:20:21 -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
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
dc37ec954d refactor(hott): rename apdo to apd 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
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
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
e515875464 feat(hott): various additions 2016-03-03 10:13:20 -08:00
Leonardo de Moura
cc8d9bc7ff refactor(hott): replace 'assert'-expr with 'have'-expr 2016-02-29 12:11:17 -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
43cf2ad23d style(hott): replace all other occurrences of hprop/hset 
They are replaced by either Prop/Set or prop/set
 2016-02-22 11:15:38 -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
816237315c feat(hott): various additions, especially for pointed maps/homotopies/equivalences 2016-02-22 11:15:38 -08:00
Jakob von Raumer
aa5e188179 feat(hott): add symmetry of pushouts and pointed pushouts 2016-01-24 16:30:26 -08:00
Jakob von Raumer
664132b845 feat(hott): add calc lemmas for pointed equivalences, make pinl and pinr constructors 2016-01-24 16:30:16 -08:00
Jakob von Raumer
8d22e454e7 feat(hott): add theory about pointed pushouts 2016-01-24 16:30:12 -08:00
Ulrik Buchholtz
b09fdc8c61 feat(hott/hit): flattening lemmas for coeq and pushout 2015-12-28 09:06:13 -08:00
Ulrik Buchholtz
f3b2c7010f feat(hott): functoriality of quotients 2015-12-28 09:06:13 -08:00
Floris van Doorn
c852f7bc71 feat(hott): use the induction tactic for trunc at some places 2015-12-17 12:46:16 -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
c44ad80e4e feat(homotopy/torus): give recursion and induction principle for the torus 
also change the surface of the torus to a square instead of an equality between paths
 2015-11-22 18:29:37 -08:00
Floris van Doorn
fe8a858d79 feat(hott): add recursor to refl_quotient 2015-11-22 18:29:37 -08:00
Floris van Doorn
ae92e8c94d feat(hit/two_quotient): give dependent eliminator for two_quotients 2015-11-22 18:29:37 -08:00
Floris van Doorn
482c68b387 feat(*/list): add some computation rules for lists in both libraries 2015-11-22 14:21:26 -08:00
Floris van Doorn
88a62f8e74 feat(algebra|types): small additions 
add to markdown file for algebra, and add some definitions in types/
 2015-11-22 14:21:25 -08:00