4

In the paper Univalence as a Principle of Logic, Awodey writes on page 7:

Let us consider the example of intensional versus extensional type theory. The extensional theory has an apparently “stronger” notion of equality, because it permits one to simply substitute equals for equals in all contexts. In the intensional system, by contrast, one can have a = b and a statement Φ(a) and yet not have Φ(b).

I do not understand this, because I thought this is the basic property of equality.

Also, in Coq one can simply prove:

Theorem subs: forall (T:Type)(a b:T)(p:a=b)(P:T-> Prop), P a -> P b. 
intros.
rewrite <- p.
assumption.
Qed.
  • 1
    This seems an error to me in the source, subs must be indeed provable for any notion of propositional equality. – András Kovács Apr 28 '18 at 8:04
  • 1
    Maybe what Steve means is that you need to use an explicit "rewrite" step to conclude Φ(b). I guess the best is to ask him directly! – ejgallego Apr 28 '18 at 14:07
3

If I am not mistaken, in Awodey's paper, the notation Φ(a) means substituting some implicit free variable in Φ for the expression a.

In my answer, I will use the following more explicit notation instead (which corresponds to Φ(a) in the paper):

Φ[z ⟼ a] 

This means that in the expression Φ, free variable z will be substituted for expression a.

Example:

(x = z)[z ⟼ a]

results in

(x = a)

Now, I will assume that you are already familiar with the usual presentation of Type Theory by means of inference rules, as in Appendix A.2 in the HoTT Book.

Type Theory uses two notions of equality.

Identity Types: Usually written using the symbol = in inference rules. In order to conclude an statement like a = b, we need to provide a proof term for it. For example, let's have a look at the introduction rule for identity types:

      a : A 
---------------- (=)-INTRO
 refl a : a = a

Here, refl a is acting as the proof term or evidence that justifies our claim that a = a holds (namely, refl a is representing the trivial or reflexivity proof). So, an statement like p : a = b is expressing that a and b can be identified due to evidence p.

Definitional Equality: Usually written using the symbol in inference rules. The statement a ≡ b means that a and b are interchangeable, replaceable anywhere, or substitutionally equivalent. This equality captures notions like "by definition", "by computation", "by simplification". This kind of equality does not carry a proof term with it, i.e. it is not a typing statement. This is the kind of equality Coq uses implicitly when you use the tactics simpl and compute. For example, let's have a look at the reflexivity rule for :

  a : A
--------- (≡)-REFLE
  a ≡ a 

Notice that there is no proof term to the left of a ≡ a (compare with the (=)-INTRO rule above). In this case, the proof system is treating a ≡ a as a fact, something that holds without the need to state explicitly its justification, since the only use of in the proof system will be for rewriting expressions.

That is used only for simplifying expressions, can be found in other inference rules, for example, the type preservation rule for :

   a : A     A ≡ B
 ------------------ (≡)-TYPE-PRESERV
        a : B

In other words, if you start with a term a of type A, and you know that types A and B are interchangeable, then term a also has type B. Notice that (and this will be important later!!) the proof term or evidence for B did not change, it is still the same proof term as the one used for A.


We can now get into the question.

What differentiates Extensional Type Theory (ETT) from an Intensional Type Theory like HoTT or CoC is the way they treat identity types and definitional equality.

ETT makes identity types and definitional equality interchangeable by adding the following inference rule:

 p : a = b
----------- (=)-EXT
   a ≡ b

In other words, the evidence p for the identity becomes irrelevant, and we treat a and b as interchangeable in the proof system (thanks to rules like (≡)-TYPE-PRESERV and other similar rules).

Starting from the hypotheses p : a = b and a : A, in ETT we can do stuff like the following:

  a : A                    p : a = b
--------- (≡)-REFLE      ----------- (=)-EXT
  a ≡ a                      a ≡ b 
------------------------------------- (=)-CONG        (*1)
            (a = a) ≡ (a = b)

Where (=)-CONG is a congruence rule (i.e. definitionally equivalent terms produce definitionally equivalent identity types), and I am calling this derivation (*1).

