Conservativity of equality reflection over intensional type theory

Martin Hofmann

Fachbereich Mathematik TH Darmstadt Schloßgartenstraße 7 D-64289 Darmstadt Germany

Abstract. We investigate the relationship between intensional and extensional formulations of Martin-Löf type theory. We exhibit two principles which are not provable in the intensional formulation: uniqueness of identity and functional extensionality. We show that extensional type theory is conservative over the intensional one extended by these two principles, meaning that the same types are inhabited, whenever they make sense. The proof is non-constructive because it uses set-theoretic quotienting and choice of representatives.

1 Extensional and intensional type theory

A distinctive feature of Martin-Löf’s type theories is the presence of two notions of equality: judgemental equality and propositional equality. Judgemental equality applies to both terms and types and is written as a judgement Γ ⊢ M = N : σ and Γ ⊢ σ = τ type. The inference rules for these judgements include congruence rules for all the type and term formers and computational rules like the β and possibly the η-rule for function types. The present study applies to dependent type theories with at least Π-types, Σ-types, identity types, and natural numbers (to have a base type). For simplicity we assume an η-rule for the Π-types. In [6] we also deal with the absence of the η-rule.

Propositional equality only applies to terms and is itself a type (of equality proofs). That is, we have a type Id_{σ}(M, N) in context Γ whenever M, N : σ.

\frac{Γ ⊢ σ type Γ ⊢ M : σ Γ ⊢ N : σ}{Γ ⊢ Id_{σ}(M, N) type} Id-Form

The formulation of equality as a type allows internal reasoning about equality, for example a propositional equality can be established by induction (N-elimination) so as to show x: N ⊢ Id_{N}(x, Suc^{x}(0)) true where Suc^{x}(0) means the x-fold application of the successor function to 0 defined by N-elimination. Here and in the sequel we write Γ ⊢ σ true to mean Γ ⊢ σ type and Γ ⊢ M : σ for some term M. Type annotations to Id and other type and term formers may be left out where appropriate.

Propositional equality is introduced via reflexivity, i.e. if M : σ then we have a canonical element Refl_{σ}(M) : Id_{σ}(M, M).

\frac{Γ ⊢ M : σ}{Γ ⊢ Refl_{σ}(M) : Id_{σ}(M, M)} Id-Intro

This, together with the congruence rules for judgemental equality gives that M = N : σ always entails that Id_{σ}(M, N) is inhabited (namely by Refl_{σ}(M)).

Now one would like to express that this is the only inhabitant of the identity type, i.e. one might wish the rule

\frac{Γ ⊢ P : Id_{σ}(M, N)}{Γ ⊢ P = Refl_{σ}(M) : Id_{σ}(M, N)} Id-Uni

However, for this rule to “type-check” we need to identify propositional and judgemental equality. This is achieved by the equality reflection rule

\frac{Γ ⊢ P : Id_{σ}(M, N)}{Γ ⊢ M = N : σ} Reflection

This axiomatisation of propositional equality is the one used in Martin-Löf’s earlier works [8] and in many proof-theoretic studies on his type theories. The type theory based on this axiomatisation is called extensional type theory, TT_{E} for short, because by rule Reflection the judgemental equality becomes extensional. For instance, since as argued above x: N ⊢ Id_{N}(x, Suc^{x}(0)) true we obtain by Reflection that x: N ⊢ x = Suc^{x}(0) : N which clearly is an extensional equality.

