Post #4230136

Playing with 2LTT in Agda leads me to wonder if some form of relative canonicity holds in particular that if context, types, and both sides of the outer identity are inner terms, then these term are actually judgementally equal. I’ve been very confused by the claim that the outer identity is the internalised judgemental equality, but IIUC this hold if the outer theory is extensional. 🤔