Not signed in (Sign In)

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 comma 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 finite 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 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 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

    Anonymous

    v1, current

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

    Anonymous

    diff, v2, current

  3. started section on the syntax of objective type theory

    Anonymous

    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

    @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

    Γ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?

    Anonymous

    diff, v18, current

    • 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)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.

    Anonymous

    diff, v19, current

  6. added rules for binary sum types

    Anonymous

    diff, v24, current

  7. added section on transport

    Anonymous

    diff, v26, current

  8. added section on dependent identities

    Anonymous

    diff, v28, current

  9. definitional equality -> judgmental equality

    Anonymous

    diff, v31, current