Timeline for Analogy between variable substitution and the moving lemma
Current License: CC BY-SA 3.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 1, 2014 at 15:11 | comment | added | Todd Trimble | @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/… | |
| Aug 3, 2014 at 17:54 | comment | added | Mike Shulman | @AndreasBlass, you're right. | |
| Aug 2, 2014 at 18:55 | comment | added | Paul Taylor | Please would someone explain what the moving lemma is, for the benefit of any type theorists reading this. | |
| Aug 2, 2014 at 15:23 | comment | added | Andreas Blass | @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. | |
| Jul 3, 2014 at 19:27 | comment | added | Adiji | Chapter 1.2 Function Types. Page 31 in my version. | |
| Jul 3, 2014 at 14:52 | comment | added | Andrej Bauer | Where in the HoTT book is this? | |
| Jul 3, 2014 at 13:01 | answer | added | user13113 | timeline score: 1 | |
| Jun 19, 2014 at 18:36 | comment | added | cody | 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. | |
| Jun 19, 2014 at 16:32 | comment | added | Mike Shulman | I also don't see anything specific to HoTT (versus type theory in general) about it. | |
| Jun 19, 2014 at 10:52 | comment | added | Zhen Lin | This is well studied in computer science, in relation to the problem of "capture-avoiding substitution". | |
| Jun 19, 2014 at 8:28 | review | First posts | |||
| Jun 19, 2014 at 8:38 | |||||
| Jun 19, 2014 at 8:12 | history | asked | Adiji | CC BY-SA 3.0 |