Constructive Kan universe

[Richard Garner]

To anyone who has not yet seen it ---

It appears that Wouter Stekelenburg has a proof of the construction of a
univalent universe in simplicial sets which is effective and does not
rely on the theory of minimal fibrations (in particular no choice is
required):--

http://arxiv.org/abs/1406.6579

Richard

[Michael Shulman]

Exciting! I'm having a bit of trouble figuring out which parts of
this paper are happening in the internal logic and which parts are
talking externally about assemblies. How much of the construction of
a univalent universe depends on the starting category being assemblies
versus e.g. an arbitrary topos? (Obviously in general one can only
have a universe of "small" fibrations.) It seems that something must
break somewhere, because there is a counterexample in a presheaf topos
showing that Kan complexes are not constructively closed under
exponentials. Right? Or is there some tweak to the definitions which
avoids that problem?

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

[Michael Shulman]

Oh no, sorry, the counterexample I was thinking of was Thierry and
Marc's showing that the fibers of a Kan fibration over Delta^1 may not
be homotopy equivalent. That still seems to be a problem though.

[Steve Awodey]

indeed — very exciting!
this is exactly the "realizability oo-topos” RT(A)_\infty that I proposed last year at IAS — where RT(A)_n = n-groupiods in assemblies over a pca A.
the hSets in there should equivalent to the usual realizability topos RT(A).
My purpose was to use the impredicative universe of modest objects to construct HITs — this should give a very nice setting for that!

Steve

[Vladimir Voevodsky]

But does he have Pi's?
V.

[Bas Spitters]

Looks very nice. Did anyone read it carefully?
Wouter is an expert on realizability of course, so I don't doubt the results.

I wonder how this relates to the work on modest groupoids by Steve and Andrej.

[Richard Garner]

Seemingly not.

Richard

[Michael Shulman]

The second bullet point in section 7 seems to claim that he has Pis.

[Thomas Streicher]

I started reading Wouter's paper. But I think the hard part is to show
that the universe is a Kan complex. That's what sofar needed minimal
fibrations.

Anyone, has found out what's the clue in his work. In any case he must
do it differently than with minimal fibrations. But the intro is a bit
minimal and doesn't convey ideas clearly.

Thomas

[Thomas Streicher]

I have had a closer look at what Steklenburg does without checking proofs.
I first thought he would have a brand new idea how to show that the
universe constructed in sSet is a Kan complex. Well, he has in a sense
but for Set, i.e. a realizability topos over the trivial pca. In this
case modest sets is just the set P(1) and, accordingly, P(1)^\Delta^op
is just sieves in \Delta, i.e.\ P(1) again.

So Steklenburg's result says nothing about simplicial sets Set.

Moreover, I guess his universe is impredicative.

Thomas

[Michael Shulman]

So you're saying that his proof only works for the specific case of
modest sets in a realizability topos and not any more generally?

[Thomas Streicher]

> So you're saying that his proof only works for the specific case of
> modest sets in a realizability topos and not any more generally?

Right, that's what I wanted to say.

Thomas

[Richard Garner]

> > So you're saying that his proof only works for the specific case of
> > modest sets in a realizability topos and not any more generally?
>
> Right, that's what I wanted to say.

I didn't see anything that was peculiar to the case of realisability. I
have been reading the construction starting from the bottom of p.11
onwards. I have completely ignored any realisability aspects, because I
don't really understand them, and have just interpreted everything in
ordinary simplicial sets. It looks like it should work perfectly well
there.

The key problem is, as usual, to show that the codomain of the universal
Kan fibration is Kan. Thus given X ----> Lambda_n^k a Kan fibration, one
must show that it can be extended to a fibration over Delta_n whose
pullback along the inclusion H: Lambda_n^k ---> Delta_n is the original
map. He does this as follows: first Pi along H. Now Pi_H(X) ---->
Delta_n can be viewed as a presheaf on Delta / n; seen as such, we
precompose it with a certain endofunctor \hat K : Delta/n ----> Delta/n.
On objects m ---> n of Delta / n which factor through Lambda_n^k, the
functor \hat K acts as the identity. For objects m ---> n which don't
factor through Lambda_n^k, it sends them to m+1 ----> n whose image
contains one more copy of k.

