Commit graph

16 commits

Author SHA1 Message Date
Floris van Doorn
24e35a9f2c fix(hott/trunc): comment out sorry 2014-11-22 17:44:12 -08:00
Floris van Doorn
e8b076e460 feat(hott/types/sigma): port large part of the sigma library from the hott library
most importantly, prove the characterization of paths in sigma types
2014-11-22 17:44:12 -08:00
Jakob von Raumer
bc33af9f51 feat(library/hott) add universe polymorphism to paths, truncation, etc... get stuck at ua to funext proof anyway 2014-11-21 10:46:16 -08:00
Jakob von Raumer
fdafb1c11f fix(library/hott) adapt trunc.lean to missing equiv coercion 2014-11-17 18:39:02 -08:00
Jakob von Raumer
df4a8db23d feat(library/hott) add to trunc.lean: contractible types are equivalent to unit 2014-11-13 20:43:46 -08:00
Floris van Doorn
107a9cf8e4 feat(library): port more of truncation library from Coq HoTT
Everything directly about truncations in the basic truncation library is ported.
Some theorems about other structures still need to be ported.
Also made some minor changes in hott.equiv
2014-11-08 19:12:54 -08:00
Floris van Doorn
cd33d2e96d refactor(typeof): move typeof to general_notation 2014-11-08 19:12:54 -08:00
Floris van Doorn
74779dd855 feat(hott/trunc): clean up some theorems, prove some basic theorems 2014-11-08 19:12:54 -08:00
Floris van Doorn
08c56188b6 feat(library/hott/trunc): prove that n-types are (n+1)-types. 2014-11-08 19:12:54 -08:00
Leonardo de Moura
6b89080b1a feat(frontends/lean): do not allow user to define notation using tokens ! and @, closes #248 2014-10-21 16:28:36 -07:00
Leonardo de Moura
98e66586e9 feat(frontends/lean/elaborator): elaborator rejects 'Type' if the universe is explicit 2014-10-02 14:29:51 -07:00
Leonardo de Moura
baf4c01de8 feat(frontends/lean): definitions are opaque by default 2014-09-19 15:54:32 -07:00
Leonardo de Moura
38a4852e7d feat(library/hott): add 'path' namespace 2014-09-09 14:03:45 -07:00
Leonardo de Moura
364bba2129 feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 17:26:36 -07:00
Leonardo de Moura
8743394627 refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 15:04:57 -07:00
Leonardo de Moura
dbaf81e16d refactor(library): remove unnecessary 'standard' subdirectory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 18:08:09 -07:00
Renamed from library/standard/hott/trunc.lean (Browse further)