Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: Michael Shulman <shulman@sandiego.edu>
To: Martin Hotzel Escardo <escardo.martin@gmail.com>
Cc: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Injective types
Date: Fri, 3 May 2019 04:45:18 -0700
Message-ID: <CAOvivQy0A3mUJ8904+PjwAzTpmx1J1A3Le9jmdjJWG7ZSvz3FA@mail.gmail.com> (raw)
In-Reply-To: <2b380e43-8623-4900-b529-1e267155562f@googlegroups.com>

I am more optimistic: I think there's a good chance we could do better
than both Coq and Agda.  Of course sometimes when we try new things
they flop; but we can't make progress without trying new things.

For one thing, I don't think we should conflate typical ambiguity with
cumulativity.  It just so happens that Coq has both and Agda has
neither, but in principle I see no reason they have to go together.  I
see typical ambiguity as basically syntactic sugar or abuse of
notation, analogous to the use of implicit arguments: the reader or
proof assistant is tasked (if they feel like it) to go through and
insert level parameters as needed, accumulating constraints on these
parameters according to how the instance are used and thereby
"elaborating" a typically ambiguous development to a fully precise one
with (polymorphic) universe levels.  Usually this will be possible,
but occasionally if the writer was careless there may be a universe
inconsistency.

It seems to me that this could be done in both a cumulative and a
non-cumulative system.  True, in a non-cumulative system we get
different constraints, e.g. if we ever write "A=B" then it must be
that A and B live in the same universe, whereas in a cumulative system
we could be looser about such constraints.  But your evidence (and
that of other universe-polymorphic users of Agda) suggests that such
constraints arising from non-cumulativity are not in practice a
problem.  In fact, the unique assignment of levels in a non-cumulative
system suggests that the universe inference algorithm in a
hypothetical typically-ambiguous non-cumulative proof assistant would
probably be *simpler*, and less error-prone, than that of Coq.  So I
don't see any argument here against typical ambiguity, as long as
there is the *option* to be unambiguous when necessary (which again,
even Coq now supports).

In particular, note that when a development is formalized in a
typically ambiguous proof assistant, it's not necessary for the
universe levels to be written in the source code, or even thought
about by the author, in order for the interested reader -- or even the
author themselves! -- to learn about what the universe constraints
are.  They only have to compile the code, in particular running it
through the universe checker/elaborator, and then inspect the
resulting universe levels/constraints.  I've done this in present-day
Coq myself, although the proliferation of universe parameters makes
the output hard to undertsand; I expect it would only be easier in a
hypothetical typically-ambiguous non-cumulative proof assistant.  So
it seems to me that it should be possible to be "fair to the reader",
as you say, and still retain (some of) the advantages of typical
ambiguity.

I also think there's a good chance we can retain some cumulativity
without losing the benefits of non-cumulativity, by using a
Tarski-style lifting coercion as I sketched in my last email.  (Isn't
this in the literature somewhere?  I didn't think I'd made it up.)  I
agree that it's rare to need this, but neither is it unheard-of; so if
we can make it more convenient to use with no drawback, why not?  (Of
course, cumulativity is also trickier to model semantically, but
probably possible.)





On Thu, May 2, 2019 at 1:46 PM <escardo.martin@gmail.com> wrote:
>
>
>
> On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael Shulman wrote
>>
>>
>> Yes, this is a good point in favor of Agda-style non-cumulative
>> Russell universes over Coq-style cumulative Russell universes.
>>
>> But isn't there a middle ground with Tarski universes?
>
>
> It would be nice to have such a middle ground, particularly because formulating universe assumptions in each single definition and theorem is unfamiliar in mathematical practice, and so "typical ambiguity" (pretending there is only one universe) is potentially a good idea for many (or even most) examples. But not in the paper I advertised in this thread.
>
> Here I post an example when Giraud did precisely that, namely to assume two arbitrary universes U and V, explaining why this is needed in that level of generality after the formulation of a theorem and its proof, given to me by Thierry Coquand:
>
>   https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (photo of one page of a book).
>
> The book is “Cohmologie non abelienne” (1971, https://www.springer.com/gp/book/9783540053071).
>
>> Suppose we
>> have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in
>> Agda we have unique small polymorphic level assignments.  But then
>> suppose we have *definitional* equalities El(Lift(A)) == El(A).  Then
>> on the (rare) occasions when we do have to explicitly lift types from
>> one universe to another,
>
>
> I can confirm from a 26k line Agda development (with comments and repeated blank lines removed in this counting of the number of lines) that not once did I need to embed a universe into a larger universe, except when I wanted to state the theorem that any universe is a retract of any larger universe if one assumes the propositional resizing axiom (any proposition in a universe U has an equivalent copy in any universe V). So I would say that such situations are *extremely rare* in practice.
>
>>
>> we would get stronger cumulativity behavior.
>> (And I could imagine a proof assistant that implements this and sugars
>> away the El to look like Russell universes to the user.)
>
>
> At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda), and there is no system that combines the virtues of Coq and Agda regarding universe handling. (And I fear that such a system would potentially multiply the vices of both. :-) )
>
> M.
>
> --
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

  reply index

Thread overview: 11+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-04-30 23:05 escardo.martin
2019-05-01  2:50 ` Michael Shulman
2019-05-01  6:25   ` escardo.martin
2019-05-01 16:55     ` Michael Shulman
2019-05-02 20:46       ` escardo.martin
2019-05-03 11:45         ` Michael Shulman [this message]
2019-05-03 13:25           ` Kenji Maillard
2019-05-03 18:23             ` Thierry Coquand
2019-05-07 12:42         ` Nils Anders Danielsson
2019-05-07 13:51           ` Andreas Nuyts
2019-05-07 22:06             ` Martín Hötzel Escardó

Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CAOvivQy0A3mUJ8904+PjwAzTpmx1J1A3Le9jmdjJWG7ZSvz3FA@mail.gmail.com \
    --to=shulman@sandiego.edu \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=escardo.martin@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox