Jakob von Raumer
b514a978b2
fix(library/hott) changed pointed.lean to use trunc.lean correctly
2014-11-13 20:43:46 -08:00
Jakob von Raumer
8dfa78e070
feat(library/hott) almost completed portin UnivalenceImpliesFunext.v
2014-11-13 20:43:46 -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
Jakob von Raumer
3ee703f5d5
feat(library/hott) Ported part of UnivalenceImpliesFunext.v
2014-11-13 20:43:46 -08:00
Jakob von Raumer
2ed7032997
chore(library/hott) cleaned up the proof a bit
2014-11-13 20:43:46 -08:00
Jakob von Raumer
b5d564431a
feat(library/hott) port the rest of Funext_Varieties.v
2014-11-13 20:43:46 -08:00
Jakob von Raumer
6296f8e092
feat(library/hott) port a good portion of FunextVarieties.v
2014-11-13 20:43:46 -08:00
Jakob von Raumer
be8c758be1
feat(library/hott) ported Pointed.v
2014-11-13 20:43:45 -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
Jeremy Avigad
05ec76185d
fix(library/hott/fibrant): set arguments for type class resolution
2014-11-07 10:23:37 -08:00
Jakob von Raumer
754901cf64
fix(library/hott) make universe index in ua.lean variable
2014-11-06 20:02:10 -05:00
Jakob von Raumer
b8ec1a1649
chore(library/hott) cleanup
2014-11-06 19:41:08 -05:00
Jakob von Raumer
f1cc0c4bd8
chore(library/hott) add note referring to missing substitution lemma
2014-11-06 19:27:27 -05:00
Jakob von Raumer
7dbd7b31f6
Added substitution lemma for equivalence calculations
2014-11-06 19:22:57 -05:00
Jakob von Raumer
fa9cbb1f6a
chore(library/hott) adapted univalence axiom to suit notation in book and def in Coq.
2014-11-06 19:22:57 -05:00
Jakob von Raumer
d842be9c52
feat(library/hott) add univalence axiom
2014-11-06 19:22:57 -05:00
Jakob von Raumer
28d1c6c5e4
chore(library/hott) move function extensionality into new axioms folder, adjust file(s) using it
2014-11-06 19:22:57 -05:00
Jakob von Raumer
9ad75108a3
chore(library/hott) clean up file and add class inference
2014-11-06 15:57:30 -08:00
Jakob von Raumer
1f5be44f51
chore(library/hott) clean up Equiv namespace
2014-11-06 15:57:30 -08:00
Jakob von Raumer
8e1949e9aa
feat(library/hott) add calc environment for equivalences
2014-11-06 15:57:29 -08:00
Jakob von Raumer
c50db9899d
feat(library/hott) add thm: to give a section of a fibration it suffices to provide it for the image of an equivalence
2014-11-06 15:57:29 -08:00
Jakob von Raumer
09b533a965
fix(library/hott) rename IsEquiv.ap to IsEquiv.ap_closed to avoid name clashes
2014-11-05 15:14:14 -08:00
Jakob von Raumer
02abc5c2ad
chore(library/hott) fixed the copyright in equiv_precomp.lean
2014-11-05 15:14:14 -08:00
Jakob von Raumer
807224f3c1
chore(library/hott) cleaned up the proof a bit
2014-11-05 15:14:14 -08:00
Jakob von Raumer
2712b9b18f
feat(library/hott) add theorem: if f is an equivalence, so is ap f
2014-11-05 15:14:14 -08:00
Jakob von Raumer
588ad210a2
feat(library/hott) add theorem: assuming function extensionality, precomposing and postcomposing of equivalences is an equivalence
2014-11-04 18:47:34 -08:00
Jakob von Raumer
efa33c5b52
chore(library/hott) move theorem about precomposition to its own file
2014-11-04 18:47:34 -08:00
Jakob von Raumer
0ed046ed80
fix(library/hott) fix funext.lean by making funext an instance
2014-11-04 18:47:34 -08:00
Leonardo de Moura
795f664964
fix(library/hott/funext): compilation error
2014-11-04 06:53:21 -08:00
Jakob von Raumer
261f8a014a
feat(library/hott) use class inference for IsEquiv
2014-11-04 06:49:42 -08:00
Jakob von Raumer
479eabb416
feat(library/hott) add: if precompositions with f are equivalences, then f is
2014-11-04 06:49:42 -08:00
Leonardo de Moura
591e566472
feat(frontends/lean): try to inject symmetry (if needed) in calc proofs, add calc_symm command for configuring the symmetry theorem for a given operator
...
This is part of #268
2014-10-30 23:24:09 -07:00
Leonardo de Moura
ea739100b3
fix(library/unifier): broken optimization in the unifier
...
See new comments and tests for details.
2014-10-28 16:09:41 -07:00
Jakob von Raumer
b575c972bd
feat(library/hott) add the proof that the inverse of an equivalence is an equivalence
...
This is done by changing the order of theorems and using the adjointification.
2014-10-25 14:20:47 -07:00
Jakob von Raumer
e7aa5f65e7
fix(library/hott) close gaps and clean up adjointification proof
2014-10-25 14:16:24 -07:00
Jakob von Raumer
16a0e970f7
feat(library/hott) add adjointification proof up to two gaps
2014-10-25 14:16:24 -07:00
Leonardo de Moura
cdcde661ef
feat(library/definitional/induction_on): automatically add 'induction_on'
2014-10-25 13:37:04 -07:00
Leonardo de Moura
a7a06ab0f8
feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes
2014-10-25 13:08:59 -07:00
Leonardo de Moura
7c016191d2
chore(library/hott): add Jakob to list of authors
2014-10-22 22:28:21 -07:00
Jakob von Raumer
f182299459
fix(library/hott) fix funext.lean to match equivalence notation
2014-10-22 22:28:21 -07:00
Jakob von Raumer
abd5c574ad
fix(library/hott) : convert to new path notations
...
Convert definitions and proofs to new notations for inverse and cocatenation. Adapt to now right associative of concatenation.
2014-10-22 22:28:14 -07:00
Jakob von Raumer
a169f791df
feat(library/hott): add adjointification and closure properties for equivalences
...
Port features from the Coq Hott library
2014-10-22 22:22:08 -07: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
dea3357d7c
refactor(library/hott/path): use HoTT book notation for path concatenation and inverse
2014-10-21 16:11:55 -07:00
Leonardo de Moura
6c7e23ecaa
refactor(library): use 'reserve' notation in the standard library
2014-10-21 15:39:47 -07:00
Leonardo de Moura
45df5cffd8
refactor(library/hott): remove unnecessary generalizations
2014-10-21 09:11:22 -07:00
Leonardo de Moura
744cee8dd8
feat(frontends/lean): force 'classes' to be declared before instances are declared, closes #228
2014-10-07 18:02:15 -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
Floris van Doorn
5396e422d2
feat(library): add constructions of categories, some changes in eq, sigma and path
...
in eq, add theorem for proof irrelevance and congruence for binary functions
in sigma, add some support for triplets
in path, comment out two unneccesary definitions
in category, add Cat, slice, coslice, product and arrow categories, also add fully bundled approach
2014-09-26 19:45:23 -04:00
Leonardo de Moura
4e2377ddfc
refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-19 15:54:32 -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
48dbd13eef
feat(frontends/lean): allow transient classes/instances, i.e.,
...
classes/instances that are not saved in .olean files
2014-09-19 15:54:32 -07:00
Jeremy Avigad
74cb289d48
refactor(library): rename algebra directory to struc, move categories.lean to algebra
2014-09-16 13:13:01 -07:00
Leonardo de Moura
bd1bc336fb
feat(library/coercion): add simple trick for defining coercions to function-class in a convenient way, closes #31
2014-09-09 14:36:36 -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
e51c4ad2e9
feat(frontends/lean): rename 'using' command to 'open'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 16:00:38 -07:00
Leonardo de Moura
f891485a26
refactor(library): use '[protected]' modifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 15:13:03 -07:00
Jeremy Avigad
1864fc2f6c
refactor(library): move more notation to general_notation
2014-08-28 17:37:32 -07:00
Jeremy Avigad
5eedca08ea
refactor(library): set up and document standard/classical/hott imports
2014-08-25 22:57:55 -07:00
Jeremy Avigad
413517b86d
fix(library): correct markdown directories, revise defaults for logic and data
2014-08-25 22:57:55 -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
Leonardo de Moura
670bfe24f5
chore(build): remove hott library directory, and move hott tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 13:30:56 -07:00
Jeremy Avigad
7d7655c3f1
refactor(library/standard): integrate hott with standard library
2014-08-15 12:58:58 -07:00
Jeremy Avigad
218c9dfc81
feat(library/hott): begin porting Coq HoTT
2014-08-15 12:58:58 -07:00
Leonardo de Moura
1a67e69678
feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 16:59:08 -07:00
Soonho Kong
8d4c7b4b2c
fix(library/hott/Makefile): specify LEAN_OPTIONS "--hott"
2014-08-07 09:59:15 -07:00
Leonardo de Moura
d9ee994281
feat(library/hott): copy basic files to hott library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 19:13:04 -07:00
Leonardo de Moura
a450ad5a95
feat(frontends/lean/inductive_cmd): improve notation for declaring 'empty' inductive datatypes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-25 11:24:01 -07:00
Leonardo de Moura
ae2ce356b4
feat(library/hott): use new 'parameters' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-17 20:49:53 +01:00
Leonardo de Moura
58da037410
feat(library/hott): add more definitions and theorems from the HoTT book
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-17 20:24:00 +01:00
Leonardo de Moura
dfe48e6abe
feat(library/hott): add more hott definitions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 22:42:38 +01:00
Leonardo de Moura
f7317a7139
feat(build): compile HoTT library when building
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 21:56:36 +01:00
Leonardo de Moura
359bfe93d5
feat(library/hott): add basic HoTT definitions and theorems
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 21:46:33 +01:00
Leonardo de Moura
79d32b768d
feat(shell): add '--hott' command line option
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 15:50:27 -07:00