universe-polymorphic assumptions

[Michael Shulman]

For implementing the general theory of higher modalities in type
theory, it is very useful to be able to make universe-polymorphic
assumptions. For instance, among the data of a modality is an
operation

O : Type -> Type

which should be regarded as a universe-polymorphic operation on
*every* universe rather than a single operation on a single universe.
In particular cases, such as the n-truncation modality, we do have
such a universe-polymorphic operation, and sometimes it matters that
we can apply it at different universe levels. However, if we want to
prove statements of the form "for any modality, ...", ordinary type
theory doesn't allow "a modality" to contain universe-polymorphic
operations, since then there would be no universe large enough for the
type of modalities to live in.

As explained here:
http://homotopytypetheory.org/2015/07/05/modules-for-modalities/
I have found a way to do this in Coq, using the fact that fields of
modules can be universe-polymorphic. Rather than defining a modality
as a Record, we define it as a Module Type, and individual modalities
as instantiating Modules. Then the general theory of modules can be
developed inside a module parametrized over an arbitrary module (O :
Modality), and instantiated at any particular example.

However, Coq modules are fraught with annoyances and (I'm told) make
the kernel much more complicated for (in most cases) little benefit,
so implementors of new proof assistants (such as Lean) are
understandably leery of mimicking them. But is there a better way to
enable universe-polymorphic assumptions? I feel like what we want is
some way to reify the metatheory without changing the strength of the
object theory, analogous to the proper classes in NBG set theory.
Perhaps what we need is a way for the user to hypothesize and
manipulate metavariables? Any ideas?

Mike

[Jason Gross]

This is kind-of heavy-weight, but if we formalize all of the ambient theory as syntax, then we can prove such theorems about the syntax, and although we can't interpret the syntax into the universe in general, we can do it on a case-by-case basis, e.g., with ltac.  (I'm working on such a formalization in my spare time, with the end goal being to prove Lob's theorem / write a well-typed quine.)  Presumably with enough syntactic sugar, writing in the metatheory will be just as easy as writing in the object theory.

-Jason

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Martin Escardo]

I think the problem is not Coq (or Agda), but rather that the official
type theories underlying them only allow schematic definitions on the
universe (i.e. indexed by external natural numbers only), as for
instance the type theory described the appendix of The Book.

Even the notion of a natural numbers type (NNT) causes problems, when
a NNT is given hypothetically, if we want our NNT to eliminate in all
universes. Agda does allow that, but this is not part of any version
of MLTT in the literature. Here are two ways:

\begin{code}

open import Agda.Primitive using (Level ; lzero ; lsuc ; _⊔_)

U : {l : Level} → Set(lsuc l)
U {l} = Set l

U₀ = U{lzero}

-- Introduces hypothesis using a module:

module induction-gives-iteration
(N : U₀)
(z : N)
(s : N → N)
(ind : ∀ i (A : N → U{i}) → A z → (∀ n → A n → A(s n)) → ∀ n → A n)

where
-- Write your conclusions here, e.g.
it : ∀ i (X : U{i}) (x : X) (f : X → X) → N → X
it i X x f = ind i (λ _ → X) x (λ n → f)

-- End of module. Without a module and some implicit parameters:

ind-gives-it :
(N : U₀)
(z : N)
(s : N → N)
(ind : ∀ {i} {A : N → U{i}} → A z → (∀ n → A n → A(s n)) → ∀ n → A n)
→ ∀ {i} {X : U{i}} (x : X) (f : X → X) → N → X
ind-gives-it N z s ind x f = ind x (λ _ → f)

\end{code}

(NB. In this Agda file, I don't exploit the "implicity" of the
universe level. But in other examples not included here, Agda can
infer a missing universe level argument, giving typical ambiguity in
restricted cases.)

I faced the same problems you discuss e.g. when formulating two
notions of univalence and showing that they are equivalent. In an
informal development eliding universe levels (e.g. in HoTT list
discussions and most of the HoTT book), this problem is invisible. In
Agda your are forced to see it, unless you use --type-in-type, and the
same goes for Coq, I presume.

Martin

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Michael Shulman]

On Tue, Jul 7, 2015 at 11:25 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> ind-gives-it :
> (N : U₀)
> (z : N)
> (s : N → N)
> (ind : ∀ {i} {A : N → U{i}} → A z → (∀ n → A n → A(s n)) → ∀ n → A n)
> → ∀ {i} {X : U{i}} (x : X) (f : X → X) → N → X

Whoa, really? Agda lets you hypothesize a universe-polymorphic
argument just like any other argument? Do people think that's
consistent? Is it one of those things that Agda just implemented
without really thinking about? What universe does ind-gives-it live
in?

Mike

[Gabriel Scherer]

I don't find it particularly worrying to assume an ordinal-indexed, rather than natural-indexed, family of universes (at least for ordinals everyone agree are predicative). Agda has a kind Set_omega that makes universe-polymorphic types kindable, but it is only a one-time thing, you cannot express it in the syntax and thus I don't think you could abstract over ind-gives-it itself.

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism

[Neelakantan Krishnaswami]

On 08/07/15 08:31, Michael Shulman wrote:
> On Tue, Jul 7, 2015 at 11:25 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> ind-gives-it :
>> (N : U₀)
>> (z : N)
>> (s : N → N)
>> (ind : ∀ {i} {A : N → U{i}} → A z → (∀ n → A n → A(s n)) → ∀ n → A n)
>> → ∀ {i} {X : U{i}} (x : X) (f : X → X) → N → X
>
> Whoa, really? Agda lets you hypothesize a universe-polymorphic
> argument just like any other argument?

Apparently so! I didn't realize that Agda permitted this, myself.

> Do people think that's consistent?What universe does
> ind-gives-it live in?

I have been thinking about this on and off for a while, and while
I haven't worked out all the details, it seems fairly straightforward
show that universe-polymorphic definitions are consistent using a PER
model of type theory (in the style of the Nuprl semantics).

Roughly speaking, a fully universe-polymorphic definition cannot
use any construction not available at all universe levels, and so it's
safe to put it in the bottom universe. This is rather powerful,
since (as Martin implicitly observes) it means that the Church naturals
live in the bottom universe, but nevertheless can be used to produce
up large eliminations.

Best,
Neel

PS -- My interest in this arises from the fact that if you additionally
internalize reasoning about parametricity, then seemingly everything we
can do with direct inductive type definitions can also be done with
Church encodings.

[Michael Shulman]

On Wed, Jul 8, 2015 at 3:52 AM, Neelakantan Krishnaswami
<n.krish...@cs.bham.ac.uk> wrote:
> it seems fairly straightforward
> show that universe-polymorphic definitions are consistent using a PER
> model of type theory (in the style of the Nuprl semantics).

