# Tag Info

10

ℕ→ℕ-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.

9

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 ...

9

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 ...

3

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 ...

3

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 ...

2

I decided to rewrite my answer, because I thought I could explain the details better. I'd still defer to someone more knowledgeable should they happen to come along. I think it is relatively safe to say that cubical type theory as an approach on the whole is compatible with the classical axioms you want. The reasons for this are: The differences people ...

1

Another thing you should know is that those truncations don't hide anything. For instance, it is relatively simple to prove the lemma: $$\mathsf{isProp}\ A → \mathsf{isProp}\ (A \uplus ¬ A)$$ which means that we can extract the evidence from $\| A \uplus ¬A \|$. I think the same is true of the $A \equiv \mathsf{Unit}$ version, because all types involved ...

1

Kan operations are likely named after Daniel M. Kan, in analogy to concepts such as Kan extensions, Kan complexes, Kan fibrations, Kan condition, and many more. Kan also introduced adjoint functors.

Only top voted, non community-wiki answers of a minimum length are eligible