What is the relationship between extension types, cubical subtypes, and cofibration splits in cooltt?

[mmcqd]

If this is answered in a paper somewhere, feel free to just point me to that. Perhaps this part of this is actually better suited for the Proof Assistant Stack Exchange? Let me know.

I'm trying to understand the theoretical and practical relationship between extension types, cubical subtypes, and cofibration splits. My current understanding is this:

• An n-ary extension type classifies a (curried) n-ary map out of the interval with certain boundary conditions. This is a type with conditions on its members
• A cubical subtype sub A phi x classifies elements of A that are definitionally equal to x when phi is true. This is also a type with conditions on its members
• A cofibration split [phi -> x | psi -> y] (where x,y : A) introduces an element of A that has certain boundary conditions. This is a term which is conditionally equal to other terms, there are no conditions in its type.

My feeling is that there is some overlap in the functionality of these concepts. Namely, it seems like extension types ought to be (almost?) expressible in terms of subtypes and splits, that is:

ext i => A with [i=0 => x | i=1 => y]

seems very similar to

(i : dim) (_ : [i=0 \/ i=1]) -> [i=0 => sub A {i=0} x | i=1 => sub A {i=1} y]

They're clearly not exactly the same (the second has an extra argument), and in fact I can't get the second type to typecheck, it asks for annotations on the subtypes.

On the other hand, these seem to actually be exactly the same:

ext => A with [true => x]

and

sub A true x

I also see that subtypes have no codes, and extension types are only codes, which seem to be translated into something like I've written above by the function unfold_el.

My two questions are:

1. What is the difference between extension types and maps out of the interval constrained by splits and subtypes?
2. Why do subtypes have no codes while extension types are only codes?

[cangiuli]

Great question, and I don't think the answer is written down anywhere...

As you noticed, terms of extension type are defined to be functions out of (n copies of) the interval into a cubical subtype. However, cubical subtypes are generally not Kan (in particular, do not in general support coercion), whereas our formation rule for extension types picks out the ones that are Kan. In cooltt, types are not assumed to be Kan in general; only types with codes in the Kan universe are Kan.

Here's my go-to example of why cubical subtypes can't always be Kan:

i => {coe {j => sub bool {j=0 \/ j=1} [j=0 => true | j=1 => false]} 0 i true}

The above (illegal) coercion produces a path from true to false. The formation rule for extension types requires phi to only depend on dimension variables that were bound "locally" by the extension type; in this case, the (non-existent) extension type binds no variables but has a phi that depends on j, which is disallowed.

[mmcqd]

Thank you! So

ext i => A [i=0 => x | i=1 => y]

is actually

(i : dim) -> sub A {i=0 \/ i=1} [i=0 => x | i=1 => y]

that makes sense.

It's interesting that types like this are Kan when they only depend on "local" dimension variables, but not otherwise. I see how your example proves it, but I don't quite have the deeper intuition for why it's true. Something for me to think about.

So the A type judgment in cooltt (aka A was produced by a Tp.tac) does not mean that A is Kan, but having a code for A in the Kan universe (which is currently the only universe) does mean that A is Kan. Is there a meaningful relationship between virtual types and non-Kan types?

[cangiuli]

why it's true

It's not too hard to show that extension types on A are Kan when A is Kan, given the locality restriction -- this generalizes the fact that path types on A are Kan when A is Kan. The above example (and others like it) shows that the locality can't be dropped.

virtual types and non-Kan types

Whereas cubical subtypes are types but not Kan types, virtual types like the interval are "not even types" (nor Kan). On the one hand, the interval is like a type in that (i : I) -> A is a type when A is a type. On the other hand, (x : A) -> I is not a type. Why? Type checking in cooltt requires deciding whether a cofibration (like i=0) is true / whether two elements of the interval are equal, modulo the cofibrations in the context (like i=j /\ j=0). To make this workable, we stratify the theory so that you can't write down elements of the interval that involve elements of other types (e.g., f 5 : I where f : nat -> I); as a result, the decision problem for elements of I/F is independent of (prior to) the rest of the theory. Virtual types achieve this stratification by ensuring that I and F only appear on the left, not on the right.

[mmcqd]

Thanks so much for the thorough answers! Your explanations were super helpful.