Equality reflection (Reflection) is intuitively appealing because it is valid in most models, in particular in the set-theoretic interpretation of type theory, and also because it leads to a single notion of equality in type theory. A serious disadvantage of extensional type theory is that judgemental equality and as a consequence type checking, i.e. the question whether a given judgement Γ ⊢ M = N : σ or Γ ⊢ M : σ holds, are undecidable. Intuitively, this is so, because a syntax-directed decision procedure for these judgements would have to “guess” the proof term P in the premise to rule Reflection. As any Π_{1}^{0} statement in Heyting arithmetic can be encoded as a certain identity type, inhabitation of identity types is at least as complex as provability of such statements. A rigorous proof of undecidability using recursively inseparable sets is given in [6]. Therefore, extensional type theory is not really in line with the Curry-Howard isomorphism because terms do not correspond to proofs, only typing derivations do. Other shortcomings of extensional type theory are that in the presence of a universe U non-normalising terms become typeable in inconsistent contexts (for example the fixpoint combinator may be typed in d: U , p: Id_{U} (d, d → d)) and— of a more aesthetic nature—that rule Reflection does not fit into the pattern of introduction and elimination rules. See, however, [10] for a formulation of Reflection as an η-like rule.

Probably for these reasons Martin-Löf has later on restricted judgemental equality to definitional expansion (definitional equality) and replaced rules Id-Uni and Reflection by his famous identity elimination rule which is motivated by the view of the identity type as an inductive family with sole constructor Refl.

The use of this elimination principle is described in detail in [9]. It is shown there, how it entails that propositional equality satisfies a Leibniz principle, that is if x: σ ⊢ τ[x] type and P : Id_{σ}(M_{1}, M_{2}) and N : τ[M_{1}] then one can construct a term Subst _{σ,τ} (M_{1}, M_{2}, P, N) : τ[M_{2}]. This Leibniz principle in turn allows one to show that propositional equality is an equivalence relation, i.e. if P : Id(M_{1}, M_{2}) then we can construct Sym (P) : Id(M_{2}, M_{1}) and for Q : Id(M_{2}, M_{3}) we get Trans (P, Q) : Id(M_{1}, M_{3}). Furthermore, it entails that Id is respected by all functions, i.e. if U : σ → τ then we find Resp (U, P) : Id(F M_{1}, F M_{2}).

Surprisingly, the intensional and extensional formulations of type theory have never been compared in the literature (to the best of our knowledge). This is the purpose of the present work. We first identify two principles which are provable in the extensional theory, but not in the intensional one and then embark on the proof that extensional type theory is conservative over the intensional one with these two principles added. We only sketch the formal argument here and refer the reader to [6] for a detailed proof.

We use a monomorphic presentation of type theory, i.e. terms with explicit type annotations, as in [9, Part III], however, without using a so-called Logical Framework, see also Sect. 3.

The material in this paper is mostly taken from the author’s PhD dissertation [6]. However, some simplifications (in particular the assumption of η-conversion for Π-types) have been made, and the example in Section 2 is new.

1.1 Functional extensionality

Suppose that Γ ⊢ U, V : Πx: σ.τ and Γ, x: σ ⊢ P : Id_{τ} (U x , V x). In extensional type theory we can conclude Γ ⊢ Id_{Πx:σ.τ} (U, V) true using Reflection, the congruence rule for λ, and η. In intensional type theory this is, however, in general not possible. A formal semantic argument for this may be found in [10]; intuitively one may argue that otherwise in the special case where Γ is empty we could deduce Id_{Πx:σ.τ} (U, V) true (from the existence of P above), but an identity type in the empty context can only be inhabited by a canonical element Refl(−), so U and V must be definitionally equal, which does not follow from the existence of the proof P which may have been obtained using induction. To achieve this principle called functional extensionality we add to intensional type theory a family of constants Ext_{σ,τ} (U, V, P) obeying the rule

\frac{\begin{matrix}Γ ⊢ U, V : Πx: σ.τ \\ Γ, x: σ ⊢ P : Id_{τ} (U x, V x) \end{matrix}}{Γ ⊢ Ext_{σ,τ} (U, V, P) : Id_{Πx:σ.τ} (U, V)} Ext-Form

1.2 Uniqueness of identity

Let M, N : σ and P, Q : Id_{σ}(M, N) be two proofs that M, N are propositionally equal. In extensional type theory it is an immediate consequence of Id-Uni that Id_{Id_{σ}(M,N)}(P, Q) true. Streicher has conjectured in [10] that this is in general not the case in intensional type theory and in [7] this has actually been proved by a semantic argument. So again, we are led to extend our axiomatisation of propositional equality in an intensional setting. It turns out that it is enough to consider the case where Q is in canonical form so that we introduce a family of constants

