Floris van Doorn
f2dfca25f9
refactor: use notation for trunc_index
2018-09-20 16:03:32 +02:00
Floris van Doorn
3468ab8a9f
rename nondep to constant
2018-09-20 15:53:05 +02:00
Floris van Doorn
183ca62cc1
reverse sigma_assoc_equiv, and add variant
2018-09-20 01:50:34 +02:00
Floris van Doorn
4b603990fc
make instances in sigma explicit
2018-09-14 17:56:25 +02:00
Floris van Doorn
c534985d3f
move files from Spectral
2018-09-11 19:25:32 +02:00
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
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
04c80c477f
add psquares with two constant sides
2018-09-07 11:58:46 +02:00
Floris van Doorn
c5d31f76d7
move definitions from spectral repository here
2018-09-07 11:58:13 +02:00
Floris van Doorn
c8477d28ba
generalize many results about pointed homotopies of nondependent maps to dependent maps
2017-07-21 15:53:34 +01:00
Floris van Doorn
1a26d405ef
define pmap in terms of ppi
2017-07-21 15:53:34 +01:00
Floris van Doorn
27cde0aeae
feat(hott): rename ppi_gen to ppi
2017-07-21 15:53:34 +01:00
Floris van Doorn
64327eb804
fix precedence of ->*
...
and some other small changes
2017-07-21 15:53:34 +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
a1126cfcf2
feat(trunc): simplify proof further
2017-06-16 14:38:46 -04:00
Floris van Doorn
9066ee4801
feat(trunc): simplify proof
...
unreachable code was reached with the old proof in some builds
2017-06-16 14:34:52 -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
9265094f96
feat(pointed): redefine pequiv
...
Now the underlying pointed function and pointed inverse are the functions which were put in definitionally
2017-06-14 21:28:31 -04:00
Floris van Doorn
66ea4a4725
fix(LES_of_homotopy_groups): make LES of homotopy groups more usable
2017-06-14 20:03:41 -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
76a8dd1816
fix(prod): revert change with unintended consequence
2017-05-24 17:13:10 -04:00
Floris van Doorn
ba5368c4ae
feat(hott): various small changes
2017-05-22 00:56:05 -04:00
Floris van Doorn
0cf04ed3f2
feat(hott): port group_power and int/order from standard library. Update markdown files
2017-05-22 00:56:04 -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
540d451e01
fix(hott): small fixes
2017-03-07 22:56:47 -05:00
Floris van Doorn
916bde4050
feat(pointed): make the definition of ap1 and ap1_con more convenient to use
2017-02-18 17:18:41 -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
2d918bafaa
feat(pointed): some definition changes to make reasoning about them easier
2017-01-18 22:25:26 +01:00
Floris van Doorn
249d57cd02
feat(hott): small additions and fixes
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
217035b06c
feat(hott): minor changes
2017-01-18 22:24:59 +01:00
Floris van Doorn
dbe4856cbd
fix(nat/hott): add constructor attribute for is_succ
2017-01-18 22:24:59 +01:00
Floris van Doorn
f87210fcf6
feat(hott): various small 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
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
c884e7bbb9
feat(hott/algebra): define additive structures to be multiplicative structures
2016-09-19 22:13:35 -04:00
Floris van Doorn
8d6010ccad
feat(pointed): use pointed equivalences instead of equalities for some lemmas
2016-09-18 02:14:32 -04:00
Floris van Doorn
e2734080c6
fix(algebra): change the reducibility of some defintions
2016-09-18 02:14:32 -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
Floris van Doorn
467001c0a9
feat(hott): minor changes
2016-09-18 02:13:21 -04:00
Floris van Doorn
ddec6f77ee
feat(category.pushout): finish second way of formulating universal property
2016-09-18 02:13:03 -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
2cc8914874
feat(homotopy): add results about infty-connectedness and loops of EM-spaces
2016-07-09 10:20:22 -07: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
