18 Commits (d5c221c93dce89f98a463cc93ad8f3bccfaab0c8)

Author	SHA1	Message	Date
Amélia Liao	d5c221c93d	some initial work on HITs	3 years ago
Amélia Liao	9c37655544	some fixes to inductive types	3 years ago
Amélia Liao	6827a8838c	Implement proper inductive types	3 years ago
Amélia Liao	7aa7a3fac8	Add where clauses	3 years ago
Amélia Liao	6d065cdddd	Use glued evaluation to get shorter normal forms	3 years ago
Amélia Liao	6d82ecd85f	Fix composition for pairs	3 years ago
Amélia Liao	e521e7f10e	Report unsolved metas & composition for the universe	3 years ago
Amélia Liao	8937bc16cc	Remove special handling of neutral I-eliminations in unifier	3 years ago
Amélia Liao	8079ef845d	built-in bools (to be removed later)	3 years ago
Amélia Liao	e09d03572f	Add let definitions	3 years ago
Amélia Liao	1e6e17c3d8	Implement Glueing	3 years ago
Amélia Liao	eb83b77bf3	Implement cubical subtypes and composition	3 years ago
Amélia Liao	30b2984e1d	Implement partial elements and systems	3 years ago
Amélia Liao	134c24cb13	Implement dependent paths (PathP's)	3 years ago
Amélia Liao	818b816860	Wired in definitions for the interval algebra	3 years ago
Amélia Liao	9be5402444	Polish up the type checker	3 years ago
Amélia Liao	b819f56aed	Definitional eta equality	3 years ago
Amélia Liao	6eae8f2d2e	Implement MLTT elaborator w/ type inference	3 years ago