[lambdas]

Oooft, in cubical.ml why is your identity equivalence `CVar "__id"`? Surely this should be some fibration/reduction?

In fact, these weird string terms pop up pretty often, but surely you’d want to be using de Brujin indices lest you accidentally string match two different things (can’t believe I’m saying that for an implementation of a dependently typed language).

I started to wonder how your types were glued, as I would have thought Sigma types glued along identity equivalences would give me some insight on the odd behaviour.

`reduce_comp` seemed like the place it should be. There I realised your `CTGlue` case is wrong: it seems like `partial_pairs` is in the head but dropped from the body, so they’re never glued by any equivalence.

[omegafixedpoint]

Seconding Debruijn indices. See here: https://github.com/yon-language/yon/blob/aa4617ced3abc92ac53...

The alpha renaming algorithm does not run under scopes, only lambdas.