[This definition sounds a bit unnatural, but maybe it makes perfect
sense if you think about it in terms of open and closed subtoposes. SSet
/ Delta_n has an open subtopos SSet / Lambda_n^k; the complementary
closed subtopos is given by presheaves on the full subcategory C of
Delta / n on those m ---> n which don't factor through Lambda_n^k. Thus
SSet / Delta_n is equivalent to the comma category of the "fringe
functor" W: SSet / Lambda_n^k -----> SSet / Delta_n ----> [C^op, Set]
given by Pi along H, followed by restriction along the inclusion C ---->
Delta / n. Wouter's construction describes a pointed endofunctor of C,
which induces a copointed endofunctor of [C^op, Set]; postcomposing W
with the copointing and using the universal property of the comma now
induces the required functor SSet / Lambda_n^k ----> SSet / Delta_n.]

The result is pretty much the same as the construction in the
Bezem-Coquand-Huber cubical sets model. Given X ----> Lambda_n^k, things
in the resultant X' ----> Delta_n over the missing n-1 dimensional face
are precisely (n,k)-horns in X; i.e., sections of X---> Lambda_n^k.
Things in X' ---> Delta_n over the missing n-dimensional face are
(n,k)-horns in X that have been "thickened" at k (i.e., over the vertex
k, there is a 1-simplex rather than a 0-simplex in X). And so on. Peter
L can explain this better than me, as I seem to recall him saying that
he'd thought about things along these lines quite a bit.

Richard

[Peter LeFanu Lumsdaine]

On Jun 27, 2014, at 11:24 PM, Richard Garner wrote:

> The key problem is, as usual, to show that the codomain of the universal
> Kan fibration is Kan. Thus given X ----> Lambda_n^k a Kan fibration, one
> must show that it can be extended to a fibration over Delta_n whose
> pullback along the inclusion H: Lambda_n^k ---> Delta_n is the original
> map. He does this as follows: first Pi along H. Now Pi_H(X) ---->
> Delta_n can be viewed as a presheaf on Delta / n; seen as such, we
> precompose it with a certain endofunctor \hat K : Delta/n ----> Delta/n.
> On objects m ---> n of Delta / n which factor through Lambda_n^k, the
> functor \hat K acts as the identity. For objects m ---> n which don't
> factor through Lambda_n^k, it sends them to m+1 ----> n whose image
> contains one more copy of k.

I haven’t read the paper this far yet, and due to an elaborate
coincidence of printer, power supply, and internet issues, I don’t
have it available beyond the first ten pages right now; but I don’t
think this can be quite what he does, since I tried it myself a while
ago and am pretty sure it doesn’t work, i.e. doesn’t preserve
fibrations.

Specifically: consider the left adjoint to this construction. It
similarly is a composite of two functors: first, L, the Kan extension
of the endofunctor of Delta/[n] to an endofunctor of SSets/Delta[n];
and then i^*, pullback along the horn inclusion.

Since we want the right adjoint to preserve fibrant objects, we hope
that the left adjoint will preserve trivial cofibrations. It doesn't
absolutely *need* to, since we don't need to preserve all fibrations
in SSets/Lambda_n^k, just fibrant objects. But it must send horn
inclusions to maps which will lift against all fibrations over
Lambda_n^k (which may or may not be a larger class of maps than
trivial cofibrations).

Anyhow, if I am not mistaken, i^* . L sends some horn inclusions to
maps which are not even monos, and so which will certainly not lift
against all fibrations over the horn. Specifically, let the base horn
that we are extending along be the inclusion

Lambda_2^1 >—> Delta[2]

Now consider the map Delta[2] -> Delta[2] induced by the map (0,0,2) :
[2] -> [2]; i.e. it lies over the 1st face, and is degenerate over the
0th vertex. Call this simplex S, as an object of SSets/Delta[2]. The
Kan extension L sends S to the 3-simplex (0,0,1,2) : [3] -> [2], i.e.
the 0-degeneracy of the entire base; i^*, restricting to the part over
the horn, then sends this to a sort of sideways Y, with the triangle
filled in. Orienting vertically to make it ascii-able:

_
\ /
|

Now consider the inclusion of Lambda_2^2 into the simplex S, i.e. the
horn omitting the degenerate edge of S; call this H, as an object of
SSets/Delta[2]. L takes each edge of this to the identity 2-simplex
over the base; i^* takes that to the identity of the base horn. So
i^*L(H) looks like a sideways V, with each edge divided in two.
Re-orienting vertically again, i^*L of this horn looks like

\ /
\/

Now, the evident inclusion of this into the Y above is not mono, and
does not lift against arbitrary fibrations over the base horn; for
instance, against the fibrant replacement of i^*L(H) itself — call
this F. So the horn inclusion H >–> S will not lift against the right
adjoint construction applied to F.

So what Wouter does must be something slightly more elaborate than
this, unless I’ve mis-calculated somewhere above. It seems very
reasonable that some construction along these lines should work — the
geometric intuition behind such a left adjoint is very compelling when
you draw pictures of it on the blackboard (I recommend trying that;
it’s good fun) — but this particular candidate doesn’t quite seem to
work.

(It does iirc preserve horn inclusions into simplices which, viewed as
simplices of Delta[2], are *non-degenerate*, however; and I’d expect
that whatever construction does work might well agree with this one on
those non-degenerate simplices.)

–p.

> [This definition sounds a bit unnatural, but maybe it makes perfect
> sense if you think about it in terms of open and closed subtoposes. SSet
> / Delta_n has an open subtopos SSet / Lambda_n^k; the complementary
> closed subtopos is given by presheaves on the full subcategory C of
> Delta / n on those m ---> n which don't factor through Lambda_n^k. Thus
> SSet / Delta_n is equivalent to the comma category of the "fringe
> functor" W: SSet / Lambda_n^k -----> SSet / Delta_n ----> [C^op, Set]
> given by Pi along H, followed by restriction along the inclusion C ---->
> Delta / n. Wouter's construction describes a pointed endofunctor of C,
> which induces a copointed endofunctor of [C^op, Set]; postcomposing W
> with the copointing and using the universal property of the comma now
> induces the required functor SSet / Lambda_n^k ----> SSet / Delta_n.]
>
> The result is pretty much the same as the construction in the
> Bezem-Coquand-Huber cubical sets model. Given X ----> Lambda_n^k, things
> in the resultant X' ----> Delta_n over the missing n-1 dimensional face
> are precisely (n,k)-horns in X; i.e., sections of X---> Lambda_n^k.
> Things in X' ---> Delta_n over the missing n-dimensional face are
> (n,k)-horns in X that have been "thickened" at k (i.e., over the vertex
> k, there is a 1-simplex rather than a 0-simplex in X). And so on. Peter
> L can explain this better than me, as I seem to recall him saying that
> he'd thought about things along these lines quite a bit.
>
> Richard
>

[Richard Garner]

> I haven’t read the paper this far yet, and due to an elaborate
> coincidence of printer, power supply, and internet issues, I don’t
> have it available beyond the first ten pages right now; but I don’t
> think this can be quite what he does, since I tried it myself a while
> ago and am pretty sure it doesn’t work, i.e. doesn’t preserve
> fibrations.

Oops!

Your counterexample seems pretty watertight. Looking at Wouter's paper,
I am fairly certain that his construction is as I described. The point
at which things appear to diverge from what you laid out is on p.14,
between equations (3) and (4). He describes what is (in your
terminology) i^*.L(Delta[m]), as a sub-simplicial set of Delta[m+1] and
then states that "to find i^*L(Lambda_m^l), we intersect these faces
with the ones in L(Lambda_m^l)."

