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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Reorganize methods	Josh Chen	2018-08-18	1	-4/+4
\|
*	Regrouping type rules	Josh Chen	2018-08-18	1	-5/+16
\|
*	Prod.thy now has the correct definitional equality structure rule. ↵	Josh Chen	2018-08-16	1	-1/+1
\| \| \| \|	Definition of function composition and properties.
*	Partway through changing function application syntax style.	Josh Chen	2018-08-06	1	-1/+3
\|
*	Pre-universe implementation commit	Josh Chen	2018-07-09	1	-1/+1
\|
*	Library snapshot. Methods written, everything nicely organized.	Josh Chen	2018-07-07	1	-1/+0
\|
*	Refactor HoTT_Methods.thy, proved more stuff with new methods.	Josh Chen	2018-07-03	1	-4/+13
\|
*	Library organization and formatting	Josh Chen	2018-06-27	1	-6/+7
\|
*	Type rules now have \"all\" premises explicitly stated, matching the ↵	Josh Chen	2018-06-12	1	-0/+15
\| \| \| \|	formulation in the HoTT book.
*	Reorganize code	Josh Chen	2018-06-09	1	-248/+0
\|
*	Symmetry and transitivity done.	Josh Chen	2018-06-07	1	-3/+26
\|
*	But also looser than Pair	Josh Chen	2018-06-07	1	-1/+1
\|
*	Nondependent function arrow should bind tighter than the Pi former, but ↵	Josh Chen	2018-06-07	1	-21/+43
\| \| \| \|	looser than equality.
*	Code formatting	Josh Chen	2018-06-05	1	-41/+54
\|
*	Proved that the inductor on Sum has the correct type.	Josh Chen	2018-06-05	1	-17/+31
\|
*	Dependent sum done, I think.	Josh Chen	2018-06-05	1	-28/+40
\|
*	Prod_comp should have a type constraint. This also fixes a false proof for ↵	Josh Chen	2018-06-04	1	-22/+31
\| \| \| \|	the dependent sum projection functions.
*	Should be final version of Prod. Theorems proving stuff about currying. ↵	Josh Chen	2018-06-01	1	-22/+15
\| \| \| \|	Rules for Sum, going to change them to use object-level arguments more.
*	New type rules for dependent product and sum.	Josh Chen	2018-05-30	1	-12/+29
\|
*	Fixed dependent product rules, hopefully final now.	Josh Chen	2018-05-30	1	-3/+2
\|
*	More rigorous rules for Product type. Propositions and proofs all working, ↵	Josh Chen	2018-05-29	1	-12/+17
\| \| \| \|	but have to think about maybe relaxing the computation rule, or else automating the currying of dependent functions.
*	Dependent product rules done and proofs of typing properties so far work. ↵	Josh Chen	2018-05-28	1	-27/+54
\| \| \| \|	Starting on dependent sums.
*	pre-system upgrade commit	Josh Chen	2018-05-23	1	-35/+40
\|
*	Added precedences. Need to figure out how to organize metatypes.	Josh Chen	2018-05-14	1	-13/+12
\|
*	Decided to go with no explicit type declarations in object-lambda ↵	Josh Chen	2018-05-10	1	-14/+25
\| \| \| \|	expressions. Everything in the proof stuff is working at the moment.
*	Init	Josh Chen	2018-05-03	1	-0/+99