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
Floris van Doorn
5328486d49
feat(hit): add elimination rule to propositions
2015-11-22 14:21:25 -08:00
Floris van Doorn
5b8486a34f
feat(set_quotient): add some properties for set_quotients
2015-11-22 14:21:25 -08:00
Floris van Doorn
a99a99f047
feat(hit/quotient): prove the flattening lemma
2015-11-08 14:04:59 -08:00
Leonardo de Moura
ede23a3267
feat(hott,library): add additional spacing hints
2015-09-30 17:41:44 -07: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
Leonardo de Moura
4a6ff8058d
fix(hott): import commands (some files have been moved to different directories)
2015-09-25 09:39:45 -07:00
Ulrik Buchholtz
384a366e0f
refactor(hott): move homotopy hits to new homotopy folder
2015-09-24 22:52:33 -04:00
Floris van Doorn
e84b22864f
feat(hott): various changes in the HoTT library
2015-09-11 23:35:21 -07:00
Floris van Doorn
fd89aa77a3
feat(hott): prove Yoneda lemma
2015-09-11 23:35:21 -07:00
Floris van Doorn
a8964adb9c
fix(hott): make sure there are no sorry's visible
2015-09-01 15:17:46 -07:00
Floris van Doorn
f4892db432
feat(types.trunc): prove the principle of unique choice
2015-09-01 15:17:46 -07:00
Floris van Doorn
ad5cda48a8
refactor(hott): move cubical folder and files eq2, function and hprop_trunc from types/ to the root HoTT directory
2015-08-07 13:34:41 -07:00
Floris van Doorn
d111607890
feat(hott): add file which maps sections of the HoTT book to the HoTT library
2015-08-07 13:34:41 -07:00
Floris van Doorn
0ec525a8ee
feat(two_quotient): finish proof of elim_incl2
2015-08-07 13:34:40 -07:00
Floris van Doorn
e198be318f
feat(circle): show that x = x in the circle is always Z
2015-08-04 13:01:11 +02:00
Floris van Doorn
7a780b1b60
feat(hott): various minor changes in the HoTT library
2015-08-04 13:01:11 +02:00
Leonardo de Moura
b3cd3efbb4
refactor(hott): fix "sorry"s at int/basic.hlean, and comment the remaining "sorry"s
2015-07-27 08:34:11 -07:00
Leonardo de Moura
584f9e3f49
fix(library/tactic/unfold_rec): support indexed families at unfold_rec
...
This commit also removes many (now unnecessary) folds from the HoTT
library.
See issue #692
We still have to implement support for recursive definitions based on
brec_on that recurse over inductive families.
2015-07-12 12:32:58 -04:00
Leonardo de Moura
4b1b3e277f
feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]'
...
see issue #693
2015-07-07 16:37:06 -07:00
Floris van Doorn
24762fe843
feat(hit): add hits with 2-path constructors
...
In hit.two_quotient we define a general construction to define hits with 2-dimensional path constructors, similar to quotients.
We can add 2-paths between any two 'words', where a word consists of 1-path constructors, concatenation and inverses.
We use this to define the torus, reflexive quotients and the reduced suspension.
There is still one 'sorry' in the construction
2015-06-25 22:31:41 -04:00
Floris van Doorn
ea0f57aef5
feat(hott): various clean-up and small additions
2015-06-25 22:31:40 -04:00
Floris van Doorn
2748525c21
feat(hit/susp): finish the proof that loop space is adjoint to the suspension
2015-06-25 22:31:40 -04:00
Floris van Doorn
124c9d3d8a
feat(hott): various cleanup and fixes, rename \~ to ~, expand types.pointed
2015-06-25 22:31:40 -04:00
Floris van Doorn
fa1979c128
feat(datatypes): let the type of unit be the lowest non-Prop universe
...
The definitional package (brec_on and cases_on) now use poly_unit instead of unit
closes #698
2015-06-25 17:33:46 -07:00
