From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.42.4 with SMTP id q4mr5814477ywq.100.1507749168164; Wed, 11 Oct 2017 12:12:48 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.13.217.195 with SMTP id b186ls155730ywe.9.gmail; Wed, 11 Oct 2017 12:12:47 -0700 (PDT) X-Received: by 10.37.190.202 with SMTP id k10mr5533938ybm.4.1507749167298; Wed, 11 Oct 2017 12:12:47 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507749167; cv=none; d=google.com; s=arc-20160816; b=PJ6WogSQsYOMyVrBZtF382qPowuEkzNgXvHe+tsBFmUkHd8wwT3DkiVtmZbTD7mrWD ruZMgzmuYsQr+8PBO7cjSs7o6cybWB2nikxF/3JrJ5HA9JMF6IE1Sifaxk+V/QfZZaLM rzoo09YB7RFtLEOlVpV37C5/2GI8sVgCNTowSn+A8nVMJS/zECVptT/RhyOPskymH82+ HEZNj6SqJ5RaiiXcptk0FZZuCA1WRySSq11DuqdcgwbB97Wn69BBx6jFVQlgmKr8eKfL eBz1myKoDI2ngPpbGZXfQi2a+CbZrxT3R5hEIUG6hBGp5XwS+4kWOBSpPOnLgxwOUCX8 y/Ng== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:dkim-signature:arc-authentication-results; bh=pVGYZMiaS5X7TcYO9c9BNOxNqaRZrj/ri3tJmtmOHoI=; b=qcadtUjDkbd1dSgR5hCHs/cBeeB8TtwsFU/i3b7OBiOF7KsVKNBmCHwzZkOwNiQPNO Hp3wXUOs8/B0XWK6IjP1/oE2e0/2q6XXU1hZRiOdcW7xYNk8Tl3/Lae254UyBkH86AnR LSKVmvkn5qMyT7kJ73CdB5iMpbwVvO+4MH/3IVXZhRFq2blqDFrHV02BxHMDIYbyHfrq V5h4/YayEpQY1qwuGJYBWP4uP2hxQagOGL/BSHbhQHgaMtCiCijG+ot6XC2ThSjKcm+S 5Q4MOivMNNAKEwYAaWURk0f1Q6DEws13cM+heED67Fk39BKtHHqRvn94NsmALc6m54mn zEMw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=iW08lqCL; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:400d:c0d::229 as permitted sender) smtp.mailfrom=steve...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qt0-x229.google.com (mail-qt0-x229.google.com. [2607:f8b0:400d:c0d::229]) by gmr-mx.google.com with ESMTPS id w205si70501ywc.24.2017.10.11.12.12.47 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 11 Oct 2017 12:12:47 -0700 (PDT) Received-SPF: pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:400d:c0d::229 as permitted sender) client-ip=2607:f8b0:400d:c0d::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=iW08lqCL; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:400d:c0d::229 as permitted sender) smtp.mailfrom=steve...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-qt0-x229.google.com with SMTP id o52so8368767qtc.9 for ; Wed, 11 Oct 2017 12:12:47 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:message-id:mime-version:subject:date:in-reply-to:cc:to :references; bh=pVGYZMiaS5X7TcYO9c9BNOxNqaRZrj/ri3tJmtmOHoI=; b=iW08lqCL+mhFg4l/x+6JWfye2WAr+GBBuez5zJKbHRI6DVc3w6NMIhP3N4r0+7TA2d yBqbqold81cylaeNBbWobLF0kopINMuOkL8JPQaIyQiPuOQcqgBHTTsDgcqE/fDM3P1c zKUe8VY0sEYA0C52KMfWNRjpZ1aRuVImlL4P/QrzICG9WaUWgJogAZ7Ecy3v/rjO/c6+ xuIEEgDpq5Y+9rqFYlmKOcj83gKlJIyeZ0c/4JGJNR8C7wpmm1Yx+mg+lkmE6iXfTfzC dei7MzPkssD16FoQljqlXy/R+KcNfioT0Uy13p4MdA3LLfG8l4YnvSx35Wae7GUnnVus j4Kg== X-Gm-Message-State: AMCzsaUizgdJS0MQjiYUI68vS/DNbwaOyoRuqqfzJzsB0uSjeySmSKJq ZtZjxvlVSDXiZBqmeeBM6n3qdVlTYmM= X-Received: by 10.55.118.193 with SMTP id r184mr65894qkc.348.1507749167029; Wed, 11 Oct 2017 12:12:47 -0700 (PDT) Return-Path: Received: from steveawodeysair.home (pool-74-98-213-110.pitbpa.fios.verizon.net. [74.98.213.110]) by smtp.gmail.com with ESMTPSA id x68sm8202344qkc.84.2017.10.11.12.12.44 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 11 Oct 2017 12:12:45 -0700 (PDT) From: Steve Awodey Message-Id: Content-Type: multipart/alternative; boundary="Apple-Mail=_402CA2FD-10C1-491F-A7B7-19A754FC91A5" Mime-Version: 1.0 (Mac OS X Mail 10.3 \(3273\)) Subject: Re: [HoTT] Re: Vladimir Voevodsky Date: Wed, 11 Oct 2017 15:06:36 -0400 In-Reply-To: Cc: Homotopy Type Theory To: "Daniel R. Grayson" References: X-Mailer: Apple Mail (2.3273) --Apple-Mail=_402CA2FD-10C1-491F-A7B7-19A754FC91A5 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 thanks for posting this Dan.=20 It=E2=80=99s very interesting to learn the background of the discovery of u= nivalence. Steve > On Oct 11, 2017, at 1:47 PM, Daniel R. Grayson > wrote: >=20 > At https://en.wikipedia.org/wiki/Homotopy_type_theory Voevodsky says this: >=20 > "Also in 2009, Voevodsky worked out more of the details of a model of typ= e > theory in Kan complexes, and observed that the existence of a universal K= an > fibration could be used to resolve the coherence problems for categorical > models of type theory. He also proved, using an idea of A. K. Bousfield, = that > this universal fibration was univalent: the associated fibration of pairw= ise > homotopy equivalences between the fibers is equivalent to the paths-space > fibration of the base." >=20 > When I asked him about that, he showed me the email from Bousfield,=20 > answering Vladimir's question as forwarded by Peter May, containing > a very nice description of the idea, and here it is: >=20 > -------------------------------------------------------------------------= ---- > Date: Mon, 01 May 2006 10:10:30 CDT > To: Peter May > > cc: jar...@uwo.ca , pgo...@math.northwestern.e= du > From: "A. Bousfield" > > Subject: Re: Simplicial question >=20 > Dear Peter, >=20 > I think that the answer to Voevodsky's basic question is "yes," and I'll > try to sketch a proof. >=20 > Since the Kan complexes X and Y are homotopy equivalent, they share the > same minimal complex M, and we have trivial fibrations X -> M and Y -> M > by Quillen's main lemma in "The geometric realization of a Kan fibration > ." Thus X + Y -> M + M is also a trivial fibration where "+" gives the > disjoint union. We claim that the composition of X + Y -> M + M with th= e > inclusion M + M >-> M x Delta^1 may be factored as the composition of an > inclusion X + Y >-> E with a trivial fibration E -> M x Delta^1 such tha= t > the counterimage of M + M is X + Y. We may then obtain the desired > fibration >=20 > E -> M x Delta^1 -> Delta^1 >=20 > whose fiber over 0 is X and whose fiber over 1 is Y. >=20 > We have used a case of: >=20 > Claim. The composition of a trivial fibration A -> B with an inclusion B > -> C may be factored as the composition of an inclusion A >-> E with a > trivial fibration E -> C such that the counterimage of B is A. >=20 > I believe that this claim follows by a version of the usual iterative > construction of a Quillen factorization for A -> C using the "test" > cofibrations > Dot Delta^k >-> Delta^k > for all k. At each stage, we use maps from the "test" cofibrations > involving k-simplices of C outside of B. >=20 > I hope that this helps -- I haven't thought about Voevodsky's more > general question. >=20 > Best regards, > Pete >=20 > On Sun, 30 Apr 2006, Peter May wrote: >=20 > Here is an extract from an email from Voevodsky (vlad...@ias.edu ) >=20 > ----------------- >=20 > =09Q. Let X and Y be a pair of Kan simplicial sets which are homotopy > =09equivalent. Is there a Kan fibration E -> \Delta^1 such that its > =09fiber over 0 is X (up to an iso) and its fiber over 1 is Y (up to an > =09iso)? >=20 > =09A more advanced version of the same question: let X' -> X and X'' -> > =09X be two Kan fibrations which are fiberwise equivalent to each other > =09over X. Is there a kan fibration over X\times\Delta^1 whose fiber > =09over X\times 0 is isomorphic to X', fiber over X\times 1 is > =09isomorphic to X'' and the homotopy between the two inclusions of X to > =09X\times\Delta^1 define the original equivalence (up to homotopy)? >=20 > =09I encountered this issue trying to write up a semantics for dependent > =09type systems with values in the homotopy category. which is in turn > =09related to the problem of creating computer programs for proof > =09verification. > -------------------------------------------------------------------------= ---- >=20 >=20 > --=20 > 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 . --Apple-Mail=_402CA2FD-10C1-491F-A7B7-19A754FC91A5 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
thanks for posting this Dan. 
It=E2=80=99s very interesting to learn the background of the discover= y of univalence.

