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

Discussion Tag Cloud

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).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeAug 22nd 2013

    at relation, right at the beginning, I have added remarks that relations are special cases of correspondences – namely the (-1)-truncated correspondences – and that the composition of correspondences induces the composition of relations, under postcomposition with (-1)-truncation. Added a similar remark also to the relevant Properties-section further below.

    Then I have tried to cross-link the relevant relational/correspondency entries here a bit more. But don’t really have the leisure.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeAug 23rd 2013

    When did span start redirecting to correspondence rather than vice versa?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeAug 23rd 2013

    Yesterday. Sorry, should have announced this. (In the days of the cache bug I wouldn’t have done it, but now that renaming works…)

    Let me advertize the change a posteriori: “correspondence” is better because it harmonizes nicely with “relation” and because “span” just as “roof” suffer from describing the notation instead of the concept. As such they are like saying “triple” for “monad”, namely a bad idea.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeAug 24th 2013

    I don’t agree. The term “span” is absolutely standard in the category-theoretic community. I guess one might argue that it does have something to do with the notation, but it doesn’t depend on a random idiosyncratic choice of notation, like some other names do which are also completely standard (\dagger-category, **-autonomous category, JJ-homomorphism, …) — as long as morphisms are denoted by arrows then a span is going to look like a span. (“Roof” is worse because it implies that the middle object is “above” the other two.) The problem with “correspondence” is that there are all sorts of correspondences in mathematics, and in everyday English language “correspondences” tend to be assumed to be one-to-one, which spans generally are not. The word “span” has no other meaning in mathematics and is hence unambiguous, unlike “triple” and also “correspondence”.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeAug 24th 2013

    Sure, no prob, I changed it back.

    The word “span” has no other meaning in mathematics

    What?? :-)

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeAug 24th 2013

    Sorry, I should have said, no other meaning as a standalone noun. Of course there is also the span of something in a vector space, but there’s no potential for confusion there. Is there another meaning that I’m forgetting?

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeAug 25th 2013

    I changed

    The notion of relation is the extension of the notion of predicate.

    back to

    A relation is the extension of a predicate.

    The extension of the notion of predicate is the collection of all predicates, not the notion of relation.

    • CommentRowNumber8.
    • CommentAuthorzskoda
    • CommentTimeAug 27th 2013

    I find correspondence more geometric terminology than span, and it is not quite the same in some contexts. I mean it may mean an entity which is like subobject of the direct product but not quite and it may be more specific; the projection morphisms may be in some other category than the original. But the idea is the same always, it is the same subject with two flavours.

    • CommentRowNumber9.
    • CommentAuthorzskoda
    • CommentTimeAug 27th 2013

    Toby: as about relations, are there some connections to the notions in modal logic, Kripke semantics etc. I mean the notions of relations there are sometimes quite involved…

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 15th 2021

    It occurred to me today that in a type-theoretic context, it might be pleasant to distinguish between

    1. spans, meaning three types A,B,CA,B,C and functions ACBA \leftarrow C \to B, and
    2. correspondences, meaning two types A,BA,B and a type family R:AB𝒰R : A\to B \to \mathcal{U}.

    The two are equivalent, but it can be useful to be clear about which one we’re talking about. At first glance, I like the above choice of terminology because in the type-family presentation it makes more sense to think of R(a,b)R(a,b) as “the ways in which aa and bb correspond”, whereas in the span presentation one has to take fibers to extract this “correspondence” information. The latter are traditionally called “relations”, but this has the undesired connotation that RR should be valued in propositions. In addition, by a one-to-one correspondence we can then mean a correspondence, in this sense, such that for each aa there is a unique bb with R(a,b)R(a,b) and oppositely, which happens (when interpreted sufficiently proof-relevantly) to be a good notion of type equivalence in HoTT.

    Any thoughts? (In particular, I wonder if someone else already proposed this and I just have source amnesia?)

    P.S. I’m tempted to similarly distinguish in the unary case between a “family” P:A𝒰P:A\to \mathcal{U} and some word like a “bundle” BAB\to A, although I’m less sure about the latter.

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 15th 2021

    Makes sense of why we say cospan rather than cocorrespondence. That made me look at the ancient page multispan, barely touched since 2009.