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

	Commit message (Collapse)	Author	Files	Lines
2018-06-27	Library organization and formatting	Josh Chen	1	-1/+0

2018-06-17	Decided on a new proper scheme for type rules using the idea of implicit ↵	Josh Chen	1	-23/+20
	well-formed contexts and guaranteed conclusion well-formedness. Product type rules now follow this scheme.
2018-06-15	projections	Josh Chen	1	-0/+3

2018-06-12	Type rules now have \"all\" premises explicitly stated, matching the ↵	Josh Chen	1	-8/+17
	formulation in the HoTT book.
2018-06-09	Reorganize code	Josh Chen	1	-9/+44

2018-06-07	Symmetry and transitivity done.	Josh Chen	1	-0/+1

2018-06-07	Nondependent function arrow should bind tighter than the Pi former, but ↵	Josh Chen	1	-5/+5
	looser than equality.
2018-06-05	Code formatting	Josh Chen	1	-0/+2

2018-06-05	Proved that the inductor on Sum has the correct type.	Josh Chen	1	-27/+50

2018-06-05	Dependent sum done, I think.	Josh Chen	1	-0/+2

2018-06-04	Prod_comp should have a type constraint. This also fixes a false proof for ↵	Josh Chen	1	-14/+38
	the dependent sum projection functions.
2018-06-01	Should be final version of Prod. Theorems proving stuff about currying. ↵	Josh Chen	1	-19/+50
	Rules for Sum, going to change them to use object-level arguments more.
2018-05-30	New type rules for dependent product and sum.	Josh Chen	1	-9/+4

2018-05-30	Fixed dependent product rules, hopefully final now.	Josh Chen	1	-72/+27

2018-05-29	More rigorous rules for Product type. Propositions and proofs all working, ↵	Josh Chen	1	-12/+55
	but have to think about maybe relaxing the computation rule, or else automating the currying of dependent functions.
2018-05-28	Dependent product rules done and proofs of typing properties so far work. ↵	Josh Chen	1	-37/+56
	Starting on dependent sums.
2018-05-23	pre-system upgrade commit	Josh Chen	1	-0/+68