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.
somebody on the nForum thread on the identity type article brought up objective type theory so I thought I would start an article on that subject
Anonymous
added section on open problems with a list of problems that the authors brought up in
Anonymous
Regarding the “open problem”
Does having an interval type imply function extensionality in objective type theory?
In regular Martin-Löf type theory, having an interval type only implies function extensionality if it has definitional computational rules for the point constructors, as explained in the blog post An Interval Type Implies Function Extensionality by Mike Shulman.
Since there is no definitional equality in objective type theory, one cannot prove function extensionality from the existence of an interval type.
@4
Mike Shulman’s proof relies on the definitional eta rule for function types in Martin-Löf type theory. In objective type theory, the eta rule for function types is a propositional eta rule, so that proof doesn’t apply to the open problem at hand.
The point of Mike Shulman’s blog post is that he and Peter Lumsdaine couldn’t prove function extensionality from the interval type with only propositional computational rules. The definitional computation rules for function types imply the propositional computational rules for function types, because given a definitional equality of two terms of a type one could derive a propositional equality for the two terms of a type
which applies to the computation rules for function types. If the propositional computational rules for function types and the point constructors of the interval type had implied functional extensionality, then they should have been able to prove functional extensionality without assuming definitional computation rules for the point constructors of the identity type. That they were unable to prove so back then indicates that function extensionality is not provable from having an interval type in objective type theory.
@4, 6
Btw, the eta rule is the uniqueness rule for function types, not the computation rules for function types.
In the van der Berg and Besten article, their dependent function types do not have an eta conversion rule. So the assumption of a typal eta conversion rule for function types is missing from the statement of the open problem
Does having an interval type imply function extensionality in objective type theory?
The statement now reads
Does having an interval type and a typal eta conversion rule for function types imply function extensionality in objective type theory?
Anonymous
@8
The reason why propositional eta rules are usually not included in any definition is because they could be proven from the formation, introduction, elimination, and beta reduction rules. So if the type theory have function types, they already satisfy the propositional eta rules.
Whoops, you are right about eta being uniqueness rules rather than computation rules.
However, the ’propositional’ uniqueness rules proven in Martin-Löf type theory aren’t fully propositional at all; according to the eta conversion article on the nLab, in the case for product types they involve a definitional equality with in the identity type of the type between a term and the pair of eliminators of the product type evaluated at . So the usual ’propositional’ uniqueness rules cannot even be expressed in objective type theory.
I think we could mark the last two open problems about proving function extensionality as not provable. In the article on interval type it says
Conversely, any contractible type satisfies the rules of an interval type up to propositional equality.
In particular, this means that the unit type satisfies the rules of an interval type up to propositional equality, and we already know that having the unit type does not imply function extensionality. Similarly, the propositional truncation of the booleans satisfies the rules of an interval type up to propositional equality, and similarly the rules of the unit type up to propositional equality.
It seems that definitional equality is a requirement for proving function extensionality.
Getting rid of the last two open problems as they are more general than just objective type theory. They could still be found in the Metatheory section of the article open problems in homotopy type theory, as a question of types having typal beta conversion and eta conversion in type theories.
Anonymous
1 to 16 of 16