Going over irrelevance stuff again.
I think it's possible to think of irrelevance
as a monadic type constructor with the property
that every object in its domain is "quasi-terminal"
in the sense that there is at most one arrow
going into a quasi-terminal object from any other
object X. I wonder if this gives rise to a natural
dual, and/or fits in with a categorical description
of LF.
