Jakob von Raumer
|
7c1b75c818
|
feat(library/hott): add proof that the type of nat trafos is a set
The characteriszation of nat trafo by sigma types up to equivalence is still to be done (two unsuccessful proof attempts included)
|
2014-12-05 22:21:36 -08:00 |
|
Jakob von Raumer
|
cc2de8a8d9
|
feat(library/hott): complete proof that object types of proper hott categories are one truncated
|
2014-12-05 22:21:31 -08:00 |
|
Jakob von Raumer
|
aad4592cad
|
feat(library/hott): complete theorems about truncatedness of isomorphism sets
|
2014-12-05 22:21:26 -08:00 |
|
Jakob von Raumer
|
5923392395
|
chore(library/hott): make precategory use the isomorphic structure
|
2014-12-05 22:21:21 -08:00 |
|
Jakob von Raumer
|
63afac301c
|
chore(library/hott): turn isomorphic into structure
|
2014-12-05 22:21:16 -08:00 |
|
Jakob von Raumer
|
dbce41114a
|
feat(library/hott): add definition of category
|
2014-12-05 22:21:12 -08:00 |
|
Jakob von Raumer
|
39ba9429f5
|
chore(library/hott): make constructions.lean compile, still lots of work to do
|
2014-12-05 22:21:06 -08:00 |
|
Jakob von Raumer
|
91862926e3
|
chore(library/hott): change precategory to structure, fix morphism.lean
|
2014-12-05 22:20:57 -08:00 |
|
Jakob von Raumer
|
b37a77d25e
|
chore(library/hott): move precategory definition to its own folder
|
2014-12-05 22:20:40 -08:00 |
|
Jakob von Raumer
|
9631c6b1a1
|
feat(library/hott): add iso_of_path lemma for precategories
|
2014-12-05 22:20:33 -08:00 |
|
Jakob von Raumer
|
a1b468d104
|
feat(library/hott): port a part of algebra/category/constructions.lean, slice category still to do
|
2014-12-05 22:20:25 -08:00 |
|
Jakob von Raumer
|
67f71ee376
|
feat(library/hott): finish porting of natural_transformation.lean
|
2014-12-05 22:20:18 -08:00 |
|
Jakob von Raumer
|
ae618c20fb
|
fix(library/hott): finish associativity proof
|
2014-12-05 22:20:11 -08:00 |
|
Jakob von Raumer
|
d8e2206bbc
|
feat(library/hott): try to replace the proof irrelevance
|
2014-12-05 22:19:50 -08:00 |
|
Jakob von Raumer
|
5fe8ee606f
|
feat(library/hott): port Floris' category implementation
|
2014-12-05 22:19:26 -08:00 |
|
Floris van Doorn
|
e52157a8ea
|
feat(hott/types): start characterization of pi-types and W-types
|
2014-12-03 20:29:16 -08:00 |
|
Floris van Doorn
|
2913035a61
|
style(hott/types): some style fixes in prod and sigma
|
2014-12-03 20:29:16 -08:00 |
|
Floris van Doorn
|
ff5e3d4403
|
style(hott/path): indent within namespace, add variables
|
2014-12-03 20:29:16 -08:00 |
|
Floris van Doorn
|
4b799a9da4
|
fix(hott/trunc): add explicit coercion so that the notation works if nat is not opened
|
2014-12-03 20:29:16 -08:00 |
|
Leonardo de Moura
|
06f436840f
|
fix(library/unifier): postpone class-instance constraints whose type could not be inferred
|
2014-12-01 22:27:23 -08:00 |
|
Leonardo de Moura
|
697d4359e3
|
refactor(library): add 'init' folder
|
2014-11-30 20:34:12 -08:00 |
|
Leonardo de Moura
|
2281fb30c8
|
refactor(library): use "symbolic" precedences in the standard library
|
2014-11-29 19:08:37 -08:00 |
|
Leonardo de Moura
|
bed9467315
|
chore(library/hott/trunc): remove set_option
|
2014-11-29 08:55:47 -08:00 |
|
Jakob von Raumer
|
7c81044a99
|
chore(library/hott) change is_pointed to structure
|
2014-11-28 22:50:43 -08:00 |
|
Jakob von Raumer
|
0417c21bbb
|
chore(library/hott) change naming in equiv_precomp
|
2014-11-28 22:50:43 -08:00 |
|
Jakob von Raumer
|
4587e46c67
|
chore(library/hott) change naming to leo's naming proposal
|
2014-11-28 22:50:43 -08:00 |
|
Jakob von Raumer
|
7374149758
|
chore(library/hott) change equiv.lean to use structures and more typeclass inference
|
2014-11-28 22:50:43 -08:00 |
|
Leonardo de Moura
|
df51ba8b7c
|
feat(library/definitional/projection): use strict implicit inference, closes #344
|
2014-11-25 18:04:06 -08:00 |
|
Jakob von Raumer
|
53d66c91fc
|
chore(library/hott) made ua_implies_funext a class instance
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
757cdcb130
|
feat(library/hott) funext from ua now with arbitrary universe levels for funext!
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
228205634d
|
chore(library/hott) make funext more general
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
12429c93c8
|
fix(library/hott) fix equiv_precomp, doesn't look nice now
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
1f6b6ff8e6
|
chore(library/hott) adjust funext_from_ua.lea to typeclass axioms
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
2d9621892b
|
fix(library/hott) fill both gaps (I don't know why it works that way), change name from funext.apply to funext.ap, since apply seems to be a tactic name?
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
fd47a162de
|
chore(library/hott) adapted theories to typeclass axioms
|
2014-11-23 17:43:55 -08:00 |
|
Jakob von Raumer
|
d8d2ea998d
|
feat(library/hott) change axioms to Leo's axioms-as-typeclass proposal
|
2014-11-23 17:43:55 -08:00 |
|
Floris van Doorn
|
3523a70b4c
|
fix(hott/path): make recursion-like definitions reducible
|
2014-11-22 17:44:13 -08:00 |
|
Floris van Doorn
|
e97b0b4e8e
|
feat(hott/types): port more of the sigma library from Coq
prove theorems about interaction of sigma types and n-types, including the fact that sigmas preserve n-types
|
2014-11-22 17:44:12 -08:00 |
|
Floris van Doorn
|
24e35a9f2c
|
fix(hott/trunc): comment out sorry
|
2014-11-22 17:44:12 -08:00 |
|
Floris van Doorn
|
bc807212ac
|
feat(hott/path): add notation for higher and dependent transports
|
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
|
19d0afe160
|
feat(library/hott) completed the funext_from_ua proof with a somewhat restricted generality on universe levels
|
2014-11-21 10:46:16 -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
|
59fbe8b53e
|
chore(library/hott) fix universe issue. note: this should be fixed when contr is not bound to universe level 1 anymore
|
2014-11-17 18:39:02 -08:00 |
|
Jakob von Raumer
|
992aad9661
|
feat(library/hott) postcomposition from ua lemma is done up to the last gap
|
2014-11-17 18:39:02 -08:00 |
|
Jakob von Raumer
|
e740fbe8c4
|
chore(library/hott) remove hott.axoims.ua from imports of funext_from_ua.lean
|
2014-11-13 20:43:46 -08:00 |
|
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 |
|