Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

(0 1)-category-theory 2-category 2-category-theory 2-monad abelian-categories accessible adjoint algebra algebraic algebraic-geometry analysis arithmetic beauty book bug bundle categories category category-theory chern-simons-theory cohesion cohesive-homotopy-type-theory cohomology combinatorics complex-geometry conference connection constructive constructive-mathematics cosmology database deformation-theory descent differential differential-cohomology differential-geometry duality enriched enriched-category-theory enrichment examples factorization-system fiber fibration forms foundation foundations functional-analysis functor galois-theory gauge-theory gebra general topology geometric geometric-quantization geometry gravity group-theory higher higher-algebra higher-category-theory higher-geometry higher-lie-theory higher-topos-theory history homological homological-algebra homotopy homotopy-theory homotopy-type-theory homtopy-type-theory infinity-groupoid infinity-topos integration-theory internal-categories kan lie-algebras lie-theory limit limits linear linear-algebra locale localization localization-theory logic manifolds mathematics measure measure-theory mechanics meta modal-logic model model-category-theory monoidal monoidal-category monoidal-category-theory morphism n-groups newpage noncommutative noncommutative-geometry object operator operator-algebra order-theory philosophy physics predicative pretopology pro-object probability-theory quantum quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry set set-theory sheaf simplicial site space stable-homotopy-theory stack string string-theory subobject supergeometry symplectic-geometry tannaka tensor terminology theory topologica-quantum-field-theory topology topos topos-theory torsor tqft type type-theory universal weighted-limit

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeMar 24th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexStarted a general page about [[beta reduction]], and a stub for [[eta reduction]] but I have to run now.

   Started a general page about beta reduction, and a stub for eta reduction but I have to run now.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeMar 25th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexNow a bit more at [[eta reduction]].

   Now a bit more at eta reduction.

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeMar 25th 2012
   • (edited Mar 25th 2012)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexSince the version with symbols is definitely ‘$\beta$-reduction’, I've moved the name without symbols to [[beta-reduction]] (with a hyphen). This triggers the cache bug, so I mention it here. The same with [[eta-reduction]] … but can I try to convince you that $\eta$-reduction is wrong and $\eta$-expansion is correct? ETA: No, the cache bug did not appear!

   Since the version with symbols is definitely ‘$\beta$-reduction’, I’ve moved the name without symbols to beta-reduction (with a hyphen). This triggers the cache bug, so I mention it here. The same with eta-reduction … but can I try to convince you that $\eta$-reduction is wrong and $\eta$-expansion is correct? ETA: No, the cache bug did not appear!

