Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Created partial map classifier, but itex won’t make harpoons even though this page claims it can.
Is the higher inductive-inductive type definition added by anonymous edit #14 correct? While admittedly I have little familiarity with HITs, the elements of the definition given don’t look like they’re trying to define a partial map classifier. And even I’m wrong and the gist is right, I think it’s riddled with typos.
It feels really out of place anyways.
It looks like an (incorrect?) transcription of the construction in https://arxiv.org/abs/1610.09254 where they construct the free omega-CPO as a QIT and use this as a partial map classifier that works without countable choice.
Maybe best to delete the section and instead leave a concrete pointer in the list of references to where the reader may find partial map classifier discussed in type theory.
Okay, I’ve removed the section. I left the references that were added in the edit, although I’ve changed the description a little bit, since I’m not confident what’s described in the references, interpreted in the context at hand, actually reproduces the concept discussed on this page.
1 to 8 of 8