Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
  1. starting stub article on enriched types in homotopy type theory, which are a synthetic version of enriched infinity-groupoids in higher category theory.

    Anonymous

    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJun 16th 2022

    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?

    diff, v2, current

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 16th 2022

    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?

    • CommentRowNumber4.
    • CommentAuthorGuest
    • CommentTimeJun 16th 2022

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

    • CommentRowNumber5.
    • CommentAuthorGuest
    • CommentTimeJun 16th 2022

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

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJun 16th 2022

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

  2. mentioned that the definition is experimental

    Anonymous

    diff, v3, current

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeJun 19th 2022

    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.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJun 19th 2022

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

    • CommentRowNumber10.
    • CommentAuthorGuest
    • CommentTimeJun 19th 2022

    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.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeJun 19th 2022

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

    • CommentRowNumber12.
    • CommentAuthorGuest
    • CommentTimeJun 19th 2022

    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.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJun 19th 2022
    • (edited Jun 19th 2022)

    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.

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 21st 2022
    • (edited Jun 21st 2022)

    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)
  3. 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 (,1)(\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 VV-enriched discrete type for monoidal Rezk type VV.