\frac{Γ ⊢ M : σ  Γ ⊢ P : Id_{σ}(M, M)}{Γ ⊢ IdUni _{σ}(M, P) : Id_{Id_{σ}(M,M)}(P, Refl_{σ}(M))} Id-Uni-I

to achieve uniqueness of identity. Axioms like Ext-Form and Id-Uni-I introduce non-canonical elements of all types in the empty context (not only of identity types). The constant Id-Uni-I can be endowed with an obvious reduction rule which eliminates all of its instances in closed terms of basic type. Things are more serious with Ext-Form since no reasonable reduction rule for these constants is known. However, in [5] we discuss a possibility for eliminating these non-canonical elements by translating the identity type into suitable equivalence relations. For the present work we shall simply regard Ext and IdUni as families of constants.

1.3 The intensional type theory TT_{I}

It is also noticed in [10] that in the presence of uniqueness of identity the elimination operator for Id can be defined in terms of its particular instance Subst mentioned above. Therefore, we shall take Subst as a primitive and define intensional type theory (TT_{I} for short) as dependent type theory with rules Id-Form, Id-Intro, Ext-Form, Id-Uni-I, and the following two rules for Subst .

\frac{\begin{matrix}Γ ⊢ P : Id_{σ}(M_{1}, M_{2}) \\ Γ, x: σ ⊢ τ[x] type  Γ ⊢ N : τ[M_{1}] \end{matrix}}{Γ ⊢ Subst _{σ,τ} (M_{1}, M_{2}, P, N) : τ[M_{2}]} Leibniz

\frac{Γ ⊢ Subst _{σ,τ} (M, M, Refl_{σ}(M), N) : τ[M]}{Γ ⊢ Subst _{σ,τ} (M, M, Refl_{σ}(M), N) = N : τ[M]} Leibniz-Comp

Recall that TT_{E} refers to extensional type theory defined by rules Id-Uni and Reflection above. Recall also that from Subst one may define operators Sym , Trans , and Resp , witnessing that Id is an equivalence relation compatible with function application.

In order to distinguish the intensional from the extensional type theory we write ⊢_{I} and ⊢_{E} for the two respective judgement relations.

The operators of TT_{I} are definable in TT_{E}, for example Subst is simply the identity in TT_{E}. More formally, we can define a “stripping map” | − | by

|Subst _{σ,τ} (M_{1}, M_{2}, P, N)| := |N| |IdUni _{σ}(M, P)| := Refl_{Id_{|σ|}(|M|,|M|)}(Refl_{|σ|}(|M|)) |Ext_{σ,τ} (U, V, P)| := Refl_{Πx:|σ|.|τ|}(|U|) homomorphically extended to all other terms, types, contexts, and judgements

Notice that Γ = |Γ | if Γ does not contain Subst , Ext, or IdUni . This mapping enjoys the following trivial soundness property

Proposition 1 If Γ ⊢_{I} J then |Γ | ⊢_{E} |J| for all contexts Γ and judgements J.

2 Conservativity of TT_{E} over TT_{I}

We are now interested in a converse of the above proposition; more precisely, we shall establish the following conservativity property.

Theorem 2 If Γ ⊢_{I} σ type and |Γ | ⊢_{E} M : |σ| for some M then there exists M′ such that Γ ⊢_{I} M′ : σ.

Before sketching the proof of this theorem we shall illustrate its strength by an example suggested by Thomas Schreiber. The crux of this example is to show how the lack of equality reflection in TT_{I} can be inconvenient when one wants to actually program with dependent types rather than use type dependency merely to express constructive predicate logic.

We assume a type Bool with two canonical elements true : Bool and false : Bool. We use the following slightly unconventional elimination rule which is expressible in terms of the usual one, see [9, Ch. 21]

