thanks for posting this Dan. It’s very interesting to learn the background of the discovery of univalence. Steve > On Oct 11, 2017, at 1:47 PM, Daniel R. Grayson > wrote: > > 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. > ----------------------------------------------------------------------------- > > > -- > 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 .