>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
On Jul 8, 2015, at 3:35 PM, Bas Spitters <b.a.w.s...@gmail.com> wrote:I guess you are saying that a predicative structural set theory will do too?
I think UniMath uses impredicative hProp in a number of places. This is impossible to do without axioms unless -type-in-type is passed. I don't know about the status of mixing files compiled with -type-in-type with those compiled without it, but it might be possible to compile a single file with -type-in-type which defines a resizing "axiom" as the identity function, and make use of that elsewhere as needed.
-Jason
There's a chance that using a resizing identity function will give you some judgmental behavior that you wouldn't otherwise be able to get? I'm not completely sure, though.
-Jason
Yes, I don't see any necessary contradiction between allowing the user to forget about universes *sometimes* and supplying more fine-grained control if desired.
Coq now allows universe annotations. In fact, they were important in
our developments.
https://github.com/HoTT/HoTT/blob/master/STYLE.md#universe-annotations
Does this provide the control you need, are do you need something else?
On Wed, Jul 8, 2015 at 11:02 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
Perhaps I am just used to terse and precise writing with not too much
motivation or explanation, as in Bourbaki, EGA, Hartshorne, etc. (I
feel that it is best to say things abstractly and precisely in the
beginning; motivation may follow, perhaps much later.) The language in
these books has a small vocabulary, and that helps the reader focus on
the concepts without distraction.
On the other hand, in the syntax of type theory, the symbols are the
only things that seem to matter. There are no meaningful objects
underlying these symbols, as far as I understand. If symbols are the
only things that matter, then changing them seems to change the
expressions which they form. This seems to be one of my troubles with
alpha-conversion and substitution.
Thanks again for taking the trouble to explain.
But the problem in HoTT at the moment is exactly that we haven't fixed
a model, no?
On Mon, Jul 13, 2015 at 2:14 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> One way of getting this
> understanding can be by looking at models of the system from outside —
> either in your informal intuition, or in other foundational systems, or even
> in the same formal system itself. Introductions to ZFC often give
> more-or-less formal discussions of the cumulative hierarchy picture, the
> iterative conception of set, and so on.
I wouldn't say that the cumulative hierarchy involves looking at a
model of ZFC from outside. The cumulative hierarchy is defined
*inside* ZFC by transfinite induction, so it seems more analogous to,
say, the h-level/n-type hierarchy in HoTT/UF. Of course such
"classifications" of the objects of a theory are also useful for
getting understanding, but as far as I can see they are both purely
internal to the theory.
We didn't give a precise definition of alpha-equivalence and
capture-free substitution, because that would have required defining
syntax precisely. However, I always figured that mathematicians in
general *know* what alpha-equivalence and capture-free substitution
are, even if they don't know those type-theoretic words for them. So
why should they suddenly need to see a precise definition of them when
learning type theory, if they've managed for their whole mathematical
lives so far without one?