Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

July 26, 2022

Identity Types in Context

Posted by Emily Riehl

guest post by Shreya Arya and Greta Coraglia

The relation between mathematicians and the notion of identity has been an interesting one. Even what is arguably the first mathematical text (that we know of) in history, Euclid’s Elements (c. 300 BC), deals with the problem of equality. In Book I, after Definitions and Postulates, Euclid details five Common Notions:

  1. Things equal to the same thing are also equal to one another.
  2. And if equal things are added to equal things then the wholes are equal.
  3. And if equal things are subtracted from equal things then the remainders are equal.
  4. And things coinciding with one another are equal to one another.
  5. And the whole [is] greater than the part.

On one hand, such notions are considered “common”, so that they are trivial enough that everyone ought to agree with them; on the other, they are not so trivial that one can avoid writing them down. Moreover, Euclid feels the need to pin-point the effect that equality must have on operations involving such objects: the underlying principle here is that two entities that are equal should share the same properties and behaviours.

What mathematicians really use is a bit stronger than that…1

The opposite formulation of such principle is sometimes called Leibniz’s law or identity of indiscernibles, and states that any two objects that share the same properties must be equal, or, in the notation of symbolic logic, F(FxFy)x=y. \forall\;F\,(Fx \leftrightarrow Fy) \;\to\; x=y \,. Of course the assumption of such principle, or even those deemed “common” by Euclid, is entirely debatable. In fact, these represent just a glimpse into the non-triviality of the treatment of equality and identity in mathematics.

The aim of this post is to compile a (non-exhaustive) survey on the different approaches that mathematicians have applied to the problem of identity throughout the centuries. Our goal is presenting some ideas - old and new - in order to better understand identity types.


First order logic and lattice-valued models

Even in a field as well established as first-order logic there is no precise convention as to whether equality should be considered as a primitive symbol satisfying certain axioms, or if it should be a treated as a non-logical symbol and introduced as a binary predicate. Still, in both versions equality is intended to be:

  1. binary, so that it pertains pairs of terms;
  2. reflexive, so that for each term tt one has t=t t=t ;
  3. substitutional (w.r.t. both to formulas and function symbols), so that it satisfies Leibniz’s law.

Substitutionality implies, amongst others, symmetry and transitivity of “=”.

For the categorical logic people: equality as a left adjoint!2

Not only it is not trivial how an equality predicate should be defined, it is not trivial how it should be interpreted. It is particularly interesting to notice how the shift from a binary, {0,1}\{0,1\} interpretation, to a multi-valued approach to models of first-order theories affected our notion of equality. Following Cohen’s proof of the independence of the continuum hypothesis from ZFC, different works aimed to provide new models witnessing it. In a paper from (1967), Scott first introduces a different way of comparing elements of a set. It is no longer the case that either two elements are equal, or they are not, but they might be to some extent or with a certain probability. We here present a slightly different version involving a generic complete Boolean algebra BB, in the original work the author considers the case where B=/[P=0]B= \mathcal{F}/[P=0] with \mathcal{F} a space of events for probability measure PP. A Boolean-valued model of a theory with an equality predicate, then, matches to each formula some value bBb\in B, and in particular it must satisfy the following inequalities

||a=a|| =1 ||a=b|| =||b=a|| ||a=b||||b=c|| ||a=c|| in1||a i=b i||||R(a 1,,a n1)|| ||R(b 1,,b n1)||\begin{aligned} ||a=a|| &= 1\\ ||a=b|| &= ||b=a||\\ ||a=b|| \wedge ||b=c|| &\leq ||a=c||\\ \bigwedge_{i \leq n-1} ||a_i = b_i|| \wedge ||R(a_1,\dots,a_{n-1})|| &\leq ||R(b_1,\dots,b_{n-1})|| \end{aligned}

which encode the basic properties described above. The interested reader can find a detailed explanation in Higgs (1970).

Equality and existence: what should ||a=a||||a=a|| be?3


In type theory

