From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.141.85 with SMTP id p82mr1810274lfd.10.1473968376898; Thu, 15 Sep 2016 12:39:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.193.78 with SMTP id r75ls430913wmf.9.gmail; Thu, 15 Sep 2016 12:39:35 -0700 (PDT) X-Received: by 10.194.79.231 with SMTP id m7mr1803114wjx.4.1473968375840; Thu, 15 Sep 2016 12:39:35 -0700 (PDT) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id e21si368794wmc.2.2016.09.15.12.39.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 15 Sep 2016 12:39:35 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.54] (helo=mailer3) by sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1bkcVT-00013o-Oc for homotopyt...@googlegroups.com; Thu, 15 Sep 2016 20:39:35 +0100 Received: from host86-137-209-253.range86-137.btcentralplus.com ([86.137.209.253] helo=[192.168.1.112]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1bkcVT-0001rT-E2 for homotopyt...@googlegroups.com using interface auth-smtp.bham.ac.uk; Thu, 15 Sep 2016 20:39:35 +0100 Subject: Re: [HoTT] weak univalence with "beta" implies full univalence References: <9F0041A0-328D-4C4F-8152-3E42305D372E@cs.cmu.edu> To: Homotopy Type Theory From: Martin Escardo Message-ID: Date: Thu, 15 Sep 2016 20:39:35 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) Nice, Dan and Anders and Thierry. Martin On 15/09/16 18:35, Anders wrote: > Hi, > > I've formalized this in cubicaltt now, a self-contained formalization > can be found here: > > https://github.com/mortberg/cubicaltt/blob/master/experiments/univalence_dan.ctt#L123 > > The proof is a little different from Dan's and follows a sketch that I > got from Thierry: > > We have that > > ua + uabeta > > implies that Equiv A B is a retract of Path U A B. Hence > > (X:U) x Equiv A X is a retract of (X:U) x Path U A X > > But (X:U) x Path U A X is contractible (contractibility of > singletons). So (X:U) x Equiv A X is contractible as it is a > retraction of a contractible type. This is an alternative formulation > of the univalence axiom as noted by Martín: > > https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ > > > One difference with Dan's proof is that this is not using the "grad > lemma" (if f has a quasi-inverse then it is an equivalence (called > "improve" in Dan's code)). It also shows that not having the > computation rule for J definitionally doesn't get in the way, however > having it would have made the proof of uabeta trivial (I now have to > do some work by hand as two transports don't disappear). > > -- > Anders > > On Wed, Sep 7, 2016 at 11:10 AM, Dan Licata wrote: >> Hi, >> >> What I’m about to say is a trivial consequence of an observation that Egbert/Martin made a couple of years ago (https://github.com/HoTT/book/issues/718), so maybe other people have already realized this, but it was surprising to me. >> >> In particular, based on Martin’s observation https://github.com/HoTT/book/issues/718#issuecomment-65378867 >> that any retraction of an identity type is an equivalence: >> >> retract-of-Id-is-Id : ∀ {A : Set} {R : A → A → Set} → >> (r : {x y : A} → x == y -> R x y) >> (s : {x y : A} → R x y → x == y) >> (comp1 : {x y : A} (c : R x y) → r (s c) == c) >> → {x y : A} → IsEquiv {x == y} {R x y} (r {x}{y}) >> >> it is enough to assert “ua” (equivalence to path) and the “beta” direction of the full univalence axiom, i.e. the fact that transporting along such a path is the equivalence: >> >> ua : ∀ {A B} → Equiv A B → A == B >> uaβ : ∀ {A B} (e : Equiv A B) → transport (\ X -> X) (ua e) == fst e >> >> The “eta” direction comes for free by Martin’s argument. >> >> Here is a self-contained Agda file that checks this: >> https://github.com/dlicata335/hott-agda/blob/master/misc/UABetaOnly-SelfContained.agda >> (Almost all of the file is boilerplate, but I wanted to make sure I wasn’t accidentally using anything from my library that relies on univalence.) >> >> Unless the absence of definitional beta reduction for J somehow gets in the way, I think this gives another arugment why the Glue type in the Cohen,Coquand,Huber,Mortberg cubical type theory gives full univalence: the only thing specifc to cubical type theory that you need to check is that ua and uaβ can be derived from Glue, and the rest of the argument can happen in book HoTT. This is a small simplification/rearrangement of the argument in Appendix B of their paper, essentially saying that condition (3) of Lemma 25 can be replaced by the retraction lemma. >> >> -Dan >> >> -- >> 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. >