aboutsummaryrefslogtreecommitdiff
path: root/Univalence.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* prune import listsJosh Chen2019-03-081-151/+8
* Make functions object-levelJosh Chen2019-03-061-21/+15
* Move definition of transport to Type_Families.thy, and change it to use meta-...Josh Chen2019-03-031-79/+32
* Defined idtoeqv. Should next state univalence in terms of an explicit inverse...Josh Chen2019-03-031-13/+50
* 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 2024-07-01 17:08:31 +0000