In the context of type theory we have two very different kinds of identities.

  1. Judgemental, or definitional: you can think of it as an identity you can reason with. It might pertain terms or types, and it is part of the basic syntax of types. In Martin-Löf’s first work on intuitionistic type theory, we have four kinds of judgements, ΓAΓa:AΓA=BΓa=b:A. \Gamma \vdash A \qquad \Gamma\vdash a:A \qquad\Gamma\vdash A=B\qquad \Gamma\vdash a=b:A\,. The fact that equality here is a judgement, instead of a proposition (a type), is a first key difference between type theory and set theory. Traditional reflexivity, symmetry, and transitivity are encoded in the form of rules added to the system. They look precisely how you think.4 Moreover, we ask that its influence is, again, propagated throughout the computation when applied to the basic features of the theory (typing and substitution), so that we require the following additional three rules. Γa:AΓA=BΓa:BΓa=a:AΓ,x:ABΓB[a]=B[a]Γa:AΓ,x:AB=BΓB[a]=B[a] \frac{ \Gamma \vdash a:A \quad \Gamma \vdash A=B} { \Gamma \vdash a:B} \qquad \frac{ \Gamma \vdash a=a':A \quad \Gamma, x:A\vdash B} { \Gamma \vdash B[a]=B[a'\!]}\qquad \frac{ \Gamma \vdash a:A \quad \Gamma, x:A\vdash B=B'} { \Gamma \vdash B[a]=B'\![a]}

  2. Propositional, or provable: you can think of it as an identity you can reason about. It only pertains pairs of terms of a type, and each pair produces a new type, called the identity type. Intuitively its terms are meant to be interpreted as proofs or witnesses of the identity of the two terms. In fact, it is no coincidence that it was first introduced in the context of intuitionistic logic - see Martin-Löf, “An Intuitionistic Theory of Types: Predicative Part” (1975).

Now, while the first kind of equality is considered a sort of “built-in” of type theory, there are many proposals regarding the second kind. Most of the literature agrees on the what the Formation and Introduction rule should look like, ΓAΓa:AΓa:AΓId A(a,a)Γa:AΓr a:Id A(a,a) \frac{ \Gamma\vdash A \quad \Gamma \vdash a:A \quad \Gamma \vdash a':A} { \Gamma \vdash \mathsf{Id}_A(a,a')} \qquad \frac{ \Gamma \vdash a:A } { \Gamma \vdash r_a:\mathsf{Id}_A(a,a)} The first depicts what the ingredients of the identity type are, the second says that there is at least one term in Id A(a,a)\mathsf{Id}_A(a,a), so that reflexivity is always provable. Elimination (and therefore Computation), instead, is the one that can be treated the most differently. We describe a few variations below, forgoing writing a possible context Γ\Gamma across-the-board.

The J-rule

Chronologically, the first proposal is the eliminator JJ, introduced in Martin-Löf (1975). x,y:A,u:Id A(x,y)Cx:Ad:C[r x]a:Ab:Ap:Id A(a,b)J(a,b,p):C[a,b,p]\frac{ x,y:A,u:\mathsf{Id}_A(x,y) \vdash C \quad x:A\vdash d:C[r_x] \quad \vdash a:A \quad \vdash b:A \quad \vdash p: \mathsf{Id}_A(a,b) }{ \vdash J(a,b,p):C[a,b,p] } Intuitively, it is saying that Id\mathsf{Id} is defined inductively out of its behaviour at r xr_x, and, in fact, when applied at r xr_x must yield the identity: its associated Computation rule is the following. x,y:A,u:Id A(x,y)Cx:Ad:C[r x]a:AJ(a,a,r a)=d[a]:C[a,a,r a]\frac{ x,y:A,u:\mathsf{Id}_A(x,y) \vdash C \quad x:A\vdash d:C[r_x] \quad \vdash a:A }{ \vdash J(a,a,r_a)=d[a]:C[a,a,r_a] } Notice that here we first see the two different identities interacting.

The reflection rule

One might want to more tightly link the two notions of identity. For example, one could ask that two terms that are provably equal must be judgementally equal, hence that the following holds. p:Id A(a,b)a=b:A\frac{ \vdash p : \mathsf{Id}_A(a,b)} { \vdash a=b:A} This is sometimes called the Reflection rule - not to be mistaken with reflexivity of the equality predicate - and it too is a possible choice for elimination of Id\mathsf{Id}. A type theory with reflection is called extensional, while if it requires the J-rule it is said to be intensional. Intensional and extensional theories have different expressiveness, and in general are very different as computational tools: the main reason is that propositional equality is undecidable, hence the reflection rule makes provable equality undecidable, as well, while it is decidable in the intensional case. This is a good reference for comparisons.

