aboutsummaryrefslogtreecommitdiff
path: root/Univalence.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Defined idtoeqv. Should next state univalence in terms of an explicit ↵Josh Chen2019-03-031-13/+50
| | | | inverse equivalence.
* finished proof of transport_biinvJosh Chen2019-03-011-16/+21
|
* Proving transport is bi-invertible is harder than expectedJosh Chen2019-03-011-83/+87
|
* transport and homotopyJosh Chen2019-03-011-21/+80
|
* Working on univalenceJosh Chen2019-03-011-46/+115
|
* RenamingJosh Chen2018-09-191-1/+1
|
* Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen2018-09-181-141/+53
|
* Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-161-19/+18
|
* Final commit before first releaseJosh Chen2018-09-121-1/+1
|
* Some final touchups before release 0.1 for the MS thesisJosh Chen2018-09-121-1/+3
|
* Add the univalence axiomJosh Chen2018-09-111-4/+64
|
* Running into trouble with the polymorphic identity functionJosh Chen2018-09-111-11/+55
|
* Implementing univalenceJosh Chen2018-09-111-0/+71
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-02 20:43:13 +0000