When considering the "perversities" of Martin-Loef's intensional identity types I came across the following problem. Let C be a contextual category (in the sense of Cartmell, see e.g. his paper in APAL) with perhaps some additional structure such as sums or products of familie s of types (see e.g. Chapter III of his Cartmell's Thesis or my Thesis for a mor e recent reference) then we say that C has weak intensional identity types iff w e have the following structure : for any object I of C different from the canonical termina object of level 0 there is a choice of an object Id(I) |> p(I)*I and a morphism r(I) : I -> Id(I ) such that (1) p(Id(I)) o r(I) = delta(I) : I -> p(I)*I where p(p(I)*I) o delta(I) = id(I) and q(p(I),I) o delta(I) = id(I), i.e. delta(I) is the fibrewise diagonal and (2) for any object A |> p(I)*I and morphism f : I -> A with p(A) o f = delta(I) there is a choice J(f) : Id(I) -> A of a morphism such that J(f) o r(I) = f and p(A) o J(f) = p(Id(I)) and (3) the Beck condition is satisfied for these data, i.e. for any morphism g : K -> J where I |> J we have g*Id(I) = Id(g*I) g*r(I) = r(g*I) g*J(f) = J(g*f) for any morphism f : delta(I) -> p(A) . Notice that the weakness arises from the restriction that A |> p(I)*I instead of A |> Id(I), i.e. the family for which one considers J-elimination does not depend on a proof object of type Id(I). This definition of weak intensional identity types is nearly literally the sameas the one given by Lawvere in his famous paper from 1970 Equality and Comprehension as Adjoint Functors. The only difference is that we are working in a framework somewhat more special than hyperdoctrines and that we do not require uniqueness of elemination. My PROBLEM now is that up to now I have been unable to find a contextual catego- ry with, say products of families of types, where one can NOT define weak inten- sional identity types. I have found a model where one has weak intensional identity types, but not stro ng ones. Simply take as types the set of all closed lambda terms modulo beta- conversion and and the empty set. But to get rid even of weak intensional identity types seems to be much harder for the following reasons. As soon has one can embed a contextual category of the kind considered above in- to a model of the calculus of constructions where the old types are exactly the propositions now, then one can define weak intensional identity types by Leibniz equality ! If one considers models where no real type dependency occurs then one can intro- duce even strong intensional identity types by putting Id(A,t,s) = N1, the type containing exactly one element.Especially, that means that if one considers int- ensional identity types then there no real need for type dependency arises !! We are back at old-fashioned Kleene realisability. Now what could be a way out of this dilemma. There are 2 possibilities (at least I guess) : (1) find a collection TYPE of pers on the natural numbers or some other partial combinatory algebra such that the product of a family of pers in TYPE inde xed over some per in TYPE is guaranteed to be in TYPE again BUT that's not so easy as - TYPE must not be reflective and - the collection of pers having only finitely many equivalence classes does not do the job of providing a counterexample as well (2) the other possibility is to consider the model where types are arbitrary cpo-s, i.e. posets where any directed subset has a supremum, without any requirements as being finitely based or so and families of types are continuous fibrations. This model surey gives rise to a contextual category with products of families of types. But up to now I have'nt been able to see that one cannot find weak intensio al identity types within that model. It si not so easy as if one restricts oneself to Scott domains then one has even strong intensional identity types (see a paper in APAL by Palmgren & Stoltenberg-Hansen following a suggestion of Martin-Loef himself). The trick is to define for a Scott domain D and objects d1, d2 in D the domain Id(D,d1,d2) as the collection of all objects d approximating BOTH d1 and d2. Of course, this trick can be made whenever the cpo has suprema of bounded subsets ! But what happens in the case that there are several different best approxi- mating elements to a given couple of elements ??? Even if the concept of intensional identity types seems to be a little bit stran ge from the point of view of "non-split" category theory, I think it makes per- fectly good sense from the point of view of "split category theory", namely con- textual categories. Therefore I'd more than appreciate any hints on this problem. For those which are more interested in the topic I have some notes on identity types in ITT. Unfortunately they are not typed in a way that I can easily put them on e-mail, but I could easily distribute them by ordinary mail or fax. Thomas Streicher