Jean Abou Samra (new account) on Nostr: Agda has an ugly soundness bug when used for UF: it considers the arms of a pattern ...

Agda has an ugly soundness bug when used for UF: it considers the arms of a pattern match to be in a strictly positive position, which looks OK at a glance until you realize that matching on an equality involves transport along an arbitrary equivalence, which is certainly not strictly positive in general. https://github.com/agda/agda/issues/4966

This makes me wonder: has anyone figured out a semantic notion of strict positivity that could replace the ad-hoc syntactic checks used in proof assistants? I mean, UF showed that there are many benefits to using the semantic notion of mere propositions instead of a separate Prop sort with its hacks like subsingleton elimination. I'm wondering if there is something similar here.