Commit graph

26 commits

Author SHA1 Message Date
Floris van Doorn
06528c4791 refactor(types): create cubical subfolder, update markdown files 2015-06-04 20:14:13 -04:00
Floris van Doorn
33e948d9d1 feat(hit/sphere): Prove that maps from S^n to an (n-1)-type are constant 2015-06-04 20:14:13 -04:00
Floris van Doorn
876aa20ad6 feat(hott): Port remainder of §6.3 and §7.2 from the HoTT book
Also prove a theorem similar to Lemma 7.3.1

There are still some sorry's in hit.suspension
2015-06-04 20:14:12 -04:00
Floris van Doorn
883b4fedb9 feat(hott): start with proof to characterize (is_trunc n A) using iterated loop spaces 2015-06-04 20:14:12 -04:00
Floris van Doorn
c64d73aae4 feat(types.nat): prove that inequalities on nat are mere propositions
Also some small changes in various other locations
2015-05-26 21:37:01 -07:00
Jeremy Avigad
33214f0895 refactor(hott/*): remove 'Module:' lines 2015-05-23 20:52:58 +10:00
Leonardo de Moura
e1c2340db2 fix(frontends/lean): consistent behavior for protected declarations
see https://github.com/leanprover/lean/issues/604#issuecomment-103265608

closes #609
2015-05-18 22:35:18 -07:00
Floris van Doorn
6ca9635d53 feat(hit.trunc): replace sorry by proof 2015-05-18 15:59:55 -07:00
Floris van Doorn
1597337c72 feat(path): add unfold-c attribute to definitions 2015-05-18 15:59:55 -07:00
Floris van Doorn
9893de6194 feat(hit/circle): prove partly that the fundamental group of the circle is int
Also add markdown files for nat and int
2015-05-07 16:39:04 -07:00
Floris van Doorn
90f1a691fd feat(hott): change notation of transport to correspond with standard library 2015-05-07 16:39:03 -07:00
Leonardo de Moura
9ba8b284a1 fix(library/tactic/apply_tactic): add eapply, and fix issue #361 2015-05-01 15:08:00 -07:00
Leonardo de Moura
3912bc24c8 feat(frontends/lean): nicer syntax for 'intros' 'reverts' and 'clears' 2015-04-30 11:00:39 -07:00
Floris van Doorn
297d50378d feat(hott): add definitions using truncations and theorems about them
define embedding, (split) surjection, retraction, existential quantifier, 'or' connective
also add a whole bunch of theorems about these definitions

still has two sorry's which can be solved after #564 is closed
2015-04-29 10:04:07 -07:00
Floris van Doorn
15c2ee289f feat(hott): make some fibrations in path.hlean implicit, and a bit of renaming in init 2015-04-29 10:04:07 -07:00
Floris van Doorn
40086d0084 feat(hott): standardize the naming of definitions proving equality of elements of a structure
examples:
foo_eq : Pi {A B : foo}, _ -> A = B
foo_mk_eq : Pi _, foo.mk _ = foo.mk _ (if constructor is called "bar", then this becomes "bar_eq")
foo_eq_equiv : Pi {A B : foo}, (A = B) ≃ _

also changed priority of some instances of is_trunc
2015-04-29 10:04:06 -07:00
Floris van Doorn
e769fdd9dc feat(hott): make some arguments in init.path implicit and rename apD to apd 2015-04-29 10:04:06 -07:00
Leonardo de Moura
75621df52b feat(frontends/lean): uniform notation for lists in tactics
closes #504
2015-03-27 17:54:48 -07:00
Floris van Doorn
3d7656078d feat(hott/types): prove that 'is_equiv f' is an hprop 2015-03-04 00:22:51 -05:00
Floris van Doorn
1559e0e58c feat(hott): some more renaming in category library 2015-02-28 01:16:23 -05:00
Floris van Doorn
f513538631 feat(hott): more cleanup of HoTT library
remove funext class,
remove a couple of sorry's,
add characterization of equality in trunctypes,
use Jeremy's format for headers everywhere in the HoTT library,
continue working on Yoneda embedding
2015-02-26 13:19:54 -05:00
Floris van Doorn
9201bd7ca6 feat (hott/init): move nat.of_num to init.num and make it reducible outside namespace nat
This is so that init.trunc can already use nat.of_num.
Also make nat.of_num reducible in the standard library
Also make gt and ge abbreviations
2015-02-26 12:28:57 -05:00
Leonardo de Moura
c04c610b7b feat(frontends/lean): add 'assert H : A, ...' as notation for 'have H [visible] : A, ...' 2015-02-25 14:30:42 -08:00
Leonardo de Moura
1cd44e894b feat(library/tactic/class_instance_synth): conservative class-instance resolution: expand only definitions marked as reducible
closes #442
2015-02-24 16:12:35 -08:00
Leonardo de Moura
3846f5a4e7 refactor(hott): use nested begin-end blocks, use cases tactic 2015-02-24 13:27:57 -08:00
Floris van Doorn
61901cff81 feat(hott): rename definition and cleanup in HoTT library
also add more definitions in types.pi, types.path, algebra.precategory

the (pre)category library still needs cleanup
authors of this commit: @avigad, @javra, @fpvandoorn
2015-02-20 21:40:42 -05:00