The K-rule

One might also wonder whether two proofs of identities should be identified or not, or that given u,v:Id A(a,b)u,v : \mathsf{Id}_A(a,b) whether there should be a term in Id Id A(a,b)(u,v). \mathsf{Id}_{\mathsf{Id}_A(a,b)}(u,v). This is usually called the Uniqueness of Identity Proofs principle (UIP). In “The groupoid interpretation of type theory” Hofmann and Streicher prove that it does not in fact follow from the JJ-rule because it does not hold (for all types AA) in their proposed model - which will be discussed in the following section. In his habilitation thesis, the second author then proposes the following alternative Elimination rule, x:A,u:Id A(x,x)Cx:Ad:C[r x]a:Ap:Id A(a,a)K(a,p):C[a,p]\frac{ x:A,u:\mathsf{Id}_A(x,x) \vdash C \quad x:A\vdash d:C[r_x] \quad \vdash a:A \quad \vdash p: \mathsf{Id}_A(a,a) }{ \vdash K(a,p):C[a,p] } and shows that it is equivalent to UIP. It is closely related to using uu as pattern matching for Id\mathsf{Id}. This is currently the way Agda automatically implements identity types.


All in all, dealing with identity is hard. “It is no wonder that twenty years passed from Martin-Löf’s proposed identity type (1975) to the interpretation in the Hofmann-Streicher paper (1996).” 5

As it is the case for fuzzy interpretations of the equality predicate in first order logic, models are precious tools we can use to better undertand the syntax we might have built for very good reasons. The following sections introduce the groupoid model of Martin-Löf’s type theory with identity types.


The Groupoid Interpretation of Identity types

We work in the setting of Martin Löf’s type theory. From now on, we write the identity type Id A(x,y)Id_A(x,y) as x= Ayx=_A y. A term of the type x= Ayx=_A y for x,y:Ax,y: A is called an identification or path from xx to yy.

