Add judgmental notion of "strictly phi-connected type"

[jonsterling]

trafficstars

[jonsterling]

I think this is actually not too far beyond what I know how to do. Semantically tp \ phi is the collection of types A equipped with a unique element a : {phi} A.

Implementation-wise, it is not a good idea to be able to state that A has a unique element under phi for a given type A; as an assumption this probably implies some implementation taboo, perhaps as strong as equality reflection.

But it is ok to speak of the collection of types that have a unique phi-element, and provide syntax for projecting this element from A : tp \ phi, and provide syntax for constructing an element (A, a) : tp \ phi from a type A and its unique phi-point a.

1. Define a judgment tp \ phi; there is no need to restrict where this judgment can occur in the cooltt LF presentation --- it can be assumed freely.

2. Add a coercion tp \ phi ---> tp, together with a partial point p : phi -> A for each A : tp \ phi, such that under every element of A is equal to p under phi.

3. Add a weak closed modality Cl[phi] : tp ---> tp \ phi. This has the same introduction rules as the mathematical closed modality for phi, but we will give a dependent induction principle without an eta law in order to facilitate implementation.

[favonia]

Clarification question: does tp\{0=1} contain the empty type? If so, what should be the p in the second requirement. If not, which part of the definition of tp \ phi rules it out? I feel I must have been confused by something.

[jonsterling]

There is a typo in the spec! The point p should be under phi.

Then the empty type is 0=1-connected: the p is the unique map from 0=1 to the empty type.