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.
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.)
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.
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.
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'.