semantic universe polymorphism
0 views
Skip to first unread message
Michael Shulman
Apr 2, 2015, 12:25:51 AM4/2/15
to homotopyt...@googlegroups.com
Has anyone studied universe polymorphism from a semantic viewpoint,
rather than as a purely syntactic device that gets "compiled away"
into explicit universe levels before being interpreted semantically?
I am imagining something like making the category of contexts into an
indexed category over a sort of "category of universe indices",
corresponding to viewing the polymorphic universe indices as an
additional "context" on the left of all judgments.
Mike
rather than as a purely syntactic device that gets "compiled away"
into explicit universe levels before being interpreted semantically?
I am imagining something like making the category of contexts into an
indexed category over a sort of "category of universe indices",
corresponding to viewing the polymorphic universe indices as an
additional "context" on the left of all judgments.
Mike
Peter LeFanu Lumsdaine
Apr 2, 2015, 7:51:22 PM4/2/15
to Michael Shulman, homotopyt...@googlegroups.com
I’ve discussed it a little with Matthieu Sozeau and Nicolas Tabareau, and have been planning to work on it with a visiting student over the summer. We haven’t got anything carefully worked out yet, though.
–p.
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Reply all
Reply to author
Forward
0 new messages