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.
quick note semi-Segal space (just recording a reference of a speaker we had today)
I have briefly added three basic definitions and a relations to semi-Segal space.
It’s probably not a surprise, but I never quite thought of it that way before: for a semi-Segal space – which is a semicategory object internal to – completeness/univalence is effectively the remaining unitality axiom…
That’s neat. It seems also related to the fact that a Kan-fibrant semi-simplicial set admits a choice of degeneracies making it simplicial.
One interesting upshot should be this: in principle then it seems we know how to say “-category” internal to HoTT, for every finite (or maybe at least for “low ”):
it’s a semi-simplicial type formalized (which is tedious but possible for “low ”) as dependent types by hand, like , etc.
satisfying the Segal-conditions;
such that the two maps are equivalences.
such that is -truncated.
I suppose. (And maybe up to correcting my counting…)
To explore the above suggestion, let’s start with the lowest-degree case: with -category types. How about the following definition?:
A -category type is
a type
a dependent type ;
we write
a dependent type
such that
0-truncation – is 0-truncated/is an h-set
1-coskeletalness – the function
is a 1-monomorphism;
Segal condition – the function
is an equivalence;
unitality – the function
is an equivalence.
And then the next step in exploring #4:
A -category type is
a type
a dependent type ;
we write
a dependent type
we write
such that
1-truncation – is 1-truncated/is an h-groupoid
2-coskeletalness – the function
is a 1-monomorphism;
Segal condition – the functions
and
are equivalences;
unitality – the function
is an equivalence.
What does it mean to say that a morphism is an “equivalence” before you have a notion of identity morphism?
Once there is a notion of composition, a morphism is an equivalence if it induces equivalences of hom-spaces under composition. Yonatan discusses this in his section 4.1.
Do you then automatically get all the higher degeneracies?
Yonatan Harpaz shows that the -category of complete Semi-Segal spaces is equivalent to that of complete Segal spaces. So in this sense, yes, the degeneracies can be recovered, up to equivalence.
Interesting.
So, I stared for a minute or two at Voevodsky’s recent code for semi-simplicial types. But I’ll need to stare at it for a few more minutes to parse it. Meanwhile, maybe you can give me a quick hint:
is his code the generalization to arbitrary degree of the low-degree expressions in #6?
If it is, then with Harpaz’ observation it would seem to be just a small remaining step to HoTT-internal -categories.
First of all, that code doesn’t work. The fact that it doesn’t work is apparently the reason that he’s currently trying to develop a new type theory with a stronger, but undecidable, judgmental equality. Many type theorists seem to be dubious.
Second, I haven’t managed to make much sense of that code myself yet either, so I don’t think I can help you.
Thanks, Mike, that’s very useful to know.
1 to 14 of 14