Andrea Vezzosi

A primitive like you suggested is sound and can simply be postulated as `IsOne _` is proof-irrelevant. More generally I would say parametrized faces are not well-supported as they go...

The models of CTT support a Prop universe. What one should do for indexed families and/or HITs in Prop would require more thought though. It does not seem like you...

It's quite possible that agda is working on unifying the type of the second element of the pair with the type `PathP (λ i → B (p i)) (snd x)...

A possible optimization is to check whether any "bad" variables are present without reduction, and only reduce if we have to make sure "bad" variable occurrences are actually rigid. This...

With `--experimental-lossy-unification` some unification variables will be solved even if they might have more than one correct solution, which means that you might have expected them to be solved some...

It does also have that drawback: picking the "wrong" solution can lead to type errors in some other part of the code. (I was going to add there is no...

@anuyts your `Ext` is `Sub` from `Agda.Builtin.Cubical.Sub` and indeed it's not Kan in general.

The current implementation for Boundaries for interaction points is indeed not ideal, and improvements are welcome! To give a bit of context, extracting information from the unification machinery did not...

`(~ r) = 0` is not the same as `Not (r = 0)`, in fact handling Not in Cof would probably be complicated: `Not (i = 0)` does not give...

I see, I misunderstood that aside, anyhow my main point was that if you try to refactor `I` to `Cof` you might bump into places where we made use of...