\frac{Γ, b: Bool ⊢ σ type Γ ⊢ B : Bool Γ, p: Id_{Bool}(B, true) ⊢ T : σ[true/b] Γ, p: Id_{Bool}(B, false) ⊢ E : σ[false/b]}{Γ ⊢ if′_{[b:Bool]σ}(B, [p: Id_{Bool}(B, true)]T, [p: Id_{Bool}(B, false)]E) : σ[B/b]} Bool-E

Notice that the free variables b in σ and p in T, E, respectively, become bound in the if′ expression. This elimination operator comes with the following two computation rules:

\frac{Γ ⊢ if′_{[b:Bool]σ}(true, [p: Id_{Bool}(true, true)]T, [p: Id_{Bool}(true, false)]E) : σ[true/b]}{Γ ⊢ if′_{[b:Bool]σ}(true, [p: Id_{Bool}(true, true)]T, [p: Id_{Bool}(true, false)]E) = T [Refl_{Bool}(true)/p] : σ[true/b] Bool-C-T}

\frac{Γ ⊢ if′_{[b:Bool]σ}(false, [p: Id_{Bool}(false, true)]T, [p: Id_{Bool}(false, false)]E) : σ[false/b]}{Γ ⊢ if′_{[b:Bool]σ}(false, [p: Id_{Bool}(false, true)]T, [p: Id_{Bool}(false, false)]E) = E[Refl_{Bool}(false)/p] : σ[false/b] Bool-C-F} Suppose that we are given a type Loc of locations together with an equality function eq : Loc → Loc → Bool and a proof term

eq correct : Πl, l′: Loc.Id_{Loc}(l, l′) ↔ Id_{Bool}(eq l l′, true)

witnessing that eq is indeed an equality function on Loc. The terms eq and eq correct may either be implemented or declared in some ambient context Γ. Furthermore, we assume a type Data depending on Loc, i.e. we have Γ ⊢ Data(M) type whenever Γ ⊢ M : Loc. We make the definition

Store = Πl: Loc.Data(l)

and our aim is to find a term

update : Πl_{0}: Loc.Πd: Data(l_{0}).Πs: Store.Store

which given l_{0}, d, s returns a store whose value at l_{0} equals d and (s l) at l ≠ l_{0}. In TT_{E} we can easily construct such an update function by

update = λl_{0}: Loc.λd: Data(l_{0}).λs: Store.λl: Loc.

if′_{[b:Bool]Data(l)}(eq(l_{0}, l) , [p: Id_{Bool}(eq(l_{0}, l), true)]d , [p: Id_{Bool}(eq(l_{0}, l), false)](s l))

The important point here is that in TT_{E} we have Data(l_{0}) = Data(l) in the presence of p: Id(eq(l_{0}, l), true) by virtue of eq correct. Therefore, we have d: Data(l) and the first branch of the if′ expression type-checks.

Write

update type = Πl_{0}: Loc.Πd: Data(l_{0}).Πs: Store.Store

and for f: update type

update spec(f) = (Πl_{0}: Loc.Πd: Data(l_{0}).Πs: Store.Id_{Data(l_{0})}(f l_{0} d s l_{0} , d)) × (Πl_{0}: Loc.Πd: Data(l_{0}).Πl: Loc.(Id_{Loc}(l, l_{0})→⊥) → Id_{Data(l)}(f l_{0} d s l , s l))

where ⊥ is the empty type. We can readily establish

Γ ⊢_{E} update spec(update) true

using if′ and equality reasoning.

Now assuming that Loc and Data already make sense in intensional type theory we can apply the conservativity theorem to the type

σ = Σf: update type.update spec(f)

giving us an update function in TT_{I} which also satisfies update spec. Coming up with such a function is not too difficult, indeed we may choose update’= λl_{0}: Loc.λd: Data(l_{0}).λs: Store.λl: Loc.

if′_{[b:Bool]Data(l)}(eq(l_{0}, l) , [p: Id_{Bool}(eq(l_{0}, l), true)]Subst _{Loc,Data}(l_{0}, l , ((eq correct l_{0} l).2 p) , d) , [p: Id_{Bool}(eq(l_{0}, l), false)](s l))

