Right now our encoding of telescopes is overly dependent. That is, any value in the telescope can appear in any of the types of the rest of the telescope. In fact, provided with a description of a telescope, we have actually no way of knowing whether said value is in fact used or not in the rest.
This is quite unfortunate, as NoConfusion and other constructions, which use homogeneous propositional equality and therefore require some lifting of types to equate values, are made utterly unusable when we have no way of expressing that values are not used. Indeed, for now we have to lift types along equalities over all the values that come before in the telescope, even values that we do not depend on.
This amounts to being able to encode an acyclic graph of dependencies somehow, will post more info later.
Right now our encoding of telescopes is overly dependent. That is, any value in the telescope can appear in any of the types of the rest of the telescope. In fact, provided with a description of a telescope, we have actually no way of knowing whether said value is in fact used or not in the rest.
This is quite unfortunate, as
NoConfusionand other constructions, which use homogeneous propositional equality and therefore require some lifting of types to equate values, are made utterly unusable when we have no way of expressing that values are not used. Indeed, for now we have to lift types along equalities over all the values that come before in the telescope, even values that we do not depend on.This amounts to being able to encode an acyclic graph of dependencies somehow, will post more info later.