1
$\begingroup$

While reading the HoTT book, I came up with the following (very) vague analogy: Consider $f(x) :\equiv \lambda y.x+y$ of type, say, $f: \mathbb{N} \to \mathbb{N} \to \mathbb{N}$. Also assume you already have $y: \mathbb{N}$.

Now, what you want is $f(y)$. But note that one has to change the local variable $y$. Otherwise you would get $\lambda y.y+y$.

I think this is quite obvious but also very similar to the idea of calculating intersections by means of the moving lemma - in particular self intersections.

So, is there more than just this intuition? I remember, that the proof for the moving lemma is pretty demanding. Maybe there is a proof approach with HoTT?

Thanks, Adrian

Improve this question
$\endgroup$
9
  • 2
    $\begingroup$ This is well studied in computer science, in relation to the problem of "capture-avoiding substitution". $\endgroup$
    – Zhen Lin
    Commented Jun 19, 2014 at 10:52
  • 5
    $\begingroup$ I also don't see anything specific to HoTT (versus type theory in general) about it. $\endgroup$
    – Mike Shulman
    Commented Jun 19, 2014 at 16:32
  • 5
    $\begingroup$ The idea of re-casting intersection theory in HoTT is appealing, but $\alpha$-equivalence does not correspond to it. In fact, $\alpha$-renaming is a "no-op" (a trivial operation) in most semantics of type theory, so there's no help there, as far as I know. $\endgroup$
    – cody
    Commented Jun 19, 2014 at 18:36
  • 2
    $\begingroup$ @MikeShulman I agree with your comment, but I think the parenthetical "versus type theory in general" is still too specific. The issue comes up in any system that uses bound variables, for example ordinary first-order logic. It doesn't even have to be logic; in calculus, the integration symbol binds a variable, which sometimes needs to be renamed. $\endgroup$
    – Andreas Blass
    Commented Aug 2, 2014 at 15:23
  • 1
    $\begingroup$ @PaulTaylor I presume what is meant is Chow's moving lemma: see en.wikipedia.org/wiki/Chow%27s_moving_lemma and en.wikipedia.org/wiki/Intersection_theory. For example, the "self-intersection" of subvariety $C$ doesn't meant a naive set-theoretic intersection but the result of intersecting $C$ with a small perturbation of itself. A classical illustration interprets the self-intersection of the diagonal embedding of a variety $M \to M \times M$ in terms of its Euler characteristic; see mathoverflow.net/questions/696/… $\endgroup$
    – Todd Trimble
    Commented Oct 1, 2014 at 15:11

1 Answer 1

Reset to default
1
$\begingroup$

(disclaimer: I am not an expert on these subjects)

The underlying principle in both cases is that you can have many different representations of the same object, and we seek to do a calculation in a representation that is the easiest to use.

Your example from logical expressions is a triviality: we designed our formal language so that it's a trivial matter to substitute in new variables that won't conflict with any old ones. (this may be a more interesting topic if, for example, we were only allowed to use 10 variables)

The moving lemma from intersection theory, however, is a deep theorem about what alternative representations exist for an algebraic cycle.

One could imagine completely different foundations for algebraic geometry that could make the moving lemma obvious, but connecting the new foundations with algebraic varieties as we know them today would likely then be quite difficult. (and as a non-expert, I don't really have any clue what such a foundation would look like)

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .