Jason (jcreed) wrote,
Jason
jcreed

-

Wrote some READMEish stuff at work.
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.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments