Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I can understand the operation of unfolding an entity in terms of coalgebra. E.g., for the endofunctor on Set, F(X) = 1 + X, I can unfold a potentially infinite stream of 1s, writing ’stop’ and ending, or ’1’ and taking the predecessor.
Can I think of unfolding a connected topological space into its Postnikov system in a similar way?
I am not sure if we can get this from a single endofunctor. But the Postnikov tower of an object $X$
$\cdots \to \tau_3 X \to \tau_2 X \to \tau_1 X \to \tau_0 X$comes from a tower of endofunctors
$\cdots \mathbf{H} \stackrel{\tau_3}{\to} \mathbf{H} \stackrel{\tau_2}{\to} \mathbf{H} \stackrel{\tau_1}{\to} \mathbf{H} \stackrel{\tau_0}{\to} \mathbf{H} \,,$where $\mathbf{H}$ is the ambient $\infty$-topos and where $\tau_n$ is the n-truncation $\infty$-functors.
I think a closer analogy would be to the coinductive definition of an $\infty$-category: a set together with hom-$\infty$-categories and composition. Each unfolding peels off one layer of structure “at the bottom” (first the objects, then the 1-morphisms, then the 2-morphisms, etc.).
That seems to give the skeletal filtration instead of the coskeletal/Postnikov tower.
That’s true! But it still seems to me to be closer to what David was asking, because the functor F in F(X)=1+X is not the “operation of unfolding”, but rather that which defines the structure under consideration (here, $\infty$-groupoids) as a coinductive object.
That reminds me of something related (or maybe not so related, I am not sure) that I wanted to ask you:
I seem to remember that a while back you said something like: it’s unclear how to define internal categories in HTT in, notably, the complete Segal space style, because it requires coding an infinite amount of data. Right?
Is that really so? Even outside HTT, in practice we never “code” an infinite amount of data, because we never can. While there is a countable number of objects/types involved in an internal Segal-style category, we never define one by listing these explicitly one-by-one. Instead, we always fall back to some finite algorithm that would produce one.
But even before coding examples, could you remind me what the problem is, if any, of coding the definition ? I would imagine we start with an $\mathbb{N}$-dependent type (of morphisms), then have some $\mathbb{N} \times \mathbb{N}$-dependent type of maps (simplicial structure) maps, and so forth.
Where does one run into problems?
The problem is that the “and so forth” stands for an infinite list of things (higher homotopy coherence of the simplicial structure maps).
stands for an infinite list of things
But it just says: for all $n \in \mathbb{N}$, a certain morphism is weak equivalence. A can’t see why this could not be coded. It’s just some condition parametrized over the type $\mathbb{N}$.
Thanks, Urs and Mike. I had the suspicion that the closest analogy would be to the coinductive Trimble $\omega$-category construction, but wondered if we could peel things off the other way. So there’s no hope of defining truncation in terms of a single endofunctor.
@Urs, I must not understand what you meant by
I would imagine we start with an $\mathbb{N}$-dependent type (of morphisms), then have some $\mathbb{N}\times\mathbb{N}$-dependent type of maps (simplicial structure) maps
Actually, what is it you are trying to define? I thought you were describing a simplicial object (so I assumed that by “morphisms” you meant “objects”).
@David, I probably wouldn’t put it so strongly as “no hope”, but it seems that right now, we don’t know how to do it. (-:
Mike,
yes, a simplicial object satisfiying the Segal condition. Why can’t this be coded in Coq?
The problem is not the Segal condition, the problem is the “simplicial object”. The Segal condition says “for all n, a certain morphism is an equivalence” — probably no problem with that. But please tell me how you plan to encode a simplicial object?
But please tell me how you plan to encode a simplicial object?
"Plan" is a good word. Here is one plan:
first I imagine I’d encode the easy bit: the notion of simplicial 0-truncated objects (all whose components are 0-truncated). I hear this has been done already, with the aim of building models for HoTT inside HoTT. (Maybe I should assume for this that there is a subcategory of discrete objects? Of course I’d be happy with making that assumption.) Similarly I’d define globular 0-truncated objects and, using Street’s combinatorics, the globular nerve operation, all on these degreewise 0-truncated structures.
Then I imagine that I can get hold of the simplicial 0-truncated object which is the nerve of $\Delta$, as well as of its globularization $N_G(\Delta)$.
Then I’d imaging that I can say that a simplicial object is
For every term $v \in N_G(\Delta)_0$ a type $X_v$.
For all $n \in \mathbb{N}$ and every term $\sigma \in N_G(\Delta)_{n+1}$, a term in $Id^{n} (source_0(\sigma) \to target_0(\sigma))$ (the $n$-fold identity type on the function type between the 0-source type of $\sigma$ and the 0-target type of $\sigma$).
Together with a choice of the relevant equivalences.
So, in summary: I first say "simplicial 0-truncated object", which should be straightforward since we may indeed speak of simplicial identities in this case. Then I’d define a specific simplicial 0-truncated object and use that now as a blueprint from which to read off, degree by degree, the "infinite amount of coherence data".
Where did you hear that simplicial 0-truncated objects have been done? I agree that it should not be as hard (in fact, I’ve been working on something similar).
I think the problem then with your plan is saying what you mean precisely by “$n$-fold identity type” and/or “relevant equivalences” (depending on how you partition up the important information between those two things). I don’t know how to convince you that this is hard other than by saying “try to do it!”
Where did you hear that simplicial 0-truncated objects have been done?
Over coffee, from a colleague who is in contact with the person who supposedly did it. I’ll get back to you tomorrow with details.
Mike and I had a little discussion on the cafe about trying to construct simplicial objects, but I can’t find it. I suggested using the decalage, I think, but it didn’t go anywhere (or I didn’t think about it long enough, most likely the former).
I suggested using the decalage,
To accoumplish what?
To define simplicial objects in Coq. I should say, use the decalage, truncated simplicial objects and maps of truncated simplicial objects so we define simplicial objects and the map from the decalage jointly. Unfortunately my google-foo and n-category-cafe-searching-foo have let me down.
fu?
…if you like….
And here’s me thinking you’d found the discussion.
Was that not the discussion you were thinking of?
Sorry, I didn’t see the link because I was using my phone on the bus. I thought it was a linguistic comment on my post. That is exactly the one, thanks!
@Urs - I hope you can make something of my idea, or perhaps a completely different approach is needed, say along the lines you mentioned (0-truncated objects etc).
I hope you can make something of my idea,
A coinductive definition as Mike and maybe you (not sure if I understood yet!) allude to would probably be way more elegant than what I was sketching. I am not so much interested in picking an implementation, since I won’t do it any time soon anyway!
I was more interested in understanding if in principle there is any obstacle to formulating categories internal to Coq, an obstacle due to the definition involving “an infinite amount” of information. It would seem to me that also outside of Coq we can never make a definition that genuinely involves an infinite amount of data. If it looks as if we do, then always because some finite algorithms for producing that data are secretly understood in the background, maybe so secretly that we don’t notice it anymore.
Urs, I agree that we never actually write down an infinite amount of data (obviously, we only have finite paper…). I see that I should have been more specific about the problem. The problem is that in formalizing an infinite amount of coherence data in a “homotopically coherent diagram” (or any homotopically coherent structure), it seems as though we need to use some notion of strict identity. E.g. the source of the associator constraint has to be $f \circ (g\circ h)$. We could ask it to only be isomorphic/equivalent, but then that isomorphism/equivalence has to have an exactly specified source and target, etc.
We had a discussion about this sort of thing a while ago at evil, with the point being made that we can make do with type dependency as a replacement for a notion of strict identity. That is, rather than saying that “the source of the associator is $f\circ (g\circ h)$ and its target is $(f\circ g)\circ h$”, which regarded as a statement involves strict equality, we give the associator the dependent type $Hom(f\circ (g\circ h), (f\circ g)\circ h)$. In principle, and in informal mathematics, this works great. However, when formalizing in type theory, we don’t have fully general language to talk internally about type dependency.
For instance, type theory cannot formalize the statement “the map $f$ is a fibration (i.e. display map, dependent type)”. We can say “let $f\colon A\to B$ be a fibration” by way of introducing the variable $f$ and the type $A$ (by translating it into “let $F\colon B\to Type$ be a dependent type”) but not assert that some already-known map is a fibration. A natural numbers type allows us to talk about “an infinite family of objects” $\{X_n\}_{n\in N}$ as an $N$-indexed type $X\colon N\to Type$, and a family of morphisms $f_{n}\colon X_{n+1} \to X_{n}$ as a dependent function $f\colon \forall n\colon N, X(n+1) \to X(n)$. But there is no obvious way to talk about an infinite tower of fibrations
$\dots \twoheadrightarrow X_{n+1}\twoheadrightarrow X_n \twoheadrightarrow \dots \twoheadrightarrow X_0$This is where the drive to coinduction comes from, because there is a way to formalize such a thing coinductively:
CoInductive tower : Type :=
| lift : forall X0 : Type, (X0 -> tower) -> tower.
But for more complicated infinite structures involving fibrations, there’s no general formula for how to coinductivify them that I know of.
Does that help at all? I wouldn’t say that there is an “in principle obstacle” in the sense of an argument that it can’t be done, but I think this is an “in principle” reason why it is difficult, and why no one has done it yet. (-:
1 to 24 of 24