Floris van Doorn
|
bac6d99cc7
|
style(hott): rename Pointed to pType
also rename sigma_equiv_sigma_id to sigma_equiv_sigma_right and similarly for pi
|
2016-02-22 11:15:38 -08:00 |
|
Floris van Doorn
|
4e2cc66061
|
style(*): rename is_hprop/is_hset to is_prop/is_set
|
2016-02-22 11:15:38 -08:00 |
|
Floris van Doorn
|
816237315c
|
feat(hott): various additions, especially for pointed maps/homotopies/equivalences
|
2016-02-22 11:15:38 -08:00 |
|
Sebastian Ullrich
|
2185ee7e95
|
feat(library/tactic): make let tactic transparent, introduce new opaque note tactic
The new let tactic is semantically equivalent to let terms, while `note`
preserves its old opaque behavior.
|
2015-12-14 10:14:02 -08:00 |
|
Floris van Doorn
|
2325d23f68
|
feat(hott): port nat and int from the standard library
|
2015-12-09 12:36:11 -08:00 |
|
Floris van Doorn
|
47be1e3a15
|
feat(types/pointed): change definition of loop space
|
2015-11-16 21:32:09 -08:00 |
|
Floris van Doorn
|
18ec5f8b85
|
feat(categories): prove introduction rule for equivalences
|
2015-11-08 14:04:58 -08:00 |
|
Ulrik Buchholtz
|
384a366e0f
|
refactor(hott): move homotopy hits to new homotopy folder
|
2015-09-24 22:52:33 -04:00 |
|