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.
Is this not rather limiting to carve out the enriching structure as the subtype of types satisfying a property? I mean, at the level of enriched categories you wouldn’t be able to capture Lawvere’s metric spaces, where hom objects are elements of the extended reals, in this way, would you?
Is there anything inherent to homotopy type theory that would prevent an identity type of a type to be valued in (extended) real numbers?
But I see where David Corfield is coming from; the definition does need to be changed. With Russell universes one could just say that for a type and all terms and , . WIth Tarski universes one has to say that for a type and all terms and , comes with a term and an equivalence
Is the definition experimental, or is there any reference for it? If it is experimental, this should be made clear in the entry.
I think this is probably too “experimental” for the nLab.
One obvious problem is that it’s not actually clear what an “enriched groupoid” is, even classically, except in the case of cartesian enrichment. This invalidates your examples (1) and (3). Another is that your definition only puts structure on the hom-objects, but not the composition maps, so you can only “enrich” in full subcategories of the ambient universe of types. This also invalidates your definitions (1) and (3). At this point you’re really just left with the notion of “separated type for a subuniverse”, which does exist in the literature and should be given that name instead.
Original research is okay on the nLab, but I would say this is more like speculation than research.
On the HoTT wiki there was an article called “groupoid enriched in monoids” but which should really have been called “locally monoidal type” since they defined such a type as a type whose identity types are have the structure of a (set)-monoid.
Whoever moved the article over here probably wanted to make it more general than just monoids, since the article on “groupoids enriched in monoids” now redirects here. However, “enriched” is not really the appropriate name for such a type, since it involves more conditions than just “every identity type has the structure of an X” whether X be abelian groups or connective spectra or whatever.
The HoTT wiki probably accumulated a lot of cruft too; I don’t think it was appropriate there either.
Yeah the HoTT wiki did have a lot of cruft, there were a whole series of articles on “decidable X” where X was a preorder, a directed graph structure, a strict order, an equivalence relation, et cetera.
And there used to be separate articles for division rings and skewfields on the HoTT wiki even though those were the same object. The articles on division rings didn’t include the fact that 0 is not equal to/apart from 1 in the definition, while the articles on skewfields did. There were 6 articles on the topic: 2 disambiguation pages for division rings and skewfields, two articles about discrete division rings/skewfields, and then two articles about Heyting division rings/skewfields.
It sounds like the Anonymous editing activity that we have lately been struggling with here had previously established itself on the HoTT wiki.
It’s a shame that we can’t figure out who these editors are (we tried, but never got a response). If we could just talk to them, I’d have hopes that, when subjected to some critique and advice, their substantial editing energy could eventually be turned into something useful.
In case anyone follows up on enriched types, there is an article which uses types as metric spaces, so understandable in Lawvere’s terms:
Defining enriched -groupoids should be possible in simplicial type theory, where one is talking about discrete types (i.e. -groupoids) enriched in some monoidal Rezk type (i.e. monoidal -category). However, as of right now I don’t think anybody in the type theory community has defined a monoidal Rezk type in simplicial type theory, let alone an -enriched discrete type for monoidal Rezk type .
1 to 15 of 15