Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 definitions 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 nlab noncommutative noncommutative-geometry number-theory object 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

1. • CommentRowNumber101.
   • CommentAuthorMike Shulman
   • CommentTimeSep 28th 2022
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexRe 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.

   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.

2. • CommentRowNumber102.
   • CommentAuthorUrs
   • CommentTimeSep 28th 2022
   • PermaLink
   Author: Urs
   Format: MarkdownItex> what I'm saying is that $Id_{Id_X(x,x')}(p \cdot id_x, p)$ and $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.

   what I’m saying is that $Id_{Id_X(x,x')}(p \cdot id_x, p)$ and $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.

3. • CommentRowNumber103.
   • CommentAuthorGuest
   • CommentTimeSep 28th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexMike 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.

   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.

4. • CommentRowNumber104.
   • CommentAuthorMadeleine Birchfield
   • CommentTimeSep 28th 2022
   • PermaLink
   Author: Madeleine Birchfield
   Format: MarkdownItexRe 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.

   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.

5. • CommentRowNumber105.
   • CommentAuthorGuest
   • CommentTimeSep 28th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexSure you can, you use the given identity type instead of definitional equality in objective type theory. You could define a term $a:A$ to be a term $b:A$ by saying that term $a:A$ comes with a path $\mathrm{def}(a, b):a =_A b$. Similarly, you could define a type $A:\mathcal{U}$ to be a type $B:\mathcal{U}$ by saying that the type $A:\mathcal{U}$ comes with a path $\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 $\mathrm{basecase}(n): 0 + n =_\mathbb{N} n$ and $\mathrm{indcase}(m, n): s(m) + n =_\mathbb{N} s(m + n)$.

   Sure you can, you use the given identity type instead of definitional equality in objective type theory. You could define a term $a:A$ to be a term $b:A$ by saying that term $a:A$ comes with a path $\mathrm{def}(a, b):a =_A b$. Similarly, you could define a type $A:\mathcal{U}$ to be a type $B:\mathcal{U}$ by saying that the type $A:\mathcal{U}$ comes with a path $\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 $\mathrm{basecase}(n): 0 + n =_\mathbb{N} n$ and $\mathrm{indcase}(m, n): s(m) + n =_\mathbb{N} s(m + n)$.

6. • CommentRowNumber106.
   • CommentAuthorGuest
   • CommentTimeSep 28th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexI 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](https://assets.openstax.org/oscms-prodcms/media/documents/CalculusVolume2-OP.pdf), they give the definition of the area of the curve under a function $f$ on page 17 as > Let $f(x)$ be a continuous, nonnegative function on an interval $[a, b]$, and let $\sum_{i = 1}^{n} f(x_i^*) \delta x$ be a Riemann sum for $f(x)$. Then the **area under the curve** $y = f(x)$ on $[a, b]$ is given by > $$A = \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.

   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 $f$ on page 17 as

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

   $$A = \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.

7. • CommentRowNumber107.
   • CommentAuthorMadeleine Birchfield
   • CommentTimeSep 28th 2022
   • (edited Sep 30th 2022)
   • PermaLink
   Author: Madeleine Birchfield
   Format: MarkdownItexRe 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 $A \; \mathrm{type}$ judgment, one would find that your statement only applies for types $A$ or $\mathrm{El}(A)$ which have a corresponding term of the universe $A: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 $B$ to be a type $A$ not in a universe doesn't work by your method. For example, in Egbert Rijke's textbook, he defines the function type $A \to B$ to be the dependent function type on a constant type family $$A \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.

   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 $A \; \mathrm{type}$ judgment, one would find that your statement only applies for types $A$ or $\mathrm{El}(A)$ which have a corresponding term of the universe $A: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 $B$ to be a type $A$ not in a universe doesn’t work by your method.

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

   $$A \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.

8. • CommentRowNumber108.
   • CommentAuthorMadeleine Birchfield
   • CommentTimeSep 28th 2022
   • (edited Sep 28th 2022)
   • PermaLink
   Author: Madeleine Birchfield
   Format: MarkdownItexAlso, 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.

   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.

9. • CommentRowNumber109.
   • CommentAuthorMike Shulman
   • CommentTimeSep 29th 2022
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWhatever 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.)

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

10. • CommentRowNumber110.
    • CommentAuthorMike Shulman
    • CommentTimeSep 29th 2022
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexSince 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. <a href="https://ncatlab.org/nlab/revision/diff/identity+type/83">diff</a>, <a href="https://ncatlab.org/nlab/revision/identity+type/83">v83</a>, <a href="https://ncatlab.org/nlab/show/identity+type">current</a>

    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

11. • CommentRowNumber111.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 29th 2022
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexCan 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')?

    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’)?