where the projection .2 yields the ←-part of eq correct, hence the first argument to Subst is of type Id_{Loc}(l_{0}, l). The conservativity theorem does not necessarily give us this very update function, but we can also use it to obtain a proof of correctness of the latter. To that end we consider the type

σ = update spec(update′)

We have |σ| = update spec(update) so Γ ⊢_{E} |σ| true and hence Γ ⊢_{I} σ true giving us the desired correctness proof for our particular function update′. Constructing such proof directly requires quite some effort as the function in question contains an instance of Subst . In this case the author has been able to construct such a proof using the Lego system. This revealed that the use of Ext can be avoided here and that IdUni is only used for the particular type Loc. As observed by Michael Hedberg IdUni is definable from Martin-Löf’s elimination rule for types with decidable equality (such as Loc) so that this example can be carried out in pure intensional Martin-Löf type theory without the additional constants Ext and IdUni .

It was pointed out by one of the referees that in the presence of patternmatching like in ALF [1] the complicated equality reasoning in the example can be avoided if one replaces eq and eq correct by a single constant

eq′ : Πl, l′: Loc.Id_{Loc}(l, l′) + (Id_{Loc}(l, l′) → ⊥)

One may then define update by pattern matching over eq′(l, l_{0}) and in the positive case we may then assume that l and l_{0} are judgementally equal. It is not clear, however, how this technique can be applied in general, in particular, the example in [6] and briefly mentioned in Section 3 does not seem to be amenable to a simple development using pattern-matching.

Proof of Thm. 2 (Sketch). The proof is based on two main ingredients. First, we observe that a consequence of this conservativity property is that types σ and σ′ which are equal in TT_{E} must be isomorphic in TT_{I} . To see this consider the type

\begin{matrix}ρ := Σf: σ → σ′.Σf^{−1}: σ′ → σ. \\ Id(λx: σ.f^{−1}(f x), λx: σ.x) × Id(λx: σ′.f(f^{−1} x), λx: σ′.x) \end{matrix}

If ⊢_{E} |σ| = |σ′| then |ρ| is inhabited by two instances of the identity function together with two instances of reflexivity. So a proof of Theorem 2 must embody a construction of these isomorphisms. Now the only way to deduce judgemental type equalities in TT_{E} is by using congruence rules and Reflection in the case of type formers containing terms like the identity type. So we can compute these isomorphisms directly by induction on the structure of any two types σ and σ′ without using conservativity in the first place.

The second ingredient is a general method for establishing conservativity between type theories. Generalising from Thm. 2 we call an extension T′ of some type theory T conservative over T if whenever a type of T is inhabited in T′ then it is already inhabited in T.

Proposition 3 Let T be a type theory and T′ an extension of T. T′ is conservative over T if and only if there exists a model Q of T′, hence of T, such that the interpretation of T in this model is full (surjective).

Proof. Suppose that σ is a type of T such that σ is inhabited in T′ by some term M. The interpretation of M in Q yields a “semantic term” of the interpretation of σ in Q which by fullness gives a term of type σ in T. For the converse we let Q be the term model of T′

At this level of generality the argument is too informal so as to be of direct use. It only serves us as a guideline which the reader is invited to bear in mind. The theories T and T′ are TT_{I} and TT_{E}, respectively, where a slight complication results from the fact that TT_{E} is not literally an extension of TT_{I} , but that we have an interpretation of one in the other, namely the stripping map. The role of “models” is played by categories with families in the sense of Dybjer [2, 4] or any other category-theoretic notion of model for type theory. For the purpose of this abstract it suffices to know that such a structure provides domains of interpretation for contexts, types, and terms^{1}, and comes with semantic type and term formers operating on these semantic objects. An interpretation function can then be defined which maps syntactic contexts, types, terms to their semantic companions and translates syntactic type and term formers into the corresponding semantic ones. Judgemental equality is then modelled by set-theoretic equality of semantic objects. Factoring the syntax by judgemental equality yields a particular model: the term model. The interpretation of the syntax in a some model induces a unique structure preserving map from the term model to this model. The model Q we use is a quotient of the term model of TT_{I} by propositional equality where in addition we identify types and contexts which are canonically isomorphic in the sense described above, i.e. which become equal in TT_{E}.

