feat(logic/basic): simplification lemmas for transport through trivial type families

[semorrison]

No description provided.

[digama0]

These theorems seem a bit specialized. Is there some principled reason that these theorems in particular are needed? Otherwise I would suggest you keep them with their uses. By the way, the first theorem eq.rec.constant follows from eq_rec_heq and eq_of_heq. For the others, you shouldn't be using ulift.rec in the first place; the recommended interface is using up and down only.

[semorrison]

Okay. All of them arise by using `cases` analysis on `ulift` or `plift` hypotheses, or `induction` on equality hypotheses. Of course other relatives of these will arise from doing case analysis on other types, I just haven't run into anything else that got stuck in the same way. I use them in the category theory library; they seemed completely out of place in the first individual files they are needed in, so I thought I'd gather them together. I'm happy if we close this request, although they'll be back later. :-)

…

On Sun, Apr 29, 2018 at 3:38 PM Mario Carneiro ***@***.***> wrote: These theorems seem a bit specialized. Is there some principled reason that these theorems in particular are needed? Otherwise I would suggest you keep them with their uses. By the way, the first theorem eq.rec.constant follows from eq_rec_heq and eq_of_heq. For the others, you shouldn't be using ulift.rec in the first place; the recommended interface is using up and down only. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#124 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAdLBN0Mfj96X0iSvmE9SKvcjRdGvk_Pks5ttVHQgaJpZM4TrNVv> .