From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 11 Oct 2017 10:47:17 -0700 (PDT) From: "Daniel R. Grayson" To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: Re: Vladimir Voevodsky MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2216_485738355.1507744037900" ------=_Part_2216_485738355.1507744037900 Content-Type: multipart/alternative; boundary="----=_Part_2217_612175496.1507744037900" ------=_Part_2217_612175496.1507744037900 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit At https://en.wikipedia.org/wiki/Homotopy_type_theory Voevodsky says this: "Also in 2009, Voevodsky worked out more of the details of a model of type theory in Kan complexes, and observed that the existence of a universal Kan 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 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: Peter May cc: jar...@uwo.ca, pgo...@math.northwestern.edu From: "A. Bousfield" Subject: Re: Simplicial question Dear Peter, I think that the answer to Voevodsky's basic question is "yes," and I'll try to sketch a proof. 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 the 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 that the counterimage of M + M is X + Y. We may then obtain the desired fibration E -> M x Delta^1 -> Delta^1 whose fiber over 0 is X and whose fiber over 1 is Y. We have used a case of: 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. 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. I hope that this helps -- I haven't thought about Voevodsky's more general question. Best regards, Pete On Sun, 30 Apr 2006, Peter May wrote: Here is an extract from an email from Voevodsky (vlad...@ias.edu) ----------------- Q. Let X and Y be a pair of Kan simplicial sets which are homotopy equivalent. Is there a Kan fibration E -> \Delta^1 such that its fiber over 0 is X (up to an iso) and its fiber over 1 is Y (up to an iso)? A more advanced version of the same question: let X' -> X and X'' -> X be two Kan fibrations which are fiberwise equivalent to each other over X. Is there a kan fibration over X\times\Delta^1 whose fiber over X\times 0 is isomorphic to X', fiber over X\times 1 is isomorphic to X'' and the homotopy between the two inclusions of X to X\times\Delta^1 define the original equivalence (up to homotopy)? I encountered this issue trying to write up a semantics for dependent type systems with values in the homotopy category. which is in turn related to the problem of creating computer programs for proof verification. ----------------------------------------------------------------------------- ------=_Part_2217_612175496.1507744037900 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
At https://en.wikipedia.org/wiki/Homotopy_type_theory= Voevodsky says this:

"Also in 2009, Voevodsk= y worked out more of the details of a model of type
theory in Kan= complexes, and observed that the existence of a universal Kan
fi= bration could be used to resolve the coherence problems for categorical
models of type theory. He also proved, using an idea of A. K. Bousfi= eld, that
this universal fibration 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 fro= m Bousfield,=C2=A0
answering Vladimir's question as forwarded= by Peter May, containing
a very nice description of the idea, an= d here it is:

------------------------------------= -----------------------------------------
Date:=C2=A0 =C2=A0 Mon,= 01 May 2006 10:10:30 CDT
To:=C2=A0 =C2=A0 =C2=A0 Peter May <.= ..@math.uchicago.edu>
cc:=C2=A0 =C2=A0 =C2=A0 jar...@uwo.ca, p= go...@math.northwestern.edu
From:=C2=A0 =C2=A0 "A. Bousfield= " <...@uic.edu>
Subject: Re: Simplicial question
=

Dear Peter,

I think that the a= nswer to Voevodsky's basic question is "yes," and I'll
try to sketch a proof.

Since the Kan compl= exes X and Y are homotopy=C2=A0 equivalent, they share the
same m= inimal complex M, and we have trivial fibrations X -> M=C2=A0 and Y ->= ; M
by Quillen's main lemma in "The geometric realizatio= n of a Kan fibration
."=C2=A0 Thus=C2=A0 X + Y -> M + M i= s also a trivial fibration where "+" gives the
disjoint= union.=C2=A0 We claim that the composition of=C2=A0 X + Y -> M + M with= the
inclusion=C2=A0 M + M >-> M x Delta^1 may be factored = as the composition of an
inclusion X + Y >-> E with a trivi= al fibration=C2=A0 E -> M x Delta^1 such that
the counterimage= of=C2=A0 M + M is=C2=A0 X + Y.=C2=A0 We may then obtain the desired
<= div>fibration

E=C2=A0 ->=C2=A0 M x Delta^1=C2= =A0 ->=C2=A0 Delta^1

whose fiber over 0 is X an= d whose fiber over 1 is Y.

We have used a case of:=

Claim. The composition of a trivial fibration A -= > B with an inclusion B
-> C may be factored as the composi= tion of an inclusion A >-> E=C2=A0 with a
trivial fibration= =C2=A0 E -> C such that the counterimage of B is A.

=
I believe that this claim follows by a version of the usual iterative<= /div>
construction of a Quillen factorization for A -> C using the &= quot;test"
cofibrations
Dot Delta^k >-> Delt= a^k
for all k. At each stage, we use maps from the "test&quo= t; cofibrations
involving k-simplices of C outside of B.

I hope that this helps --=C2=A0 I haven't thought abou= t Voevodsky's=C2=A0 more
general question.

Best regards,
Pete

=C2=A0 =C2=A0 = On Sun, 30 Apr 2006, Peter May wrote:

=C2=A0 =C2= =A0 Here is an extract from an email from Voevodsky (vlad...@ias.edu)
=

=C2=A0 =C2=A0 -----------------

=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 tha= t its
=09fiber over 0 is X= (up to an iso) and its fiber over 1 is Y (up to an
=09iso)?

=09A more advanced version of the same question= : let X' -> X=C2=A0 and X'' ->
=09X be two Kan fibrations which are fiberwise equiv= alent to each other
=09ove= r X. Is there a kan fibration over X\times\Delta^1 whose fiber
=09over X\times 0 is isomorphic to X&#= 39;, fiber over=C2=A0 X\times 1 is
=09isomorphic to X'' and the homotopy between the two incl= usions of X to
=09X\times\= Delta^1 define the original equivalence (up to homotopy)?

=09I encountered this issue = trying to write up a semantics for dependent
=09type systems with values in the homotopy category. wh= ich is in turn
=09related = to the problem of creating computer programs for proof
=09verification.
-------------------= ----------------------------------------------------------

------=_Part_2217_612175496.1507744037900-- ------=_Part_2216_485738355.1507744037900--