Let us now look at some of the details. In order to define the canonical isomorphisms between types one also needs to consider isomorphisms between contexts to get the inductive definition through. In order to specify those we extend propositional equality to contexts and context morphisms (substitutions) using Σ-types. It turns out that for this extension the same combinators as for ordinary propositional equality can be defined. Then by simultaneous induction on contexts and types we construct possibly undefined “isomorphism candidates” between any two contexts and types. That is, for contexts Γ, Δ we have a (possibly undefined) context morphism (a |Δ|-tuple of terms) co_{Γ,Δ} : Γ → Δ

1 … and substitutions, but we gloss over this point here.

which if defined possesses an inverse up to propositional equality. For types Γ ⊢_{I} σ type, Δ ⊢_{I} τ type we have a (possibly undefined) term

Γ, x: σ ⊢_{I} ty_{Γ,Δ,σ,τ} [x] : τ[co_{Γ,Δ}]

which—if defined—is an isomorphism w.r.t. propositional equality. We use square brackets to denote (generalised) substitution, i.e. if f : Γ → Δ and Δ ⊢ σ type then Γ ⊢ σ[f] type and similarly for other judgements. The isomorphism between contexts of different length is always undefined and between contexts of the same length it is obtained from the isomorphisms between types. An isomorphism between types can only be defined if they share the same outermost type former. In the case of Π and Σ-types the isomorphism is the obvious lifting of the isomorphism for the respective components. Functional extensionality is used to verify the isomorphism property in the case of Π-types. The interesting case is where σ and τ are identity types. For simplicity we assume that they are both in the same context and over the same type. I.e. let Γ ⊢_{I} M_{1}, M_{2}, N_{1}, N_{2} : ρ and put σ = Id_{ρ}(M_{1}, M_{2}) and τ = Id_{ρ}(N_{1}, N_{2}). The isomorphism

Γ, p: Id_{ρ}(M_{1}, M_{2}) ⊢_{I} ty_{Γ,Γ,σ,τ} [p] : Id_{ρ}(N_{1}, N_{2})

is defined iff M_{1}, N_{1} and M_{2}, N_{2} are propositionally equal. In this case we pick Γ ⊢_{I} P_{1} : Id_{ρ}(M_{1}, N_{1}) and Γ ⊢_{I} P_{2} : Id_{ρ}(M_{2}, N_{2}) and set

ty_{Γ,Γ,σ,τ} [p] := Trans (Trans (Sym (P_{1}), p), P_{2})

Notice that in this case ty is defined w.r.t. some arbitrary choice of these proofs P_{i}. The isomorphism property is readily established using IdUni .

Having defined these isomorphisms we construct a model of TT_{E} in which

– contexts are equivalence classes of contexts, two contexts being identified if the isomorphism between them is defined,

– types in context [Δ]_{∼} are equivalence classes of pairs (Γ, σ) where Γ ∈ [Δ]_{∼}, and Γ ⊢_{I} σ type, and two such pairs are identified if the corresponding ty-isomorphism is defined,

– terms of type [(Δ, τ)]_{∼} are equivalence classes of triples (Γ, M, σ) where (Γ, σ) ∈ [(Δ, τ)]_{∼}, and Γ ⊢_{I} M : σ, and two such triples (Γ, M, σ) and (Γ′, N′, σ′) are identified if

Γ ⊢ Id_{σ′}(ty_{Γ,Γ′,σ,σ′}[M] , M′[co_{Γ,Γ′}]) true

i.e., if M and M′ with suitably adjusted source and target are propositionally equal in TT_{I} .

We have used here the notation [−]_{∼} for equivalence classes associated to a representative.