= Steve

On Oct 11, 2017, at 1:47 PM, Daniel R.= Grayson <danielri= ch...@gmail.com> wrote:

At https://en.w= ikipedia.org/wiki/Homotopy_type_theory Voevodsky says this:

"Also in 2009, Voevodsky wor= ked out more of the details of a model of type
theory = in Kan complexes, and observed that the existence of a universal Kan
<= div class=3D"">fibration could be used to resolve the coherence problems fo= r categorical
models of type theory. He also proved, u= sing an idea of A. K. Bousfield, that
this universal f= ibration was univalent: the associated fibration of pairwise
homotopy equivalences between the fibers is equivalent to the paths-= space
fibration of the base."
When I asked him about that, he showed me= the email from Bousfield, 
answering Vladimir's = question as forwarded by Peter May, containing
a very = nice description of the idea, and here it is:

----------------------------------------------= -------------------------------
Date:    Mon= , 01 May 2006 10:10:30 CDT
To:      Pet= er May <m...@math.u= chicago.edu>
cc:      jar...@uwo.ca, pgo...@math.northwestern.edu
=
From:    "A. Bousfield" <bo...@uic.edu>
Subject: = Re: Simplicial question

Dear Peter,

I think that the answer to Voevodsky's basic question is "yes," and I'll<= /div>
try to sketch a proof.

