[WIP] Groupoid interpretation - #168

Draft

Vtec234 wants to merge 36 commits into

Commits on Feb 11, 2026

chore: start port
Vtec234
committed
8fb146b
chore: import
Vtec234
committed
31aa326
chore: rfl
Vtec234
committed
3f81c94
more adaptations
Vtec234
committed
94c4ec5
import
Vtec234
committed
5b2bcf1
feat: theory
Vtec234
committed
ac43449
feat: generalize interpretation universes
Vtec234
committed
fab85c8
feat: scaffolding for semantics
Vtec234
committed
a5259b8
chore: universe
Vtec234
committed
90e367a
feat: internal theory
Vtec234
committed
aa46e17
chore: add univMax_le field
Vtec234
committed
edf582a
fix: prop
Vtec234
committed
b62336a
doc: trunc levels
Vtec234
committed
b970286
feat: add Bhavik's example
Vtec234
committed
001d93b
fix: slen le
Vtec234
committed
be364b8
feat: @[reflect] attribute
Vtec234
committed
56f7c87
fix: unitt test
Vtec234
committed
bc9b97c
feat: signature maps
Vtec234
committed
b28a452
more internal theory lemmas
Vtec234
committed
56e0dc8
misc
Vtec234
committed
27691de
chore: move lemmas
Vtec234
committed
0e89c81
feat: theory maps
Vtec234
committed
7496dfc
feat: snoc takes a wf-type
Vtec234
committed
d31d9b5
chore: disambiguate lib
Vtec234
committed
fcdfdfc
chore: trace and doc
Vtec234
committed
719bcd6
feat: Val.map
Vtec234
committed
5b361d1
feat: instances
Vtec234
committed
839a5fd
feat: typecheck theory maps
Vtec234
committed
93142a6

Commits on Feb 12, 2026

chore: Checked -> Reflected
Vtec234
committed
7901d70
fix: some tests
Vtec234
committed
32d3963
feat: unbracket
Vtec234
committed
da0fe3c
refactor: Qq madness
Vtec234
committed
7d03d94

Commits on Feb 13, 2026

feat: delaborators
Vtec234
committed
a70ccb8
feat: ctx widget
Vtec234
committed
3429724

Commits on Feb 19, 2026

feat: improve index tactic
Vtec234
committed
78b9760
feat: type deinterp
Vtec234
committed
9e11a6c