Isabelle-HoTT - trying to make Isabelle/HoTT work with Isabelle 2021-1

	Commit message (Collapse)	Author	Age	Files	Lines
*	prune import lists	Josh Chen	2019-03-08	1	-151/+8
\|
*	Make functions object-level	Josh Chen	2019-03-06	1	-21/+15
\|
*	Move definition of transport to Type_Families.thy, and change it to use ↵	Josh Chen	2019-03-03	1	-79/+32
\| \| \| \|	meta-functions for type families again. This together with the previous commit simplifies the definitions and proofs for idtoeqv greatly.
*	Defined idtoeqv. Should next state univalence in terms of an explicit ↵	Josh Chen	2019-03-03	1	-13/+50
\| \| \| \|	inverse equivalence.
*	finished proof of transport_biinv	Josh Chen	2019-03-01	1	-16/+21
\|
*	Proving transport is bi-invertible is harder than expected	Josh Chen	2019-03-01	1	-83/+87
\|
*	transport and homotopy	Josh Chen	2019-03-01	1	-21/+80
\|
*	Working on univalence	Josh Chen	2019-03-01	1	-46/+115
\|
*	Renaming	Josh Chen	2018-09-19	1	-1/+1
\|
*	Theories fully reorganized. Well-formedness rules removed. New methods etc.	Josh Chen	2018-09-18	1	-141/+53
\|
*	Reorganized HoTT_Base, updated theories	Josh Chen	2018-09-16	1	-19/+18
\|
*	Final commit before first release	Josh Chen	2018-09-12	1	-1/+1
\|
*	Some final touchups before release 0.1 for the MS thesis	Josh Chen	2018-09-12	1	-1/+3
\|
*	Add the univalence axiom	Josh Chen	2018-09-11	1	-4/+64
\|
*	Running into trouble with the polymorphic identity function	Josh Chen	2018-09-11	1	-11/+55
\|
*	Implementing univalence	Josh Chen	2018-09-11	1	-0/+71