Floris van Doorn
ae1b2e854c
feat(hott): various minor changes
2016-07-09 10:20:21 -07:00
Floris van Doorn
8db4676c46
feat(hott): various changes and additions in the HoTT library
...
Add more theorems about mapping cylinders, fibers, truncated 2-quotient, truncated univalence, pre/postcomposition with an iso in a precategory.
renamings: equiv.refl -> equiv.rfl and equiv_eq <-> equiv_eq'
2016-05-06 14:27:27 -07:00
Floris van Doorn
dc37ec954d
refactor(hott): rename apdo to apd
2016-04-11 09:45:59 -07:00
Floris van Doorn
5cacebcf86
feat(hott): replace assert by have and merge namespace equiv.ops into equiv
...
The coercion A ≃ B -> (A -> B) is now in namespace equiv. The notation ⁻¹ for symmetry of equivalences is not supported anymore. Use ⁻¹ᵉ
2016-03-03 10:13:21 -08:00
Floris van Doorn
e5d5ef9d55
feat(hott/library): various changes and additions.
...
Most notably:
Give le.refl the attribute [refl]. This simplifies tactic proofs in various places.
Redefine the order of trunc_index, and instantiate it as weak order.
Add more about pointed equivalences.
2016-03-03 10:13:20 -08:00
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
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
115dedbd1c
fix(hott): notation spacing and markdown files
2015-10-02 16:26:10 -07:00
Floris van Doorn
3c4c722afd
feat(hott): port more from chapters 4 and 6 of the book
2015-09-28 09:09:21 -07:00
Floris van Doorn
c24fd508b6
feat(hott/types): add more about pathovers in type constructors, prove that double negation elimination doesn't hold universally
2015-09-01 15:17:46 -07:00
Floris van Doorn
cfddfdfa84
feat(hott/types): add characterization of lift, prove that Type.{u} is not an hset
2015-09-01 15:17:46 -07:00
