From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a81:7a01:: with SMTP id v1-v6mr3173621ywc.168.1526658060910; Fri, 18 May 2018 08:41:00 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:3988:: with SMTP id g130-v6ls497207ywa.43.gmail; Fri, 18 May 2018 08:41:00 -0700 (PDT) X-Received: by 2002:a0d:f082:: with SMTP id z124-v6mr2974419ywe.73.1526658060004; Fri, 18 May 2018 08:41:00 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1526658059; cv=none; d=google.com; s=arc-20160816; b=mPf3Tc3d/0w6rS7iYAacv6peWrbh2mk/WLHZa4QpRO23yintn/Khuq25bgrbW2c9iT Z6ngudn1/mfvLYNRphbMKFycKzXRDZRw6BhKJXQJ6LCaEInxu1FGXgnD4BX8/hTaD636 JBxP11bp8wuoErS4tZYnDB+mVs5+8TDggbWwLet+ZaqsAB6K8bH/Uu4sSGKTpkZocf5u 35gDe8jTl7F7Kw2OPHH01z5NlDWWrV1L35AldVTZjUSO/ombGEH3e6/UsrQz5T6IiaQK fSzw2ktN4MNfVB9G6BV8y01Y7M2FOBWrIUTBxGqkWl9O9zZakX3GhajZ+MJopEzKpfFB dyBQ== 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=xhCai/s9DdFXyjadYuRDhr1eI3EH5i4OiHSP04dju/E=; b=ox2RmKGrjp58J3cDBUuI5B/wgL72wF1xdcEW6UKMv27a6aGFj+2fC3Gaz+khU0tes7 yIhzCsK9tyubuLz2nXZT1WQo0KrqzNml4IRTiPX5gUjoLthH84obNfYEK5pP3x2l7F4o w+dfEAntHeJH5jsAgDlFlqNzYDxs2332LNlbkzEGUWLhQdieTibtL4yXdekZ/RzuFj1B pD9AHfW4aCGZ2T/mK6nAXLO5Wn67lsCRtoQBZtja1vLLvCpr3TyvKQKHW/oLzrcf4EiQ ZWDyi5SnR44aZ17IjdNq9QZmomELIY1hB+eL9+bu9JmeARWdIpcGe2CIedSffht7Bjb8 JCYQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=tjnwTMR5; spf=neutral (google.com: 2607:f8b0:4002:c05::22a is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x22a.google.com (mail-yw0-x22a.google.com. [2607:f8b0:4002:c05::22a]) by gmr-mx.google.com with ESMTPS id x4-v6si571012ybk.2.2018.05.18.08.40.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 18 May 2018 08:40:59 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22a is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::22a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=tjnwTMR5; spf=neutral (google.com: 2607:f8b0:4002:c05::22a is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x22a.google.com with SMTP id m8-v6so2536318ywd.2 for ; Fri, 18 May 2018 08:40:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=xhCai/s9DdFXyjadYuRDhr1eI3EH5i4OiHSP04dju/E=; b=tjnwTMR5C/A27U7vqZjPjKD2TfXDrYIe5nH3Kr7IorUQEEf/W0Z2CpJB3gvCv/lkmz VBZJPVxWMPs5yQ8ymeRKJxHq+qrHMy+pq8foGiwHc7gnGBUiaFnUjZ/ur8HkmrrxxZhn /ersT553x3h0AyxVKKrQkTqj5W5wFnt4662PGQAF5ctSqHqASdCS5wTIOA8XZRv2lpN2 DK66QgAwrpys7ZI3nZacOjdtfyGDrhzL1Hh9+KVWEW+D1AgxOip8FeDLFarb7JBXka1y pf92s3msJHJUY+/bWJU5XxyXLrlmzs6+9bMVfBfkWlvT0onYA5KDyd/78oQlqSAL1WcW HjOA== X-Gm-Message-State: ALKqPwcYA9WdH4kiYLkAGuljQIhrj4IBBYd5cvCUjJ+b0hBsPTJ29FNI p/QESs3uKVOpxwYOaBUHQ9dQ5oAm X-Received: by 2002:a81:6282:: with SMTP id w124-v6mr5191239ywb.58.1526658059562; Fri, 18 May 2018 08:40:59 -0700 (PDT) Return-Path: Received: from mail-yb0-f179.google.com (mail-yb0-f179.google.com. [209.85.213.179]) by smtp.gmail.com with ESMTPSA id 79-v6sm3265372ywr.2.2018.05.18.08.40.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 18 May 2018 08:40:59 -0700 (PDT) Received: by mail-yb0-f179.google.com with SMTP id v12-v6so2830094ybl.10 for ; Fri, 18 May 2018 08:40:59 -0700 (PDT) X-Received: by 2002:a25:2bc1:: with SMTP id r184-v6mr5590450ybr.120.1526658059048; Fri, 18 May 2018 08:40:59 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d297:0:0:0:0:0 with HTTP; Fri, 18 May 2018 08:40:38 -0700 (PDT) In-Reply-To: References: <4f23688f-af7c-43cb-946c-988f9d476848@googlegroups.com> From: Michael Shulman Date: Fri, 18 May 2018 08:40:38 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Univalence <-> equivalence induction To: Egbert Rijke Cc: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I certainly knew that univalence is equivalent to equivalence-induction *with* computation rule, which I think is what is in Egbert's notes. But I don't think I knew that you can do without the computation rule. Can you give a link to the "some years ago" discussion claiming it strictly weaker? On Fri, May 18, 2018 at 6:04 AM, Egbert Rijke wrote: > Hi Martin, > > I think it was known. I taught this in my intro to HoTT class this semest= er: > > http://www.andrew.cmu.edu/user/erijke/hott/univalence.pdf > > Best wishes, > Egbert > > On Fri, May 18, 2018 at 2:36 AM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 > wrote: >> >> Equivalence induction says that in order to prove something for all >> equivalences, it is enough to prove it for all identity equivalences for= all >> types. >> >> This follows from univalence. But also, conversely, univalence follows >> from it: >> >> http://www.cs.bham.ac.uk/~mhe/agda-new/UF-Univalence.html#JEq >> >> Is this known? Some years ago it was claimed in this list that equivalen= ce >> induction would be strictly weaker than univalence. >> >> To prove the above, I apply a technique I learned from Peter Lumsdaine, >> that given an abstract identity system (Id, refl , J) with no given >> "computation rule" for J, produces another identity system (Id, refl , J= ' , >> J'-comp) with >> a "propositional computation rule" J'-comp for J'. >> >> http://www.cs.bham.ac.uk/~mhe/agda-new/Lumsdaine.html >> >> Martin >> >> -- >> 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. > > > > > -- > egbertrijke.com > > -- > 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.