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.
subsmust be indeed provable for any notion of propositional equality. – András Kovács Apr 28 '18 at 8:04