michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/hott/init
History
Floris van Doorn 6cdbc0f79f feat(pointed/equiv): add more theorems 
The theorems are mostly about the interaction between pointed equivalences and pointed homotopies
Some of these theorems were missing for (unpointed) equivalences, so I also added them there
2016-02-22 11:15:39 -08:00
..
bool.hlean fix(hott): notation spacing and markdown files 2015-10-02 16:26:10 -07:00
connectives.hlean feat(hott): port nat and int from the standard library 2015-12-09 12:36:11 -08:00
datatypes.hlean feat(hott/algebra): port abstract structures 2015-12-09 12:34:06 -08:00
default.hlean feat(hott): various changes 2016-02-22 11:15:38 -08:00
equiv.hlean feat(pointed/equiv): add more theorems 2016-02-22 11:15:39 -08:00
function.hlean refactor(*): normalize metaclass names 2015-12-28 10:39:15 -08:00
funext.hlean style(hott): replace all other occurrences of hprop/hset 2016-02-22 11:15:38 -08:00
hedberg.hlean style(hott): replace all other occurrences of hprop/hset 2016-02-22 11:15:38 -08:00
hit.hlean refactor(frontends/lean): use attribute_manager to simplify decl_attributes 2015-12-17 22:28:53 -08:00
init.md feat(hott): use pathovers in all the recursors of hits 2015-05-26 21:37:01 -07:00
logic.hlean feat(hott): various changes 2016-02-22 11:15:38 -08:00
nat.hlean feat(init/wf): port from standard library to HoTT library 2016-02-09 10:03:48 -08:00
num.hlean feat(hott/algebra): port abstract structures 2015-12-09 12:34:06 -08:00
path.hlean feat(init.path): update init.path to use tactics, also some additions 2016-02-22 11:15:38 -08:00
pathover.hlean feat(hit/two_quotient): give dependent eliminator for two_quotients 2015-11-22 18:29:37 -08:00
relation.hlean refactor(hott/*): remove 'Module:' lines 2015-05-23 20:52:58 +10:00
reserved_notation.hlean feat(hott): various changes 2016-02-22 11:15:38 -08:00
tactic.hlean fix(hott/init/tactic): add replace 2016-02-07 14:06:28 -08:00
trunc.hlean feat(hott): various changes 2016-02-22 11:15:38 -08:00
types.hlean feat(hott): various changes 2016-02-22 11:15:38 -08:00
ua.hlean chore(*): add me as author to files where I made nontrivial contributions 2015-11-22 14:21:26 -08:00
util.hlean style(*): rename is_hprop/is_hset to is_prop/is_set 2016-02-22 11:15:38 -08:00
wf.hlean feat(init/wf): simplify definition acc.drec 2016-02-09 10:03:48 -08:00