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

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeNov 17th 2011
   • PermaLink
   Author: Urs
   Format: MarkdownItexearlier today I had started splitting off entries [[intensional type theory]] and [[extensional type theory]] from [[type theory]]. But then the Lab halted and now it's left in somewhat stubby form.

   earlier today I had started splitting off entries intensional type theory and extensional type theory from type theory. But then the Lab halted and now it’s left in somewhat stubby form.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI added an additional equivalent characterization of [[extensional type theory]]: that equality in the total space of a dependent type implies equality in the fiber. (This is a frequent "how do I prove this obvious fact?" question on the coq-club mailing list.)

   I added an additional equivalent characterization of extensional type theory: that equality in the total space of a dependent type implies equality in the fiber. (This is a frequent “how do I prove this obvious fact?” question on the coq-club mailing list.)

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeNov 28th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI split the definition of [[extensional type theory]] into "definitional" and "propositional" flavors, and included a proof I just learned which shows that in the presence of Id-induction, the equality reflection rule is enough to make the theory extensional: you don't need to assert separately that any proof of equality is equal to reflexivity. I left a query box there after responding to it, in hopes that its poster would find it and come here.

   I split the definition of extensional type theory into “definitional” and “propositional” flavors, and included a proof I just learned which shows that in the presence of Id-induction, the equality reflection rule is enough to make the theory extensional: you don’t need to assert separately that any proof of equality is equal to reflexivity.

   I left a query box there after responding to it, in hopes that its poster would find it and come here.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeJun 21st 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWell, it didn't work, so I'm moving the discussion to here: --- I don't want to unilaterally edit this page, but #3 above is fairly different than any of the others (except maybe #2), and it is pretty much the only one that I've ever heard type theorists talking about when they say "extensional type theory." It is the difference between Martin-Löf's intensional and extensional type theory. Intensional has the J eliminator, and extensional has the _inference rule_ from propositional equality to judgmental equality. Dependent pattern matching, K, uniqueness of identity proofs and the like don't get you the equivalent of reflecting the propositions back into the judgments, and that is what makes extensional type theory in the eyes of type theorists (as far as I've encountered), not the dimension of the identity types. For instance, Agda is considered intensional despite having K, and even Observational Type Theory ala Conor McBride, which adds lots of extensionality axioms for various types, and eta-ish rules when possible, is still arguably intensional in this sense. And that is the whole point in OTT's case, because the [[decidability]] issues (mentioned below) are tied to extensionality in the inference rule sense, not any homotopy sense.' Also, I expect the bit about functional extensionality came from a discussion with me on n-cafe. But, it's not really true that type theorists use 'extensional type theory' to refer to theories in which functional extensionality holds. I believe my point in that discussion was that 'extensional equality type' (or similar) suggested to me a type that reified the extensional equivalence (equality) relation of the type it was defined for (so, Eq A a b would have an inhabitant if a is extensionally equal to b of type A), and didn't immediately suggest an identity type that was a homotopy proposition. For instance, the identity types in OTT reify extensional equality in this sense. And extensional type theories (for instance, NuPRL) typically incorporate this, because they can, whereas Agda (for instance) does not. HTT identity types are reifying extensional equality of functions, as well, and perhaps would work for coinductive types as well (whenever those get worked out). But that is about my impression of "(extensional identity) type" not "extensional (identity type)," the latter of which might be an identity type in extensional type theory, which has little to do with what sort of relations it's reifying. --- Dan Doel Thanks for your suggestions; I've tried to incorporate some of them. If you want to discuss this more, I suggest opening a post at the [nForum](http://nforum.mathforge.org/) (and copying this query box there). You could join [this discussion](http://nforum.mathforge.org/discussion/3305/extensional-and-intensional-type-theory) for instance. -- Mike Shulman

   Well, it didn’t work, so I’m moving the discussion to here:

   ---

   I don’t want to unilaterally edit this page, but #3 above is fairly different than any of the others (except maybe #2), and it is pretty much the only one that I’ve ever heard type theorists talking about when they say “extensional type theory.” It is the difference between Martin-Löf’s intensional and extensional type theory. Intensional has the J eliminator, and extensional has the inference rule from propositional equality to judgmental equality.

   Dependent pattern matching, K, uniqueness of identity proofs and the like don’t get you the equivalent of reflecting the propositions back into the judgments, and that is what makes extensional type theory in the eyes of type theorists (as far as I’ve encountered), not the dimension of the identity types. For instance, Agda is considered intensional despite having K, and even Observational Type Theory ala Conor McBride, which adds lots of extensionality axioms for various types, and eta-ish rules when possible, is still arguably intensional in this sense. And that is the whole point in OTT’s case, because the decidability issues (mentioned below) are tied to extensionality in the inference rule sense, not any homotopy sense.’

   Also, I expect the bit about functional extensionality came from a discussion with me on n-cafe. But, it’s not really true that type theorists use ’extensional type theory’ to refer to theories in which functional extensionality holds. I believe my point in that discussion was that ’extensional equality type’ (or similar) suggested to me a type that reified the extensional equivalence (equality) relation of the type it was defined for (so, Eq A a b would have an inhabitant if a is extensionally equal to b of type A), and didn’t immediately suggest an identity type that was a homotopy proposition. For instance, the identity types in OTT reify extensional equality in this sense. And extensional type theories (for instance, NuPRL) typically incorporate this, because they can, whereas Agda (for instance) does not. HTT identity types are reifying extensional equality of functions, as well, and perhaps would work for coinductive types as well (whenever those get worked out).

   But that is about my impression of “(extensional identity) type” not “extensional (identity type),” the latter of which might be an identity type in extensional type theory, which has little to do with what sort of relations it’s reifying.

   — Dan Doel

   Thanks for your suggestions; I’ve tried to incorporate some of them. If you want to discuss this more, I suggest opening a post at the nForum (and copying this query box there). You could join this discussion for instance.

   – Mike Shulman