Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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.
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.
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.
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)$.
I would even argue that defining terms and types using the identity type is more in line with how mathematicians define terms and types elsewhere in mathematics. For example, in the Openstax Calculus Volume 2 textbook by Strang, Herman, et al, they give the definition of the area of the curve under a function $f$ on page 17 as
Let $f(x)$ be a continuous, nonnegative function on an interval $[a, b]$, and let $\sum_{i = 1}^{n} f(x_i^*) \delta x$ be a Riemann sum for $f(x)$. Then the area under the curve $y = f(x)$ on $[a, b]$ is given by
$A = \lim_{n \to \infty} \sum_{i = 1}^{n} f(x_i^*) \delta x$
The authors used propositional equality rather than the assignment operator or definitional equality.
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.
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.
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.)
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.
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’)?
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.
There should be a common philosophical core behind Martin-Löf-ian and inferentialist justification strategies.
I think it would be useful to add the other version of the elimination and computation rules for identity types, known as based path induction in the HoTT book. Using the existing notation on the page:
$\frac{\Gamma, x:A, y:A, p:\mathrm{Id}_A(x, y), \Delta(x, y, p) \vdash C(x, y, p):\mathrm{Type}}{\Gamma, x:A, t:C(x, x, r(x)), y:A, p:\mathrm{Id}_A(x, y), \Delta(x, t, y, p) \vdash J(x, t, y, p):C(x, y, p)}$and
$\frac{\Gamma, x:A, y:A, p:\mathrm{Id}_A(x, y), \Delta(x, y, p) \vdash C(x, y, p):\mathrm{Type}}{\Gamma, x:A, t:C(x, x, r(x)), \Delta(x, t) \vdash J(x, t, x, r(x)) \equiv t:C(x, x, r(x))}$ $\frac{\Gamma, x:A, y:A, p:\mathrm{Id}_A(x, y), \Delta(x, y, p) \vdash C(x, y, p):\mathrm{Type}}{\Gamma, x:A, t:C(x, x, r(x)), \Delta(x, t) \vdash \beta(x, t):\mathrm{Id}_{C(x, x, r(x))} (J(x, t, x, r(x)), t)}$I have added inference rules for based path induction to the article, section headers for path induction and based path induction, and a explanation to what the inference rules for based path induction mean, in contrast to that of the usual path induction. I have also added the reference to section 1.12 of the HoTT book which explains path induction and based path induction, as well as a reference to section 5.1 of Rijke’s Introduction to Homotopy Type Theory which explains a similar distinction.
There are duplicated sentences between the two sections which I have left in the article for the time being, but which may not be necessary.