This seems to implicitly assume that the left Kan extension L preserves
monomorphisms, which as your counterexample shows is not in general
true. (If F : C ---> D, then Lan_F : [C^op, Set] ---> [D^op, Set]
preserving monomorphisms is I suspect pretty close to it being
comonadic; I think that's true iff F is a local right adjoint). In fact
back on p.13 point (2) in the numbered list at the bottom of the page
already suggests that he considers that L(Lambda_m^l) is going to be a
sub-simplicial set of Delta[m+1].

So either something weird to do with realisability makes this all OK, or
this is an error in Wouter's proof (Lemma 24 claims exactly the thing
that you just showed is implausible).

Thomas: I see that we are taking colimits in the small complete category
of modest sets. Is there any chance that this could account for the
difference? It seems a bit odd that working in the realizability setting
should suddenly make this left Kan extension preserve monomorphisms, but
maybe that's so?

Peter: when you get a chance, I'd be interested to know what you make of
these couple of pages!

Richard

[Thomas Streicher]

> Thomas: I see that we are taking colimits in the small complete category
> of modest sets. Is there any chance that this could account for the
> difference? It seems a bit odd that working in the realizability setting
> should suddenly make this left Kan extension preserve monomorphisms, but
> maybe that's so?

Not that I knew. But, of course, Mod has colimits for diagrams in Asm,
i.e. large colimits. But I don't see that this would help, does it?

Thomas

[Richard Garner]

No, that's my feeling too. So maybe this is a bug in Wouter's paper.

Richard

[Bas Spitters]

Wouter put up a new version on the arxiv. Quickly reading it, the
claimed result still looks quite surprising.

The simplicial assemblies carry a model structure (thm 27) and an
(impredicative) univalent universe of modest sets (thm 45).

I am wondering why the construction works in such a straight forward
way in realizability, but cannot be done constructively in general. Is
it possible to isolate the extra axioms that realizability provides
here?

http://arxiv.org/pdf/1406.6579v4.pdf

[Bas Spitters]

This new paper by Wouter Steckelenburgh seems to answer my question below.

Constructive Simplicial Homotopy
Wouter Pieter Stekelenburg

"This paper aims to help the development of new models of homotopy
type theory, in particular with models that are based on realizability
toposes. For this purpose it develops the foundations of an internal
simplicial homotopy that does not rely on classical principles that
are not valid in realizability toposes and related categories."
http://arxiv.org/pdf/1604.04746

The introduction says:
---
In the intended model types are homotopy types of certain simplicial
objects in a realizability topos.
These toposes lack some of the structure of the category of sets
underlying classical homotopy theory. In the internal logic the
principle
of the excluded middle and the axiom of choice can be invalid. They
can lack infinite
limits and colimits. We work around these issues in the following way.
1. Limit the class of cofibrations. In classical simplicial homotopy
theory every mono
morphism is a cofibration. We demand that certain properties of the monomor-
phisms are decidable so classical arguments remain valid.
2. Strengthen the lifting property. Fibrations come equipped with a
filler operator
that gives solutions for a family of basic lifting problems.
3. Build the homotopy category out of fibrant objects only, so we
don’t need fibrant
replacements.
To avoid distracting peculiarities of the realizability topos this
paper works with a generic
Π-pretopos with a natural number object. That makes our simplicial
homotopy predicative
as well as constructive.
---

These seem like natural requirements that we also see in related
developments. Unfortunately, I have not found the time to read to the
paper in detail yet.

[Richard Williamson]

It should perhaps be emphasised that the model structure is, in
the classical case, on the category of Kan complexes viewed as a
full sub-category of the category of simplicial sets; and the
requirement that the category be complete and co-complete is
dropped.

In particular, this category is not particularly nice; it does
not have even basic colimits, such as glueing together a pair of
intervals at their endpoints. Thus, many of the things that a
model structure usually gives one, such as homotopy colimits and
limits, are of limited use here.

If one requires that a morphism of Kan complexes preserves the
fillers, i.e. one works with the category of algebraic Kan
complexes, one then has a nice category. Putting a model
structure on this kind of category in a constructive way is
something that I have thought a lot about.