Now we prove that this structure, which we call Q, does indeed form a model of TT_{E} and that in particular the required semantic type and term formers are given by applying their syntactic companions (in TT_{I} ) to equivalence classes. Here Ext and IdUni are used to show that various settings are independent of the choice of representatives and thus are well-defined on equivalence classes. For example, if [(Γ, M, σ)]_{∼} and [(Γ′, N′, σ′)]_{∼} are two semantic terms of (semantic) type [(Δ, σ)]_{∼} then we define the associated identity type as the equivalence class of the pair of Γ and

Γ ⊢ Id_{σ′}(ty_{Γ,Γ′,σ,σ′}[M] , M′[co_{Γ,Γ′}]) type

Since we have defined equality of terms in Q precisely as inhabitedness of this type the rule Reflection is valid in Q. Uniqueness of identity is required here to show that this setting is independent of the chosen representatives (Γ, M, σ) and (Γ′, N′, σ′).

The above can be summarised by the following diagram of structure preserving maps between models.

Q

[figure: [[−]]_{I}; [−]_{∼}; [[−]]_{E}]

TT_{I}  \overline{| − |} TT_{E}

where TT_{I} and TT_{E} refer to the term models of the respective type theories. [[−]]_{I} and [[−]]_{E} denote the interpretations of TT_{I} and TT_{E} in Q, which being a model for TT_{E} also models TT_{I} . Finally, [−]_{∼} : TT_{I} → Q is the projection map associating equivalence classes which is structure preserving by definition of Q.

By induction on derivations or—more elegantly—by an initiality argument we find that all three structure preserving maps from TT_{I} to Q are equal, more precisely, we have

[−]_{∼} = [[−]]_{I} = [[−]]_{E} ∘ | − |  (1)

Intuitively, we can now argue that the interpretation of TT_{I} in Q is surjective because we have characterised it as the projection associating equivalence classes and then apply Prop. 3. More formally, suppose that Γ ⊢_{I} σ and |Γ | ⊢_{E} M : |σ|. Let [[M]]_{E} = [(Γ′, M′, σ′)]_{∼} be the interpretation of M in Q. By definition, we have Γ′ ⊢_{I} M′ : σ′. Moreover, by Eqn. 1 we find

[Γ]_{∼} = [[|Γ |]]_{E} = [Γ′]_{∼}

and

[(Γ, σ)]_{∼} = [[|(Γ, σ)|]]_{E} = [(Γ′, σ′)]_{∼}

This in turn implies that co_{Γ,Γ′} and ty_{Γ,Γ′,σ,σ′} are defined. Therefore, we have

Γ ⊢_{I} ty^{−1}_{Γ,Γ′,σ,σ′}[M′[co_{Γ,Γ′}]] : σ

giving the desired inhabitant of σ in TT_{I} . □

We remark that we can even show that the stripping of the thus constructed inhabitant of σ is equal to M in TT_{E} by showing that the stripping map respects the equality in Q and thus lifts to a structure preserving map from Q to TT_{E} which again by initiality must be a left inverse to [[−]]_{E}. We refer to [6] for details.

3 Discussion

Although relatively complex, the described method is fairly robust w.r.t. extensions of the type theory. For it to be extensible to a new type former it is enough that this type former admits an action on propositional isomorphisms. In [6] we demonstrate this by adding quotient types and a universe. We remark, however, that this condition is not met in the presentation of type theory using the Logical Framework in the sense of [9, Part III]. The reason is that there we can have variables of type Set → Set which act as completely unspecified type formers. Nevertheless, it is plausible that Thm. 2 continues to hold in this case. A possible proof could use a one-step definition of the isomorphism candidates by which for example the isomorphism ty_{Γ,Γ,σ,τ} would be defined iff there exists a context Δ, a type ρ, and context morphisms f, g : Γ → Δ such that Γ ⊢_{I} σ = ρ[f], Γ ⊢_{I} τ = ρ[g], and f, g are (component-wise) propositionally equal. We leave the details to a future paper.

