weak intensional identity types

29 Dec 1990

      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