search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

All modalities can have definitional computation #1283

Open mikeshulman opened 4 years ago

mikeshulman commented 4 years ago

Here's another trick we could play using mapping cylinders: make all modalities (and reflective subuniverses) have definitional computation laws, by defining "the" reflector to be the mapping cylinder of the "reflector" that's given as a field of the record. So O_rec_beta, O_ind_beta, and other things derived from them like to_O_natural would be definitional equalities for all reflective subuniverses, they way they already are for the special cases of Trunc and Loc.

I'm not sure whether this would be a good idea or not.

Alizter commented 7 months ago

@jdchristensen As you have worked with theory about reflective subunivereses, can I get your opinion on whether you think this might be useful to have?

jdchristensen commented 7 months ago

@Alizter @mikeshulman Hmm, interesting idea! If we went this way, I think we'd need to do it for every reflective subuniverse, so that general things proved using this trick apply to the specific examples. So that means that Trunc and Loc would get an extra wrapper around them which would be redundant. I'm not sure that that is worth it, especially since all of the proofs are already there without strictness. If I had to write the Modalities folder from scratch, this trick might then be worth it.

An alternative would be a function that strictifies a given RSU, and also returns an equivalence between the two. Then there could be a tactic strictify_rsu O which replaces the goal with a goal involving a strict O. For that we'd need to know that the goal is invariant under isomorphisms of RSUs, which might be tricky since most results don't need univalence.

Alizter commented 7 months ago

I guess for it to be worth it, we would need an example of a proof which is simplified a lot by being strict. If it's only removing a few lines from existing proofs, then it might not be wroth doing. I can't think of any examples of such proofs off the top of my head.