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 limit 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 subobject 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).
    • CommentRowNumber101.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2022

    Re 77

    However, definitional equality isn’t really relevant here: definitional equality of two elements implies having a term of the identity type between two elements; i.e. the definitional computational rules of Martin-Löf identity types imply the propositional computation rule, and the definitional transport rules of cubical/higher observational’s identity/path types imply the propositional transport rules.

    and 80

    And non-dependent identity types have certain properties which hold universally across type theories regardless if the non-dependent identity types are primitive in the theory or derived from some other type family, such as the propositional J-rule, propositional transport, and reflexivity, and the fact that their categorical semantics is a path space object. So we could and should motivate general identity types by these properties which hold for all definitions of non-dependent identity types.

    (I can’t tell whether these were the same Guest, because these Guests are still not using identifiable pseudonyms; but they seem similar, so maybe.)

    The factual statements here are true, but I don’t think it follows that definitional equality isn’t relevant or that we should motivate general identity types by the properties which hold for all of them. The definitional equalities that hold in a particular type theory are an indication of how that type theory philosophically/intuitively holds things to be defined, as opposed to the properties that those things have after they’ve been defined, and hence determines the motivation that is most relevant to it.

    • CommentRowNumber102.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2022

    what I’m saying is that Id Id X(x,x)(pid x,p)Id_{Id_X(x,x')}(p \cdot id_x, p) and Id x:XId X(x,x)((x,id x),(x,p))Id_{\sum_{x':X} Id_X(x,x')}((x,id_x),(x',p)) are different types.

    Okay, I am not concerned with the first type and frankly i can’t tell why you bring it up.

    I wrote out standard or at least well-known facts, with a fair bit of effort in typesetting them readably, illustrating their meaning and referencing them in more detail than usual. If there are typos left, I’ll fix them. Otherwise I am bowing out of this thread.

    • CommentRowNumber103.
    • CommentAuthorGuest
    • CommentTimeSep 28th 2022

    Mike Shulman wrote

    The factual statements here are true, but I don’t think it follows that definitional equality isn’t relevant or that we should motivate general identity types by the properties which hold for all of them. The definitional equalities that hold in a particular type theory are an indication of how that type theory philosophically/intuitively holds things to be defined, as opposed to the properties that those things have after they’ve been defined, and hence determines the motivation that is most relevant to it.

    Regarding definitional equalities holding in a particular type theory, objective type theory simply does not have definitional equality in the theory at all, yet it still has identity types. Any discussion about identity types and its motivations has to deal with the fact that objective type theory does not have definitional equality and yet is still able to define identity types.

  1. Re 103

    Just a note, objective type theory is an incomplete theory, and in particular, the authors of the objective type theory paper never addressed how to define types and terms in objective type theory without definitional equality.

    Usually, defining a type or a term involves the usage of the operator \coloneqq, which was formally defined in Egbert Rijke’s Introduction to Homotopy Type Theory textbook on page 14 in Remark 2.2.1. Egbert’s formal definition uses definitional equality, and I’m not aware of any definition of \coloneqq which doesn’t use definitional equality.

    So I would be wary of making any philosophical claims about definitions in objective type theory until the theory is more fully fleshed out.

    • CommentRowNumber105.
    • CommentAuthorGuest
    • CommentTimeSep 28th 2022

    Sure you can, you use the given identity type instead of definitional equality in objective type theory. You could define a term a:Aa:A to be a term b:Ab:A by saying that term a:Aa:A comes with a path def(a,b):a= Ab\mathrm{def}(a, b):a =_A b. Similarly, you could define a type A:𝒰A:\mathcal{U} to be a type B:𝒰B:\mathcal{U} by saying that the type A:𝒰A:\mathcal{U} comes with a path def(A,B):A= 𝒰B\mathrm{def}(A, B):A =_\mathcal{U} B.

    Something similar happens for inductive definitions. For example, addition on the natural numbers could be defined as a function ()+():×(-)+(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N} with paths basecase(n):0+n= n\mathrm{basecase}(n): 0 + n =_\mathbb{N} n and indcase(m,n):s(m)+n= s(m+n)\mathrm{indcase}(m, n): s(m) + n =_\mathbb{N} s(m + n).

    • CommentRowNumber106.
    • CommentAuthorGuest
    • CommentTimeSep 28th 2022

    I would even argue that defining terms and types using the identity type is more in line with how mathematicians define terms and types elsewhere in mathematics. For example, in the Openstax Calculus Volume 2 textbook by Strang, Herman, et al, they give the definition of the area of the curve under a function ff on page 17 as

    Let f(x)f(x) be a continuous, nonnegative function on an interval [a,b][a, b], and let i=1 nf(x i *)δx\sum_{i = 1}^{n} f(x_i^*) \delta x be a Riemann sum for f(x)f(x). Then the area under the curve y=f(x)y = f(x) on [a,b][a, b] is given by

    A=lim n i=1 nf(x i *)δxA = \lim_{n \to \infty} \sum_{i = 1}^{n} f(x_i^*) \delta x

    The authors used propositional equality rather than the assignment operator or definitional equality.

    • CommentRowNumber107.
    • CommentAuthorMadeleine Birchfield
    • CommentTimeSep 28th 2022
    • (edited Sep 30th 2022)

    Re 105

    van der Berg and Besten did not define universes in objective type theory yet. If one tried to define universes, one could either define Russell universes or weakly Tarski universes. (strict Tarski universes aren’t possible because of the definitional equality in the definition of strict Tarski universes)

    Regardless of which definition one uses, if the type theory has a separate AtypeA \; \mathrm{type} judgment, one would find that your statement only applies for types AA or El(A)\mathrm{El}(A) which have a corresponding term of the universe A:UA:U. If the type theory has types which don’t belong to a universe, or if the type theory doesn’t have weakly Tarski universe or Russell universes, then defining a type BB to be a type AA not in a universe doesn’t work by your method.

    For example, in Egbert Rijke’s textbook, he defines the function type ABA \to B to be the dependent function type on a constant type family

    AB x:ABA \to B \coloneqq \prod_{x:A} B

    He has not introduced universes yet in his theory, and so the dependent function type do not belong to a universe. Defining function types in this way by your method isn’t possible in objective type theory at this stage of the theory.

    • CommentRowNumber108.
    • CommentAuthorMadeleine Birchfield
    • CommentTimeSep 28th 2022
    • (edited Sep 28th 2022)

    Also, Benno van der Berg and Martijn Besten explicitly state that objective type theory is a modification of Martin-Löf type theory with all definitional equalities replaced with identifications in the computation rules. So the motivation in objective type theory is the same as the motivation in Martin-Löf type theory; the only difference being that the definitional equality is swapped out with an identification in the computation rules.

    One could do the same thing in cubical type theory and swap all the definitional equalities out for path types, but the motivation there for introducing path types is still different from the motivation in Martin-Löf type theory, even if one gets rid of all definitional equality and replaces it with path types.

    • CommentRowNumber109.
    • CommentAuthorMike Shulman
    • CommentTimeSep 29th 2022

    Whatever the status of objective type theory, I’m happy to suppose for the sake of argument that it’s possible to have a type theory with identity types and without definitional equality. I don’t think that changes the fact that for type theories that do have definitional equality, the definitional equalities that they have are an indication of the intuition and motivation behind their identity types (or any other types). Even in a type theory without definitional equality, one can get some of the same information from which propositional equalities are posited “by definition” and which are derived from that. (E.g. in Book HoTT, the computation rules for eliminators on path-constructors of higher inductive types hold only propositionally, but we still regard them as “by definition” for purposes of intuition and motivation.)

    • CommentRowNumber110.
    • CommentAuthorMike Shulman
    • CommentTimeSep 29th 2022

    Since I’ve apparently failed to communicate my point to Urs in this discussion, I’ve gone ahead and edited the page; maybe these changes will make it clearer.

    I don’t know what “Identifications are preserved under composition with self-identifications” means or what it has to do with the uniqueness principle. In particular, there is no “composition” in the uniqueness principle, and I don’t know what is being “preserved”. The best slogan I could think of that comes close to expressing what the uniqueness principle says is “An identification identifies itself with a self-identification”.

    I’ve also added some text to the “semantics” paragraph explaining how the picture drawn doesn’t quite match what the type theory says.

    diff, v83, current

    • CommentRowNumber111.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 29th 2022

    Can I ask you, Mike, what you take to be the relationship between a type-theoretic justification of a construction and a category-theoretic one, e.g., as indicated for identity types in #95? Klev in that article makes the Martin-Löf move of criticising Walsh’s category-theoretic justification of path-induction as just translating from one language to another, when what’s needed is some proper grounding, as in the meaning explanation he gives for the J-rule. But as Walsh explains, the category-theoretic version of harmony isn’t just free-floating, it comes with an inferentialist justification, expressions take their meaning from how they’re formed/justified and how they’re used. The web of adjunctions that is logic dictates an introduction/elimination format and keeps everything harmonious, just as the inferentialist would want.

    I was invited by Klev to Prague back in the summer. He thinks in a purely type-theoretic way. It seems an odd situation to me that these different styles of justification exist, especially when they deliver the same practical answer. Is there something beyond ’constructions are important so long as they make sense to all sides’ (computational trinitarianism) towards ’constructions that make good sense to any side should make good sense to the others’ (perhaps due to a ’triality’)?

    • CommentRowNumber112.
    • CommentAuthorMike Shulman
    • CommentTimeSep 29th 2022

    I have not read Klev’s papers (and they’re paywalled for me). I do find it a very powerful observation that type theorists and category theorists have independently arrived at very similar ways of justifying/defining/characterizing objects via introduction and elimination. And I agree that in general, we should expect something that makes sense in one language to also make sense in another language, although it’s also true that sometimes certain things are easier to express in one language versus another (otherwise there would be no point in having more than one language!). It seems silly to me to argue about whether the type-theoretic or category-theoretic form of this justification is better or more meaningful, when they carry essentially the same information.

    • CommentRowNumber113.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 3rd 2022

    There should be a common philosophical core behind Martin-Löf-ian and inferentialist justification strategies.

  2. added redirects for identification type and identification types


    diff, v91, current

  3. starting section “note on terminology” about the different names used for identity types and terms of identity types


    diff, v91, current

  4. Mike Shulman said that dependent type theory is not sequent calculus, so removed mention of sequent calculus from article


    diff, v97, current

    • CommentRowNumber117.
    • CommentAuthorUrs
    • CommentTimeSep 15th 2023

    I have rolled back the deletion

    and replaced “sequent calculus” by “natural deduction” (here)

    diff, v98, current

  5. I think it would be useful to add the other version of the elimination and computation rules for identity types, known as based path induction in the HoTT book. Using the existing notation on the page:

    Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓ,x:A,t:C(x,x,r(x)),y:A,p:Id A(x,y),Δ(x,t,y,p)J(x,t,y,p):C(x,y,p)\frac{\Gamma, x:A, y:A, p:\mathrm{Id}_A(x, y), \Delta(x, y, p) \vdash C(x, y, p):\mathrm{Type}}{\Gamma, x:A, t:C(x, x, r(x)), y:A, p:\mathrm{Id}_A(x, y), \Delta(x, t, y, p) \vdash J(x, t, y, p):C(x, y, p)}


    Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓ,x:A,t:C(x,x,r(x)),Δ(x,t)J(x,t,x,r(x))t:C(x,x,r(x))\frac{\Gamma, x:A, y:A, p:\mathrm{Id}_A(x, y), \Delta(x, y, p) \vdash C(x, y, p):\mathrm{Type}}{\Gamma, x:A, t:C(x, x, r(x)), \Delta(x, t) \vdash J(x, t, x, r(x)) \equiv t:C(x, x, r(x))} Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓ,x:A,t:C(x,x,r(x)),Δ(x,t)β(x,t):Id C(x,x,r(x))(J(x,t,x,r(x)),t)\frac{\Gamma, x:A, y:A, p:\mathrm{Id}_A(x, y), \Delta(x, y, p) \vdash C(x, y, p):\mathrm{Type}}{\Gamma, x:A, t:C(x, x, r(x)), \Delta(x, t) \vdash \beta(x, t):\mathrm{Id}_{C(x, x, r(x))} (J(x, t, x, r(x)), t)}
  6. I have added inference rules for based path induction to the article, section headers for path induction and based path induction, and a explanation to what the inference rules for based path induction mean, in contrast to that of the usual path induction. I have also added the reference to section 1.12 of the HoTT book which explains path induction and based path induction, as well as a reference to section 5.1 of Rijke’s Introduction to Homotopy Type Theory which explains a similar distinction.

    There are duplicated sentences between the two sections which I have left in the article for the time being, but which may not be necessary.

    diff, v101, current