4. • CommentRowNumber4.
   • CommentAuthorTobyBartels
   • CommentTimeMar 25th 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI put in a stub for [[alpha-equivalence]].

   I put in a stub for alpha-equivalence.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThanks. I'm glad you brought up the reduction/expansion issue. What about calling the page [[eta-equivalence]] or [[eta-conversion]]? I know there are situations in which $\eta$-expansion seems to match better with $\beta$-reduction than $\eta$-reduction does (looking like the unit and multiplication of a monad or something, I don't recall the details), but I don't recall being convinced that that is a universal phenomenon. Is there a reason to believe that $\eta$-conversion has a well-defined "correct" directionality at all? Also, by the "trivial type" do you mean the [[unit type]]? If so, I don't understand your remark about it. Are you thinking of a positive or a negative definition of the trivial type?

   Thanks. I’m glad you brought up the reduction/expansion issue. What about calling the page eta-equivalence or eta-conversion? I know there are situations in which $\eta$-expansion seems to match better with $\beta$-reduction than $\eta$-reduction does (looking like the unit and multiplication of a monad or something, I don’t recall the details), but I don’t recall being convinced that that is a universal phenomenon. Is there a reason to believe that $\eta$-conversion has a well-defined “correct” directionality at all?

   Also, by the “trivial type” do you mean the unit type? If so, I don’t understand your remark about it. Are you thinking of a positive or a negative definition of the trivial type?

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI like [[eta-conversion]] so moved the page. However, I understand that term a bit differently from you; see my edits. Yes, I meant the unit type, defined negatively. I altered your material on the product type to produce material on the unit type, so you can see for yourself.

   I like eta-conversion so moved the page. However, I understand that term a bit differently from you; see my edits.

   Yes, I meant the unit type, defined negatively. I altered your material on the product type to produce material on the unit type, so you can see for yourself.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThanks; your meaning of $\eta$-conversion is better. And I see what you mean about the unit type. Interestingly, the positive definition of the unit type does have a well-defined $\eta$-reduction; I added some details to [[unit type]]. Now I'm wondering about the [[empty type]]. Its positive presentation is "dual" to the negative unit type in that there are no constructors, and a single eliminator $$e\colon \emptyset \vdash abort_C(e)\colon C.$$ So there can again be no $\beta$-reduction, but it seems like the $\eta$-conversion should be $e \;\leftrightarrow_\eta\; abort_{\emptyset}(e)$, which makes sense both as an expansion and as a reduction. Am I wrong? If not, why the asymmetry, I wonder? Is it because we've already broken the symmetry by formulating everything with variables and terms instead of covariables and coterms?

   Thanks; your meaning of $\eta$-conversion is better. And I see what you mean about the unit type. Interestingly, the positive definition of the unit type does have a well-defined $\eta$-reduction; I added some details to unit type.

   Now I’m wondering about the empty type. Its positive presentation is “dual” to the negative unit type in that there are no constructors, and a single eliminator

   $$e:\varnothing ⊢{\mathrm{abort}}_C(e):C.$$

   So there can again be no $\beta$-reduction, but it seems like the $\eta$-conversion should be $e{\leftrightarrow }_{\eta }{\mathrm{abort}}_{\varnothing }(e)$, which makes sense both as an expansion and as a reduction. Am I wrong? If not, why the asymmetry, I wonder? Is it because we’ve already broken the symmetry by formulating everything with variables and terms instead of covariables and coterms?

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAh, no, I'm wrong. The $\eta$-conversion for the positive empty type says that (in the context of a term $e\colon\emptyset$), any term $c\colon C$ of *any* type is convertible to $abort(e)$. This also only makes sense as an expansion.

   Ah, no, I’m wrong. The $\eta$-conversion for the positive empty type says that (in the context of a term $e:\varnothing$), any term $c:C$ of any type is convertible to $\mathrm{abort}(e)$. This also only makes sense as an expansion.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI've updated [[empty type]] with this, and also corrected the $\eta$-rule at [[sum type]] in the corresponding way.

   I’ve updated empty type with this, and also corrected the $\eta$-rule at sum type in the corresponding way.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMar 27th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI added some comments to [[eta-conversion]] about propositional $\eta$-conversions and how they are related to dependent eliminators. I also expanded [[function type]] and [[dependent product type]] to describe not only the usual negative presentations, but also the "higher-order" positive presentations and their relationship.

    I added some comments to eta-conversion about propositional $\eta$-conversions and how they are related to dependent eliminators. I also expanded function type and dependent product type to describe not only the usual negative presentations, but also the “higher-order” positive presentations and their relationship.

11. • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeMar 30th 2012
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexI've never seen the positive approach to dependent product types seriously considered, although it's implicit (in my opinion) in Martin-Löf's earliest work. So I'm glad to see that people have worked it out (even though I don't really like it for requiring a stronger metatheory).

    I’ve never seen the positive approach to dependent product types seriously considered, although it’s implicit (in my opinion) in Martin-Löf’s earliest work. So I’m glad to see that people have worked it out (even though I don’t really like it for requiring a stronger metatheory).

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeMar 30th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYeah, the stronger metatheory is a shame. But as Richard's paper shows, the resulting dependent eliminator sheds a useful light on the propositional eta conversion rule.

    Yeah, the stronger metatheory is a shame. But as Richard’s paper shows, the resulting dependent eliminator sheds a useful light on the propositional eta conversion rule.