Start a new discussion

Not signed in

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

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

1. 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

2. added section on open problems with a list of problems that the authors brought up in

Anonymous

3. started section on the syntax of objective type theory

Anonymous

• CommentRowNumber4.
• CommentAuthorGuest
• CommentTimeOct 11th 2022

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.

• CommentRowNumber5.
• CommentAuthorGuest
• CommentTimeOct 11th 2022

@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.

• CommentRowNumber6.
• CommentAuthorGuest
• CommentTimeOct 11th 2022

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

$\frac{\Gamma \vdash a \equiv b:A}{\Gamma \vdash p:a =_A b}$

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.

• CommentRowNumber7.
• CommentAuthorGuest
• CommentTimeOct 11th 2022

@4, 6

Btw, the eta rule is the uniqueness rule for function types, not the computation rules for function types.

4. 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?

Does having an interval type and a typal eta conversion rule for function types imply function extensionality in objective type theory?

Anonymous

• CommentRowNumber9.
• CommentAuthorGuest
• CommentTimeOct 11th 2022

@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.

• CommentRowNumber10.
• CommentAuthorGuest
• CommentTimeOct 11th 2022

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 $refl_{(a, b)}$ in the identity type of the type between a term $p$ and the pair of eliminators of the product type evaluated at $p$. So the usual ’propositional’ uniqueness rules cannot even be expressed in objective type theory.

• CommentRowNumber11.
• CommentAuthorGuest
• CommentTimeOct 11th 2022

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.

5. 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

6. added rules for binary sum types

Anonymous

Anonymous

8. added section on dependent identities

Anonymous

9. definitional equality -> judgmental equality

Anonymous