In his paper Structuralism, Invariance and Univalence (pdf), Steve Awodey makes the following claim about constructive type theory:
The system of type theory has the important property that any definable property of objects is invariant. Thus if $P(X)$ is any type that is definable in the system over a basic type $X$, then the following inference is derivable: $$ A \cong B, P(A) \vdash P(B) $$ The proof is a straightforward induction on the construction of $P(X)$.
My question is: can anyone give me a precise formulation of this theorem and perhaps point me to a proof? The first stumbling block for me is that I don't know how $A \cong B$ is formalised in type theory.
As for the system of type theory he is referring to, he writes:
The basic operations of what is called constructive type theory, starting with a basic object or "type of individuals" $X$, are as follows: $$ 0, 1, A+B, A \times B, A \rightarrow B, \sum_{(x : A)} B(x), \prod_{(x : A)} B(x), Id_{A}(x, y) $$