non-dependent recursors for HITs

[ecavallo]

The eliminator for a HIT takes fhcoms to coms in the target type. When the motive is non-dependent, the output com is in a constant line, so the desired behavior could be accomplished more efficiently with an hcom. It might then be useful to have a separate non-dependent recursor which uses hcom instead of com. (Note that the two options are not even equal, because we don't have regularity.)

I don't know how much of a difference it would make, but synthetic homotopy proofs involve plenty of non-dependent functions between / out of HITs.

[mortberg]

Very interesting observation!

[favonia]

I am worried that this would lead to incoherent results after we allow users to make something opaque. It seems possible for an opaque operator to create a "false" dependency that results in a different value.

[jonsterling]

@favonia

1. I think the proposal is not to have the single eliminator detect whether it is being dependent, but instead to provide two different eliminators to the user. The complication is that I think it would not be good to have a use of one eliminator be definitionally equivalent to a use of another one---though you could usually prove this in propositional equality or paths, etc. Does this make any sense?

2. Regardless of the above: It's worth noting that generally you lose that sort of coherence when you add some kinds of opaqueness, regardless of this ticket; that's why I think it might not be safe to do what they do in cubicaltt, which is to "temporarily" make something opaque, and then make it transparent again. But I think it is generally sensible to allow opaque definitions like in Coq and also redtt, which you can think of as just working in the slice. My intuition (which I haven't proved) is that those temporary opaque things in cubicaltt must disrupt the transitivity of definitional equivalence.

[favonia]

I see! Alright, then this is not (too) difficult to support.

[mortberg]

What we do in cubicaltt for opaque/transparent is not safe and was never meant to be. It is easy to see that you can break subject reduction using it. It was mainly added to be able to typecheck some examples which were too slow with everything transparent and this was the easiest way to do it. For a proper proof assistant something more carefully designed is necessary. What they do in Coq is not very satisfactory either and I have some ideas on how to make it better behaved (I think there should be different levels of opacity that the typechecker can take into account, with modes like "transparent", "unfold only if necessary", "completely opaque forever"...). Anyway this discussion is orthogonal to the ticket opened by Evan so let's continue in another thread if you plan to add opacity to the system.

[mortberg]

Oops, I wrote something stupid in a comment that I deleted. Sorry for the noise.

[jonsterling]

Back to the main topic of this ticket, I say let's try it out! It sounds like a good idea.