"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
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:
-----------------
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
.