TRULY INTENSIONAL MODELS OF TYPE THEORY ARISING FROM MODIFIED REALIZABILITY The definition of what is a model structure for intensional Martin-Loef Type Theory has been given by John Cartmell in his Thesis (Oxford 1978). Essentially it is like semantics for extensional type theory with the only exception that one drops uniqueness constraints and replaces them by the constraint that Eliminators are preserved by substitution. There has been described quite a lot of models for extensional type theory mainly based on the idea of Kleene realizability. The most important structure in this context is the category of so called realizability sets which we will refer to by r-Set and the full reflective internally complete subcategory PER. It seems to be impossible to find truly intensional models for type theory in this setting as extensionality is built in almost by definition. (Extensionality for me means that the terminal object is a generator). But instead of considering a category of Kleene realizability sets one can also build a category based on KreiselBs Modified Realizability. Whereas in Kleene realizability propositions are considered as arbitrary sets of natural numbers the key idea of modified realizability is to endow any such set A of natural numbers with a subset B . The set A has to be thought of as the collection of potential realizers and the subset B as the collection of ACTUAL REALIZERS. This intuitive idea can be lifted to realizability sets. Based on the category r-Set of realizability sets we construct a category mr-Set of so called "modified realizability sets". Description of mr-Set : objects : triples ( X , d(X) , r(X) ) such that (1) X is a set (2) d(X) is a subset of X (objects in d(X) will be called "defined") (3) ( X , r(X) ) is an r-set , i.e. r(X) is a relation between natural numbers and X such that for any x in X there is a natural number n with n r(X) x morphisms : a morphism from ( X , d(X) , r(X) ) to ( Y , d(Y) , r(Y) ) is a set-theoretic function f : X -> Y such that (1) f (x) is in d(Y) provided that x is in d(X) (i.e. f preserves actual realizers !) (2) f is a morphism from ( X , r(X) ) to ( Y , r(Y) ) in r-Set ( i.e. there is a natural number n such that for all x in X and m with m r(X) x : {n}(m) is defined and {n}(m) r(Y) f(x) ) . More abstractly the category mr-Set can be described as the result of the Grothendieck construction applied to the fibration of REGULAR MONOs in r-Set over r-Set . The category r-Set is a full reflective subcategory of mr-Set by the embedding sending ( X , r(X) ) to ( X , X , r(X) ) . THEOREM Just as r-Set is locally cartesian closed so is mr-Set. The category mr-Set is not extensional. Proof : Obviously, mr-Set has finite limits. The Pi-s are computed as in r-Set , BUT elements are defined iff they preserve definedness. The underlying r-set of the terminal object in mr-Set is the terminal object in r-Set and all elements are defined. Of course, there exist two different parallel morphisms in mr-Set which coincide on defined elements and such morphisms cannot be separated by global elements, i.e. morphism whose source is the terminal object. As mr-Set is left exact it constitutes a model of extensional type theory. Nevertheless we can interpret intensional identity typs in a way such that they do not fulfill the laes of extensional identity types. For this purpose we consider mr-Set as a model of the ambient logical framework. For what Martin-Loef calls "constructive set theory" we have to identify a certain full subcategory of mr-Set. DEFINITION A small set is an object ( X , d(X) , r(X) ) in mr-Set such that (1) n r(X) x1 and n r(X) x2 implies x1 = x2 (2) for some object x in X we have 0 r(X) x . In the sequel we shall need two distinguished small sets : Succeed = ( {e , r} , {r} , { ( 0 , e ) , (1 , r ) }) and Fail = ( {e} , {} , { (0,e) } ) . Now we shall interpret Martin-Loefs identity types in mr-Set in such a way that they do not satisfy the laws of extensional identity types. If A is a small set and a1 , a2 are objects of the underlying set of A then Id A a1 a2 = Fail if a1 and a2 are different Id A a a = Succeed . For any small set A and a in A (not necessarily defined!) r A a = r . Finally we give the definition of the elimination operator J . Given A : Set and a family C : {a1 , a2 : A} {c : Id A a1 a2} Set and a function d : {a : A} C a a (r A a) the function J A C d : {a1 , a2 : A} {c : Id A a1 a2} C a1 a2 c is defined as follows J A C d a a r = d a J A C d a1 a2 e = the unique object in C a1 a2 e realized by 0 . Obviously, J is realizable as one simply performs a decidable case analysis on the realizer for the lasr argument. THEOREM The following sequents are NOT valid in this model : (1) A : Set , x : A , y : A , z : Id A x y |- x = y : A [ but, of course, theer is a term t such that A : Set , x : A , y : A , z : Id A x y |- t : Id Ax y : A ] (2) A : Set , C : A -> Set , x : A , y : A , z : Id A x y |- C x = C y [ put for A a small set with at least two different objects a and b where a is assumed to be defined and for C the family [x:A] Id A a x ; then we have Id A a a = Succeed but Id A a b = Fail although e : Id A a b ] . (3) The socalled Equality Reflection Lemma (terminology of LuoBs Thesis) holds If |- p : Id A t s is valid in the model then |- t = s : A is valid in the model, too. (The restriction to the empty context is important, see (1) ! The interpretation of the empty context contains one defined and no undefined object ! ). THEOREM In the model defined above the principle of extensionality {A,B : Set} {f,g : A->B} ({x:A} Id B (f x) (g x)) -> Id (A->B) f g is NOT realized !! Proof : by a continuity argument !! //** In General Leibniz Equality is different from Martin-Loef Idenity Types **// Interpret Prop as small sets and interpret Type(0) as those mr-sets where the underlying r-set is a per. Then both Prop and Type(0) are closed under arbitrary internal products. In Type(0) we can interpret (even extensional) Martin-Loef identity types as we have mr-sets whose underlying r-set is empty. On the other hand we can define Leibniz equality employing Prop . Now let A be a type containing ar least two different defined elements a1 and a2 . Then LE A a1 a2 is in Prop containing no defined element BUT surely a nondefined element realized by 0 . Id A a1 a2 contains not even an undefined element. Therefore there cannot exist a morphism from LE A a1 a2 to Id A a1 a2 !! Thomas Streicher