Hmm, I suppose that answers concerns about consistency. But to echo
Thorsten's comment in the other thread, I'm not really interested in
that sort of model except as a curiosity. (-:O

[Martin Escardo]

On 08/07/15 11:52, Neelakantan Krishnaswami wrote:
> I have been thinking about this on and off for a while, and while
> I haven't worked out all the details, it seems fairly straightforward
> show that universe-polymorphic definitions are consistent using a PER
> model of type theory (in the style of the Nuprl semantics).

This doesn't show consistency of universe polymorphism with univalence
or HITs, right? (Until there are verified/refereed PER models of them.)

> Roughly speaking, a fully universe-polymorphic definition cannot
> use any construction not available at all universe levels, and so it's
> safe to put it in the bottom universe. This is rather powerful,
> since (as Martin implicitly observes) it means that the Church naturals
> live in the bottom universe, but nevertheless can be used to produce
> up large eliminations.

I am not defending universe polymorphism `a la Agda.

But it is, indeed, a problem to work with hypothetical propositions or
data, as illustrated in Mike's blog post. There are many more examples
like this.

Martin

[Michael Shulman]

On Wed, Jul 8, 2015 at 1:17 AM, Gabriel Scherer
<gabriel...@gmail.com> wrote:
> I don't find it particularly worrying to assume an ordinal-indexed,
> rather than natural-indexed, family of universes (at least for
> ordinals everyone agree are predicative).

Yes, that's reasonable, as long as the system is careful to ensure
that "universe-polymorphic" things can only be applied to universes
that they're actually polymorphic over. I.e. if a
"universe-polymorphic" definition is one that lives in Setω, then it
can't be applied to Setω itself. But Agda appears to be reasonably
careful about that.

> Agda has a kind Set_omega that makes
> universe-polymorphic types kindable, but it is only a one-time thing, you
> cannot express it in the syntax and thus I don't think you could abstract
> over ind-gives-it itself.

Actually, you can!

test : ((∀ {i} (A : Set i) → Set i) → (∀ {i} (A : Set i) → Set i)) → Set₀

Here is a function whose argument is a function that takes a
universe-polymorphic argument. There seems to be no limit.

> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism

I had heard of Agda's Setω, but for some reason I read the comment

"The only type constructor that can be applied to expressions of kind
Setω is →."

as saying only that we can form (x : A) → B when B : Setω. But
evidently A is allowed to live in Setω too!

I haven't actually tried yet, but I think this may allow a similar
development of modalities (though not comodalities) in Agda. Thanks
everyone for pointing it out.

Mike

[Michael Shulman]

It seems to me now that if we have ω+1 inaccessible cardinals in ZFC,
we should be able to build a univalent model in simplicial sets (or
wherever else we can build univalent models) containing that many
nested universes, and then simply forget about the fact that the ω^th
universe has any type constructors other than Π, to get a univalent
model of Agda's universe polymorphism. Is that not right?

On Wed, Jul 8, 2015 at 7:26 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>
>
> On 08/07/15 11:52, Neelakantan Krishnaswami wrote:

>> I have been thinking about this on and off for a while, and while
>> I haven't worked out all the details, it seems fairly straightforward
>> show that universe-polymorphic definitions are consistent using a PER
>> model of type theory (in the style of the Nuprl semantics).
>

> This doesn't show consistency of universe polymorphism with univalence
> or HITs, right? (Until there are verified/refereed PER models of them.)
>

>> Roughly speaking, a fully universe-polymorphic definition cannot
>> use any construction not available at all universe levels, and so it's
>> safe to put it in the bottom universe. This is rather powerful,
>> since (as Martin implicitly observes) it means that the Church naturals
>> live in the bottom universe, but nevertheless can be used to produce
>> up large eliminations.
>

[Thomas Streicher]

On Wed, Jul 08, 2015 at 08:47:46AM -0700, Michael Shulman wrote:
> It seems to me now that if we have ??+1 inaccessible cardinals in ZFC,

> we should be able to build a univalent model in simplicial sets (or
> wherever else we can build univalent models) containing that many

> nested universes, and then simply forget about the fact that the ??^th
> universe has any type constructors other than ??, to get a univalent

> model of Agda's universe polymorphism. Is that not right?

You are absolutely right and this was clear from work of the 2nd half
of the 80s.
But it is Vladimir's insight that fomulating the models as models of
essentially algebraic theories renders the existence of initial models
as automatic.
What I did in my book was showing that the term model for a syntax with
variables is initial.

My view now is that one should take up Vladimir's suggestion as a
convincing argument for the existence of initial models. I'd leave the
proof of isomorphism with the initial model based on syntax with
binding for those who like it. I am ready to take it for granted.

Thomas

[Vladimir Voevodsky]

It makes a lot of sense to use rational numbers to number universes. Then the problem of compatibility of various inequalities becomes a problem of linear programming that can be solved reliably  and easily. And obviously any solution in rational numbers can be translated into a solution in natural numbers by multiplying with the common denominator and shifting.

Vladimir.

[Michael Shulman]

On Wed, Jul 8, 2015 at 10:24 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> It makes a lot of sense to use rational numbers to number universes. Then
> the problem of compatibility of various inequalities becomes a problem of
> linear programming that can be solved reliably and easily.

That's a very interesting suggestion! Has anyone ever tried
implementing such a thing?

> And obviously
> any solution in rational numbers can be translated into a solution in
> natural numbers by multiplying with the common denominator and shifting.

Any solution with finitely many universes, at least. Of course,
omega+1 and many higher ordinals also order-embed into the rationals.

I guess any particular development *without* universe-polymorphic
hypotheses will only ever need finitely many fixed universes, but it's
less clear to me what will happen if we allow (as I want to do)
polymorphic hypotheses in some way.

Mike

[Peter LeFanu Lumsdaine]

Another alternative: instead of making the modalities polymorphic over the canonical universes that the type theory provides, one could axiomatise the class of universes one wants (define, say, a “higher Grothendieck universe” as a type family closed under products, sums, and whatever HITs are needed), and define/assume modalities as polymorphic over all “higher Grothendieck universes”.  Then could then be a universe-polymorphic theorem that “Type is a higher Grothendieck universe”, allowing the modalities (whether assumed or constructed) to be instantiated on each Type as required.

This is again a bit heavyweight, but seems not unnatural, and also a bit more foundation-agnostic.

–p.

[Michael Shulman]

On Wed, Jul 8, 2015 at 1:45 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> Another alternative: instead of making the modalities polymorphic over the
> canonical universes that the type theory provides, one could axiomatise the
> class of universes one wants (define, say, a “higher Grothendieck universe”
> as a type family closed under products, sums, and whatever HITs are needed),
> and define/assume modalities as polymorphic over all “higher Grothendieck
> universes”. Then could then be a universe-polymorphic theorem that “Type is
> a higher Grothendieck universe”, allowing the modalities (whether assumed or
> constructed) to be instantiated on each Type as required.

Interesting idea! Of course the notion of "higher Grothendieck
universe" would also be parametrized over a canonical universe in
which the type family lives, but everything we say about them would be
polymorphic in that parameter, so I don't think it would be a problem.

I do worry a little bit about whether you might need a hypothesis like
"every HGU is contained in a bigger one", which is of course
consistent to assume (modulo large cardinals), but couldn't actually
be instantiated, since there aren't infinitely many canonical
universes below any given canonical universe. But maybe that wouldn't
ever come up.

What worries me more is that a hypothesized universe of that sort
could only be weakly Tarski, which means that not only would you have
'El's floating around everywhere, but explicit coercions from "El (Pi
A B)" to "forall x:El A, El (B x)" and so on. I suspect that that
would be a colossal pain.

(On the other hand, if we used weakly Tarski universes *everywhere*,
then the theory would be closer to being interpretable in any oo-topos
using known models. But I haven't yet been willing to inflict the
necessary pain on myself with only that motivation.)

Mike

[Martin Escardo]

Last night I spent some time, both on paper and Agda, thinking about
universes a la Tarski indexed by (countable) ordinals. And then I
spent sometime today thinking about that with my student Cory Knapp,
and experimenting with ideas and Agda code with him.

I want to report some of this here, for discussion.

When you want *one* universe a la Tarski, using induction-recursion,
in Agda you can do it like this (which I think this is written by
Peter Dybjer):

http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.RulesForTheStandardSetFormers

I will redo this in more generality here.

I want to have many universes a la Tarski, indexed by ordinals.

I will choose Hilbert-Brouwer ordinals. These are really trees, that
code (at least classically) countable ordinals, but the trees
themselves are our primary object of interest here:

data L : U where
zero : L
succ : L -> L
sup : (ℕ -> L) -> L

The type L will be our (internal!) type of universe levels within U.

We start with a universe U (a la Russell) as in the HoTT book, and we
assume that it is closed under induction-recursion.

For each i:L, we will define a universe a la Tarski V_i : U and a
function El_i : V_i -> U. The idea is that the points of V_i are
(non-syntactical) codes of types in U, found by El_i.

So V_i will be the ith universe a la Tarski within U.

Each v : V_i gives rise to a type El_i v : U.

In pseudo-Agda notation, the inductive-recursive definition is this,
where Π' codes Π, and V' gets V i to be a point of V(i+1) :

Π : (A : U) → (A → U) → U
Π A B = (x : A) → B x

data V : L → U
El : (i : L) → V i → U

data V where
Π' : (i : L) (c : V i) → (El i c → V i) → V i
V' : (i : L) → V(succ i)
up : (i : L) → V i → V(succ i)
Up : (α : ℕ → L) (n : ℕ) → V(α n) → V(sup α)

El i (Π' i c d) = Π (El i c) (λ x → El i (d x))
El (succ i) (V' i) = V i
El (succ i) (up i v) = El i v
El (sup α) (Up α n v) = El (α n) v

I've included only Π' and V' for simplicity/illustration. In practice
we have to include all type formers we wish our universes be closed
under (and we do this in our Agda files). The constructors up and Up
always have to be there, to get cummulativity.

Now, Agda complains that this is not a strictly positive
definition. It is, but I don't blame Agda for the oversight (see
the parenthetical discussion below for a justification).

This is very obvious and pleasing, and gives a family of universes
strongly a la Tarski within our Russell universe U (which shows that
induction-recursion is very powerful indeed).

This works in MLTT. If we have propositional truncations, we can
"russellify" the universe a la Tarski V_i to get a universe a la
Russell U_i.

Just take the image of El_i, which gives

U_i = Sigma(X:U).||Sigma(v:V_i). El_i v = X||.

Each U_i is then closed under the standard type formers (where
"standard" is whatever you choose, within reason). Here the
ordinal-indexed sequence of predicates P_i : U -> U

P_i(X) = ||Sigma(v:V_i). El_i v = X||

gives a cumulative sequence of subuniverses of U, each of them closed
under the standard type formers. (So again I emphasize that
induction-recursion cannot be seen as coming for free.)

(We also know how to get around the Agda positivity problem, when we
code all this in Agda with all details. However, when we do that, we
get universes weakly a la Tarski, unfortunately. I leave this for a
future discussion, if anybody is interested. The basic idea is to use
induction-recursion to close a family of types under the standard type
formers (for your favourite notion of standard), and then
transfinitely iterate this closure operations. Agda then takes back
its previous complaint about positivity when we reformulate the
construction this way.)

Martin

[Michael Shulman]

On Thu, Jul 9, 2015 at 11:49 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> This works in MLTT. If we have propositional truncations, we can
> "russellify" the universe a la Tarski V_i to get a universe a la
> Russell U_i.
>
> Just take the image of El_i, which gives
>
> U_i = Sigma(X:U).||Sigma(v:V_i). El_i v = X||.

In what sense is this more of a universe a la Russell than V_i is? It
seems to me there is stil an "El" that has to be applied to get to an
"actual" type, only now it is the first projection of the Sigma.

[Martin Escardo]

On 09/07/15 19:53, Michael Shulman wrote:
> On Thu, Jul 9, 2015 at 11:49 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> This works in MLTT. If we have propositional truncations, we can
>> "russellify" the universe a la Tarski V_i to get a universe a la
>> Russell U_i.
>>
>> Just take the image of El_i, which gives
>>
>> U_i = Sigma(X:U).||Sigma(v:V_i). El_i v = X||.
>
> In what sense is this more of a universe a la Russell than V_i is? It

> seems to me there is stil an "E "l" that has to be applied to get to an

> "actual" type, only now it is the first projection of the Sigma.

Maybe I should say "weakly a la Russell".

I see this analogous to the definition

Set = Sigma(X:U).isSet(X).

Then Set is a universe weakly a la Russell, closed under various type
formers, including N, Sigma, Pi, ..., in that the "carrier" is a type,
rather than a code for a type, and where the operations N,Sigma,Pi,...
on Set are inherited from U.

In the above construction, we can see induction-recursion, and the codes
it allows one to construct, as merely a tool to get a family of
proposition-valued predicates

P_i : U -> U

such that

U_i ={def} Sigma(X:U).P_i(X)

is closed under the "standard" type formers and is cumulative, with
N,Sigma,Pi,... inherited from U, rather than coded.

Martin

[Michael Shulman]

On Thu, Jul 9, 2015 at 11:49 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

> Just take the image of El_i, which gives
>
> U_i = Sigma(X:U).||Sigma(v:V_i). El_i v = X||.
>
> Each U_i is then closed under the standard type formers (where
> "standard" is whatever you choose, within reason).

Hmm... now I'm not sure I believe that. Suppose I have

A : U

B : proj1 A -> U

(omitting the subscript i) and I want to construct their Pi. I have

proj2 A : || Sigma(v:V). El v = proj1 A ||

proj2 o B : Pi(a : proj1 A). || Sigma(v:V). El v = proj1 (B a) ||

and I want something of type

|| Sigma(v:V). El v = Pi(a : proj1 A). proj1 (B a) ||.

Now the v:V in the goal wants to be "Sigma A' B'" where

El A' = proj1 A
El (B' a) = proj1 (B a).

We can get A' by stripping the truncation from proj2 A since the goal
is truncated, but I don't see how to get B', since the truncation in
"proj2 o B" is inside the Pi. We seem to need an axiom of choice over
proj1 A.

Am I confused?

Mike

[Martin Escardo]

I don't see how to get rid of choice in my proposed russellification.

So it seems that if you want to go the inductive-recursive way to get an
ordinal indexed, cumulative hierarchy of Tarski universes V_i within
your Russell universe U, you will need to carry some intensional
information, to avoid choice. But I would like to understand this better.

Martin

[Michael Shulman]

Well, if *higher* inductive-recursive types exist (which is still
conjectural), then they can construct a univalent Tarski universe
within a given univalent Russell universe, which therefore forgets any
intensional information (at least up to homotopy):
http://homotopytypetheory.org/2014/06/08/hiru-tdd/

(Actually, the existence of even *ordinary* inductive-recursive types
in *univalent* models is still conjectural, isn't it?)

On Thu, Jul 9, 2015 at 1:33 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> I don't see how to get rid of choice in my proposed russellification.
>
> So it seems that if you want to go the inductive-recursive way to get an
> ordinal indexed, cumulative hierarchy of Tarski universes V_i within
> your Russell universe U, you will need to carry some intensional
> information, to avoid choice. But I would like to understand this better.
>
> Martin
>
> On 09/07/15 20:57, Michael Shulman wrote:

[Martin Escardo]

On 08/07/15 18:24, Vladimir Voevodsky wrote:
> It makes a lot of sense to use rational numbers to number
> universes.

Nice. But how do you justify the existence of rational-indexed
universes to yourself? Or maybe this is not the right question: what
is the right question, in this case?

Martin

[Michael Shulman]

On Thu, Jul 9, 2015 at 1:57 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> It makes a lot of sense to use rational numbers to number
>> universes.
>
> Nice. But how do you justify the existence of rational-indexed
> universes to yourself? Or maybe this is not the right question: what
> is the right question, in this case?

I took Vladimir's suggestion to be that the rational indices would
happen only in the syntax; any particular term will involve only
finitely many universes which can thus be re-labeled by natural
numbers (clearing denominators).

The actual existence of a Q-indexed family of universes is, I believe,
inconsistent with the axiom of choice, which implies that
cardinalities are well-ordered. But I seem to recall vaguely that
maybe if choice fails then it is possible to have a densely ordered
family of (non-well-orderable) cardinalties?

[Martin Escardo]

On 09/07/15 21:37, Michael Shulman wrote:
> Well, if *higher* inductive-recursive types exist (which is still
> conjectural), then they can construct a univalent Tarski universe
> within a given univalent Russell universe, which therefore forgets any
> intensional information (at least up to homotopy):
> http://homotopytypetheory.org/2014/06/08/hiru-tdd/
>
> (Actually, the existence of even *ordinary* inductive-recursive types
> in *univalent* models is still conjectural, isn't it?)

Like I said repeatedly in my original message about this:

> (So again I emphasize that
> induction-recursion cannot be seen as coming for free.)

Martin

[Peter LeFanu Lumsdaine]

On Thu, Jul 9, 2015 at 11:17 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

On 09/07/15 21:37, Michael Shulman wrote:
> Well, if *higher* inductive-recursive types exist (which is still
> conjectural), then they can construct a univalent Tarski universe
> within a given univalent Russell universe, which therefore forgets any
> intensional information (at least up to homotopy):
> http://homotopytypetheory.org/2014/06/08/hiru-tdd/
>
> (Actually, the existence of even *ordinary* inductive-recursive types
> in *univalent* models is still conjectural, isn't it?)

Like I said repeatedly in my original message about this:

> (So again I emphasize that
> induction-recursion cannot be seen as coming for free.)

Certainly not for free, but in traditional set models, it costs 1 Mahlo cardinal per inductive-recursively closed universe (iirc).  The question is surely whether the same price buys you IR in SSets or other homotopical models :-)

–p.

[Martin Escardo]

On 09/07/15 22:37, Peter LeFanu Lumsdaine wrote:
> On Thu, Jul 9, 2015 at 11:17 PM, Martin Escardo <m.es...@cs.bham.ac.uk

> Like I said repeatedly in my original message about this:
>
> > (So again I emphasize that
> > induction-recursion cannot be seen as coming for free.)
>
>
> Certainly not for free, but in traditional set models, it costs 1 Mahlo
> cardinal per inductive-recursively closed universe (iirc). The question
> is surely whether the same price buys you IR in SSets or other
> homotopical models :-)

Yes, this is the question, from the point of view of set models. (And
the question is serious and important despite the presence of your ":-)".)

But one thing that we should not forget is that MLTT was put forward as
a foundation of constructive mathematics, supposed to be meaningful in
itself, without the need of reducing it to other existing foundations
for the purposes of understanding it.

Needless to say, MLTT comes in various flavours, which reflect both (i)
the open-endedness of the idea, and also (ii) the fact that it is open
to revision (like set theory was until it was canonized as ZFC) and even
the possibility of incompatible, accepted variations.

It is reassuring that people agree what type theory is and disagree (or
even don't know) what its syntax is. This means that they understand the
mathematical idea without having the syntax as the main parameter. This
doesn't mean that the syntactical problem can be safely ignored. Of
course, it should be taken seriously.

I regard it as a rather interesting mathematical "coincidence" that the
ideas from constructive mathematics that led to the conception of MLTT
turned out to be naturally compatible with, and relevant to, the ideas
of homotopy theory, and, moreover, useful (at least according to some
enthusiasts) for the purposes of homotopy theory and more generally the
foundations of any kind of mathematics, including abstract mathematics.

So, in this sense, it becomes pressing, for example, to understand
whether e.g. induction-recursion can be directly justified, rather than
reduced to another theory where also there is no justification, but
there is a nice name ("Mahlo") corresponding to it. I see such
reductions as showing that if one theory falls apart, so does the other.
But the point of constructive mathematics, beyond being able to compute,
is that is should stand on its own without the need for auxiliary
justification, and be intrinsically meaningful.

Martin

[Michael Shulman]

While all that is true (and not, as I see it, specific in any way to
constructivism -- any foundation for mathematics ought to be
meaningful in itself), it's still generally the case that when
considering a new rule or axiom to be added to a theory, by comparing
it to ones that have already been studied one can get a better sense
for its likely strength and consistency (or lack thereof).

In particular, I think knowing that extensional IR follows from Mahlo
cardinals does tell us something useful about its consistency and
meaningfulness, because set theorists have studied large cardinals for
many decades and placed them in a very detailed yardstick of
consistency strength, with Mahlo cardinals being relatively low on
that hierarchy. If it required, for instance, a rank-into-rank, then
I would be much more dubious about it, even though that is also just a
nice name.

[Martin Escardo]

On 10/07/15 00:28, Michael Shulman wrote:
> While all that is true (and not, as I see it, specific in any way to
> constructivism -- any foundation for mathematics ought to be
> meaningful in itself), it's still generally the case that when
> considering a new rule or axiom to be added to a theory, by comparing
> it to ones that have already been studied one can get a better sense
> for its likely strength and consistency (or lack thereof).

Agreed. In particular the question Peter L poses regarding Mahlo vs
induction-recursion in the presence of univalence is very interesting
and should be answered.

> In particular, I think knowing that extensional IR follows from Mahlo
> cardinals does tell us something useful about its consistency and
> meaningfulness, because set theorists have studied large cardinals for
> many decades and placed them in a very detailed yardstick of
> consistency strength, with Mahlo cardinals being relatively low on
> that hierarchy. If it required, for instance, a rank-into-rank, then
> I would be much more dubious about it, even though that is also just a
> nice name.

I am sorry I put things this way.

Best,
Martin

[Martin Escardo]

I meant to write this minor comment immediately when Thomas made the
comment below, but I couldn't then and then I forgot. But here it goes a
bit late.

Programming-languange theorists distinguish between concrete and
abstract syntax.

The initial model is the abstract syntax.

The concrete syntax is needed in practice, and usually its relation to
the abstract syntax is regarded as well understood (via the concepts of
lexical analysis (regular expressions) and parsing (context free
grammars usually, but not always). Hence the concrete syntax is
invariably ignored by programming language theorists and left to
compiler writers, who understand this (and much more) very well.

But in the presence of dependent types, the relationship between
concrete and abstract syntax is less clear and (perhaps surprisingly)
much subtler, and hence deserves attention by theoreticians
(mathematicians, logicians or computer scientists). I wouldn't say this
is well understood for dependent types.

Martin

[Thomas Streicher]

Dear Martin,

certainly, things are more complicated with dependent types.

But the translation from ordinary syntax with variables to the
combinator version is "just" interpretation in the free semantical
structure and back we get by replacing the combinators by their
corresponding terms.

In concreto that's always simple but lengthy. A problem certainly is
to write this down in general. Questions like "What is a logic?"
usually lead to an excess of bureaucracy.

But semantically things are easier: think of display map categories or
more briefly tribes.

But the problem is a genuinely syntactical one.

[Martin Escardo]

I fully agree with you, Thomas.

BUT:

The current practice of the construction of terms involves first the
consideration of raw terms, which are meaningless, followed by a second
step to carve out the intended, meaningful terms.

There have been attempts to directly define, by some suitable form of
induction, only the intended terms, but so far they are only partially
successful.

I regard this as both puzzling and embarrassing: While I consider
language as coming after the thoughts we want to talk about or record
for ourselves or other people, in some sense we should be able to define
such a language in terms of what we want to talk about.

In this sense, having to define the concrete language used for
communication as a subset of a meaningless language of raw terms is
embarrassing: If we do have direct thoughts about certain objects that
exist in our brains or our conception of reality, we should have direct
means of expressing them, without having an artificial step introducing
a meaningless language out of which the intended language is carved out.

Martin

[Andrew Polonsky]

So, in this sense, it becomes pressing, for example, to understand
whether e.g. induction-recursion can be directly justified, rather than
reduced to another theory where also there is no justification, but
there is a nice name ("Mahlo") corresponding to it. I see such
reductions as showing that if one theory falls apart, so does the other.
But the point of constructive mathematics, beyond being able to compute,
is that is should stand on its own without the need for auxiliary
justification, and be intrinsically meaningful.

I think the type-theoretic/constructive justification for induction-recursion is well-understood.  Dybjer and Setzer's "IR codes" fall squarely into the type-theoretic methodology, with intro-elim-computation rules, equality rules, meaning explanations, etc. [1]

The interpretation in ZF with a Mahlo cardinal was just a blunt approximation to get a model.  A more refined result is that the proof-theoretic strength of IR is that of Kripke-Platek set theory with a recursively Mahlo ordinal, and perhaps a chain of admissible ordinals above it. (Corollary 6.4.2 in [1].)

By the way, Setzer introduced his type-theoretic "Mahlo universe" around the same time.  [2]  This also has all the standard features of a type constructor.

Cheers,

Andrew

1) P. Dybjer and A. Setzer, 

Induction-recursion and initial algebras. 

Annals of Pure and Applied Logic 124 (2003)

http://www.cse.chalmers.se/~peterd/papers/InductionRecursionInitialAlgebras.pdf

2) A. Setzer,

A model for a type theory with Mahlo universe (1996)

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.7858

[Martin Escardo]

I am happy to understand that induction-recursion corresponds to Mahlo,
both set theoretically (via a model) and type theoretically (by just
adding formation rules in type theory that correspond to
Mahlo/induction-recursion (as Setzer does).

Some people, including perhaps Martin-Loef and Anton Setzer, may be
happy with "meaning explanations" of induction-recursion (=Mahlo by
definition). But I am not. I am happy to work with this hypothesis,
though. However, I fail to see "directly" that induction-recursion does
define something, without falling into some form of circularity. (I do
understand how it can be reduced to Mahlo.)

Certainly, induction-recursion is very appealing, and there are natural
examples that lead to it (including a transfinite tower of universes a
la Tarski).

Moreover, from a programming point of view, induction-recursion is very
natural too (but then so is general recursion). But what does it mean?
And how do we justify to ourselves that these induction-recursions, in
particular, give rise to terminating programs? I can't see this
directly. And of course I shouldn't, because even in ZFC, with all its
strength and mighty, the existence of Mahlo cardinals is undecided.

Having said that, induction-recursion is very nice, and I will be happy
to use it (but with my fingers crossed).

Best,
Martin

[Andrew Polonsky]

Ooh, YES!!  Finally! The Grand Metaphysical Syntax vs. Semantics Debate!

On Saturday, July 11, 2015 at 12:36:05 AM UTC+2, Martín Escardó wrote:

The current practice of the construction of terms involves first the
consideration of raw terms, which are meaningless, followed by a second
step to carve out the intended, meaningful terms.

There have been attempts to directly define, by some suitable form of
induction, only the intended terms, but so far they are only partially
successful.

I thought the desire for all expressions to be meaningful is precisely the reason why Martin-Löf introduced judgmental equality into his formulation of type theory (and is the only reason judgmental equality exists, as a concept).  Do you find this solution lacking, in some way?

 

I regard this as both puzzling and embarrassing: While I consider
language as coming after the thoughts we want to talk about or record
for ourselves or other people, in some sense we should be able to define
such a language in terms of what we want to talk about.

In this sense, having to define the concrete language used for
communication as a subset of a meaningless language of raw terms is
embarrassing: If we do have direct thoughts about certain objects that
exist in our brains or our conception of reality, we should have direct
means of expressing them, without having an artificial step introducing
a meaningless language out of which the intended language is carved out.

Good!  I completely disagree! :))

To me, it is more natural to first have the raw terms, which give the equational, non-logical, computational level -- and then have the logical structure built on top of that.

Because, computational information is more fundamental than logical information.

As an illustration, consider the lambda calculus.  Any (logically consistent) type system can be projected to an (incomplete) subset of it: only the normalizing terms have types.  For any particular system (simple types, system F, calculus of constructions...), we can prove by logical relations, that the Church-Rosser property is valid.

But we can also prove it in the *untyped* world, for terms which don't even normalize.  If we only worked with typed calculi, we would have never discovered that these terms have their own internal structure, a kind of "computational consistency".  This property is independent of the typing, and is therefore "pre-logical".

As for communication, I find natural language, and human interaction in general, to be terribly untyped!  We just exchange symbols, and it is up to the receiver to figure out what they mean, if anything.  It is easy to write grammatical sentences with no meaning, e.g.

- This sentence is false.

- The present king of France is bald.

- Colorless green ideas sleep furiously.

- Beware the Jabberwock, my son!

Moreover, one can even write sentences that are ungrammatical, but have meaning, viz.

- This sentence no verb.

- Syntax good, semantic bad, very bad.

- Y u no text me back?

In linguistics, the meaning of a sentence is usually considered to be the so-called "logical form" associated to its syntax tree.  It's a Church-typed lambda term.  It takes time to compute it, and the process is not guaranteed to succeed in general.

Why should communicating mathematics be any different?

There is another reason I prefer untyped conversion between raw terms over judgmental equality with "globally meaningful" typing judgments:

It explains, at least on the intuitive level, how we can believe type checking to be feasible in the first place.

Admitted, if you only care about having a language that faithfully captures your semantic world, you don't care about efficiency.  But in practice, if your "proof object" consisted of the entire derivation tree, it would be terribly huge, because of all the type conversions that have to be coded by hand.

The fact that you can forget about typing when you check the applicability of the conversion rule, is a Very Good Thing.  (And a difficult result, too. It might be one of the most under-appreciated theorems in the metatheory of type systems!)  It means that you can just give the term as the proof, and your interlocutor is guaranteed to still be able to reconstruct all the conversions that are necessary.

The situation is somewhat reminiscent of cut-elimination: if you only care about a sound proof system that gives you completeness ("logical consequence has finitary character"), then why add the cut rule in the first place?

(Answer. Because you won't formalize a lot of math if you cannot make lemmas along the way.)

I think there are certain properties which we implicitly expect our formal system/language of communication to have.  These properties are of a computational nature.

And they are absolutely essential.

Cheers,

Andrew

[Martin Escardo]

On 12/07/15 01:36, Andrew Polonsky wrote:
> As for communication, I find natural language, and human interaction in
> general, to be terribly untyped! We just exchange symbols, and it is up
> to the receiver to figure out what they mean, if anything. It is easy
> to write grammatical sentences with no meaning, e.g.
>
> - This sentence is false.
> - The present king of France is bald.
> - Colorless green ideas sleep furiously.
> - Beware the Jabberwock, my son!

When I referee a paper, in mathematics or in computer science, I
expect all sentences to be meaningful (even when they are false). Raw
terms are ruled out. Any gramatical errors are considered as
oversights, to be fixed in the final version, if the submission has
sufficiently many true, interesting claims.

Of course, occasionally there is indeed the odd paper in which the
claims are not even false, as the saying goes, in that it is not even
possible to make sense of what is described in the paper.

Surely English does allow you to say that colorless green ideas sleep
furiously (which, by the way, is vacuously true, as there can't be any
colorless green idea, or colorless green anything). The possibility of
saying false things (and hence vacuously true things as in this
example) is always to be allowed. There are lots of gramatically
correct false statements (in English, in ZFC, in type theory). What
shouldn't be allowed, of course, is a proof of false statement, but
this beyond the well-formedness of statements.

Martin

[Andrej Bauer]

On Sun, Jul 12, 2015 at 3:08 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> When I referee a paper, in mathematics or in computer science, I
> expect all sentences to be meaningful (even when they are false). Raw
> terms are ruled out. Any gramatical errors are considered as
> oversights, to be fixed in the final version, if the submission has
> sufficiently many true, interesting claims.

But there are numerous occasions in your rich history of refereeing
when the author spends time showing that a claim or a phrase is
meaningful. For instance, he may speak about the supremum of a set in
a Scott domain, and he argues separately that the set is directed.
This is a case of "raw syntax" becoming "honest syntax". We even
teach children that division is raw until the denominator is shown to
be non-zero.

Only in artificially designes situations is grammar so simple that we
need no fancy processing to verify it. Human language possible raw
syntax to use is, think of how children small speak to learn. Quite
often correct application of grammatical rules requires semantic
knowledge.

Thus I would say that the complications involving the syntax of
dependent types are rather the norm. The simple syntax of first-order
logic an set theory is an idealization (in the sense of it being
unrealistic and unusuable in practice) made by logicians for
logicians. Real mathematicians speak something that is closer to
dependent type theory than to first-order logic and set theory (even
though they are told otherwise).

With kind regards,

Andrej

[Michael Shulman]

It's true that 'colorless green ideas sleep furiously' is *grammatical* English, but I would rather regard it as meaningless, because in it adjectives are applied beyond their domain of applicability, in the same way that 'the square root of two has pullbacks' is meaningless in mathematics. I.e. in natural language, 'grammatically correct' is a weaker condition than 'well-typed'.

[Thomas Streicher]

Cleaner languages are those without semantical side conditions. In
this sense Latin (and derived languages) are cleaner than English
where semantical grammatical rules abound.

The crux is that in dependent type theories "syntactical judgements"
like "A type" may depend on "semantical judgements" like "t : A" or
"A inhabited". This is unavoidable when you want to have propositions as
types (and it is this feature besides having 2 equalities which makes
it difficult for "ordinary" mathematicians to get used to type theory).

Now making this choice you have to pay: either type checking becomes
undecidable or you have to give up extensionality. At least that's
what it looked like recently. We have to see whether a sufficient
amount of extensionality can be saved when replacing orthodox type
theory by say "cubical type theory". But even if successful (which is
not unlikely) the resulting system is more difficult to swallow even
than traditional type theory.

But even then a price has to be paid when dealing with universes since
it seems to force us to identify equality with isomorphism (formulated
appropriately). Whether this is good or not depends on one's purposes
and preferences.

There is no reason to choose once and forever.

For this reason the option of extensional type theory and even more
traditional systems shouldn't be abandoned.

Thomas

[Michael Shulman]

On Fri, Jul 10, 2015 at 3:36 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> In this sense, having to define the concrete language used for
> communication as a subset of a meaningless language of raw terms is
> embarrassing: If we do have direct thoughts about certain objects that
> exist in our brains or our conception of reality, we should have direct
> means of expressing them, without having an artificial step introducing
> a meaningless language out of which the intended language is carved out.

I used to think this way, but more recently I've come around to
thinking that "carving meaning out of non-meaning" is actually basic
to human thought. Not just in the "syntactic" case of finding
well-typed and grammatical sentences among the nonsensical ones, but
also in a more semantic sense involving impredicativity and
self-reference. Mathematicians can hem and haw about universe sizes,
but outside of our carefully guarded preserve of consistency and
predicativity, self-reference in natural language and ordinary human
thought is the rule rather than the exeception. The statement "This
sentence has five words" is clearly intelligible and true to any
speaker of English, but has somehow to be carved out from a context
which includes meaninglessness like "This sentence is false".

(Which means that I'm actually more sympathetic to proposals like
strict resizing axioms than it might have seemed from the other
thread. One might argue that Type:Type more accurately reflects human
thought, and the closer we can get to that ideal while maintaining a
usable mathematics the better.)

Mike