Skip to main content
2 votes

Higher Observational Type Theory: variables becoming free in reduction rules

I would guess the issue comes from the $\Delta$ you assumed was missing. As far as I can tell, when living over a general telescope, already $$ Id_{Δ.(Π (x : A) B)}^δ(f, g) ≡ \Pi (u, v : A). \Pi(p: ...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible