Talked with tom7 over dinner a bit. Sort of reassured myself that linear top doesn't interfere in any consequential way with the monotonicity property I've been trying to come up with to more tastefully generalize what it is about the image of the translation from LLF that should behave usefully in coverage checking. Tom also pointed out the possibility of something kind of like top that would have the same behavior up to provability, but would fail as a terminal object, having many more proofs, one for each way of disposing the elements of the context. Were top to behave like that, worlds under translation into HLF would no longer be proof-irrelevant, and everything might be a bit simpler. This is certainly nothing I'm considering working on very hard within the scope of my thesis project, but it's an interesting idea that I never took seriously until now.