* Coquand's list of open problems
@ 2018-01-24 15:13 Bas Spitters
2018-01-24 22:36 ` Martín Hötzel Escardó
0 siblings, 1 reply; 5+ messages in thread
From: Bas Spitters @ 2018-01-24 15:13 UTC (permalink / raw)
To: homotopytypetheory
At the EUTypes meeting Thierry presented a list of five open problems in HoTT.
I've added them here. Maybe they should be moved to the various
categories we have there.
However, I did not immediately see where to put them.
https://ncatlab.org/homotopytypetheory/show/open+problems#coquands_five_open_problems
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Coquand's list of open problems
2018-01-24 15:13 Coquand's list of open problems Bas Spitters
@ 2018-01-24 22:36 ` Martín Hötzel Escardó
2018-01-24 22:40 ` [HoTT] " Nicola Gambino
0 siblings, 1 reply; 5+ messages in thread
From: Martín Hötzel Escardó @ 2018-01-24 22:36 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 2546 bytes --]
Thanks for posting this.
I am particularly interested in Problem 3, namely propositional resizing,
although of course all problems are relevant and interesting.
When one starts transcribing classical mathematics in constructive type
theory, it is not only excluded middle and choice that arise as obstacles,
but also the fact that a number of constructions don't preserve universe
levels (such as powersets, ideal completions, spaces of filters, etc), as
is well-known. So a positive solution to Problem 3 gets this out of the way.
However, in the absence of resizing, life doesn't look that bad, at least
at first sight. For example, the powerset construction (-) -> Prop (once we
fix the type Prop for a particular universe) is not a monad because of the
violation of universe levels, but other than that is has all the expected
structure needed to define a monad, as well as the required properties.
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.
This problem doesn't arise in 1-topos theory, which, by stipulation, has
propositional resizing of sorts, as this is implied by the very definition
of subobject classifier. But it seems that this is not a problem in a
univalent type theory: Maps X->Prop (even if Prop may be in a universe
higher than that of X) correspond to embeddings X'->X. Propositional
resizing then probably arises by analogy from 1-topos theory. But is it
really needed? This is not a rhetorical question, but a genuine
"operational" mathematical question: how does life without resizing look
like? We know a lot about how life without excluded middle (and hence
choice) looks like, but I think we know much less about life without
propositional resizing. I propose this as " Problem 3' ".
Martin
On Wednesday, 24 January 2018 15:14:05 UTC, Bas Spitters wrote:
>
> At the EUTypes meeting Thierry presented a list of five open problems in
> HoTT.
> I've added them here. Maybe they should be moved to the various
> categories we have there.
> However, I did not immediately see where to put them.
>
>
> https://ncatlab.org/homotopytypetheory/show/open+problems#coquands_five_open_problems
>
[-- Attachment #1.2: Type: text/html, Size: 3623 bytes --]
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [HoTT] Re: Coquand's list of open problems
2018-01-24 22:36 ` Martín Hötzel Escardó
@ 2018-01-24 22:40 ` Nicola Gambino
2018-01-25 10:14 ` Martín Hötzel Escardó
2018-01-25 10:23 ` Bas Spitters
0 siblings, 2 replies; 5+ messages in thread
From: Nicola Gambino @ 2018-01-24 22:40 UTC (permalink / raw)
To: Homotopy Type Theory, escardo...@gmail.com
[-- Attachment #1: Type: text/plain, Size: 1062 bytes --]
Dear Martin,
On 24 Jan 2018, at 22:36, Martín Hötzel Escardó <escardo...@gmail.com<mailto:escardo...@gmail.com>> 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 #2: Type: text/html, Size: 2670 bytes --]
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [HoTT] Re: Coquand's list of open problems
2018-01-24 22:40 ` [HoTT] " Nicola Gambino
@ 2018-01-25 10:14 ` Martín Hötzel Escardó
2018-01-25 10:23 ` Bas Spitters
1 sibling, 0 replies; 5+ messages in thread
From: Martín Hötzel Escardó @ 2018-01-25 10:14 UTC (permalink / raw)
To: Homotopy Type Theory
[-- 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 --]
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [HoTT] Re: Coquand's list of open problems
2018-01-24 22:40 ` [HoTT] " Nicola Gambino
2018-01-25 10:14 ` Martín Hötzel Escardó
@ 2018-01-25 10:23 ` Bas Spitters
1 sibling, 0 replies; 5+ messages in thread
From: Bas Spitters @ 2018-01-25 10:23 UTC (permalink / raw)
To: Nicola Gambino; +Cc: Homotopy Type Theory, escardo...@gmail.com
> life without propositional resizing
That's what used to be called predicativity, isn't it :-)
More seriously, yes, in my experience, working in HoTT with a large
universe polymorphic hProp one can nicely encapsulate some of the
predicativity issues.
But we definitively need more experience doing it.
Are you aware of the relative universes presentation of CwFs?
Ahrens, Lumsdaine, Voevodsky:
https://arxiv.org/abs/1705.04310
On Wed, Jan 24, 2018 at 11:40 PM, Nicola Gambino <N.Ga...@leeds.ac.uk> wrote:
> Dear Martin,
>
> On 24 Jan 2018, at 22:36, Martín Hötzel Escardó <escardo...@gmail.com>
> 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/
>
> --
> 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.
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2018-01-25 10:23 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-01-24 15:13 Coquand's list of open problems 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ó
2018-01-25 10:23 ` Bas Spitters
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).