We can think of the identity = A=_A as an “equivalence relation.” More precisely, we have the following:

  1. Reflexivity: There is a term r x:x= Axr_x: x=_A x for all x:Ax: A.

  2. Symmetry: If p:x= Ayp:x=_A y is a path from xx to yy, we have an inverse path p 1:y= Axp^{-1}:y=_A x.

    This can be seen by defining the inverse operation inv: (x,y:A(x= Ay)(y= Ax) \mathrm{inv}: \prod_{(x,y:A} (x=_A y) \to (y=_A x) where we let inv(p)=p 1\mathrm{inv}(p)=p^{-1}. By path induction (J-rule) it is suffices to construct inv(r x):x= Ax. \mathrm{inv}(r_x) : x=_A x. Define inv(r x)r x. \mathrm{inv}(r_x) \coloneqq r_x.

  3. Transitivity: We can concatenate paths p:x= Ayp:x=_A y and q:y= Azq:y=_A z to produce a new path pq:x= Azp\circ q:x=_A z.

    This can be seen by the concat operation: concat: (x,y,z:A(x= Ay)(y= Az)(x= Az). \mathrm{concat}: ∏_{(x,y,z:A} (x=_A y) \to (y=_A z) \to (x=_A z). Denote concat(p,q)=pq\mathrm{concat}(p,q) = p\circ q. Again, by path induction it suffices to construct concat(r x): (z:A(x= Az)(x= Az). \mathrm{concat}(r_x): ∏_{(z:A} (x=_A z) \to (x=_A z). Define concat(r x) zid (x= Az) \mathrm{concat}(r_x)_z \coloneqq id_{(x=_A z)}

symmetry (left) and transitivity (right)

Exercise 1: Show that concatenation is associative and satisfies pp 1=r xp\circ p^{-1} = r_x and p 1p=r yp^{-1}\circ p =r_y. In other words construct a term α pqr:(pq)r=p(qr)\alpha_{pqr}: (p\circ q)\circ r = p \circ (q\circ r) and λ x:pp 1=r x\lambda_x: p\circ p^{-1} = r_x and λ y:p 1p=r y\lambda_y: p^{-1}\circ p =r_y.

Upshot:{\color{#008B00} Upshot:} We can interpret types as groupoids!

A groupoid is category in which every morphism is invertible. In other words, every arrow in a groupoid can be inverted. The objects of the category are terms of a type AA and the morphisms between two terms x,y:Ax,y :A are paths between xx and yy. Every morphism is invertible because of the existence of inverse paths. An explicit construction of this can be seen in this paper.


Towards an \infty- groupoid structure of type theory

The first thing to observe is that x= Ayx=_A y is also a type and so it can be recognised as a groupoid. The morphisms in this groupoid are paths p:α= x= Ayβp: \alpha =_{x=_A y} \beta. There is no reason to stop here as we can also model the type α= x= Ayβ\alpha =_{x=_A y} \beta as a groupoid. The arrows in this groupoid are now the higher dimensional paths η:p= α= x= Ayβq \eta: p =_{\alpha =_{x=_A y} \beta} q. We can continue this process “up to infinity.”
As a result of the iterated application of J-rule, these “higher” types satisfy some nice coherence properties. These coherence properties allow us to the package this into an infinity groupoid.

An infinity groupoid can be thought of as a family of sets G nG_n for n=0,1,2,...n=0,1,2,... with additional structure: compositions, identity morphisms and inverse elements that satisfy unit, inverse and associativity laws “up to the next level.” Here is what “up to the next level” means in context of composition and associativity:

To summarise, G 0G_0 is the set of points, G 1G_1 is the set of 1-dimensional arrows between the points, G 2G_2 is the set of 2-dimensional arrows (or the 2-cells) from any parallel pair of 1-dimensional arrows and so on.

Infinity groupoids

Types can be packaged as infinity groupoids in the following sense:

Infinity groupoid model for types.

The iterated application of J-rule for identity types gives us the coherence relations for free.
For example, in Exercise 1 we constructed a proof of associativity α pqr:(pq)r=p(qr). \alpha_{pqr}: (p\circ q)\circ r = p \circ (q\circ r). Here α pqr\alpha_{pqr} is a 2-cell and can be seen as term of G 2G_2. Similarly λ x\lambda_x and λ y\lambda_y are also 2-cells.

There are other models of type theory.6 Voevodsky observed that the groupoid and simplicial models of type theory satisfies a key property- called univalence. Univalence makes the relation between homotopy theory and type theory very clear. This is an extremely humble introduction to univalence, the true genuis of univalence can be seen here.


Univalence

In traditional set theory, any proof of x=yx=y should be equal. Following an example from Grayson, in classical set theory the following sentence is false. ={x|x0}. \mathbb{N} = \{x\in \mathbb{Z}| x \ge 0\}. This is because, if \mathbb{Z} is defined as a certain quotient of ×\mathbb{N}\times \mathbb{N}, their elements are different. If you’d ask any mathematician, though, they would say that there is really no problem in treating them as if they were the same, and in fact there is an isomorphism - actually more than one. Univalence is meant to implement this “as if” into a formal system. Before we state the axiom, we give a few definitions:

Let ff and gg be two functions. A homotopy from ff to gg is a function of type fg x:A(f(x)=g(x)). f\sim g \coloneqq \prod_{x:A}(f(x)=g(x)).

A type AA is contractible when there is a point in (x:A) (y:A)x= Ay\sum_{(x:A)} \prod_{(y:A)} x=_A y. This means that there is some x:Ax:A such that x=yx=y for every y:Ay:A.7

The fiber of a function f:ABf:A\to B over a point y:By:B is fib y(f) x:A(f(x)=y). \mathrm{fib}_y(f) \coloneqq \prod_{x:A} (f(x)=y).

The function f:ABf:A \to B is an equivalence of types if the fiber of ff is contractible over all points y:By:B. We say ff is a term of type ABA\cong B.

Example: A contractible type AA is equivalent to 1 (the type with one term \star). This can be seen by the equivalence f:Af:A \to 1 sending aa \mapsto \star for evry a:Aa:A .

We are now ready to define the Univalence Axiom.

Univalence Axiom (UA):{\color{#EE1289} \text{Univalence Axiom (UA):}} For any two types AA and BB, (A=B)(AB). (A = B) \cong (A\cong B).

Equivalent types maybe identified.

Here, we haven’t specified in which type ‘=’ holds. There is a notion of types of types called universes and so we say more precisely, a universe UU is univalent if (A= UB)(AB) (A =_U B) \cong (A\cong B) for all types A,B:UA,B: U.

The power of the univalence axiom will be given in the next section and for now we content the reader with an example. The UA states that at element of A=BA=B can be thought of as providing a way to identify AA with BB.

In the presence of univalence, we no longer need to abuse notation to write ={x|x0}.\mathbb{N} = \{x\in \mathbb{Z}| x \ge 0\}.


H-levels

Voevodsky observed that types can be stratified according to homotopy levels or h-levels. The h-level expresses the homotopy level of a type AA in following sense:

h-level 0:{\color{#008B00} \text{h-level 0}:} Contractible types AA

h-level n+1:{\color{#008B00} \text{h-level n+1}:} Types AA such that x= Ayx=_A y has h-level nn.

Note: In modern notation, h-level 0 is written as h-level -2 so that sets have homotopy level 0.
We now describe types of h-levels 1 and 2.
A type A is a proposition if any two terms of A are equal. In other words, isProp(A) (x,y:A)x= Ay. \mathrm{isProp}(A) \coloneqq\prod_{(x,y:A)} x=_A y. This is in accordance with our intuition that any two proofs of a proposition are equal. By definition of h-levels, the h-level of propositions is 1.

A type A is a set if for all x,y:Ax,y:A and all p,q:x=yp,q:x=y, we have p=qp=q. In other words, any two terms of a set are propositions. Formally,

isSet(A) (x,y:A) (p,q:x=y)p=q. \mathrm{isSet}(A) \coloneqq\prod_{(x,y:A)}\prod_{(p,q:x=y)} p=q.

Intuitively, we want a set to be a type that does not contain any higher homotopical information. This coincides with our intuition of sets- proofs of equality of sets are equal.

Example: \mathbb{N} is a set.
Non-Example: The type Group is not a set.

In the presence of UA, for any two groups GG and HH we have an equivalence, f:(G=H)(GH). f: (G=H) \to (G\cong H). There may be multiple isomorphisms from GG to HH and so (GH)(G\cong H) may have more than one element. So, the UA implies that (G=H)(G=H) may have more than one element which means that Group is NOT a set! But, the group isomorphisms (GH)(G\cong H) type is a set and so under UA, the type (G=H)(G=H) is a set. This gives groups a h-level of 3. More generally, groupoids have h-level 3.

As you may guess, nn-groupoids have h-level nn. We end with a schematic view of the homotopy levels of types.

H-levels of types

We have touched on different approaches and facets to identity in maths in general, and in type theory in particular. Pursuing a better understanding of it is not only the first step in the direction of a complete formalisation of mathematics, but a continuous source of inspiration.


1 … and can be made precise with the name of Equivalence Principle (EP). It intuitively states that two objects which are the same according to some notion of sameness share the same properties, if one only consider those that are relevant to that notion. A first attempt at relating this to univalence, introduced below, can be found here.

2 In “Equality in hyperdoctrines and the comprehension schema as an adjoint functor” (1970) Lawvere shows that in the language of doctrines such properties fit into the description of a left adjoint: consider a functor P:𝒞 opCatP:\mathcal{C}^{op}\to\mathbf{Cat} (in loc.cit. the author assumes 𝒞\mathcal{C} and P(C)P(C) to be cartesian closed for all CC in 𝒞\mathcal{C}). We can think of 𝒞\mathcal{C} as the category of contexts or lists of sorts, and its morphisms as terms, then PP maps to each context the Lindenbaum-Tarski algebra of well-formed formulae in such context. Such a functor (called a doctrine) is said to be elementary if the image of the (parametrized) diagonal id C×Δ A:P(C×(A×A))P(C×A) id_{C \times \Delta_A}: P(C\times (A\times A)) \to P(C\times A) has a left adjoint = A C=^C_A satisfying Frobenius reciprocity and Beck-Chevalley. The unit of such an adjoint pair, for example, describes the reflexivity of this so called “equality”.

3 Again, such interpretetation is merely a choice, for example in Identity and existence in intuitionistic logic (1979) Scott even questions the fact that ||a=a|| ||a=a|| should be the top element in the Boolean (in this case, Heyting) algebra, so that the one element should be equal to itself not with maximum “probability” or “certainty”, but only to the extent is exists in the system.

4 ΓAΓA=AΓA=BΓB=AΓA=BΓB=CΓA=C \frac{ \Gamma \vdash A} { \Gamma \vdash A=A} \qquad \frac{ \Gamma \vdash A=B} { \Gamma \vdash B=A} \qquad \frac{ \Gamma \vdash A=B \quad \Gamma\vdash B=C} { \Gamma \vdash A=C}   Γa:AΓa=a:AΓa=b:AΓb=a:AΓa=b:AΓb=c:AΓa=c:A \frac{ \Gamma \vdash a:A} { \Gamma \vdash a=a:A} \qquad \frac{ \Gamma \vdash a=b:A} { \Gamma \vdash b=a:A} \qquad \frac{ \Gamma \vdash a=b:A \quad \Gamma\vdash b=c:A} { \Gamma \vdash a=c:A}

5 This is from a very nice PhD course held by F. Dagnino and J. Emmenegger in Genova in the spring of 2022.

6 Historically, there have been many definitions of \infty-groupoids- globular sets, quasi categories (or Kan complexes) and topological categories. The model described above uses the globular sets defintion of \infty-groupoids follwowing Berg and Garner.The Grothendieck homotopy hypothesis says

“Any topological space up to homotopy is essentially the same as an ∞-groupoid”.

In the Kan complex definition of ∞-groupoids, this hypothesis is true. There is a model of type theory in Kan complexes given by Veovodsky & Streicher (2006/2009). This allows us to interpret “types as topological spaces.” This was generalised to model structures in abstract homotopy theory by Awodey and Warren in 2006.

7 Construct a type that checks if AA is contractible as follows: isContractible(A) (x:A) (y:A)x= Ay \mathrm{isContractible}(A) \coloneqq \sum_{(x:A)} \prod_{(y:A)} x=_A y

Posted at July 26, 2022 5:51 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3410

5 Comments & 0 Trackbacks

Re: Identity types in context

Elimination (and therefore Computation), instead, is the one that can be treated the most differently. We describe a few variations below, forgoing writing a possible context Γ\Gamma across-the-board.

There is also the variant of the J-rule which is only valid up to a path, rather than judgmental equality; these are frequently found in cubical type theories for path types.

Posted by: Madeleine Birchfield on July 26, 2022 6:15 PM | Permalink | Reply to this

Re: Identity types in context

Minor error here:

As you may guess, nn-groupoids have h-level nn.

It should be

As you may guess, nn-groupoids have h-level n+2n + 2.

Posted by: Madeleine Birchfield on July 26, 2022 6:21 PM | Permalink | Reply to this

Re: Identity types in context

In modern notation, h-level 0 is written as h-level -2 so that sets have homotopy level 0.

While I am all for the “modern” indexing convention (which is actually the much older one in classical homotopy theory – Voevodsky’s starting-at-0 convention, though logical in the abstract, was a break with tradition), I think it’s too confusing to use the same word “h-level” for both of them. Usually people talk about “nn-types” instead of “types of h-level nn” when using the (2)(-2)-based convention. So a set is a 0-type and has h-level 2, a proposition is a (-1)-type and has h-level 1, and so on.

Posted by: Mike Shulman on July 30, 2022 5:20 AM | Permalink | Reply to this

Re: Identity types in context

I don’t know of any recent existing sources in the HoTT literature which defines “h-level” starting from -2.

On the other hand, there is at least one fairly recent source in the HoTT literature which defines “h-level” to begin from zero: Ayberk Tosun’s thesis on formal topology in univalent foundations from 2020.

Posted by: Madeleine Birchfield on July 31, 2022 5:20 AM | Permalink | Reply to this

Re: Identity types in context

Yes, that’s exactly my point. When it starts from 2-2 (which is, in my opinion, the better convention, for strong historical and sociological reasons), we don’t use the word “h-level”, and conversely.

Posted by: Mike Shulman on August 2, 2022 5:10 AM | Permalink | Reply to this

Post a New Comment