Looking at the doc on master, there is an example of a non-terminating term: https://coq.github.io/doc/master/refman/addendum/sprop.html?highlight=sprop#non-termination-with-uip . Termination is the key behind consistency (or at least weak normalization). I am not sur to understand the implication of this for the consistency of Coq. In particular, I am surprised that it is not mentioned in the documentation.

is this a question or an observation? It's well known that some axioms are fine when added to Coq in isolation, but lead to inconsistency when combined (in this case, UIP and an impredicative Set/Type). More discussion on what axioms don't go together here: https://coq.discourse.group/t/what-do-you-think-of-axioms/231

I am trying to understand the implications here. Because from what I understand, `Definitional UIP`

may reduce a match using a local hypothesis. Therefore if we follow the paper : https://arxiv.org/pdf/1911.08174.pdf , it says that normalisation breaks IIUC. So is it related to an extra axiom?

If just having `Definitional UIP`

breaks normalisation (without other axioms), why is it interesting to activate it since it breaks consistency?

It doesn't break consistency

So you mean having a non-terminating term does not break the consistency? It is indeed clearly stated in the paper but I found it surprsing, thanks.

Consistency is broken by fixpoints, but a merely non-terminating term is not enough to break it.

You lose decidability of type-checking though...

By the way, would we lose something to restrict definitional UIP on equality-like types with indices in small types (i.e. types in `Prop`

or `Set`

)? The most interesting uses of `SProp`

are with equality in data-types such as `nat`

, no?

Also, I only recently started to explore what we can do with `SProp`

, but would there be negative consequences of allowing elimination from `SProp`

to `Type`

for syntactic singleton types (i.e. not only from `False:SProp`

but also from `True:SProp`

, `and:SProp->SProp->SProp`

)? Associated reduction rules could typically be derived as if eta-expanding on the fly.

Last updated: Jun 23 2024 at 23:01 UTC