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

	Commit message (Collapse)	Author	Age	Files	Lines
...
\| * \|	Update README.md	Josh Chen	2018-09-11	1	-3/+7
\| \| \|
* \| \|	Some final touchups before release 0.1 for the MS thesis	Josh Chen	2018-09-12	6	-7/+9
\|/ /
* \|	Add the univalence axiom	Josh Chen	2018-09-11	3	-4/+71
\| \|
* \|	Running into trouble with the polymorphic identity function	Josh Chen	2018-09-11	3	-17/+80
\| \|
* \|	Implementing univalence	Josh Chen	2018-09-11	3	-0/+81
\| \|
* \|	Go back to higher-order application notation	Josh Chen	2018-09-11	11	-139/+138
\| \|
* \|	Merge branch 'master' of github.com:jaycech3n/Isabelle-HoTT	Josh Chen	2018-08-30	1	-1/+1
\|\ \
\| * \|	Update README.md	Josh Chen	2018-08-30	1	-1/+1
\| \| \|
* \| \|	Some higher groupoid structure proofs	Josh Chen	2018-08-30	2	-2/+56
\|/ /
* \|	Should write the correct rule for Ord_leq_min. Another exercise.	Josh Chen	2018-08-30	2	-2/+18
\| \|
* \|	Add leq relation to meta-ordinals, it helps with proofs	Josh Chen	2018-08-30	2	-7/+12
\| \|
* \|	Rename LICENSE.md to LICENSE	Josh Chen	2018-08-21	1	-0/+0
\| \|
* \|	Create LICENSE.md	Josh Chen	2018-08-21	1	-0/+165
\|/
*	Forgot to add the theories for Empty and Unit	Josh Chen	2018-08-18	2	-0/+63
\|
*	Distinguish the typing judgment	Josh Chen	2018-08-18	1	-2/+1
\|
*	Move Empty and Unit types to their own theories	Josh Chen	2018-08-18	3	-32/+2
\|
*	.gitignore	Josh Chen	2018-08-18	1	-0/+7
\|
*	Update Test.thy	Josh Chen	2018-08-18	1	-12/+12
\|
*	Reorganize methods	Josh Chen	2018-08-18	13	-94/+98
\|
*	Regrouping type rules	Josh Chen	2018-08-18	16	-108/+102
\|
*	HoTT_Test.thy should go in test/	Josh Chen	2018-08-18	1	-1/+1
\|
*	Comments on subgoal test theory	Josh Chen	2018-08-18	1	-23/+29
\|
*	Rename	Josh Chen	2018-08-18	1	-1/+2
\|
*	.gitignore	Josh Chen	2018-08-18	1	-0/+1
\|
*	Test theories	Josh Chen	2018-08-18	2	-9/+64
\|
*	Misc formatting	Josh Chen	2018-08-18	3	-3/+2
\|
*	Output formatting	Josh Chen	2018-08-18	1	-1/+1
\|
*	Ignore more files	Josh Chen	2018-08-18	1	-0/+3
\|
*	Update license	Josh Chen	2018-08-18	1	-1/+1
\|
*	Update test file	Josh Chen	2018-08-18	1	-113/+19
\|
*	Fixed mistake in Equal_elim and proof of rpathcomp_comp	Josh Chen	2018-08-18	2	-26/+26
\|
*	Update README.md	Josh Chen	2018-08-17	1	-9/+5
\|
*	Merge branch 'master' of github.com:jaycech3n/Isabelle-HoTT	Josh Chen	2018-08-17	1	-2/+3
\|\
\| *	Update README.md	Josh Chen	2018-08-17	1	-2/+3
\| \|
* \|	Fix silly mistakes in Coprod.thy	Josh Chen	2018-08-17	1	-10/+10
\| \|
* \|	Cleanups	Josh Chen	2018-08-17	1	-4/+4
\|/
*	Merge branch 'master' of github.com:jaycech3n/HoTT	Josh Chen	2018-08-17	1	-0/+22
\|\
\| *	Update README.md	Josh Chen	2018-08-17	1	-1/+6
\| \|
\| *	Add contact	Josh Chen	2018-08-17	1	-1/+1
\| \|
\| *	Update README.md	Josh Chen	2018-08-17	1	-1/+1
\| \|
\| *	Update README.md	Josh Chen	2018-08-17	1	-1/+2
\| \|
\| *	Create README.md	Josh Chen	2018-08-17	1	-0/+16
\| \|
* \|	Properties of function composition	Josh Chen	2018-08-17	1	-24/+5
\|/
*	Remove test commit folder	Josh Chen	2018-08-17	1	-1/+0
\|
*	Partway through updating proofs after the change of the function composition ↵	Josh Chen	2018-08-17	1	-46/+11
\| \| \| \|	definition
*	Axiomatizations should be definitions	Josh Chen	2018-08-17	1	-4/+2
\|
*	Make function composition a definition instead of an axiomatization (should ↵	Josh Chen	2018-08-17	1	-9/+1
\| \| \| \|	not need to worry about preconditions)
*	Change unnecessary axiomatization to a definition	Josh Chen	2018-08-17	1	-2/+2
\|
*	Testing with the new theory	Josh Chen	2018-08-17	1	-29/+25
\|
*	second test	Josh Chen	2018-08-16	1	-0/+1
\|