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.
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.
Now I have turned that into a proposition and spelled out a proof.
I must be very confused. Did you mean to say dependent type $a: A \vdash B(a): Type$ (which would be given by a suitable arrow $B \to A$), or did you mean just a term expression $a: A \vdash b(a): B$ (represented by a morphism $A \to B$) where you have $a: A \vdash b(a): B(a)$,or did you mean something else?
Ah, I wrote “dependent type” for $a : A \vdash b(a) : B$. Of course I should have said “dependent term”. Hence a function
$\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.
I don’t think you mean “dependent term” either, just “term”, since $B$ is not dependent on $A$ here.
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$, while $b'$ denoted a term/variable of type $B$. So I changed the function name to $f$.
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 $b$ and what you now named $f$ is not a function. It is a term that involves the free variable $a$.
I think my notation made very good sense: we consider two terms of $B$, called $b$ and $b'$. One happens to depend on another variable, the other not.
The corresponding function of function type $A \to B$ does not actually appear in either the statement or the proof of the proposition.
Am I wrong?
What I would suggest to improve the notation is to go back to my “$b$” 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 $b$ as
$[A] \stackrel{[b]}{\to} [B] \,.$or more explicitly as
$[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?
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.
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)$ could denote a term $b$ containing a free variable $a$, but could also denote a function $b$ applied to an input $a$. Logicians and type theorists nowadays often write just $b$ to mean the term, with the presence of a free variable implied by the judgment $(a:A)\vdash(b:B)$. Then if you need to do a substitution, you write that using substitution notation like $b[a'/a]$, rather than $b(a')$.
I think I still maintain that even if we let ourselves write $b(a)$ to mean a term with a free variable $a$, then it is confusing for $b$ to be a term and $b'$ to be a variable. How would you feel about using $x$ for the variables of type $A$ and $y$ for the variables of type $B$, with $b$ for the term of type $B$ containing the free variable $x:A$?
a notation like $b(a)$ could denote a term $b$ containing a free variable $a$, but could also denote a function b applied to an input $a$.
But the nice thing is that these are the same, by the computation rule for function types: if a term $b(a)$ depends on a free variable $a$ then it is the value of the corresponding function $b(-) = (a \mapsto b(a))$ applied to $a$.
it is confusing for $b$ to be a term and $b'$ to be a variable
Here I am not following. What is it exactly that is wrong with that? When you write $\sum_{Y : Type} (X = Y)$ isn’t $Y$ a variable and $X$ a term in the same sense as $b'$ and $b$ 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 $b$ that depends on free variables $x$ is a term in context of a type $X$. That is written $x : X \vdash b : B$. And that’s in general a term of an $X$-dependent type. Could you say again what you are objecting to here? I am not sure I am following.
But the nice thing is that these are the same
No, the term $b$ is not the same as its corresponding function. The expression $x^2$ is not the same as the function which takes one input and squares it; the latter is written $\lambda x.x^2$. In particular, in the latter $x$ is a bound variable, while in the former $x$ 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! (-:
No, the term b is not the same as its corresponding function.
That’s the very point that I am making.
In that case, you ought to agree that it is confusing to use the same notation for both of them.
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.
Okay, sounds good to me. (-: How would you feel about getting rid of the page ’dependent term’?
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”?
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.
Okay, good. I have now cross-linked it also with generic judgment.
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…)
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.
So that should link to stuff, structure, property, right?
Sure. I have added some cross links between 1-image/2-image and ternary factroization system and stuff, structure, property and Postnikov tower.
1 to 22 of 22