12. • CommentRowNumber112.
    • CommentAuthorMike Shulman
    • CommentTimeSep 29th 2022
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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.

    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.

13. • CommentRowNumber113.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 3rd 2022
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexThere should be a common philosophical core behind Martin-Löf-ian and inferentialist justification strategies.

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

14. • CommentRowNumber114.
    • CommentAuthornLab edit announcer
    • CommentTimeJan 19th 2023
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexadded redirects for [[identification type]] and [[identification types]] Anonymous <a href="https://ncatlab.org/nlab/revision/diff/identity+type/91">diff</a>, <a href="https://ncatlab.org/nlab/revision/identity+type/91">v91</a>, <a href="https://ncatlab.org/nlab/show/identity+type">current</a>

    added redirects for identification type and identification types

    Anonymous

    diff, v91, current

15. • CommentRowNumber115.
    • CommentAuthornLab edit announcer
    • CommentTimeJan 19th 2023
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexstarting section "note on terminology" about the different names used for identity types and terms of identity types Anonymous <a href="https://ncatlab.org/nlab/revision/diff/identity+type/91">diff</a>, <a href="https://ncatlab.org/nlab/revision/identity+type/91">v91</a>, <a href="https://ncatlab.org/nlab/show/identity+type">current</a>

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

    Anonymous

    diff, v91, current

16. • CommentRowNumber116.
    • CommentAuthornLab edit announcer
    • CommentTimeSep 14th 2023
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexMike Shulman said that dependent type theory is not sequent calculus, so removed mention of sequent calculus from article contributor <a href="https://ncatlab.org/nlab/revision/diff/identity+type/97">diff</a>, <a href="https://ncatlab.org/nlab/revision/identity+type/97">v97</a>, <a href="https://ncatlab.org/nlab/show/identity+type">current</a>

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

    contributor

    diff, v97, current

17. • CommentRowNumber117.
    • CommentAuthorUrs
    • CommentTimeSep 15th 2023
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have rolled back the deletion and replaced "sequent calculus" by "natural deduction" ([here](https://ncatlab.org/nlab/show/identity+type#ExplicitDefinition)) <a href="https://ncatlab.org/nlab/revision/diff/identity+type/98">diff</a>, <a href="https://ncatlab.org/nlab/revision/identity+type/98">v98</a>, <a href="https://ncatlab.org/nlab/show/identity+type">current</a>

    I have rolled back the deletion

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

    diff, v98, current

18. • CommentRowNumber118.
    • CommentAuthorMadeleine Birchfield
    • CommentTimeDec 4th 2023
    • (edited Dec 4th 2023)
    • PermaLink
    Author: Madeleine Birchfield
    Format: MarkdownItexI 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: $$\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)}$$ and $$\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))}$$ $$\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)}$$

    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:

    $$\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)}$$

    and

    $$\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))}$$ $$\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)}$$
19. • CommentRowNumber119.
    • CommentAuthorMadeleine Birchfield
    • CommentTimeDec 5th 2023
    • PermaLink
    Author: Madeleine Birchfield
    Format: MarkdownItexI 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. <a href="https://ncatlab.org/nlab/revision/diff/identity+type/101">diff</a>, <a href="https://ncatlab.org/nlab/revision/identity+type/101">v101</a>, <a href="https://ncatlab.org/nlab/show/identity+type">current</a>

    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

20. • CommentRowNumber120.
    • CommentAuthornLab edit announcer
    • CommentTimeAug 18th 2024
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdd missing \Delta(x,y,p) to #### Standard J rule Fylwind <a href="https://ncatlab.org/nlab/revision/diff/identity+type/117">diff</a>, <a href="https://ncatlab.org/nlab/revision/identity+type/117">v117</a>, <a href="https://ncatlab.org/nlab/show/identity+type">current</a>

    Add missing \Delta(x,y,p) to #### Standard J rule

    Fylwind

    diff, v117, current