Judgemental equality

Question

TL;DR: in Agda, given a : A and proof : A == B, can I obtain an element a : B?

---

In my ongoing attempt to learn Agda, I've created the following Prime : nat -> Set datatype, which is a witness to the primality of a natural.

Prime zero = False
Prime (succ zero) = False
Prime (succ (succ n)) = forall {i : nat} -> divides i p -> i <N p -> zero <N i -> i == (succ zero)
  where
    p = succ (succ n)

Here:

• False is a data type with no constructors;
• divides a b is a data type that contains a witness k to the fact that a * k = b;
• a <N b is a data type that contains a witness k to the fact that a + k = b;
• == is the equality type, with just one constructor refl;
• the natural numbers are defined in the obvious way with zero : nat and succ : nat -> nat.

I've successfully exhibited a member of Prime (succ (succ zero)), and proved that the statement Prime (succ (succ (succ (succ zero))))) implies False.

Now I'm trying to prove that primes are greater than one:

primesAreGreaterThanOne : (p : Sg nat Prime) -> (succ zero <N value p)

where

• Sg A pred is the dependent pair (p, pred(p)) where p : A;
• value : Sg A pred -> A extracts the value and discards the proof.

I've already proved trichotomy of the order: for all a, b it is true either that a <N b, or a == b, or b <N a. (This lemma, I hope, should help us avoid any excluded-middle problems.) So by working casewise on the ordering relation between succ zero and value p, I've reduced to the case that I have a proof of p == zero and a proof of Prime p and the statement that Prime zero is defined to be False.

Now, of course, these statements are contradictory: since I have a proof that p == zero, I can exhibit an inhabitant of the type Prime p == Prime zero, and hence I have an inhabitant of Prime p == False.

But how can I take my element proof : Prime p (the proof which is the second component of p : Sg nat Prime) and "cast" it to an element of False? The types are propositionally equal, but not judgementally equal.

Answer 1

This turns out to be easy; Just Do It (tm).

typeCast : {a : _} {A : Set a} {B : Set a} (el : A) (pr : A == B) -> B
typeCast {a} {A} {.A} elt refl = elt

Answer 2

I would like to point out some theoretical background on this particular topic.

Agda's core is Martin Löf's logical framework (LF), which is a minimal dependently typed lambda calculus that gives us the dependent functions among other things. And overall, Agda is based on intensional ML type theory.

In LF, there is a rule called type conversion rule which states that

 Γ ⊢ t : A     Γ ⊢ A = B
--------------------------
        Γ ⊢ t : B

This coerces terms along type equality. Where two types are definitionally equal established by computation (beta) and extensionality (eta).

Edit to clarify: In intensional TT, judgmental equality and propositional equality are separated and propositional equality doesn't give you judgmental. If you want a rule that given two propositionally equal terms to be also judgmentally equal, then you would be in an extensional TT, which is often undesirable since it makes type checking undecidable. So, in intensional TT, it is not always true.