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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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).

nLab > Latest Changes: Initiality Project - Type Theory - Term equality

Bottom of Page

1 to 8 of 8

  1.  
    • CommentRowNumber1.
    • CommentAuthorkyod
    • CommentTimeOct 30th 2018

    Page created, but author did not leave any comments.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeOct 30th 2018

    Remove term validity assumption from reflexivity and add it to transitivity, in accord with previous discussion re: presuppositions

    diff, v2, current

    • CommentRowNumber3.
    • CommentAuthormaxsnew
    • CommentTimeOct 31st 2018

    It doesn’t matter much for the interpretation because this is all proof-irrelevant, but what are we making admissible vs primitive rules of equality? For instance there’s no need to make reflexivity a primitive rule since it’s directly provable from the congruence rules that we have to add for every rule anyway. In addition, there should also be a principle that substitution preserves judgmental equality.

    I propose we make reflexivity and substitution principles admissible.

    The only benefit to taking the substitution principle as primitive I know of is it can simplify the presentation of the η\eta principles because then we just have to state them for variables, like f=λx.fxf = \lambda x. f x for η\eta which directly corresponds to the universal property, which then implies the presentation we currently have M=λx.MxM = \lambda x. M x using the substitution principle.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeOct 31st 2018

    I agree that substitution into all judgment forms should definitely be admissible.

    For reflexivity, I suppose we could make it admissible, but I think we would still need a “base case” rule that every variable is equal to itself, no? I’m not sure what the benefit would be of this.

    • CommentRowNumber5.
    • CommentAuthoratmacen
    • CommentTimeOct 31st 2018
    Mike's premise-free reflexivity also lets you derive reflexivity instances for complete nonsense. It's an experiment: can we get away with completely separating validity and equality?
    • CommentRowNumber6.
    • CommentAuthormaxsnew
    • CommentTimeOct 31st 2018

    Yes you need reflexivity for variables, which I was including as a kind of congruence rule. I agree that it is a small difference but I also think it’s silly to include unnecessary rules.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeOct 31st 2018

    For the purposes of this project, there’s a good reason to reduce the number of rules, since each rule involves its own clauses in the various inductions we have to do. And we should also choose rules whose corresponding inductive clauses will be simpler. But I don’t see any reason that the inductive clauses for a general reflexivity rule would be any more complicated than that for a variable; both of them are essentially trivial since equality in the semantics is reflexive.

    • CommentRowNumber8.
    • CommentAuthorkyod
    • CommentTimeOct 31st 2018

    I generally agree with @maxsnew that minimizing the set of primitive rules usually allow to have more canonical derivations. However in the case of type equality (here), we cannot expect to have any form of canonical equality derivation, and restricting the reflexivity rule to variables makes it (ever so slightly) more complicated.

1 to 8 of 8

  1.