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 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 nforum 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 sheaves 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: definition

Bottom of Page

1 to 11 of 11

  1.  

  1. Moving info regarding the use of equality in definitions from equality to this page

    Anonymous

    diff, v7, current

  2. Started section on inductive definitions

    Anonymous

    diff, v7, current

  3. Inductive and recursive definitions

    Anonymous

    diff, v7, current

  4. added section on inductive and recursive definitions and addition of natural numbers as an example of a recursively defined function

    Anonymous

    diff, v10, current

  5. Adding example of isProp

    Anonymous

    diff, v12, current

  6. Added transport as an example of an inductively defined function, and added a link to natural deduction

    Anonymous

    diff, v12, current

  7. moved info originally in assignment operator

    Anonymous

    diff, v16, current

  8. moved information on inductive definitions in type theory over to inductive definition

    Anonymous

    diff, v19, current

    • CommentRowNumber9.
    • CommentAuthorGuest
    • CommentTimeNov 9th 2022

    The notion of definitional equality should be about syntactical expressions, where we define a syntactical expression to be another syntactical expression. In this sense, it should have more in common with alpha equivalence than computational equality. For example, we should be able to define the symbol Ξ\Xi as the context (Γ,a:A)(\Gamma, a:A), Ξ≡(Γ,a:A)ctx\Xi \equiv (\Gamma, a:A) \; \mathrm{ctx}. Currently, definitional equality is only defined for types and terms.

    Johannes Schmidt

  10. moving info over to definitional equality

    Anonymous

    diff, v20, current

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeNov 9th 2022
    • (edited Nov 9th 2022)

    At the end of the Idea-paragraph (here) it would be good to mention more typical examples of “definitions”, and how they fit in, for instance the definitions of “groups”, “algebras”, “modules”, etc.

    I guess you will mean to say that these fall under the second clause of “definition via equality with an existing type”, in that they can be defined to be certain iterated dependent products. But this would be great to make explicit.

    diff, v21, current

1 to 11 of 11

  1.