RE: [Agda] Universes à la Tarski and induction-recursion

[Peter Dybjer]

Hi Dan,

Let me just tell you my recollection of discussions with Martin-Löf and colleagues here in Gothenburg in the 1980s.

The universe a la Tarski appeared for the first time, I believe, in the book Intuitionistic Type Theory (Bibliopolis) from 1984. It was based on lectures in Padova given in 1980. Previously, universes were a la Russell. Aczel had a universe a la Tarski in his 1974/1977 paper about the Interpretation of Martin-Löf Type Theory in a First Order Theory of Combinators.

You are quite right that in Bibliopolis and Martin-Löf's papers from the 1970s there is no universe elimination rule. But I recall discussions with him at the time (early and mid 1980s) where he entertained the possibility. I believe universe elimination is included in the book by Bengt Nordström, Kent Petersson, and Jan Smith.

The discussion revolved around the issue whether a universe should be considered to be open, in the sense that a new type former could be added whenever there is a need for it. And as soon as you have universe elimination you close the universe, there is no longer a possibility of adding new type formers. 

Martin-Löf has also expressed the view that the decoding in a universe a la Tarski is the proper elimination rule. One should not consider an eliminatin rule beyond that.

The basic idea of induction-recursion is that constructions such as the universe a la Tarski and similar things, are indeed to be viewed as closed, and an inductive-recursive definition comes with an elimination rule, so that you can define functions on U after simultaneously having defined U and T.

Personally, I have a position on the "closed vs open universe" issue, but I don't have time at the moment to expand on it. Anyway, it's philosophy.

Peter
________________________________________
From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] On Behalf Of Dan Doel [dan.doel at gmail.com]
Sent: Tuesday, February 01, 2011 8:07 AM
To: agda at lists.chalmers.se
Subject: [Agda] Universes à la Tarski and       induction-recursion

Greetings,

Not long ago, I was gearing up to explain induction-recursion somewhere, and I
happened upon an (I think) interesting observation, so I thought I'd share it
here.

It's common (I think) to suggest that the prototypical example of induction-
recursion is Martin-Löf's universe à la Tarski. And indeed, we can define a
universe with the same codes. In Agda, it looks like:

  mutual
    data U : Set where
      n     : U
      fin   : ℕ → U
      _+_   : U → U → U
      i     : (s : U) → T s → T s → U
      π σ w : (s : U) → (T s → U) → U

    T : U → Set
    T n         = ℕ
    T (fin k)   = Fin k
    T (s + t)   = T s ⊎ T t
    T (i s x y) = x ≡ y
    T (π s f)   = (x : T s) → T (f x)
    T (σ s f)   = Σ (T s) (\x → T (f x))
    T (w s f)   = W (T s) (\x → T (f x))

However, I happened to look back at a set of Martin-Löf's lecture notes from
the 80s, and I noticed the following: there are no elimination rules given for
U. And in this sense, the above inductive-recursive universe diverges from the
original formulation.

Without the elimination rule, the universe behaves much like the built-in
universes in Agda. For instance, we know that if:

  f : (A : Set) → A → A

then f must be the identity function. We don't know this, however, for:

  f : (a : U) → T a → T a

for the above inductive-recursive universe. f could inspect its first
argument, and do different things based on its value. However, with the
original U given by Martin-Löf, we again know that f must be the identity
function, because no inspection of U is possible. In other words, functions
(other than T) must be parametric in arguments of type U.

I don't really have any moral to end this up with. I just thought it was
interesting that the prototypical example of induction-recursion doesn't
actually appear to match up precisely with actual i-r.

Thoughts?

-- Dan
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda