From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.55.125.67 with SMTP id y64mr6001281qkc.38.1516875834756; Thu, 25 Jan 2018 02:23:54 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.237.56.67 with SMTP id j61ls2428330qte.13.gmail; Thu, 25 Jan 2018 02:23:53 -0800 (PST) X-Received: by 10.200.3.87 with SMTP id w23mr6985469qtg.5.1516875833843; Thu, 25 Jan 2018 02:23:53 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1516875833; cv=none; d=google.com; s=arc-20160816; b=JSfgccZpwalp8HxcgleZQWaAjS0G4rcTcrnBeHU91PxQRExsRpU8E9roq9Wbcu301p fd68WRK4+k5p7R68yZM6vE9XFtTg2ar3BYU9wWhn1rN8vZKxtoibZmnITP/aWWpQBpd5 W9Aav333hMmRtoOeBOzP/FYgwsjeu95Ad8wg5e403LUdq9a5s8F2D6ZT4RkLAgXdk1a8 /vG6+66YMNr8gBmGTHSn26rQ/WX+SUr4UNt1JVO+SW04IJvRiOPfOFRnlQuir7A8szUt Vxq0bRReYPcpk/eycK9xlUOKjxB/rx9DzhtZhfOaxcPOsvIXjx8ZPKyT7x3WBsknxfCY MUZw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=uUI1kyZ57WsNqKv8UqgU3OQXKckln+7BF8epucE3Xps=; b=ZiAJz6UhE4NLgBJM5KSCrmMjo7QqHycUKpBTGRFtJKIQK6SYN9E7oSLUEK9jT0wlW4 iawggjDDswZlG/x4cLzrtVtcD54TPHkQSIwgXOKuPwJFtI2ypjxugxzIThhlc15Jp8za 7tXuKlx4In4be9wYX4dvQn2a/haO395wS5db6xWixUoHdyP/UF4NGPyw59rCR1Vq7TBb S7jtKtRUbQsRjzczmaf9u8/HjBDjCEI+OdM+v+FGZz+mhY2y559a34V/A3QNba6210Fi 8URKHi+FaSbrvtEaQolZEYUMWE5Y1mCixRnIRtmUVcXNMdFgby9Cr/N2QFYoG9a03ufH f5+w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Xq9Lqjof; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400d:c0d::233 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qt0-x233.google.com (mail-qt0-x233.google.com. [2607:f8b0:400d:c0d::233]) by gmr-mx.google.com with ESMTPS id r22si372601qtj.2.2018.01.25.02.23.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 25 Jan 2018 02:23:53 -0800 (PST) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400d:c0d::233 as permitted sender) client-ip=2607:f8b0:400d:c0d::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Xq9Lqjof; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400d:c0d::233 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-qt0-x233.google.com with SMTP id f4so17876709qtj.6 for ; Thu, 25 Jan 2018 02:23:53 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=uUI1kyZ57WsNqKv8UqgU3OQXKckln+7BF8epucE3Xps=; b=Xq9LqjofC3qDAwqoZRao9jaNPgW0zgZ3p7CNGW8ngh0htg6K/EeljgOqnW3SCjEaKo /oKicjbYIGlRrruN6Pk+aeYajCcOQLO3j5D8bDABSctl7ZhlNabm3RlzBct5cDZh4sH+ swUpIPwTcNQ/bVxKGC4fMoQnsyS+WlirgKoEyY9DUoCxUKRUZPJf7B0UMXGHNmvFWilo PNn+F8RcKA+DlMYa5Rn0FxwVnu8KOUVBcAo/yhBIyqPcB+jvKozQz3NeDwHYNHwzwgTN dsQmE7ovk925oes/05YvYay05oRBPoZEdZTqQA87BI82THcfsy6qhHrwLo1ccukxcIMZ Y0lw== X-Gm-Message-State: AKwxytfR1KPTJ54gLY+OF8lC8Rt+qvyTeNWUO9emaXSAjiq2aa23+Uea Z41R6rJ1ms4RM1EhzR1/EeS3BjbLMrERgj5hRX1pOq1t X-Received: by 10.200.23.219 with SMTP id r27mr15562556qtk.314.1516875833603; Thu, 25 Jan 2018 02:23:53 -0800 (PST) MIME-Version: 1.0 Received: by 10.12.149.188 with HTTP; Thu, 25 Jan 2018 02:23:33 -0800 (PST) In-Reply-To: References: <17bbe329-b471-490c-b11d-31c50f1334f1@googlegroups.com> From: Bas Spitters Date: Thu, 25 Jan 2018 11:23:33 +0100 Message-ID: Subject: Re: [HoTT] Re: Coquand's list of open problems To: Nicola Gambino Cc: Homotopy Type Theory , "escardo...@gmail.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > 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 wrot= e: > Dear Martin, > > On 24 Jan 2018, at 22:36, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 > 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 juggli= ng" > (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 preshea= f > construction that takes a small category to a locally small one (and henc= e > jumps up a universe) as a relative pseudomonad. Here, =E2=80=9Cpseudo=E2= =80=9D 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.