Floris van Doorn
a69a4226c6
reorder arguments of definitions about squares and squareovers
...
This is to be consistent with the order of the type square. These arguments are mostly implicit, with as most notable exception the square(over) fillers.
2018-09-07 11:58:46 +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
540d451e01
fix(hott): small fixes
2017-03-07 22:56:47 -05: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
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
Jakob von Raumer
811f3067ff
feat(hott): join associativity proof done up to small auxiliary lemmas, add transposition, inversion of cubes
2015-12-02 23:13:12 -08:00
Jakob von Raumer
e481e541a2
feat(hott/homotopy): more progress on join associativity
2015-12-02 23:13:03 -08:00
Jakob von Raumer
6c6dde7e48
feat(hott/homotopy): progress on join associativity, many coherence lemmas about square operations needed
2015-12-02 23:12:59 -08:00
Jakob von Raumer
1b52ae8858
feat(hott/cubical): add cube concatenations
2015-12-02 23:12:54 -08:00
Jakob von Raumer
3f1cf3835f
chore(hott/cubical): change order of visible arguments in cube
2015-12-02 23:12:50 -08:00
Jakob von Raumer
54b1d1a9fe
feat(hott/homotopy): more steps towards join associativity, cube composition
2015-12-02 23:12:46 -08:00
Jakob von Raumer
e1e8680474
feat(hott/homotopy): continue defining squares for join associativity
2015-12-02 23:12:41 -08:00
Jakob von Raumer
2bc45f4de1
feat(hott/cubical): add cubes which are degenerate in one dimension
2015-12-02 23:12:37 -08:00
Jakob von Raumer
bba6ab5a6d
feat(hott/cubical): add fillers and other little lemmas for squares and cubes
2015-12-02 23:12:34 -08: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
