30 Commits (feature/web)

 

All Branches   

Search

Author	SHA1	Message	Date
Amélia Liao	2ff359d1e9	initial work on web ughr	3 years ago
Amélia Liao	de5e1e33b8	Fix recursive local lets	3 years ago
Amélia Liao	f3dc148bb5	misc fixes + proof that T² = S¹×S¹	3 years ago
Amélia Liao	9365797b0c	put all the disgusting magic variables in one place	3 years ago
Amélia Liao	7bcbc28419	fix composition for the universe	3 years ago
Amélia Liao	f695f9bcc2	more pain and suffering	3 years ago
Amélia Liao	fb87b16429	some initial work on HITs	3 years ago
Amélia Liao	15cfd9abf1	some fixes to inductive types	3 years ago
Amélia Liao	b42384125d	Implement proper inductive types	3 years ago
Amélia Liao	97613613be	Add where clauses	3 years ago
Amélia Liao	7d3ed1ca30	Use glued evaluation to get shorter normal forms	3 years ago
Amélia Liao	28e1867f76	Fix composition for pairs	3 years ago
Amélia Liao	afa944066d	include proof of strong funext	3 years ago
Amélia Liao	2fdd17b847	Report unsolved metas & composition for the universe	3 years ago
Amélia Liao	f7d8fa0ee8	Composition for the universe	3 years ago
Amélia Liao	27e9be176f	Remove special handling of neutral I-eliminations in unifier	3 years ago
Amélia Liao	46b47037dd	built-in bools (to be removed later)	3 years ago
Amélia Liao	ce9e9876e2	Document glueing + univalence	3 years ago
Amélia Liao	d261ccc347	Add let definitions	3 years ago
Amélia Liao	5c50e1f98e	Implement Glueing	3 years ago
Amélia Liao	2d0b00380e	Implement cubical subtypes and composition	3 years ago
Amélia Liao	29285d0be5	Implement partial elements and systems	3 years ago
Amélia Liao	79cb94757c	Implement dependent paths (PathP's)	3 years ago
Amélia Liao	a1a8a96fa9	Wired in definitions for the interval algebra	3 years ago
Amélia Liao	92b50a4718	Polish up the type checker	3 years ago
Amélia Liao	6ee7be2872	Implement offside rule for toplevel statements	3 years ago
Amélia Liao	954356fd92	Definitional eta equality	3 years ago
Amélia Liao	b1e2e72242	Tweak the parser a bit	3 years ago
Amélia Liao	fcd5428ee0	Implement MLTT elaborator w/ type inference	3 years ago
Amélia Liao	bd3efa2cd6	initial commit w/ lexer & parser	3 years ago