Not signed in (Sign In)

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

  • Sign in using OpenID

Site Tag Cloud

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 galois-theory 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 nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics planar 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 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

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
  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


    v1, current

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


    diff, v2, current

  3. started section on the syntax of objective type theory


    diff, v4, current

    • 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


    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

    Γab:AΓp:a= Ab\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?

    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?


    diff, v18, current

    • CommentRowNumber9.
    • CommentAuthorGuest
    • CommentTimeOct 11th 2022


    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)refl_{(a, b)} in the identity type of the type between a term pp and the pair of eliminators of the product type evaluated at pp. 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.


    diff, v19, current

  6. added rules for binary sum types


    diff, v24, current

  7. added section on transport


    diff, v26, current

  8. added section on dependent identities


    diff, v28, current

  9. definitional equality -> judgmental equality


    diff, v31, current

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)