Since the Kan complexes X and Y are homotopy&nb= sp; equivalent, they share the
same minimal complex M,= and we have trivial fibrations X -> M  and Y -> M
by Quillen's main lemma in "The geometric realization of a Kan fibr= ation
."  Thus  X + Y -> M + M is also a = trivial fibration where "+" gives the
disjoint union.&= nbsp; We claim that the composition of  X + Y -> M + M with the
inclusion  M + M >-> M x Delta^1 may be factor= ed as the composition of an
inclusion X + Y >-> = E with a trivial fibration  E -> M x Delta^1 such that
the counterimage of  M + M is  X + Y.  We may then = obtain the desired
fibration

E  ->  M x Delta^1  ->= ;  Delta^1

w= hose fiber over 0 is X and whose fiber over 1 is Y.
We have used a case of:

Claim. The composition of a triv= ial fibration A -> B with an inclusion B
-> C ma= y be factored as the composition of an inclusion A >-> E  with a=
trivial fibration  E -> C such that the count= erimage of B is A.

I believe that this claim follows by a version of the usual iterative
construction of a Quillen factorization for A -> C usi= ng the "test"
cofibrations
Dot De= lta^k >-> Delta^k
for all k. At each stage, we u= se maps from the "test" cofibrations
involving k-simpl= ices of C outside of B.

I hope that this helps --  I haven't thought about Voevodsky's&= nbsp; more
general question.

Best regards,
Pete

    On Su= n, 30 Apr 2006, Peter May wrote:

=
    Here is an extract from an email from Voevods= ky (vlad...@ias.edu)

    -------= ----------

=09Q. Let X and Y be a pair of = Kan simplicial sets which are homotopy
=09equivalent. Is there a Kan fibration = E -> \Delta^1 such that its
=09fiber over 0 is X (up to an iso) and its fibe= r over 1 is Y (up to an
=09iso)?

=09A more adv= anced version of the same question: let X' -> X  and X'' ->
=09X be = two Kan fibrations which are fiberwise equivalent to each other
=09over X. Is t= here a kan fibration over X\times\Delta^1 whose fiber
= =09over X\times 0 is isom= orphic to X', fiber over  X\times 1 is
=09isomorphic to X'' and the homoto= py between the two inclusions of X to
=09X\times\Delta^1 define the original eq= uivalence (up to homotopy)?

=09I encounter= ed this issue trying to write up a semantics for dependent
=09type systems wit= h values in the homotopy category. which is in turn
=09related to the problem o= f creating computer programs for proof
=09verification.
--= ---------------------------------------------------------------------------=


--
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 e= mail to H= omotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--Apple-Mail=_402CA2FD-10C1-491F-A7B7-19A754FC91A5--