aboutsummaryrefslogtreecommitdiff
path: root/Univalence.thy (unfollow)
Commit message (Collapse)AuthorFilesLines
2019-03-03Move definition of transport to Type_Families.thy, and change it to use ↵Josh Chen1-79/+32
meta-functions for type families again. This together with the previous commit simplifies the definitions and proofs for idtoeqv greatly.
2019-03-03Defined idtoeqv. Should next state univalence in terms of an explicit ↵Josh Chen1-13/+50
inverse equivalence.
2019-03-01finished proof of transport_biinvJosh Chen1-16/+21
2019-03-01Proving transport is bi-invertible is harder than expectedJosh Chen1-83/+87
2019-03-01transport and homotopyJosh Chen1-21/+80
2019-03-01Working on univalenceJosh Chen1-46/+115
2018-09-19RenamingJosh Chen1-1/+1
2018-09-18Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen1-141/+53
2018-09-12Final commit before first releaseJosh Chen1-1/+1
2018-09-12Some final touchups before release 0.1 for the MS thesisJosh Chen1-1/+3
2018-09-11Add the univalence axiomJosh Chen1-4/+64
2018-09-11Running into trouble with the polymorphic identity functionJosh Chen1-11/+55
2018-09-11Implementing univalenceJosh Chen1-0/+71
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-27 07:13:21 +0000