Not signed in (Sign In)

Start a new discussion

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 galois-theory 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 homology homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory itex 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 science set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory 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: identity type

Bottom of Page

1 to 100 of 115

  1. <
  2. 1
  3. 2
  4. >
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 18th 2011

    added to identity type a mentioning of the alternative definition in terms of inductive types (paths).

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeNov 18th 2011

    Thanks! It’s not really an alternative definition, though, just an encompassing of the other definition into a general framework. Also, it predates HoTT by a lot. I edited the page some trying to clarify.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeNov 18th 2011

    Ah, okay. That wasn’t clear to me. Thanks.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeDec 13th 2011

    I have added to identity type some discussion of the stability/coherence obstacles to interpreting identity types categorically in a WFS, along with some more references.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeMar 26th 2012

    I added to identity type a discussion of how the definitional eta-conversion rule for identity types forces us into extensional type theory.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeMar 26th 2012

    I wonder: is there a negative presentation of identity types?

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeMay 9th 2012

    at identity type in the section on categorical semantics I have added some actual details on how that proceeds. (to the existing discussion of what conditions on the ambient category we need for this.)

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeNov 30th 2014

    For fun, I have given identity type a lead-in quote

    everything is identitcal with itself (WdL §863)

    no two things are like each other (WdL §903)

    Beyond being fun, it is reminiscent of how there is no way to prove equality than by reducing to reflection.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeNov 30th 2014

    In a similar vein, I have been amused to notice that as Arthur grows up, one of the more difficult things for him to learn is that two things can be isomorphic without being identical (e.g. the beans on his plate and the beans on Dad’s plate).

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 30th 2014

    You do realise that you and Urs now have the perfect opportunity to see how children brought up in the HoTT spirit will think mathematically.

    Think how much harder at a later stage to work out how money works. Not only do they go through the stage of worrying about which particular coin they have, but that it’s treated as the same as combinations of coins.

    • CommentRowNumber11.
    • CommentAuthorNikolajK
    • CommentTimeDec 1st 2014

    David,

    Even in my daily life, I’m often confronted with how plain bijections are not good isomorphisms in the category of coins, closed under addition. If it were, it would spare me some NP-complete problems.

    Sure, everything I can buy with a 5er, I can also by with five 1’s. But if some machine takes two 1’s, I can’t use my 5er to get gum out of a machine. Its curious how money is partitioned into 1’s, 2’s, 5’s and 10-multiples of it. When I’m waiting in a cue, I always compute if I can generate all composites to pay “right”: With {1,2,2,5} you can pay 1,2,3,4,5,6,7,8,9. Funny how changing a 2 with a 1 only changes the upper bound, but not e.g your ability to produce 4. With more money, {1,5,5} say, you have far less options :) Having 11 units of money really isn’t just having 11 units of it. I was in Russia last month and when I ran out of money for some days, the boss of the firm we worked in said he’d help me out with some cash - of course I’d give him back whatever I didn’t need. Well, this guy then gave me a note worth a huge amount. I assume he meant the best, but to me it was an ass move as I just couldn’t break the note and give him back some small ones. He gave me too much and so he gave me nothing.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 1st 2014

    On my end, the Proceß has not expressed the moment of quantity yet, it still needs to sublate becoming into a more determinate being first. Also, I am still worried not so much about the identity type of beans as about it being inhabited at all.

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 2nd 2018

    Some of the βs and ηs had become ∞\infty in links, so I fixed this.

    I guess we just live with using η-reduction, -conversion, -expansion interchangeably.

    diff, v40, current

  14. Thanks David! This one was my fault, sorry, again it’s related to the unicode issues. When I get the time to try to fix things once and for all, I’ll look out for occurrences of this one.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMay 2nd 2018

    As explained at the page eta-conversion, η\eta-reduction, η\eta-conversion, and η\eta-expansion are technically all slightly different things, though of course very closely related. η\eta-conversion is an undirected equivalence relation; η\eta-reduction and η\eta-expansion are the two opposite ways to “direct” this relation. Would it be useful to mention this point on the page identity type?

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 2nd 2018

    I wonder if we use these consistently, e.g., at Extensionality and η-conversion.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2018

    also pointer to Licata 11. Is that where the observation originates?

    diff, v41, current

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)

    Hm, it seems that my first edit-message did not get through:

    I had added pointer to Shulman 12 and was asking: Where is the origin of the observation that identity types are simply indctive type families generated by reflection?

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeAug 5th 2018

    Oh, way earlier than that. For instance, identity types are defined that way in Coq and have been since ever that I know of.

    • CommentRowNumber20.
    • CommentAuthorColin Tan
    • CommentTimeNov 28th 2018

    From say the inductive definition of identities types, it is clear that the interpretation of Id A(x,y)Id_A(x,y) as the type of proofs that x is less than or equal to y is excluded?

    For example, what if a type A is really an oo-category? So that Id A(x,y)Id_A(x, y) is the type of morphisms from an object x of A to another object y of A. It would still be true that there is an identity morphism in Id A(x,x)Id_A(x, x).

    • CommentRowNumber21.
    • CommentAuthorAli Caglayan
    • CommentTimeNov 28th 2018

    @Colin I think what you are trying to say is “can we have directed ’identitity’ types”. From the given inductive definition, the answer is a straight no however many people have and still are investigating similar types where they behave more like arrows of a category rather than of groupoids.

    I wouldn’t call this the identitiy type however. The symmetry of Id_A(x,y) isn’t something we add on but it is actually something that can be proven so if you were to have an arrow type it wouldn’t look very similar to the identity type.

    I would look at directed type theory, although I must say it isn’t very developed yet.

    • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 28th 2018
    • (edited Nov 28th 2018)

    You can of course do category theory in HoTT, see sec 9.1 of the HoTT book. This will involve a type of objects and then a dependent type of morphisms between two objects. But that’s not the identity type. In a category, the type of isomorphisms between two objects will equal their identity type.

    As Alizter says, also look at directed homotopy type theory.

    • CommentRowNumber23.
    • CommentAuthorAli Caglayan
    • CommentTimeNov 28th 2018

    There isn’t much content in the article David linked, but you should definitely look at some of the references. That is pretty much all the work that has been done on the topic.

    • CommentRowNumber24.
    • CommentAuthorColin Tan
    • CommentTimeNov 28th 2018

    Alizter, thank you very much for the pointers and for articulating what I was trying to ask in better language. Do you have a reference for a proof that Id A(x,y)Id_A(x, y) is symmetric? Mike also makes a comment on the derivability of this at Martin-Löf+dependent+type+theory#equality_types.

    • CommentRowNumber25.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 28th 2018

    Lemma 2.1.1 of the HoTT book. Essentially, by induction for identity types, you just have to show that the reflrefl terms have inverses, which clearly they do.

  26. Fixed a tiny typo: an -> a

    anqurvanillapy

    diff, v42, current

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeJun 25th 2019

    pointers to the original observations relating identity types to groupoids and higher groupoids were and still largely are missing from this entry. But I have now added at least these two:

    • Martin Hofmann, Thomas Streicher The groupoid interpretation of type theory, in: Giovanni Sambin et al. (ed.) , Twenty-five years of constructive type theory, Proceedings of a congress, Venice, Italy, October 19—21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 83-111 (1998). (ps)

    • Steve Awodey, Michael Warren, Homotopy theoretic models of identity type, Mathematical Proceedings of the Cambridge Philosophical Society vol 146, no. 1 (2009) (arXiv:0709.0248)

    diff, v43, current

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    added ISBN and uploaded the pdf for:

    • Martin Hofmann, Thomas Streicher The groupoid interpretation of type theory, in: Giovanni Sambin et al. (eds.) , Twenty-five years of constructive type theory, Proceedings of a congress, Venice, Italy, October 19—21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 83-111 (1998). (ISBN:9780198501275, ps, pdf)

    diff, v48, current

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    This entry has offered no original references. I have now added pointer to

    • Per Martin-Löf, Section 1.7 in: An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ’73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 Pages 73-118, Elsevier 1975 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)

    but that (that section 1.7) is hardly satisfactory. What’s a canonical original reference?

    diff, v49, current

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021
    • (edited May 12th 2021)

    this one shows the rules, but gives no discussion otherwise:

    diff, v49, current

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    This one has more:

    diff, v49, current

    • CommentRowNumber32.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2021

    added pointer to:

    diff, v50, current

    • CommentRowNumber33.
    • CommentAuthorGuest
    • CommentTimeJan 26th 2022
    Whenever editing is re-enabled a link to cocylinder should be placed in the Related concepts section.
    • CommentRowNumber34.
    • CommentAuthorGuest
    • CommentTimeMay 21st 2022

    This article only focuses upon the identity types that appear in Martin-Löf type theory. So what do we do about all the other inequivalent identity types in other type theories, such as the identity types in cubical type theory defined using a primitive interval, and the identity types in higher observational type theory?

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeMay 21st 2022

    You need to ask what a reader deserves to see when looking for information and happening upon a page with a given title.

    I suppose that a reader looking to understand what is meant by “identity type” will want to be shown all possible meanings. So if there are more than currently discussed in the page, then the page deserves to be re-organized/expanded.

  36. started brief section on identity types in higher observational type theory, somebody with a better understanding of the subject like Mike Shulman could expand on it further

    Anonymous

    diff, v56, current

    • CommentRowNumber37.
    • CommentAuthorGuest
    • CommentTimeAug 6th 2022

    path type redirects here, but in the cubical type theory literature, path types are different from identity types in that most of them do not satisfy the J rule definitionally, but only up to a path.

    • CommentRowNumber38.
    • CommentAuthorGuest
    • CommentTimeSep 2nd 2022

    created path type article. propositional equality redirects here as well, but should be created and made into a disambiguation article with links to both identity type and path type.

    • CommentRowNumber39.
    • CommentAuthorMike Shulman
    • CommentTimeSep 3rd 2022
    • (edited Sep 3rd 2022)

    I would actually prefer that the phrase “identity type” be usable for whatever notion is appropriate for the particular type theory. This includes the Martin-Lof identity type (a.k.a. “jdentity type”), the path type of cubical type theroies, and the identity type of higher observational type theory, all of which satisfy different formal rules but are still “types of identifications”.

    • CommentRowNumber40.
    • CommentAuthorGuest
    • CommentTimeSep 3rd 2022

    Andrew Swan thinks differently in this article

    We give a collection of results regarding path types, identity types and univalent universes in certain models of type theory based on presheaves.

    The main result is that path types cannot be used directly as identity types in any Orton-Pitts style model of univalent type theory with propositional truncation in presheaf assemblies over the first and second Kleene algebras.

    We also give a Brouwerian counterexample showing that there is no constructive proof that there is an Orton-Pitts model of type theory in presheaves when the universe is based on a standard construction due to Hofmann and Streicher, and path types are identity types. A similar proof shows that path types are not identity types in internal presheaves in realizability toposes as long as a certain universe can be extended to a univalent one.

    We show that one of our key lemmas has a purely syntactic variant in intensional type theory and use it to make some minor but curious observations on the behaviour of cofibrations in syntactic categories.

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeSep 3rd 2022

    Yes, I’m aware that cubical type theorists tend to use “identity type” to mean the Martin-Lof one. (Although in cubical type theory there is also a “Swan identity type” that’s different from both path types and ML identity types.) I’m saying I would rather advocate a different usage. Some cubical type theorists have taken to calling the ML identity type the “jdentity type”, since its defining feature is the J rule.

    • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeSep 3rd 2022

    As evidence supporting my preference, let me point out that the phrase “identity type” is already used in both intensional type theory and extensional type theory, even though the identity types of those two theories satisfy different rules.

    • CommentRowNumber43.
    • CommentAuthorGuest
    • CommentTimeSep 3rd 2022

    Many cubical type theorists make the distinction between identity types like Martin-Löf’s identity types, Swan’s identity types, and the higher observational type theory identity types, where the rules for the identity types all imply the definitional J rule as a theorem (and they call all 3 types ’identity types’), vs the cubical path types where the rules only imply the J rule up to a path, and additional regularity rules are needed to make the J rule definitionally valid.

    No additional regularity rule has been found to be compatible with univalence in cubical type theories yet.

    • CommentRowNumber44.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 3rd 2022

    Can we do better than this?

    Identity types in cubical type theory are called path types and are defined using a primitive interval. I’m not exactly sure how they work so somebody with more expertise with cubical type theory should expand on it.

    • CommentRowNumber45.
    • CommentAuthorMike Shulman
    • CommentTimeSep 3rd 2022

    The identity types of higher observational type theory also do not satisfy definitional computation for J.

    • CommentRowNumber46.
    • CommentAuthorMike Shulman
    • CommentTimeSep 3rd 2022

    Also, if someone wants to do mathematics “agnostically” in higher type theory, so that what they write could be interpreted equally well in Book HoTT, cubical type theory, or higher observational type theory, they can do that technically by assuming just an “identity type” with a propositional J-rule. But they then have to call that type something, and I don’t know what they could call it other than an “identity type”.

    • CommentRowNumber47.
    • CommentAuthorGuest
    • CommentTimeSep 3rd 2022

    @Guest at 43

    Cubical type theorists make the distinction between path types and identity types because path types are literally functions out of an interval, just like how paths in Euclidean space are functions out of the unit interval, not because of the definitional/propositional J distinction. Otherwise, why are the types in XTT called “path types” instead of “identity types”? They satisfy definitional J by coercion and regularity.

    Nathan

    • CommentRowNumber48.
    • CommentAuthorGuest
    • CommentTimeSep 3rd 2022

    @Mike Shulman at 46

    The definitional/propositional J could be distinguished by calling the identity type with definitional J a “strict identity type” and the identity type with propositional J a “weak identity type”. Type theory already uses “strict” and “weak” terminology for other such objects in type theory: compare “strict Tarski universe” vs “weak Tarski universe”, “strict proposition” and “weak proposition”, “strict squash type” and “weak squash type”, et cetera, where the difference between the structures are that the “strict” versions use definitional equality while the “weak” versions use propositional equality.

    Nathan

    • CommentRowNumber49.
    • CommentAuthorGuest
    • CommentTimeSep 3rd 2022

    Nathan,

    If one includes the interval type in MLTT then identity types between objects of a type are also functions out of the interval to the type. But identity types in homotopy type theory (or any model of MLTT with the interval type) are not usually called “path types”. So that doesn’t explain why path types are called path types in cubical type theory.

    • CommentRowNumber50.
    • CommentAuthorGuest
    • CommentTimeSep 4th 2022

    The definitional J rule implies the propositional J rule, but the converse doesn’t hold, so one should take the propositional J rule to be the defining characteristic of identity types, as those apply for all known identity types, not just the Martin-Löf identity types. This is similar to the case for W-types and higher inductive types, the computation rules are only up to a path, rather than involving definitional equality.

    • CommentRowNumber51.
    • CommentAuthorGuest
    • CommentTimeSep 4th 2022

    The real problem with path types in cubical type theory are that technically they aren’t identity types, they are dependent identity types, in the same way a dependent function type is not a function type, and so they should actually be described on the article on dependent identity types rather than this article.

    • CommentRowNumber52.
    • CommentAuthorGuest
    • CommentTimeSep 4th 2022

    @50

    What do you mean by “propositional J rule”?

    Suppose one has a cubical higher observational type theory with Swan’s identity types; there are 3 separate identity types idHOTT\mathrm{idHOTT}, idSwan\mathrm{idSwan}, and Path\mathrm{Path}. From there one could define 4 separate propositional computational rules (the elimination rule being the same for all 4) for the Martin-Löf identity types, resulting in 4 separate identity types idML0\mathrm{idML}0, idML1\mathrm{idML}1, idML2\mathrm{idML}2, idML3\mathrm{idML}3:

    Γ⊢a:AΓ,x:A,p:idML0 A(a,x)⊢P(x,p)typeΓ,u:P(a,refl A)⊢q:idML0 P(a,refl A)(indeq a(u,a,refl A),u)\frac{\Gamma \vdash a:A \quad \Gamma, x:A, p:\mathrm{idML}0_A(a, x) \vdash P(x, p) \; \mathrm{type}}{\Gamma, u:P(a, \mathrm{refl}_A) \vdash q:\mathrm{idML}0_{P(a, \mathrm{refl}_A)}(\mathrm{indeq}_a(u, a, \mathrm{refl}_A), u)} Γ⊢a:AΓ,x:A,p:idML1 A(a,x)⊢P(x,p)typeΓ,u:P(a,refl A)⊢q:idHOTT P(a,refl A)(indeq a(u,a,refl A),u)\frac{\Gamma \vdash a:A \quad \Gamma, x:A, p:\mathrm{idML}1_A(a, x) \vdash P(x, p) \; \mathrm{type}}{\Gamma, u:P(a, \mathrm{refl}_A) \vdash q:\mathrm{idHOTT}_{P(a, \mathrm{refl}_A)}(\mathrm{indeq}_a(u, a, \mathrm{refl}_A), u)} Γ⊢a:AΓ,x:A,p:idML2 A(a,x)⊢P(x,p)typeΓ,u:P(a,refl A)⊢q:idSwan P(a,refl A)(indeq a(u,a,refl A),u)\frac{\Gamma \vdash a:A \quad \Gamma, x:A, p:\mathrm{idML}2_A(a, x) \vdash P(x, p) \; \mathrm{type}}{\Gamma, u:P(a, \mathrm{refl}_A) \vdash q:\mathrm{idSwan}_{P(a, \mathrm{refl}_A)}(\mathrm{indeq}_a(u, a, \mathrm{refl}_A), u)} Γ⊢a:AΓ,x:A,p:idML3 A(a,x)⊢P(x,p)typeΓ,u:P(a,refl A)⊢q:Path P(a,refl A)(indeq a(u,a,refl A),u)\frac{\Gamma \vdash a:A \quad \Gamma, x:A, p:\mathrm{idML}3_A(a, x) \vdash P(x, p) \; \mathrm{type}}{\Gamma, u:P(a, \mathrm{refl}_A) \vdash q:\mathrm{Path}_{P(a, \mathrm{refl}_A)}(\mathrm{indeq}_a(u, a, \mathrm{refl}_A), u)}

  53. added some more details about identity types in cubical type theory, mentioning both the dependent identity type called the path type and the non-dependent identity type by Andrew Swan

    Anonymous

    diff, v63, current

    • CommentRowNumber54.
    • CommentAuthorGuest
    • CommentTimeSep 4th 2022

    dependent path types in cubical type theory are not dependent identity types, because the interval primitive II is not a type!

    That is another reason why path types in cubical type theory should be considered different from identity types.

    • CommentRowNumber55.
    • CommentAuthorMike Shulman
    • CommentTimeSep 4th 2022

    This discussion would be a lot easier to follow if everyone would sign their comments with a name. Pseudonyms would be fine, just something so we can distinguish between all the Guests and Anonymice. Please?!?

    Re 48: I suppose, although I would prefer the meaning of “identity type” to be theory-dependent. In HOTT I wouldn’t want to have to always say “weak identity type” rather than just “identity type”.

    Re 49: Not by definition. Book HoTT doesn’t have a notion of “extension type” that one could use to define a notion of “path type” out of the interval with fixed endpoints. So even though in some imprecise sense, identifications in Book HoTT are “equivalent to” functions out of the interval type, they’re not defined to be such the way they are in cubical type theories.

    Re 51: The general form of path-types is a dependent identity type, but they specialize to non-dependent identity types in the case of constant dependence or reflexivity in the base. So they are identity types, and more. The identity types of HOTT also behave like this.

    Re 52: But because any weak identity type is equivalent to any other, all of those propositional computation rules are inter-derivable. So the difference doesn’t really matter.

    Re 54: What do you mean? The interval is not a type, but the path types are types!

    • CommentRowNumber56.
    • CommentAuthorsteveawodey
    • CommentTimeSep 4th 2022
    I agree that the various identity/path/identification/equality types are all “identity types” in a general sense and can usefully be discussed and distinguished in the same place.

  57. added a brief list of the kinds of identity types to the introduction section, and also an explanation to what distinguishes identity types from other type families and an explanation of the two different J-rules.

    Anonymous

    diff, v65, current

  58. adding paragraph to explain the difference between dependent and non-dependent identity types

    Anonymous

    diff, v65, current

  59. There exist intensional type theories for which there is no such notion of definitional equality, and so the only possible notion of identification elimination in that theory is the one which uses the identity type for equality. Benno van den Berg and Martijn den Besten came up with such a type theory:

    • CommentRowNumber60.
    • CommentAuthorMike Shulman
    • CommentTimeSep 6th 2022

    Clarified the paragraph about dependent identity types a bit.

    diff, v67, current

    • CommentRowNumber61.
    • CommentAuthorMike Shulman
    • CommentTimeSep 6th 2022

    Although I’m not sure that this much detail about dependent identity types is appropriate in the “Idea” section. Maybe it should appear further down.

    • CommentRowNumber62.
    • CommentAuthorGuest
    • CommentTimeSep 9th 2022

    What does the semicolon mean in the judgment J(t;x,y,p):C(x,y,p)J(t;x,y,p):C(x,y,p)?

    • CommentRowNumber63.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2022

    It’s just a way of separating the first argument of JJ from the last three. Optional.

    • CommentRowNumber64.
    • CommentAuthorUrs
    • CommentTimeSep 23rd 2022

    I am removing the following redirects and copying them instead into the entry transport:

      [[!redirects principle of substitution]]

  [[!redirects principle of substitution of equals for equals]]

  [[!redirects principle of substituting equals for equals]]

    diff, v69, current

    • CommentRowNumber65.
    • CommentAuthorUrs
    • CommentTimeSep 25th 2022
    • (edited Sep 25th 2022)

    I am going to add to this page a semi-formal explanation of Id-types that has a chance of being intelligible to intelligent outsiders.

    The strategy would be to recall from the forefathers that identifications satisfy three rules:

    1. everything is canonically identified with itself;

    2. identified things are indiscernible

    3. identifications have reverses.

    and then to observe that the evident operational/constructive formulation of these three items is, in this order, nothing but:

    1. IdId-intro

    2. transport

    3. IdId-uniqueness principle

    and finally to conclude with proving that

    • (2) and (3) ⇔\;\;\Leftrightarrow\;\; J-rule .

    This is, of course, essentially the (meta-)logic proposed by Ladyman & Presnell 2015, minus some verbosity.

    I admit that I only recently looked at their article in detail, for the first time, and took note of their actual point. Now I am struck by how relevant this is. The (straightforward but not completely trivial) formal proofs for the last step are also spelled out in the Bachelor thesis Götz 2018.

    This leads to an evident bibliographic question: Is it the case that the literature making explicit the above foundational point of HoTT consists of one Philosophy-article and one Bachelor thesis?

    I suppose experts will feel this is all well-known, but before I write an exposition into the nLab entry: Are there other references making this explicit?

    diff, v70, current

    • CommentRowNumber66.
    • CommentAuthorUrs
    • CommentTimeSep 25th 2022

    An early version of the kind of motivation/overview/explanation that I want to add is now here: MetaLogicOfIdentifications-220925.jpg. Will further fine-tune tomorrow.

    • CommentRowNumber67.
    • CommentAuthorMike Shulman
    • CommentTimeSep 26th 2022

    Well, L&P say clearly in the beginning of section 6

    It is known to type theorists that the two principles discussed below entail path induction – see, for example, [12, pp. 23- 29], but as far as we are aware they do not put this fact to use in the way we do here.

    [12] is

    Thierry Coquand. Equality and Dependent Type Theory. A talk given for the 24th AILA meeting, Bologna, February 2011.

    This fact is also the way that the J-rule is proven from the other primitives in cubical type theory and in H.O.T.T.

    In general, I’m not hugely impressed with that L&P paper. It seems to me that if you’re willing to accept equality in a based path space as the correct notion of “uniqueness” for Id-types, there’s nothing preventing you from similarly accepting the based J-rule as justified by a claim that “all identifications are refl” (which they reject) in exactly the same sense that equality in a based path space is the proper sort of uniqueness.

    I’m also not convinced that Id-uniqueness corresponds to “reverses”. It’s true that one of the two possible orientations of Id-uniqueness involves in particular a path in the opposite direction (although the other possible orientation does not). But even then, there’s still something nontrivial going on in identifying the obvious equality p•p −1=reflp \bullet p^{-1} = refl with the necessary equality in a Sigma-type. Indeed, I have no idea how to prove that those two equalities are equivalent without already using the J-rule or something equivalent to it.

    • CommentRowNumber68.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2022

    in exactly the same sense

    That’s the point: but it makes it explicit and disentangles it from the transport aspect.

    In contrast, what trips newcomers when they are first shown the J-rule is that, first, it comes as a surprise to consider dependency on identifications in a fundamental axiom; and, second, that it remains mysterious how those identifications-of-identifications work. Both of these puzzles are clarified by decomposing J as Transport plus Reversal.

    And if, as you say

    This fact is also the way that the J-rule is proven from the other primitives in cubical type theory and in H.O.T.T.

    it seems worthwhile even beyond the pedagogic aspect.

    Regarding:

    Thierry Coquand. Equality and Dependent Type Theory

    Thanks for the pointer! I had missed that. So in addition to one Phil-article and one Bachelor thesis there is one slide! I will add these pointers to the entry now, with commentary.

    • CommentRowNumber69.
    • CommentAuthorMike Shulman
    • CommentTimeSep 26th 2022

    As I said, I don’t believe that Id-uniqueness is correctly described as “reversal”.

    I can see a pedagogical point to derive J from Id-uniqueness (as well as its practical uses). I was just saying that I don’t think it changes the philosophical situation any.

    • CommentRowNumber70.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2022

    I heard you say it, but don’t know what you mean, it sounds counterfactual.

    • CommentRowNumber71.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 26th 2022

    I’m struggling to see what’s at stake here.

    • Is the objection to L&P in #67 that they’re looking to derive the J-rule from other assumptions, but to show this derivation fully they would need to rely on the J-rule? And in any case, the kinds of reasoning to justify these other assumptions are of the same kind that would justify the J-rule straight off?

    • Is there a difference between book HoTT and cubical type theory or H.O.T.T. in this regard?

    • What is the “philosophical situation” (#69)?

    • CommentRowNumber72.
    • CommentAuthorAlmaza213434567
    • CommentTimeSep 26th 2022
    • (edited Sep 26th 2022)
    I heard you say it, but don’t know what you mean, it sounds counterfactual.
    https://elpasofenceinstallationcompany.com/
    • CommentRowNumber73.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2022

    re #71: The entry identity type currently does a terrible job at explaining its subject to an audience not yet familiar with it.

    I’ll write an intelligible Idea-section, using exposition as shown #66. Still busy with something else, though.

    • CommentRowNumber74.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 26th 2022

    I certainly agree that the current state of the page is bad. And one might hope for there to be some account which both is excellent pedagogically and gets at the essence of the concept.

    Does the need to do this simultaneously for all type theories present a problem?

    • CommentRowNumber75.
    • CommentAuthorMike Shulman
    • CommentTimeSep 26th 2022

    Is the objection to L&P in #67 that they’re looking to derive the J-rule from other assumptions, but to show this derivation fully they would need to rely on the J-rule? And in any case, the kinds of reasoning to justify these other assumptions are of the same kind that would justify the J-rule straight off?

    More the latter. They don’t call Id-elimination “reversal”, which is where I think you already need to have the J-rule.

    Is there a difference between book HoTT and cubical type theory or H.O.T.T. in this regard?

    I believe so. CTT and HOTT don’t take the J-rule as primitive, so the problem of justifying their rules is a different one.

    What is the “philosophical situation” (#69)?

    A reference back to #67.

    • CommentRowNumber76.
    • CommentAuthorMike Shulman
    • CommentTimeSep 26th 2022

    Urs, I don’t know what you mean by “it sounds counterfactual”. I’m saying that the version of Id-uniqueness that you need in order to derive J does not coincide with any intuitive statement of “reversal”, unless you already have the J-rule to prove them equivalent.

    • CommentRowNumber77.
    • CommentAuthorGuest
    • CommentTimeSep 26th 2022

    The only difference w/regards to the J-rule between the identity/path types in cubical type theory and higher observational type theory and the identity types as usually presented in Martin-Löf type theory is that in cubical/higher observational, the computation rule uses an identity type while in Martin-Löf the computation rule uses definitional equality.

    With transport, the situation is reversed: in cubical/higher observational, transport uses definitional equality, while Martin-Löf uses an identity type.

    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.

    As a result, one could replace both instances of definitional equality with propositional equality in the definition of an identity type the resulting definition will apply to more type theories, including those like objective type theory mentioned above in comment 59 which lack definitional equality entirely.

    • CommentRowNumber78.
    • CommentAuthorGuest
    • CommentTimeSep 26th 2022

    David Corfield wrote

    Is there a difference between book HoTT and cubical type theory or H.O.T.T. in this regard?

    Yes. Book HoTT’s identity types are by default homogeneous identity types, while both cubical type theory’s path types and H.O.T.T.’s identity types are heterogeneous identity types.

    The motivation for making homogeneous identity types the default and constructing heterogeneous identity types out of homogeneous identity types is likely different from the motivation for making heterogeneous identity types the default and constructing homogeneous identity types out of heterogeneous identity types.

    Scott Morris

    • CommentRowNumber79.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2022

    the version of Id-uniqueness that you need in order to derive J does not coincide with any intuitive statement of “reversal”

    The intuitive picture is this:

    x some identification↙ ⇒ ↘ trivial identification y →−−−−−−−−−reverse identification x \array{ && x \\ & \mathllap{{}^{\text{some identification}}}\swarrow &\Rightarrow& \searrow{}^{\mathrlap{\text{trivial identification}}} \\ y && \underset{\mathclap{\text{reverse identification}}}{\xrightarrow{\phantom{---------}}} && x }
    • CommentRowNumber80.
    • CommentAuthorGuest
    • CommentTimeSep 26th 2022

    @79

    Whether the default identity type in the type theory is heterogeneous or homogeneous is irrelevant to this discussion; I think by the fact that we have a separate article for dependent identity type strongly indicates that this article is about the homogeneous/non-dependent identity types. 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.

    • CommentRowNumber81.
    • CommentAuthorGuest
    • CommentTimeSep 26th 2022

    sorry I meant @78 not @79

    • CommentRowNumber82.
    • CommentAuthorGuest
    • CommentTimeSep 27th 2022

    There are also Swan identity types. What are the motivation behind those identity types, and how is that different from the motivation behind Martin-Löf identity types?

    • CommentRowNumber83.
    • CommentAuthorUrs
    • CommentTimeSep 27th 2022

    Oh, I see. I guess you mean that we need the identification-of-identifications in the other direction. In which case it expresses that identifications may be composed with self-identifications. In fact that’s closer to what Leibniz actually says – for what it’s worth.

    • CommentRowNumber84.
    • CommentAuthorUrs
    • CommentTimeSep 27th 2022
    • (edited Sep 27th 2022)

    I have now re-written the Idea-section of the entry (starting here).

    The main new part is the sub-section “Idea – ML identity types” (now here) which means to introduce the reader to what’s going on in a more generally intelligible way.

    (The previous statement of the J-rule was a bit like showing ASCII art after removing all its whitespace characters. That statement is still kept in the Definition-section, where it used to be. But if we had more energy, this would deserve to be typeset more readably, too.)

    I have tried to keep all material previously in the Idea-section, after re-arranging it slightly. That old material, subject to little adjustments, is now in brief sub-sections “Idea – Cubical identity types” (here) and “Idea – Strict identity types” (here). There is still much room to improve these further.

    diff, v75, current

    • CommentRowNumber85.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 27th 2022

    Should we have something on this page on identity types and adjunctions? I remember this paper as arguing against the justification in Ladyman & Presnell 2015, and in favour of one by adjoints:

    • Patrick Walsh, Categorical harmony and path induction, Review of Symbolic Logic 10(2): 301-321 (2017) (pdf)

    See in particular p. 20.

    His own justification is on p. 18

    1. Identity is a concept determined by adjoint and so has a meaning-bearing inferential role, being categorically harmonious;
    2. The inferential role of identity in these hyperdoctrines indeed provides a justification for path induction.

    He notes

    The proof that path induction is derivable from the definition of identity in a hyperdoctrine can be found in the appendix to [35]. The proof there is due to Steve Awodey.

    [35] is his masters thesis.

    • CommentRowNumber86.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 27th 2022

    Another criticism of L&P’s justification of path induction comes in

    • Ansten Klev, (2019a). The justification of identity elimination in Martin-Löf’s type theory. Topoi, 38, 577–590. (doi:10.1007/s11245-017-9509-1)

    The justification of Id-elimination suggested by Ladyman and Presnell (2015, p.401ff.) consists in treating (Ind) and (Uniq) as primitive principles of type theory and showing how Id-elimination may be derived on that basis. It is not clear to me what is gained by this approach. Although the postulation of (Ind) and (Uniq) allows one to derive Id-elimination, these postulations themselves of course have to be justified.

    His own justification comes from Martin-Löf’s meaning explanation.

    More by him on justifying the identity elimination rule here:

    • CommentRowNumber87.
    • CommentAuthorUrs
    • CommentTimeSep 27th 2022

    arguing against

    It really is self-evident – I bet you could check this on lay people and kids in your vicinity:

    Given an identification x→pyx \xrightarrow{\; p \;} y, there is an evident identification-of-identifications between id x∘pid_x \circ p and pp.

    The forefathers would have stated this, had they only thought about identifications being constructions instead of just properties. But a contemporary kid who knows what a computer is will know that a computer decrypting an email and one decrypting that email and then doing nothing have performed the same task.

    • CommentRowNumber88.
    • CommentAuthorUrs
    • CommentTimeSep 27th 2022

    I have the impression that the names of Ladyman and Presnell keep derailing the discussion unnecessarily. We saw above that their idea is due to Coquand and is at the heart of modern HoTT-provers – that should be sufficient proof by authority that this is worthwhile, if that is necessary and if we cannot agree on what is “pre-mathematically self-evident”.

    But mainly – and this is what got me here before I even reminded myself of Ladyman and Presnell’s – it seems clearly helpful for appreciating the J-rule to realize that it is transport along the evident paths-of-paths. I find it puzzling that such an obvious and obviously helpful remark leads to debate. Every introduction to HoTT ought to say this.

    Anyway, I have now made the edits to the entry that I had announced in #65. I feel like this drastically improves on the expository use of the entry. I can try to make further tweaks where it helps the exposition, otherwise I will bow out of the debate.

    • CommentRowNumber89.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 27th 2022
    • (edited Sep 27th 2022)

    Typo: in the box in IIb, above the ’w’ of ’with the self-identification’, it should be x′x' rather than xx.

    It really is self-evident

    Walsh just says

    How are we to justify, without mathematical knowledge, the claim that identity types should be inhabited by terms identical to the trivial identification up to propositional identity over E aE_a? Although I think this is patently not pre-mathematical, I will not dwell on the point here.

    Where you write

    Given an identification x→pyx \xrightarrow{\; p \;} y, there is an evident identification-of-identifications between id x∘pid_x \circ p and pp,

    isn’t it Mike’s point above (#67) that the passage from an obvious composition of identities (as in yours here) to an equality in a Sigma-type (which is what you need) is not obvious:

    there’s still something nontrivial going on in identifying the obvious equality p•p −1=reflp \bullet p^{-1} = refl with the necessary equality in a Sigma-type.

    I guess in your case he’s asking how p¯ *\bar{p}_{\ast} is constructed.

    • CommentRowNumber90.
    • CommentAuthorGuest
    • CommentTimeSep 27th 2022

    Is equality in classical mathematics definitional equality? I was under the impression that it was a form of propositional equality, since material set theory over first order logic is a simple type theory which consists of a type SetSet or VV of sets and a type PropProp of propositions, and equality is defined as an equivalence relation on sets which is a binary predicate valued in propositions.

    • CommentRowNumber91.
    • CommentAuthorGuest
    • CommentTimeSep 27th 2022

    @90

    That is one presentation of material set theory over first order logic, and not the most usual presentation of material set theory over first order logic in type theory.

    In the usual presentation of material set theory over first order logic, one judges ApropA \; \mathrm{prop} directly, rather than judge Proptype\mathrm{Prop} \; \mathrm{type} and A:PropA:\mathrm{Prop}. Similarly, one judges BsetB \; \mathrm{set} directly, rather than judge Settype\mathrm{Set} \; \mathrm{type} and B:SetB:\mathrm{Set}.

    In this regards, it is very similar to a system like simplicial type theory or cubical type theory where there are different levels for the propositional logic or face formulas and the set theory or type theory

    • CommentRowNumber92.
    • CommentAuthorGuest
    • CommentTimeSep 27th 2022

    But regardless, one would still say that given two sets AA and BB, equality A=BA = B is judged to be a proposition.

    In homotopy type theory, one see the same thing with universes and type judgments. One often works with Russell universes (where every type is a judged to be a member of a universe type like A:𝒰 iA : \mathcal{U}_i, where ii is a natural number representing the universe level. But one could equally work with Coquand type judgments, where one has an hierarchy of type judgments Atype iA \; \mathrm{type}_i rather than a hierarchy of universes A:𝒰 iA : \mathcal{U}_i. So I don’t see how switching between judgments and universes/type of sets/type of propositions changes anything substantial semantically, whether it be for homotopy type theory or for set theory over first order logic.

    • CommentRowNumber93.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2022
    • (edited Sep 28th 2022)

    re: #89:

    The typo in the box in (IIb) I have fixed now, thanks for catching this!

    Also, I have added the previously missing computation rule to the box for (IIa).

    in your case he’s asking how p¯ *\bar{p}_{\ast} is constructed.

    But it’s clearly not “constructed”: It’s the “meaning explanation” of what the uniqueness axiom bluntly asserts! I have recalled the illustration in #79 (and for the reverse direction in the entry here).

    If anyone is lacking the “pre-mathematical” intuition to read this diagram (?), they can regard it as literally being the 2-simplex which models the corresponding path-of-paths in the simplicial model. (I have now added a corresponding comment to the entry, here, if it helps.)

    \,

    re: #90:

    Thanks for catching this, that was my bad. You were referring to the words “definitional equality” in the second paragraph here, and I have deleted these two words now.

    diff, v78, current

    • CommentRowNumber94.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2022

    have added (here) also a box for path lifting

    diff, v81, current

    • CommentRowNumber95.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 28th 2022
    • (edited Sep 28th 2022)

    But it’s clearly not “constructed”: It’s the “meaning explanation” of what the uniqueness axiom bluntly asserts!

    So I guess two wings (of the computational trilogy/trinity) are objecting to that axiomatic assertion.

    Klev (acknowledging Sundholm and Martin-Löf) in the first paper in #86 provides what he takes to be the meaning explanation for the J-rule, arguing that it fits in with the typical ML approach to type formation. By contrast,

    The approach suggested by Ladyman and Presnell moreover breaks the general pattern in type theory of furnishing set-forming operators with introduction- and elimination rules, since the Id-elimination rule is now replaced by two postulates that cannot be regarded as elimination rules. It seems to me a great insight, first developed in Martin-Löf (1971), that propositional identity can be treated by means of such rules.

    For him, postulation of the uniqueness axiom is no better justified than other proposals, such as UIP, for Id-types (is that what Mike is saying in #67?), not the right kind of justification he sees as possible for the J-rule (as he gives in section 4).

    Then Walsh (acknowledging Awodey) takes his departure from the universal constructions of category-theoretic adjunctions. Presumably as a positive type, the Id-introduction and elimination rules just fall out as usual as the unit of the corresponding monad/ Hom isomorphism (as here). Why, from a category-theoretic point of view, would one expect further analysis of what is the expression of a left universal property to be illuminating? Do we ever do that for other universal constructions?

    So both parties want Intro/Elim as basic, but for different reasons (or maybe not so different). The type theorists because this is how to give proper meaning explanations, and the category theorist because this is how to express universal constructions.

    • CommentRowNumber96.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2022

    I promised to bow out of this kind of kind of discussion. (E.g. I find it weird to cite people not for their insight but for their insistence on not understanding something! ;-o)

    But I’ll offer this, for comparison:

    Here at math.SE:q/4379724 is exhibited the typical puzzlement that newcomers have with the J-rule – there are two parts of puzzlements:

    1. Why consider a dependency on identifications in the first place and

    2. how is it that identifications all relate to the trivial one?

    The top reply math.SE:a/4379766 starts with a verbose part

    It’s tricky… It’s extremely surprising …. struggled with this …

    but eventually, in its last paragraph, it gives the explanation: by pointing out that one is evaluating transport on the paths that contract the based path space. This is what addresses both points of the puzzlement.

    Of course, young genius readers of the nLab who grasp the J-rule without this kind of explanation are free to skip the Idea-section and jump to the Definition-section of our entry. I think no harm is done by my attempt at an exposition – particularly since I just list a bunch of facts, no philosophy involved (apart from some ancient Latin quotes, for entertainment).

    • CommentRowNumber97.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2022

    Urs, what I’m saying is that Id Id X(x,x′)(p⋅id 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. The latter is equivalent to ∑ q:Id X(x,x′)Id Id X(x,x′)(q⋅id x,p)\sum_{q:Id_X(x,x')} Id_{Id_X(x,x')}(q\cdot id_x, p), so we can inhabit it if we can inhabit the first one — but the proof of that equivalence uses the J-rule. So if you’re trying to motivate the J-rule, you can’t use that equivalence. Thus, motivating the fact that Id Id X(x,x′)(p⋅id x,p)Id_{Id_X(x,x')}(p \cdot id_x, p) is inhabited doesn’t suffice to motivate the J-rule, because to derive the J-rule you need instead to know that Id ∑ x′:XId X(x,x′)((x,id x),(x′,p))Id_{\sum_{x':X} Id_X(x,x')}((x,id_x),(x',p)) is inhabited.

    • CommentRowNumber98.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2022

    Re 90:

    Is equality in classical mathematics definitional equality?

    First-order logic does not really have a “definitional equality” in the way that type theory does. Or if it does, it’s fairly trivial. As you say, mathematics formulated in first-order logic, like ZFC, uses a propositional equality.

    • CommentRowNumber99.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2022

    Re 82

    There are also Swan identity types. What are the motivation behind those identity types, and how is that different from the motivation behind Martin-Löf identity types?

    Interesting question! I don’t know whether Swan identity types have any philosophical justification; the point as I understand it is just to get a kind of identity type in cubical type theory that satisfies a definitional computation rule for J. I mean, you can look at their construction and try to consider that a motivation, but you’d have to already have and understand the cubical identity types.

    • CommentRowNumber100.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2022

    Re 78

    Book HoTT’s identity types are by default homogeneous identity types, while both cubical type theory’s path types and H.O.T.T.’s identity types are heterogeneous identity types.

    There’s definitely a difference, but I wouldn’t phrase it like that. In particular, I’m not sure what “by default” means. All three theories have both homogeneous and heterogeneous identity types, and it’s not possible to have only heterogeneous ones because they have to depend on the homogeneous ones.

    I would say the difference is in how the heterogeneous identity types “reduce to” the homegeneous ones when the type dependence is trivial. In Book HoTT, this reduction is only up to equivalence. In HOTT, it’s a definitional equality. I’m not positive about cubical type theory, but I think there it is a definitional isomorphism.

1 to 100 of 115

  1. <
  2. 1
  3. 2
  4. >