Floris van Doorn
540d451e01
fix(hott): small fixes
2017-03-07 22:56:47 -05:00
Floris van Doorn
8bdd699fca
feat(functor.adjoint): give another way to construct an adjunction
2017-03-07 22:48:44 -05:00
Floris van Doorn
5eafb1f6b2
feat(algebra): use infinity groups
2017-02-02 21:38:48 -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
217035b06c
feat(hott): minor changes
2017-01-18 22:24:59 +01:00
Jeremy Avigad
bb67a3b9bf
feat(hott/algebra/homomorphism): more general treatment of homomorphisms
2017-01-11 13:45:42 -05: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
ecbe4af3c7
fix(hott:group): use only reducible definitions in instances
2016-12-02 16:55:23 -08:00
Floris van Doorn
d12a2a264b
fix(hott:group_theory): change group to has_mul
2016-12-02 16:55:23 -08:00
Floris van Doorn
d5a72f6327
feat(homotopy_group): use is_succ for homotopy groups
...
Now you can use πg[n] as long as Lean can find an instance that n is a successor, you don't have to always write πg[k+1]
2016-09-22 16:00:27 -04: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
554abe88c2
feat(hott/algebra): define bundled additive groups as multiplicative groups
2016-09-19 22:13:42 -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
11c08c51e6
fix(algebra/group_theory): split homomorphisms into additive and multiplicative homomorphisms
2016-09-18 02:14:31 -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
fe1fbae540
feat(category.pushout): give the universal property of the pushout of categories
2016-09-17 17:05:46 -04:00
Jakob von Raumer
c81c86a9b8
chore(hott) remove duplicate lemma, make defs private, update book.md
2016-09-08 19:34:54 -07:00
Jakob von Raumer
e79063970d
feat(hott) finish proof of lemma 9.9.4
2016-09-08 19:34:54 -07:00
Jakob von Raumer
5f06496f89
feat(hott) almost finish 9.9.4 proof
2016-09-08 19:34:54 -07:00
Jakob von Raumer
3e1ee4b714
feat(hott) add functor axioms for lemma 9.9.4 construction
2016-09-08 19:34:54 -07:00
Jakob von Raumer
d26d98531c
feat(hott) add morphism part of construction for lemma 9.9.4
2016-09-08 19:34:54 -07:00
Jakob von Raumer
8718a649c4
feat(hott) add first bit of proof of 9.9.4: construction of some gadgets and prove that they are contractible
2016-09-08 19:34:54 -07:00
Jakob von Raumer
548671ce1b
feat(hott) prove lemma 9.9.2: essentially surjective and full functors induce fully faithful functors in the functor category
2016-09-08 19:34:54 -07:00
Jakob von Raumer
0ff8a96be1
feat(hott) formalize book lemma 9.9.1: essentially surjective functors induce faithful functors in the functor category
2016-09-08 19:34:54 -07:00
Jakob von Raumer
cc70845332
chore(hott) update book.md and constructions.md to include rezk completion
2016-07-09 10:32:50 -07:00
Jakob von Raumer
18a27cf963
chore(hott) merge namespaces in rezk completion
2016-07-09 10:31:42 -07:00
Jakob von Raumer
82a8d137da
feat(hott) prove that rezk functor is a weak equivalence
2016-07-09 10:31:42 -07:00
Jakob von Raumer
57bf0a09dd
feat(hott) add rezk completion as univalent category
2016-07-09 10:31:42 -07:00
Jakob von Raumer
86d9a1c84d
feat(hott) add id_of_iso of rezk completion
2016-07-09 10:31:42 -07:00
Jakob von Raumer
6d6ab3f36b
feat(hott) instantiate rezk completion as precategory
2016-07-09 10:31:42 -07:00
Jakob von Raumer
64e1e5404c
feat(hott) add composition for rezk completion
2016-07-09 10:31:41 -07:00
Jakob von Raumer
5c4aac6c8a
feat(hott) add idenity for rezk completion
2016-07-09 10:31:41 -07:00
Jakob von Raumer
a5fe82f177
feat(hott) add carrier and hom set of rezk completion
2016-07-09 10:31:41 -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
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
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
2afdaf6906
fix(groupoid): redefine groupoid given by a group
...
The composition was in the reverse order
2016-05-06 14:27:27 -07:00
