4
$\begingroup$

For context, I am reading "Principles of Dependent Type Theory".

Intensional Type Theory is a dependent type theory where we take out equality reflection to make type conversion decidable. I'm trying to figure out if definitional equality is stronger or weaker than definitional equality (beta-eta-equality) with this change.

My intuitive understanding is when proving a complicated P a b with equality a = b in the context, we can instead prove the simpler P a a via the J rule, promoting id into a definitional equality. Moreover, statement like subst (type conversion through equality) or trans seem like typing hints in simpler type systems meant to make type checking syntax-directed and thus decidable. Yet, we can only construct id when two terms are definitionally equal so maybe all a = b terms are definitionally equal?

Concretely, is it the case that empty context |- p : a = b, then empty context |- refl : a = b? As in the id type is no stronger than definitional equality.

I don't mean to ask if we can prove that all equality types being equal are provable in the system, but more meta-theoretically if given infinite compute to run the theoretically decidable conversion checker can we just write refl everywhere to prove things are equal or is there a counter example that needs the user to do calculations?

Improve this question
$\endgroup$
0

1 Answer 1

Reset to default
6
$\begingroup$

If you work in plain intensional type theory with no axioms, then indeed every term $\vdash p : a = b$ in the empty context is judgementally $\mathrm{refl}$, and this implies that $a$ and $b$ are judgementally equal: this is a form of canonicity for the identity type. See also this answer.

This breaks as soon as you consider open contexts (in particular, if you postulate axioms), so this result is not particularly useful from the point of view of implementation. As a trivial example, in the (inconsistent) context $\Gamma = (p : 0 = 1)$ (or $\Gamma = \bot$), there is a term of type $0 = 1$ that is not $\mathrm{refl}$. As a slightly less trivial example, in the context $\Gamma = (\mathsf{FunExt}, f : A \to B, g : A \to B, H : \forall a. f\,a = g\,a)$, there is a term of type $f = g$ (obtained via function extensionality) that is not $\mathrm{refl}$.

It also breaks if you work in something like cubical type theory, which extends intensional type theory with things like univalence and higher inductive types: there, you can expect to construct closed non-trivial loops of type $\mathrm{Bool} = \mathrm{Bool}$ or $S^1 = S^1$ (where $S^1$ is the circle HIT), or closed paths between judgementally inequal terms.

Improve this answer
$\endgroup$
2
  • 3
    $\begingroup$ A non-degenerate example, but without relying on funext, is given by the converse direction: in the context $f : A \to B,\, g : A \to B, h : f = g$, there’s a non-refl term of type $\prod (a \mathord{\colon} A)\, f a = g a$. $\endgroup$ Commented 2 days ago
  • $\begingroup$ If we're listing non-degenerate examples, in the context $h : 0 = 0$ there is a non-refl term of type $0 = 0$. But I suppose this one is degenerate in a different way. $\endgroup$ Commented 13 hours ago

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.