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
    • CommentTimeSep 26th 2012

    As already mentioned in another thread, I have added to infinity-image a brief new section Syntax in homotopy type theory. But please check! And even if correct, it’s still a bit rough.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2012

    Now I have turned that into a proposition and spelled out a proof.

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 26th 2012

    I must be very confused. Did you mean to say dependent type a:AB(a):Typea: A \vdash B(a): Type (which would be given by a suitable arrow BAB \to A), or did you mean just a term expression a:Ab(a):Ba: A \vdash b(a): B (represented by a morphism ABA \to B) where you have a:Ab(a):B(a)a: A \vdash b(a): B(a),or did you mean something else?

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2012

    Ah, I wrote “dependent type” for a:Ab(a):Ba : A \vdash b(a) : B. Of course I should have said “dependent term”. Hence a function

    a:Ab(a):B(ab(a)):AB \frac{a : A \vdash b(a) : B}{ \vdash (a \mapsto b(a)) : A \to B}

    of which we want to determine the image.

    I have fixed that now.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeSep 26th 2012

    I don’t think you mean “dependent term” either, just “term”, since BB is not dependent on AA here.

    Also, I found it very confusing for lowercase aa to denote a term/variable of type BB, but for lowercase bb to denote a function from AA to BB, while bb' denoted a term/variable of type BB. So I changed the function name to ff.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2012

    I don’t think you mean “dependent term” either, just “term”, since B is not dependent on A here.

    Can’t I say “dependent term” for this? A term depending on a free variable!

    Also, I found it very confusing for lowercase a to denote a term/variable of type B, but for lowercase b to denote a function from A to B,

    Wait, no. What I called bb and what you now named ff is not a function. It is a term that involves the free variable aa.

    I think my notation made very good sense: we consider two terms of BB, called bb and bb'. One happens to depend on another variable, the other not.

    The corresponding function of function type ABA \to B does not actually appear in either the statement or the proof of the proposition.

    Am I wrong?

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2012
    • (edited Sep 26th 2012)

    What I would suggest to improve the notation is to go back to my “bb” in the type theory syntax, but then notationally highlight the step to the categorical semantics more: so at categorical semantics, and following common practice, we have square brackets for the interpretation, and so it would be more explicit to write the morphism interpreting the term bb as

    [A][b][B]. [A] \stackrel{[b]}{\to} [B] \,.

    or more explicitly as

    [A][b(a)][B] [A] \stackrel{[b(a)]}{\to} [B]

    or the like.

    Of course this may feel awkward if in the syntax square brackets means something entirely unrelated (truncation).

    Is there some other standard notation for categorical interpretation? Angular brackets? Overlines? Something like this?

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeSep 27th 2012

    I haven’t really heard anyone ever say “dependent term” to mean anything at all. But on our page dependent term, you defined it to mean a term belonging to a dependent type.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeSep 27th 2012

    The notation [[]][[-]] is not infrequently used to mean the semantics of something in a model. Unfortunately, iTeX doesn’t seem to support the commands \llbracket and \rrbracket which are the good way of writing that.

    I see what you are saying about terms. There’s an unfortunate confusion of notation, though, in that a notation like b(a)b(a) could denote a term bb containing a free variable aa, but could also denote a function bb applied to an input aa. Logicians and type theorists nowadays often write just bb to mean the term, with the presence of a free variable implied by the judgment (a:A)(b:B)(a:A)\vdash(b:B). Then if you need to do a substitution, you write that using substitution notation like b[a/a]b[a'/a], rather than b(a)b(a').

    I think I still maintain that even if we let ourselves write b(a)b(a) to mean a term with a free variable aa, then it is confusing for bb to be a term and bb' to be a variable. How would you feel about using xx for the variables of type AA and yy for the variables of type BB, with bb for the term of type BB containing the free variable x:Ax:A?

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeSep 27th 2012
    • (edited Sep 27th 2012)

    a notation like b(a)b(a) could denote a term bb containing a free variable aa, but could also denote a function b applied to an input aa.

    But the nice thing is that these are the same, by the computation rule for function types: if a term b(a)b(a) depends on a free variable aa then it is the value of the corresponding function b()=(ab(a))b(-) = (a \mapsto b(a)) applied to aa.

    it is confusing for bb to be a term and bb' to be a variable

    Here I am not following. What is it exactly that is wrong with that? When you write Y:Type(X=Y)\sum_{Y : Type} (X = Y) isn’t YY a variable and XX a term in the same sense as bb' and bb are such?

    on our page dependent term, you defined it to mean a term belonging to a dependent type.

    I didn’t think I was doing anything controversial. Let’s see: a term bb that depends on free variables xx is a term in context of a type XX. That is written x:Xb:Bx : X \vdash b : B. And that’s in general a term of an XX-dependent type. Could you say again what you are objecting to here? I am not sure I am following.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2012

    But the nice thing is that these are the same

    No, the term bb is not the same as its corresponding function. The expression x 2x^2 is not the same as the function which takes one input and squares it; the latter is written λx.x 2\lambda x.x^2. In particular, in the latter xx is a bound variable, while in the former xx is free.

    Re: “dependent term”, I asked a couple of type theorists and they had never heard of the phrase “dependent term” to mean anything at all. So I suggest we don’t use it; type theory has enough confusing terminology without introducing new phrases! (-:

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2012
    • (edited Sep 28th 2012)

    No, the term b is not the same as its corresponding function.

    That’s the very point that I am making.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2012

    In that case, you ought to agree that it is confusing to use the same notation for both of them.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2012
    • (edited Sep 28th 2012)

    Never mind, Mike, somehow we don’t manage to communicate here. But also I don’t think we actually disagree on anything. One can tell that as soon as we each feel the need to explain to the other the difference between a function and its values, somewhere something went wrong in the communication. :-)

    I don’t know where. I feel that you haven’t been reacting to what I actually said here. But you probably feel the same about me! But it’s not worth hashing it out. Next time when I meet you over a coffee personally, it will be a breeze to sort this out.

    Let’s turn to something more productive now.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2012

    Okay, sounds good to me. (-: How would you feel about getting rid of the page ’dependent term’?

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2012

    I know you are waiting for me to do this. So let me ever so slightly re-enter that discussion after all:

    would you be happy if I rename it to “term in context”?

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2012

    I wasn’t waiting for you to do it, I’m happy to do it myself; I was just waiting for agreement. So since I like your suggestion, I went ahead and renamed it to term in context.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2012

    Okay, good. I have now cross-linked it also with generic judgment.

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeNov 13th 2012

    added to infinity-image a paragraph As the ∞-colimit of the kernel ∞-groupoid that means to make explicit the relation between the definition via epi/mono-factorization and that via the \infty-analog of “coequalizer of kernel pair”.

    (And it is still a nuisance that the latter traditionally goes by the name of coimage…)

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeNov 22nd 2012
    • (edited Nov 22nd 2012)

    I have added to infinity-image an basic example Of functors between 1-groupoids.

    This is meant to be expositional/helpful for the novice, but I am not sure if it really succeeds in that. Also, the same discussion could just as well go into some other entry. But I’ll leave it like that just for the moment.

    • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 22nd 2012

    So that should link to stuff, structure, property, right?

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeNov 22nd 2012

    Sure. I have added some cross links between 1-image/2-image and ternary factroization system and stuff, structure, property and Postnikov tower.