What could be improved about the universe handling? Cumulativity? Or something more like McBride's blog post? pigworker.wordpress.com/2015/01/09/uni (I've had trouble getting my head around how to turn the latter into an implementation... 🙄)
Conversation
This Tweet was deleted by the Tweet author. Learn more
This Tweet was deleted by the Tweet author. Learn more
Cool! I was interested in adopting it in Pikelet - I guess the main impediment is not having a detailed example of it (either in formal notation or an implementation).
This Tweet was deleted by the Tweet author. Learn more
This Tweet was deleted by the Tweet author. Learn more
Yeah, would love to chat. Is this in redtt or redprl somewhere too?
2
Ahhha, I have found an Lvl github.com/RedPRL/redtt/b - I did see a comment about mcbride-style universes in redtt or redprl a while back, but never got around to investigating further... although I was interested!
1
Would be handy to have a description of MiniTT or something using it. I'm guessing, going off RedTT's source you have a shift on each var (defaulting to 0 for convenience)? And then apply the shift when looking up the type of a variable in the context?
This Tweet was deleted by the Tweet author. Learn more
Wait whaaaat - I didn't realise that Mini-TT was showing off a cubical tt thingo! Shows how good (terrible) my paper comprehension skills still are! homotopytypetheory.org/2017/09/16/a-h .___.