it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer
My understanding is that it matches points of path rather than path itself. This is why the matching is on posneg x (where x : I) rather than posneg itself.
Since paths can be seen as (special) maps from I, we can think of HIT constructors as just a ...
ℕ→ℕ-undecidable is not provable in Agda. If we postulate the law of excluded middle (LEM), it follows that equality on every set is decidable, contradicting ℕ→ℕ-undecidable. Since Agda is consistent with LEM, it follows that ℕ→ℕ-undecidable is not provable in base Agda. This holds the same for cubical and vanilla Agda.
There are potentially multiple ways of presenting canonicity (and I think complications depending on the theory). However, I think the simplest way to think about it is from the perspective of a programmer wanting to use the type theory to compute something. For instance, we might want to compute some natural number satisfying some specification we've come ...
The original statement in my question
sym (ua (isoToEquiv fIso)) ≡ ua (isoToEquiv (invIso fIso))
is a valid statement in Homotopy Type Theory but because (homotopy-) isomorphisms are a special case of equivalences, the statement can be generalized to
sym (ua fEquiv) ≡ (ua (invEquiv fEquiv)) (*)
It is one of the properties of ua that are informally proven ...
The only way to prove ∥ X ∥ is to prove X (unless you admit some other axiom).
So, assuming P is a proposition, there is no way to prove ∥ ((A) ⊎ (¬ A)) ∥ if you cannot prove ((A) ⊎ (¬ A)).
It is not a correct intuition that undecidable propositions are either true or false, just we do not know about it.
A formal system S with an undecidable proposition P ...