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
|
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
|
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
|
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
|
fcf06ae2f5
|
feat(vankampen): prove the van Kampen theorem with basepoints
|
2016-07-09 10:20:21 -07:00 |
|
Floris van Doorn
|
735230ad07
|
feat(hott): small changes, simplify van Kampen
|
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 |
|