Family intersection types about sml-redprl HOT 6 CLOSED

I think this is okay for pretypes, but I don't think it naively works for Kan types.

from sml-redprl.

Since the Enlightenment of Kinds, this of course works for discrete types. What do we want except embedding the entire Nuprl type theory?

from sml-redprl.

@favonia Indeed!

By the way, Mark Bickford has proved that some version of family intersections are Kan for the CCHM type theory; see the bottom of http://www.nuprl.org/wip/Mathematics/cubical!type!theory/.

I wonder if we can get such a result in our setting (low priority, but interesting).

/cc @cangiuli

from sml-redprl.

At least, I think he is proved this; I'm not familiar enough with that development to really understand it.

from sml-redprl.

Just to update the public record, Mark Bickford has defined family intersections for CCHM cubical sets, but has not proven they are Kan.

from sml-redprl.

Mark Bickford has defined family intersections for CCHM cubical sets, but has not proven they are Kan.

Alright. It should be possible to add them for discrete Kan types and stable ones to RedPRL, and that more or less matches Mark's progress, I guess.

from sml-redprl.