michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/hott/types
History
Floris van Doorn facd94a1b4 feat(hott): various changes 
more about pointed truncated types, including pointed sets.
also increase the priority of some basic instances that nat/num/pos_num/trunc_index have 0, 1 and + (in both libraries)
also move the notation + for sum into the namespace sum, to (sometimes) avoid overloading with add
2016-02-22 11:15:38 -08:00
..
int style(*): rename is_hprop/is_hset to is_prop/is_set 2016-02-22 11:15:38 -08:00
nat style(hott): rename instances of pType using pfoo instead of Foo 2016-02-22 11:15:38 -08:00
arrow.hlean style(hott): rename Pointed to pType 2016-02-22 11:15:38 -08:00
arrow_2.hlean feat(hott): prove HoTT book 7.5.4 and 7.5.5 2015-09-28 09:09:21 -07:00
bool.hlean style(hott): replace all other occurrences of hprop/hset 2016-02-22 11:15:38 -08:00
default.hlean refactor(hott): move cubical folder and files eq2, function and hprop_trunc from types/ to the root HoTT directory 2015-08-07 13:34:41 -07:00
eq.hlean style(*): rename is_hprop/is_hset to is_prop/is_set 2016-02-22 11:15:38 -08:00
equiv.hlean style(hott): rename Pointed to pType 2016-02-22 11:15:38 -08:00
fiber.hlean style(hott): rename Pointed to pType 2016-02-22 11:15:38 -08:00
fin.hlean style(*): rename is_hprop/is_hset to is_prop/is_set 2016-02-22 11:15:38 -08:00
lift.hlean style(hott): rename instances of pType using pfoo instead of Foo 2016-02-22 11:15:38 -08:00
list.hlean style(*): rename is_hprop/is_hset to is_prop/is_set 2016-02-22 11:15:38 -08:00
num.hlean feat(hott): port nat and int from the standard library 2015-12-09 12:36:11 -08:00
pi.hlean style(hott): rename Pointed to pType 2016-02-22 11:15:38 -08:00
pointed.hlean feat(hott): various changes 2016-02-22 11:15:38 -08:00
pointed2.hlean feat(hott): various changes 2016-02-22 11:15:38 -08:00
prod.hlean feat(hott): port finite ordinal sets from the std library, with all things related to nat.mod and to fintype still missing. 2016-02-09 09:58:10 -08:00
pullback.hlean style(*): rename is_hprop/is_hset to is_prop/is_set 2016-02-22 11:15:38 -08:00
sigma.hlean style(hott): rename Pointed to pType 2016-02-22 11:15:38 -08:00
sum.hlean style(*): rename is_hprop/is_hset to is_prop/is_set 2016-02-22 11:15:38 -08:00
trunc.hlean feat(hott): various changes 2016-02-22 11:15:38 -08:00
types.md feat(hott): various additions, especially for pointed maps/homotopies/equivalences 2016-02-22 11:15:38 -08:00
unit.hlean feat(hott): port nat and int from the standard library 2015-12-09 12:36:11 -08:00
univ.hlean style(hott): rename Pointed to pType 2016-02-22 11:15:38 -08:00
W.hlean feat(hott/function): show that a function is embedding iff it has propositional fibers 2015-11-16 21:32:09 -08:00