From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.237.43.135 with SMTP id e7mr1850125qtd.121.1500533783885; Wed, 19 Jul 2017 23:56:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.79.21 with SMTP id c21ls414817itb.16.gmail; Wed, 19 Jul 2017 23:56:23 -0700 (PDT) X-Received: by 10.107.173.225 with SMTP id m94mr1832187ioo.114.1500533783156; Wed, 19 Jul 2017 23:56:23 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500533783; cv=none; d=google.com; s=arc-20160816; b=ogsIUC6FKPegP2yiOyCzD6BqyfkE1YTIzz8ha0PLF8NsYwfZgQHrDKPX1UtDi08ogw zWaFi4y8sRNsJQNrGBPREGv2Cz9yLO7vny1cxYFxuClRGItLllS3eQ5bdzz2LDfLdbNc dg/14DYFg7g4hcanZBzv1wk+tljbYHThKGdx0pbsEY4946x+/DcXFHMGBQPMnaWOQBY7 EAs61HZHr+qKbTaetJBXyBmbSFJR1uB9xI2nTPyWrKqOu0hka5+OjOf18y2bYzAHlM3T diQktyWZit5+56jaELUGxpSclXW+9efJc4hrlVMJhlMBRQ/BH2tzOo0KPbTfUZgy5XEC HDXQ== 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=jMZyV/vYnVJk42UMIWNI8fci7HZvNCtp76v2Di6DUWk=; b=x3lap4HXQV16LpHwcvcf/aTRWeOs9lgqEUWZgawXhxQ5UJ6v2ITKW3+K+MdROcbdW7 L6I0TPwzZqoGEfm14cxCDHTHR3aN9QJdfqPomUwgqyS/39FJwf8+Kmu1BegtcesKKA/C mtywVXNx2K5vtWtGxJDOpGJbwjCBOwqi5iYMD3pq2rNU+Q7pcah7AOfdOOpVqdlzCPyb 7fm9uEuCXWER9VCymfqeBKhicMg/9UW/f6y6Dc4vCIYllvtdxWgVZKmPybK0SV/5uEK4 sOh5dThjVz5jbxkWaGp6/rYz14An/STC3PcOnZdiPGyHTvQwfMKMpsRtq63LoTmUJCAS vC2A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.b=eK3JbWNi; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c08::22b 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-ua0-x22b.google.com (mail-ua0-x22b.google.com. [2607:f8b0:400c:c08::22b]) by gmr-mx.google.com with ESMTPS id j134si109297vke.5.2017.07.19.23.56.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 19 Jul 2017 23:56:23 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c08::22b as permitted sender) client-ip=2607:f8b0:400c:c08::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.b=eK3JbWNi; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c08::22b 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-ua0-x22b.google.com with SMTP id 80so16262770uas.0 for ; Wed, 19 Jul 2017 23:56:23 -0700 (PDT) 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=jMZyV/vYnVJk42UMIWNI8fci7HZvNCtp76v2Di6DUWk=; b=eK3JbWNiwIPsqDqVHr/uRe2bxEMwP3LWyTO8xDzr6b7FxYfJhJh9sWL39oV4fYVPXs Kj0Q7V/BHNlebXvn7Jk8pBbCAw94i11SO11Elrti7JwB3q3/r/uk2aahVAz2XiRlkZ0J 1r15McrFlWATIaRtyJ3Tzrw/WW0dgRyXpqNWLNUXoGHrL7Ycd5nUTUNqxN3rKDq2uPGB eMHPkj7iMWO+RHisfTtwcnStbWzHvQTXo7uv8DbqhnepB+HOwnXSp90T3FbMF5WpFwrs xzQvGtpAIreY7RkMcGNHarHUyi/ALI3FxClS9beNc78cG4P1kBd/N/XNUvDy3Tw3Y4oY sBIg== X-Gm-Message-State: AIVw111DuafrDtjUVGV6pRDEKBbOLF6x4xJb4LHo3SkkIihfBEbPCwIh IC1Nu6OmUeKZzr9lb/B2y5iaxXtd3OcSdg4= X-Received: by 10.159.34.85 with SMTP id 79mr1626154uad.86.1500533782911; Wed, 19 Jul 2017 23:56:22 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.19.129 with HTTP; Wed, 19 Jul 2017 23:56:02 -0700 (PDT) In-Reply-To: References: From: Bas Spitters Date: Thu, 20 Jul 2017 08:56:02 +0200 Message-ID: Subject: Re: [HoTT] Weaker forms of univalence To: Michael Shulman Cc: Ian Orton , "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable >It was observed previously on this list, Maybe we should be using our wiki more? https://ncatlab.org/homotopytypetheory/ On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman wrot= e: > It was observed previously on this list, I think, that full univalence > (3) is equivalent to > > (4) forall A, IsContr( Sigma(B:U) (A =E2=89=83 B) ). > > This follows from the fact that a fiberwise map is a fiberwise > equivalence as soon as it induces an equivalence on total spaces, and > the fact that based path spaces are contractible. But the > contractibility of based path spaces also gives (2) -> (4), and hence > (2) -> (3). > > I am not sure about (1). It might be an open question even in the > case when A and B are propositions. > > > On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton wrote: >> Consider the following three statements, for all types A and B: >> >> (1) (A =E2=89=83 B) -> (A =3D B) >> (2) (A =E2=89=83 B) =E2=89=83 (A =3D B) >> (3) isEquiv idtoeqv >> >> (3) is the full univalence axiom and we have implications (3) -> (2) -> = (1), >> but can we say anything about the other directions? Do we have (1) -> (2= ) or >> (2) -> (3)? Can we construct models separating any/all of these three >> statements? >> >> Thanks, >> Ian >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.