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

[James Chapman]

I was under the impression that one could trace back the first uses of
induction-recursion by Martin-Löf to the informal metatheoretic
definitions of strong computability predicates in normalization proofs
such as the one reprinted in "Twenty Five Years of Constructive Type
Theory". A book I used to have until I made the fatal error of lending
it to a certain Professor Ghani.

The below citation taken from P. Dybjer, and A. Setzer:
Induction-Recursion and initial algebras:

P. Martin-Löf. An intuitionistic theoy of types. In G. Sambin and J. Smith,
editors, Twenty-Five Years of Constructive Type Theory, pages 127–172. Ox-
ford University Press, 1998. Reprinted version of an unpublished report from
1972.

Best wishes,

James


On Wed, Feb 2, 2011 at 9:11 AM, Peter Dybjer <peterd at chalmers.se> wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>