We also point out the non-constructive nature of the proof. Not only has the axiom of choice been used in the definition of the canonical isomorphisms co and ty; more seriously the interpretation of TT_{E} in Q associates equivalence classes to contexts, types, and terms. In order to get an inhabitant of type σ in the proof above we must arbitrarily choose a representative of the corresponding class. We have done so implicitly by writing [[M]]_{E} = [(Γ′, M′, σ′)]_{∼}. So the present proof does not directly give rise to an algorithm which effectively computes an inhabitant of σ from a derivation of |σ| true in TT_{E}. Now such algorithm trivially exists by Markov’s principle, that is we simply try out all possible terms and derivations and from the non-constructive proof of existence we know that this search always succeeds. But of course, one would like a more efficient algorithm which makes use of the given derivation in TT_{E}. It is, however, not clear whether the described argument gives rise to one such. An idea would be to carry out the construction of Q in some “setoid model” where quotients come with a canonical choice of representatives. This is, however, not possible using a semantics which interprets judgemental equality as set-theoretic extensional equality as we have done.

It appears that a constructivisation of the result could give rise to tactics facilitating theorem proving in TT_{I} , the idea being that parts of a proof or program development could be carried out in TT_{E}. The resulting derivation would then be automatically translated into TT_{I} . In [6] we give a proof in TT_{E} of a theorem of Mendler’s stating that the dependent sum (Σ) preserves limits of ω-chains. Although the proof in TT_{E} is relatively straightforward it was despite considerable effort so far not possible to obtain a fully formal development in TT_{I} . The reason was that in this case one has to prove a property about a term which contains instances of Subst inside a primitive recursion over natural numbers rather than just booleans as in the case of the update function above. Given sufficient time and energy one could certainly push this proof through, but a systematic treatment based on the conservativity result would seem to save much work in such cases.

We remind the reader that the conservativity result applies to intensional type theory with functional extensionality and uniqueness of identity added. Another issue is the conservativity of the latter two over pure intensional type theory or rather the characterisation of those types and contexts for which they are conservative. This question remains unanswered and is left for future research. A brief discussion of the topic may be found in [6].

Judgemental equality has played a minor role in the present proof and it appears that the whole development would go through if TT_{I} was replaced by a type theory without judgemental equality at all and rules like β or Leibniz-Comp replaced by corresponding constants of identity types in the style of IdUni. The construction of the model Q would remain unchanged since propositionally equal objects are identified in Q, some care has to be taken, however, with the extension of propositional equality to contexts.

This generalisation would also answer affirmatively the question of conservativity of the original TT_{I} over this new type theory without judgemental equality.

Acknowledgement. I wish to thank Thomas Streicher and the anonymous referees for suggesting improvements of an earlier draft.

References

1. Thorsten Altenkirch, Veronica Gaspes, Bengt Nordström, and Björn von Sydow. A User’s Guide to ALF. Chalmers University of Technology, Sweden, May 1994. Available on the WWW: file://ftp.cs.chalmers.se/pub/users/alti/alf.ps.Z.

2. Peter Dybjer. Internal type theory. In Proc. BRA TYPES workshop, Torino, June 1995, Springer LNCS, 1996. To appear.

3. Solomon Feferman. Theories of finite type. In Jon Barwise, editor, Handbook of Mathematical Logic, chapter D.4. North-Holland, 1977.

4. Martin Hofmann. Syntax and sematnics of dependent types. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation. Cambridge University Press, 199?

5. Martin Hofmann. Elimination of extensionality for Martin-Löf type theory. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs. Springer, 1994. LNCS 806.

6. Martin Hofmann. Extensional Concepts in Intensional Type Theory. PhD thesis, Univ. of Edinburgh, 1995.

7. Martin Hofmann and Thomas Streicher. A groupoid model refutes uniqueness of identity proofs. In Proceedings of the 9th Symposium on Logic in Computer Science (LICS), Paris, 1994.

8. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis·Napoli, 1984.

9. B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf’s Type Theory, An Introduction. Clarendon Press, Oxford, 1990.

10. Thomas Streicher. Semantical Investigations into Intensional Type Theory. Habilitationsschrift, LMU München, 1993.

This article was processed using the L^{A}TEX macro package with LLNCS style