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
|
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
|
efa33c5b52
|
chore(library/hott) move theorem about precomposition to its own file
|
2014-11-04 18:47:34 -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
|
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
|
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
|
6c7e23ecaa
|
refactor(library): use 'reserve' notation in the standard library
|
2014-10-21 15:39:47 -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
|
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
|
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 |
|
Jeremy Avigad
|
1864fc2f6c
|
refactor(library): move more notation to general_notation
|
2014-08-28 17:37:32 -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 |
|