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

Anonymous

]]>added redirects for identification type and identification types

Anonymous

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

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

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

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

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

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.

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

]]>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

$A = \lim_{n \to \infty} \sum_{i = 1}^{n} f(x_i^*) \delta x$area under the curve$y = f(x)$ on $[a, b]$ is given by

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

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

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

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

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

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

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.

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

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

]]>Urs, 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. The latter is *equivalent* to $\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 \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_{\sum_{x':X} Id_X(x,x')}((x,id_x),(x',p))$ is inhabited.

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:

Why consider a dependency on identifications in the first place and

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

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

]]>have added (here) also a box for path lifting

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

]]>But regardless, one would still say that given two sets $A$ and $B$, equality $A = 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 : \mathcal{U}_i$, where $i$ 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 $A \; \mathrm{type}_i$ rather than a hierarchy of universes $A : \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.

]]>