makkai - Type theory implementation

Age	Commit message (Collapse)	Author
2026-05-07	regression in WiP work to improve sets	tslil

2026-05-07	finish the implementation, we don't have motives so this is how it will have ↵	tslil
	to stay
2026-05-06	WiP	tslil

2026-05-05	repair binding for nesting in for	tslil

2026-05-05	address remaining TODO, fix issues with left-nesting for for and ext, add ↵	tslil
	motivation blurb to the readme
2026-05-01	add monotic counters, fix element binding case in app->for	tslil

2026-04-29	switch to references in many places for check_*, complete logic of Var case ↵	tslil
	for App
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-28	snapshot of working through instances/singatures <> sets/elements	tslil

2026-04-28	move assert unbound to only top-level decls to allow shadowing	tslil

2026-04-28	rework checking logic to revolve around "stuck" computations, the meaning of ↵	tslil
	Hypothetical is now reserved for formal bindings
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-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-24	minor cleanup	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