From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.37.66.87 with SMTP id p84mr3150623yba.45.1516806845158; Wed, 24 Jan 2018 07:14:05 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.37.189.70 with SMTP id p6ls466532ybm.13.gmail; Wed, 24 Jan 2018 07:14:04 -0800 (PST) X-Received: by 10.129.199.2 with SMTP id m2mr3603761ywi.14.1516806844241; Wed, 24 Jan 2018 07:14:04 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1516806844; cv=none; d=google.com; s=arc-20160816; b=WqRGeG7tadJ0U6AidERbOaO3Yta/Z3H54QeR+pX47oUF6S4YH9Df4bD54pjQMVf7cN x460gpCb3+eTWOTptpZbfClv0bPWdul7ovwqYj7DjEkf2vKqzY6CgShQmturFICX1vdM OK57BM2sgDEGgSWhr9fODbrbzwfx9X9sz6TIad4H3nliWMdHOJPgLHs32dl4FoSAB8Aj xKHW3EN+LkZf0foLgEgO2cUv6cdmsCaynhj+620V9xDLl9x9KSrdt6rH85ok9DIgVau2 RB3kWo4vL6oV8ORg9IX4t0pPh1ZV0/gCIT1VC9yqhqeGmrSWNsNNsvmdssvfzYOqyhfq ZFKA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature :arc-authentication-results; bh=uLndREyIbOJCH4rChD+VdtSw0hGI0GuQwXawMvmECuk=; b=dRTjXJ0cmzFqbPjE/6vQxs3Y+qEDcqIty84vXa2XGqcTZsI+prTwO5VfEhzZLeAlzn Kn+CzTXxFFVNlCZnuwXHu/PQLtrtGsdumbxbdNJ4AGkeDIxxPZLrHJEkV8cpMRrSlNI7 GEkxam/vc/I3fVFBd7O/70R7dxL9a48HMWzPoxHYYZ3wis3czKnMElBPetEXA0yYKuB3 o/bZPojqbhBUofV15/Aoi+98mcgv1FX3A0vvVhOJJtKeyYu0IWSMlYakWJH2/+PE0QA7 HVhuNCr80yMtLtoqjBTn80xWBtgDwcBtwJCvNw9PuMP/WFJKUm4I0c6UnEyKy3xGAon0 vZXQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=owOXhK/n; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400d:c0d::242 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-x242.google.com (mail-qt0-x242.google.com. [2607:f8b0:400d:c0d::242]) by gmr-mx.google.com with ESMTPS id t4si728181ybl.3.2018.01.24.07.14.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 24 Jan 2018 07:14:04 -0800 (PST) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400d:c0d::242 as permitted sender) client-ip=2607:f8b0:400d:c0d::242; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=owOXhK/n; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400d:c0d::242 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-x242.google.com with SMTP id o35so11054247qtj.13 for ; Wed, 24 Jan 2018 07:14:04 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to; bh=uLndREyIbOJCH4rChD+VdtSw0hGI0GuQwXawMvmECuk=; b=owOXhK/ngs8VZfbVuWgQEQ9j3yi547hPj7q0fsi7lrX+q3ESUtnPETxVS36z/EQzmU WhWKcC9Yh1hQ5EG68gKVifw6iv26aH/6LzbNNcr8NderacDaS4MFEm6Xyf/W1ESJtyZQ QA7SUi0OywuAgUmw/O+ncib/Uscsp50Wf1mwx+q+cdPcpg+IYVH2D8J5SBx0UvFvMclo RYoAXS8tWqWyVKdIjd9fNRvkOp3W7V2sfTvw7K3YQzjiABXW8MhGq9nsfu5KXRmdLEGt MNWkw97Zjlnf8mSm9sI7iFVuWYl+x/cDpXCUPSiQ0AV237LPeXVJx6QnawQhbFi5S9Gs dY5w== X-Gm-Message-State: AKwxytdHmo9d29f6QGZ5spqYwwYr50rnR2hajXUW/m/y6DA9+WY2k1zR 1hgbnqyKUPYT2rKEaQhkraolHcSZE8rJv+NQ5W8Xicbx X-Received: by 10.55.168.83 with SMTP id r80mr10111367qke.89.1516806843842; Wed, 24 Jan 2018 07:14:03 -0800 (PST) MIME-Version: 1.0 Received: by 10.12.149.188 with HTTP; Wed, 24 Jan 2018 07:13:43 -0800 (PST) From: Bas Spitters Date: Wed, 24 Jan 2018 16:13:43 +0100 Message-ID: Subject: Coquand's list of open problems To: homotopytypetheory Content-Type: text/plain; charset="UTF-8" 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