From: "Martín Hötzel Escardó" <"escardo..."@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Re: Coquand's list of open problems
Date: Thu, 25 Jan 2018 02:14:20 -0800 (PST) [thread overview]
Message-ID: <8e5014ee-eaa1-47f3-abe0-56d49e50728f@googlegroups.com> (raw)
In-Reply-To: <ADD54048-83CE-422B-99ED-80F8406E29DC@leeds.ac.uk>
[-- Attachment #1.1: Type: text/plain, Size: 3234 bytes --]
Right, this kind of thing is indeed what I have in mind.
Another example (with Cory Knapp) is a lifting monad induced by a
dominance. Fix a universe U. Then its type of propositions, Prop, lives in
the next universe U'. A dominance is a subset of Prop subject to certain
conditions. Prop itself is a dominance, and let's consider this for
simplicity. Then a partial element of a type X is a proposition P (the
extent of definition of the partial element) together with a function P->X.
The lifting of X is then
LX := Sigma(P:U), isProp P * (P->X).
If X is in a universe V, then LX is in the universe U' \/ V (namely the
least universe after U' and V, where we are assuming a sequence of
universes). However, if we apply L once more to get L(L X), this is in the
same universe as L X (we increase the universe levels only once), and we
get well typed functions eta : X->LX and mu : L(LX)->LX that satisfy the
monad laws.
If we assume propositional resizing, then all propositions live in the
first universe U0, and so does Prop, and then L becomes a monad in the
usual sense. But it is not clear what is gained by this (in this example)
other than getting something one is more familiar with.
In other examples, resizing does make a difference (of course). Consider
for example the assertion that Prop is a complete lattice with respect to
the "->" ordering . If we say that every family has a least upper bound,
then we don't need resizing to prove that (we use the propositional
truncation of the sum of the family to calculate the join). But to get
that every *subset* of Prop (that is, map s : Prop->Prop) has a least upper
bound, we would need resizing, as the natural candidate Sigma(P:Prop), s(P)
is a proposition in the next universe and hence is not in Prop unless we
have resizing. In this second example, the problem is solved by working
with families rather than subsets. Are there examples in which there is no
(known) way out without resizing?
Martin
On Wednesday, 24 January 2018 22:40:59 UTC, Nicola Gambino wrote:
>
> Dear Martin,
>
> On 24 Jan 2018, at 22:36, Martín Hötzel Escardó <escar...@gmail.com
> <javascript:>> wrote:
>
> So one vague question is how much one can do *without* propositional
> resizing and living with the fact that universe levels may go up and down
> in constructions such as the above. (A vague answer is "a lot", from my own
> experience of formalizing things.)
>
> A more precise question is that if we have a monad "up to universe
> juggling" (such as the above), what kind of universal property "up to
> universe juggling" does it correspond to.
>
>
> You may have a look at relative monads (Altenkirch et al) and relative
> pseudomonads (Fiore, Gambino, Hyland, Winskel). We considered the presheaf
> construction that takes a small category to a locally small one (and hence
> jumps up a universe) as a relative pseudomonad. Here, “pseudo” refers to
> coherence issues, which I am not sure arise in type theory.
>
> Best wishes,
> Nicola
>
> Dr Nicola Gambino
> School of Mathematics, University of Leeds
> Web: http://www1.maths.leeds.ac.uk/~pmtng/
>
>
[-- Attachment #1.2: Type: text/html, Size: 5082 bytes --]
next prev parent reply other threads:[~2018-01-25 10:14 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-01-24 15:13 Bas Spitters
2018-01-24 22:36 ` Martín Hötzel Escardó
2018-01-24 22:40 ` [HoTT] " Nicola Gambino
2018-01-25 10:14 ` Martín Hötzel Escardó [this message]
2018-01-25 10:23 ` Bas Spitters
Reply instructions:
You may reply publicly 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=8e5014ee-eaa1-47f3-abe0-56d49e50728f@googlegroups.com \
--to="escardo..."@gmail.com \
--cc="HomotopyT..."@googlegroups.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
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).