makkai - Type theory implementation

Age	Commit message (Collapse)	Author
2026-04-30	wip case for instances	tslil

2026-04-30	fill in some more todos	tslil

2026-04-30	lost track of what's going on	tslil

2026-04-29	wip on App For	tslil

2026-04-29	implement canonicalisation in case arms, work through first bit of app	tslil

2026-04-29	wire in instance checking to the main checker	tslil

2026-04-29	fix parser bug, fix beta reduction for setcoerce, disambiguate set coerce in ↵	tslil
	parser
2026-04-28	snapshot of working through instances/singatures <> sets/elements	tslil

2026-04-27	add tough example	tslil

2026-04-27	fix the graph signature, it must have set-of to be correct	tslil

2026-04-27	flip to agda-like grammar, sets & signatures do not have dots in their ↵	tslil
	fields, but applications of those do as do constructions
2026-04-27	prepare for more work on signatures, in particular this means processing ↵	tslil
	records in telescoped contexts rework ElementValue, CheckedElement to be type aliases for the generic version over Term : Type
2026-04-27	refactor equality checking and fields as we start to build towards signatures	tslil

2026-04-27	add distinction between hypothetical and concrete elements to the set ↵	tslil
	checker, it now enforces that all arms in case are well typed!
2026-04-27	change the "claimed set" notation to "set-of" so that David isn't confused	tslil

2026-04-24	computing cases	tslil

2026-04-24	refactor: separate checker into _state, _set, and principle export	tslil

2026-04-24	checking for injections, projections, rm vesitigial App	tslil

2026-04-23	start work on elements	tslil

2026-04-23	Progress on checking sets	tslil

2026-04-23	basic checking sketch	tslil

2026-04-23	Init	tslil