Using (*1), we can then derive:

     a : A                           
----------------- (=)-INTRO    -------------------- (*1)
 refl a : a = a                 (a = a) ≡ (a = b)
-------------------------------------------------- (≡)-TYPE-PRESERV
                    refl a : a = b

Where in (*1) we insert the derivation we did above.

In other words, if we ignore the hypotheses a : A and intermediate steps, it is as if we did the following inference:

p : a = b            refl a : a = a
-------------------------------------
          refl a : a = b 

Since ETT is treating a and b as interchangeable (thanks to the hypothesis p : a = b and the (=)-EXT rule), the proof refl a for a = a can be also seen as a proof for a = b. So, it is not hard to see that, in ETT, having a proof for an identity like a = b is sufficient for replacing some or all occurrences of a for b in ANY statement involving a.

Now, what happens in an Intensional Type Theory (ITT)?

In an ITT, the (=)-EXT rule is not assumed. Therefore, we cannot carry out the derivation (*1) we did above, and in particular, the following inference is invalid:

p : a = b            refl a : a = a
-------------------------------------
          refl a : a = b 

This is an example where we have an identity p : a = b, but from the statement (refl a : a = z)[z ⟼ a], we cannot conclude the statement (refl a : a = z)[z ⟼ b]. This is an instance of what Awodey's paper was referring to I think.

Why is this an invalid inference? Because refl a : a = b is forcing a and b to be definitionally equal (i.e. the only way to introduce refl a into a derivation is through the (=)-INTRO rule), but this is not necessarily true from the hypothesis p : a = b. In HoTT, for example, the interval type I (Section 6.3 in the HoTT Book), has two terms 0 : I and 1 : I, they are not definitionally equal, but we have a proof seg : 0 = 1.

The fact that there might exist other identity proofs that are not the trivial or the reflexivity proof, it's what gives an Intentional Type Theory its richness. It is what allows HoTT to have Univalence and Higher Inductive Types, for example.

So, what can we conclude from the hypotheses p : a = b and refl a : a = a in an ITT?

In your question, the theorem you proved in Coq is called the "transport" function in HoTT (Section 2.3 in the HoTT Book). Using your theorem (removing the implicit parameters), you will be able to do the following derivation:

  p : a = b               refl a : a = a
------------------------------------------
   subs p (λx => a = x) (refl a) : a = b 

In other words, we can conclude that a = b, but our proof term for this changed! In ETT we simply carried out a substitution (because a and b were interchangeable) allowing us to use the same evidence in the conclusion (namely refl a). But in an ITT, we cannot treat a and b as substitutionally equivalent, due to the richness of the identity types. And to reflect this intention, we need to combine the proofs of the hypotheses to build our new evidence in the conclusion.

So, from (refl a : a = z)[z ⟼ a] we cannot conclude (refl a : a = z)[z ⟼ b], but we can conclude subs p (λx => a = x) (refl a) : a = b, which is not the result of a simple substitution from the hypothesis, as in ETT.

-3

The rewrite tactic in Coq can fail - it can generate an ill-typed term.

If I remember correctly, it's sometimes possible to get around this with some careful manipulations, but if you do this by (implicitly or explicitly) introducing an additional axiom, such as functional extensionality or JMeq_eq, it's no longer the case that the first goal simply follows from the second.

  • I cannot see the relation of your answer.to my question. – Cryptostasis Apr 28 '18 at 7:28
  • Because rewrites do not always work, and this is due to a typing issue not due to a simple bug in Coq, that explains why Φ(a) does not necessarily imply Φ(b) if a=b, in the logic of Coq. – Robin Green Apr 28 '18 at 7:32
  • My question says just the opposite. In COQ it works in general, but Awodey says it doesn't work in general .... – Cryptostasis Apr 28 '18 at 7:34
  • No, it doesn't work in general in Coq. Your theorem doesn't say what you think it says. I mean it looks like it does, but it is a theorem in the logic, not in the metalogic. Awodey is speaking at the metalogical level. – Robin Green Apr 28 '18 at 7:38

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.