Defining enriched $\infty$-groupoids should be possible in simplicial type theory, where one is talking about discrete types (i.e. $\infty$-groupoids) enriched in some monoidal Rezk type (i.e. monoidal $(\infty,1)$-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 $V$-enriched discrete type for monoidal Rezk type $V$.

]]>In case anyone follows up on enriched types, there is an article which uses types as metric spaces, so understandable in Lawvere’s terms:

- Jason Reed and Benjamin C. Pierce. 2010.
*Distance makes the types grow stronger: a calculus for differential privacy.*In Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland,USA, September 27-29, 2010, Paul Hudak and Stephanie Weirich (Eds.). ACM Press, 157-168, (doi:10.1145/1863543.1863568)

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.

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

]]>The HoTT wiki probably accumulated a lot of cruft too; I don’t think it was appropriate there either.

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

]]>Original research is okay on the nLab, but I would say this is more like speculation than research.

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

]]>mentioned that the definition is experimental

Anonymous

]]>Is the definition experimental, or is there any reference for it? If it is experimental, this should be made clear in the entry.

]]>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 $T$ and all terms $a:T$ and $b:T$, $a =_T b:C_\mathcal{U}$. WIth Tarski universes one has to say that for a type $T$ and all terms $a:T$ and $b:T$, $C$ comes with a term $A:C_\mathcal{U}$ and an equivalence $e:(a =_T b) \simeq \mathcal{T}_{C_\mathcal{U}}(A)$

]]>Is there anything inherent to homotopy type theory that would prevent an identity type of a type to be valued in (extended) real numbers?

]]>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?

]]>have hyperlinked more of the keywords, and have slightly touched the wording.

In particular, where you claimed that enriched types interpret to enriched $\infty$-groupoids, I have added the word “should”.

Do you have a reference?

]]>starting stub article on enriched types in homotopy type theory, which are a synthetic version of enriched infinity-groupoids in higher category theory.

Anonymous

]]>