What a gate's branch dispatches on

A gate block's branch checkpoint dispatches on the tag its witness flags decode. The decoding itself (DescriptiveComplexity.Draw.Data.GateTagsAre) is one-hotness of finitely many control flags, so it is definable outright. The total dispatch (DspTagsAre) adds a default branch for the block values no point encodes, and that branch names a tag – which the interpretation may only do if the tag is the same at every instance.

DescriptiveComplexity.Draw.Data.defTag is chosen from a nonemptiness of the tags rather than from a point, exactly so that it is – by proof irrelevance, the structure that witnessed the tags inhabited does not survive into the value – and DescriptiveComplexity.Draw.Data.uConst_defTag is that fact: one environment is all it takes, and every other names the same tag.

theorem DescriptiveComplexity.Draw.Data.uConst_defTag {L : FirstOrder.Language} {dt : Data L} (e₀ : Env L) : UConst fun (e : Env L) => dt.defTag

The default tag is the same at every instance: it is Classical's choice at a Prop, so which structure witnessed the tags inhabited does not survive into it. One environment is all it takes to name it.