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.
created function extensionality
I put in a simpler Idea section.
I have tried to polish the statements about function extensuionality at intensional type theory and extensional type theory, making explicit the distinction between function extensionality that holds by identities and that which holds by equivalences.
So, this is not the only meaning of extensional/intensional as applied to type theories. Many people, especially in the HoTT community (like me), use it to refer to the behavior of identity types, not the behavior of function types. According to this usage, type theory is extensional if all identity types are (-1)-truncated, and intensional otherwise. This distinction is orthogonal to the question of function extensionality. OTOH many type theorists do seem to use the words in the way that you did. I think the former usage is more useful when talking about HoTT, but perhaps our pages should mention both usages for disambiguation.
Also, I don’t understand what you mean by the difference between function extensionality holding by identities and holding by equivalences. The function extensionality principle says that if $\forall x, f(x) = g(x)$, then $f=g$. Of course we interpret the $=$ signs by identity types; I don’t see any other option. If the theory is intensional/homotopic then we think of the identity types as path types, but the formal statement of function extensionality is the same. Can you explain further what you’re thinking of?
(There are also different “strong”, “weak”, “dependent” and “non-dependent” flavors of function extensionality, but that seems to be an orthogonal question….)
Hi Mike,
thanks for the comment.
What happend was that I saw somewhere the definition of “extensional type theory” as one which has function extensionality. Then I noticed that this is in conflict with function extensionality in HoTT and concluded that what must be meant is that in the latter case function extensionality holds by terms of “intensional identity types” (equivalences) instead of by terms of “extensional identity types”.
So thanks for the clarification. I have tried to reword the intro at extensional type theory accordingly, but please check.
I can certify that the literature on this point is not very helpful to newcomers. So it would be good if eventually the $n$Lab could improve on this situation.
One aspect that keeps bugging me: I have no idea why the English words “extensional” and “intensional” have been chosen. (This and the completely intransparent term “univalence” were quite a hinderance for me at the beginning to get a quick feel for what all the type theory speak is about. It’s a bit of a secret language at the beginning, that gives little hints to the outsider.)
The only English sense that I can make of “extensional” is as in “an argument-wise identity of functions extends to an identity of the functions themselves”. But by what you just said, this is precisely not the right interpretation. :-/
In general, “extensional” means that something is determined by its extension, which is to say how it behaves on the collection of things to which it applies. Thus the axiom of extensionality in set theory means that a set is determined by its extension — the collection of things that belong to it. Function extensionality means that a function is determined by its meaning on its extension — its values on all possible inputs (the collection of things to which it applies). Extensional identity types mean that an identity type is determined by its extension — the collection of points $x$ and $y$ such that $x=y$. They are not entirely parallel (for instance, in HoTT with function extensionality, identity types are extensional as functions $A\to A\to Type$), but there is some consistency at least. I’ve edited extensional type theory some; intensional type theory still needs some work.
I do agree that terminology in type theory is difficult for newcomers! I was in that boat not too long ago (and still am, in some respects). I explained the origin of the term “univalence” in my blog post about it, but I’ve now also added a summary thereof to univalence axiom. It’s perhaps not the most evocative word, but at least for me it doesn’t conjure up any other meanings, so I have no trouble remembering what it means.
In general, “extensional” means that something is determined by its extension,
Ah, I see. I didn’t know this use of the word “extension” at all.
I have made extension (semantics) an $n$Lab stub, for future use.
Okay, I updated intensional type theory too.
A question:
Given that it is still open whether $HoTT+UV_{strict}$ has interpretation in (suitable model categories presenting) any $\infty$-stack $\infty$-topos, and since the problematic piece is just the $UV_{strict}$, how about modelling the weaker axiom of function extensionality?
Does $HoTT + FunExt$ have interpretation in (suitable model categories presenting) any $\infty$-stack $\infty$-topos?
Is this easy to see? If not, what’s a sticking point?
Yes, the constructions of Cisinski-Shulman and Gepner-Kock give right proper Cisinski model categories, and those support funext too. Categorically, funext means that dependent product along fibrations preserves acyclic fibrations, which follows in a Cisinski model category from the fact that pullback preserves monomorphisms.
Thanks!
Categorically, funext means that dependent product along fibrations preserves acyclic fibrations,
This I need to think about. That’s neat. We should spell this out on the $n$Lab.
Oh, sorry, now I see that this is of course in your arXiv.1203.3253, around p. 27. I’ll have a closer look…
So I have recorded this cool statement here and here.
Too bad that I had missed this all along.
There are loads of proofs that use FunExt but not full UV. Such as most of Felix Wellen’s results. Now I see that all this provably has interpretation in all the $\infty$-toposes. I could have saved myself some headaches had I appreciated this earlier.
Note, though, that the problem is not just with univalence, but with strict universe objects. The type theory used by Coq and Agda has strict universes, so formally speaking it is not known to be interpretable in an arbitrary ∞-topos, even if you don’t use univalence. Sometimes it is obvious that the universes are not really being used and essentially the same proof could be written in a type theory (with funext but) without any universes at all (which is what we can interpret in any locally cartesian closed (∞,1)-category, modulo the initiality conjecture for type theory), but other times the universe is actually playing a role even if it isn’t univalent.
but other times the universe is actually playing a role even if it isn’t univalent.
Is it hard to say this precisely?
I am thinking: the plain universe is used to get type families essentially equivalent to dependent types, and so its strictness is the strictness of the pullbacks in the model, and that is part of the coherence/rectification business which we think of as being packaged away and solved independently as we speak.
Is that it, or is there more to it?
Yes, there’s more. (Sorry, I didn’t notice this until now.) Sometimes in type theory we really do use the fact that the universe is a type, not just that maps into it have strict composition. One of the most common instances of this in when mapping into it with the eliminator of an inductive type; for a HIT this requires the universe to be univalent, but for an ordinary inductive type it doesn’t. In particular, without a universe, it’s not possible to prove in type theory that $0\neq 1$.
And any time you say in formalized type theory something like “a group is a type together with …”, formally what you are doing is making a $\sum$-type over the universe, which therefore has to be a type. And any time you prove a theorem in type theory like “for any type $A$…”, formally you are quantifying over the universe, i.e. defining an element of a $\prod$-type over the universe. Often (usually?) one can imagine circumlocutions and meta-theoretic ways of saying equivalent things without a universe, but the fact remains that an actual formalization in existing proof assistants technically uses universes all over the place.
In particular, without a universe, it’s not possible to prove in type theory that $0\neq 1$.
This seems like an odd way to put it. Assuming that by $0$ and $1$ you mean the empty and trivial types (rather than the natural numbers, which would make this an even odder thing to say), then without a universe for these types to belong to and to have its own equality types, you cannot formally state $0 \ne 1$. But to the extent that you can state it, you can prove it.
For example, Martin-Löf type theory has equality judgements between types, independently of any universes (which in some versions of his theory don't exist, at least not at all levels). So you can state $0 = 1$ (but not $0 \ne 1$) in this way, and then you can derive a contradiction from that. Therefore, $0$ does not equal $1$.
Similarly, in ZFC, you cannot state $Ord \ne Card$, because you cannot speak about the proper classes $Ord$ and $Card$, but you can prove $\neg\;(\forall x,\; O(x) \;\Leftrightarrow\; K(x))$, where $O(x)$ and $K(x)$ are translations of $x \in Ord$ and $x \in Card$ into proper ZFC. But it would be odd to explain the usefulness of GNB by saying that you cannot prove $Ord \ne Card$ in ZFC. It would be even odder to explain the usefulness of MK in this way, to the point of being downright wrong, since MK is a stronger theory whose additional strength is not necessary to prove this theorem.
Circumlocutions for the examples in #18 are also possible, and the one for
And any time you prove a theorem in type theory like “for any type $A$…”, formally you are quantifying over the universe, i.e. defining an element of a $\prod$-type over the universe.
is bog standard. You absolutely can write $A Type \vdash \cdots$ without universes. You may or may not allow introduction of type variables on the left side of a sequent, but you can allow it without promoting $Type$ to a type.
All of this is important, because it speaks to the strength of the theory. Just as $MK$ is stronger than $ZFC$ (but $NBG$ is not), so type theory with universes (even just one level) is stronger than type theory without them. But if you think that this means that type theory without universes is too weak to prove $0 \ne 1$, anything about groups, or anything about all types, then that is not so. If you just want a convenient language and don't care about proof-theoretic strength, then sure, use universes. But if you do care about strength (and lots of people do), then you shouldn't say that you need universes for something that can be said in another way without them.
By $0$ and $1$ I meant the natural numbers. It is actually true that type theory without universes cannot prove that the natural numbers 0 and 1 are unequal. I don’t know about formal “proof-theoretic strength”, but type theory without universes has posetal models in which in fact $0=1:\mathbb{N}$.
Martin-Löf type theory has equality judgements between types, independently of any universes (which in some versions of his theory don't exist, at least not at all levels). So you can state $0 = 1$ (but not $0 \ne 1$) in this way, and then you can derive a contradiction from that.
This is I guess true in some way, but it’s not formally completely analogous to $\neg\;(\forall x,\; O(x) \;\Leftrightarrow\; K(x))$, since the latter is a single theorem of ZFC, whereas a judgmental equality cannot be hypothesized inside MLTT. You can prove a meta-theorem like “in MLTT augmented with an additional rule allowing us to judge $Empty \equiv Unit$, we can derive an inhabitant of $Empty$,” but that’s not just a restatement of a theorem inside the theory that $Empty \neq Unit$. For instance, inside MLTT we can prove that $Empty$ has no elements, but it is a very different thing to say meta-theoretically that there are no terms of MLTT that can be judged to be of type $Empty$; the latter is a consistency statement about the theory that requires a substantial amount of work, whereas the former is essentially trivial by the internal definition of $Empty$ and “no elements”.
You may or may not allow introduction of type variables on the left side of a sequent, but you can allow it without promoting $Type$ to a type.
Well, to start with, even that falls substantially short of the things we can (and often do) do with a universe (even before assuming univalence). For instance, if we want to prove “if excluded middle holds, then …”, we are hypothesizing a statement of the form “for all propositions/types $A$, …”, which simply having type variables on the left of a sequent doesn’t allow. Similarly, the theory of modalities involves universal properties, which are also quantifications over all types; so any time you want to assume that something has a universal property, you are out of luck if all you can do is put type variables on the left of a sequent.
But most relevantly to the original point, the type theory that we know how to model in arbitrary ∞-toposes does not allow type variables on the left of a sequent. I’ve occasionally thought about whether we could model such a theory, but I haven’t come up with any ideas for how to do that without essentially modeling universes. So these examples are relevant to Urs’s real question of what type-theoretic arguments we know how to internalize in all ∞-toposes.
It is actually true that type theory without universes cannot prove that the natural numbers 0 and 1 are unequal.
Can you explain what you mean by ‘type theory without universes’? Since you speak of its models, you presumably have something specific in mind. (I guess that you mean a theory that can be internalized in all $\infty$-toposes.) There exist type theories without universes but with Peano (or Heyting) arithmetic, which is what your comment at first seems to deny; but if by ‘type theory without universes’ you mean a specific theory, then my remarks may be out of order.
(Ironically, it seems to have been fashionable in the middle of the 20th century for formal systems in constructive mathematics to define $\neg{P}$ as $P \Rightarrow (0 =_{\mathbb{N}} 1)$, out of a desire to avoid admitting $\bot$ to the ambient propositional calculus. Then $\neg(0 =_{\mathbb{N}} 1)$ becomes very easy to prove. But as far as I know, this was never incorporated into any type theories.)
For instance, if we want to prove “if excluded middle holds, then …”, we are hypothesizing a statement of the form “for all propositions/types $A$, …”
When I write something like that, I'm definitely thinking ‹If we allow ourselves to use excluded middle in our reasoning›, which formally is much more like adding an additional rule to the theory than making a hypothesis within the theory. Or if we think about internalizing things in [higher] categories, a statement that begins ‘if excluded middle holds’ isn't a statement that I intend to internalize; it's saying that I intend to internalize whatever follows only in categories with this additional feature. You make it sound like saying ‘if excluded middle holds’ while doing constructive math is analogous to saying ‘if the Riemann hypothesis holds’ (or perhaps, saying ‘if $\mathrm{P} = NP$’) when doing number theory; but to me it indicates that I'm not doing constructive math anymore, at least temporarily.
Yes, by “type theory without universes” I mean the type theory that we know how to model in ∞-toposes: MLTT with $\sum,\prod,+,0,1,Id,\mathbb{N}$ and function extensionality, but no universes. Any Heyting algebra also models it.
Perhaps excluded middle was a bad example to make my point. How about instead “if $f:A\to B$ is left orthogonal to all $\bigcirc$-modal types”?
Yes, that example works better.
MLTT usually has universes, so even ‘MLTT with $\sum,\prod,+,0,1,Id,\mathbb{N}$ and function extensionality, but no universes’ is a little unclear, since what you get upon removing an axiom depends on how you present it. (For instance, you might think that removing the axiom of choice from ETCS leaves you with the theory of a well-pointed Boolean topos with an NNO, but if you follow the presentation of Lawvere's original paper, then you can't even prove that you have a topos without Choice.) Since even this theory has type formation judgements, then arguably such judgements should be allowed in the elimination rules of inductive types, which allows you to prove $\neg\; 0 =_{\mathbb{N}} 1$ and the like. But then that can't be modelled in a Heyting algebra or a topos (and while I don't know $\infty$-toposes so well, I wouldn't expect them to fix this).
But if you use MLTT without universes and only allow judgements of the form $a\colon A$ (where $A$ is a type) in the elimination rules, then I agree, you cannot prove $\neg\; 0 =_{\mathbb{N}} 1$, or indeed the negation of any equality.
(Allowing type formation judgements in the elimination rules lets you define families of types and so is like the axiom of replacement in set theory. So a step up in strength, albeit less of a step up than a full-fledged universe.)
Right, assuming “large elims” as basic recovers some of the strength of a universe. However, I’ve never seen “MLTT” presented with large elims as basic, so I would never assume that they were still there upon removing the universes from MLTT. But you’re right that it’s always better to be specific.
I haven't seen that either, but I've only ever seen it presented with universes. (He did reportedly have a version with only one (predicative) universe, but I haven't seen that one.) I have seen it presented with judgemental identity in elimination rules, however, in versions where identity is intensional, and I would argue that a version without universes should include type formation judgements on the same principle.
Anyway, I know what theory you meant, and we're not disagreeing about that.
Wow, I’ve never seen judgmental equality in elimination rules. That’s also wrong homotopically.
Can you explain briefly why it's wrong homotopically?
The elimination rule for the identity type, in particular, is generally interpreted categorically by a weak factorization system such as (acyclic cofibrations, fibrations). This only works to eliminate into other fibrations, since the elimination is a lifting according to the factorization system. But judgmental equality is generally interpreted by the categorical diagonal, which is not a fibration at all. Voevodsky’s HTS has a distinction between “fibrant types” and “non-fibrant types”, with judgmental equality reified as a non-fibrant “strict equality” type, and only fibrant types can be eliminated into by the rules of other fibrant types.
Actually, wouldn’t eliminating from the identity type into judgmental equalities internally imply the reflection rule and make the type theory extensional?
Eliminating from $\Gamma \vdash p\colon eq_A(x, y)$ to $\Gamma \vdash x = y\colon A$ would make the theory extensional, but I don't think that that's supposed to happen.
The rules that should appear here (going by intuition, not memory) should be like
$\frac{\vdash z\colon A + B;\; x\colon A \vdash u =_C v;\; y\colon B \vdash u =_C v} {\vdash u =_C v} .$That is, if either a term of type $A$ or a term of type $B$ is sufficient to judge $u$ qnd $v$ identical of type $C$, then a term of type $A + B$ should also be sufficient.
Actually, the full version of that rule (with all terms and types dependent on the full context) would be
$\frac{\vdash z\colon A + B;\; x\colon A \vdash s[x] =_{C[x]} t[x];\; y\colon B \vdash u[y] =_{D[y]} v[y]} {\vdash match (z, s, u) =_{match (z, C, D)} match (z, t, v)} .$(Incidentally, $match (z, C, D)$ is the type guaranteed by my type formation elimination rule if there is no universe to do it in.)
The abbreviated (non-dependent) version of the equality-type elimination rule would be:
$\frac{x\colon A \vdash u =_C v;\; \vdash p\colon eq_A(a,b)} {\vdash u =_C v} ,$which doesn't say anything; and here's the full (dependent) version:
$\frac{x\colon A \vdash u[x,x,refl_x] =_{C[x,x,refl_x]} v[x,x,refl_x];\; \vdash p\colon eq_A(a,b)} {\vdash u[a,b,p] =_{C[a,b,p]} v[a,b,p]} .$OK, I agree that this is a problem; if $C[x,y,q] \coloneqq A$, $u[x,y,q] \coloneqq x$, and $v[x,y,q] \coloneqq y$, then from $p\colon eq_A(a,b)$, this proves $a =_A b$.
The best thing that I can say now, without remembering where I saw this done, is that you just shouldn't include this rule; leave out the elimination rule for identity judgements from equality types.
For consistency, one ought then to leave out the elimination rule for identity judgments from any type, no?
Maybe. Although equality types are different from other inductive types (or at least the other common ones), so there is a general rule that could be applied here. I'm not sure what the philosophy was behind the system where I saw this.
I can tell you something of the system that I was going to put on my personal web, but never did (since I decided that HoTT was a better approach to foundations). Here, I not only rejected universes (which was just to keep things simple, and in fact I also considered how to add them as an optional feature) but also rejected equality types (which was the main point). So I needed my elimination rules to produce both type formation judgements and identity judgements (actually I ended up using non-symmetric convertibility judgements). And since I didn't have equality types (in general, I allowed only restricted inductive families in the sense of this paper by Dybjer & Setzer, although that is not where I learnt about them), this did not cause any problems.
Thanks for all the reactions to #9! (Belated thanks, sorry.)
I see. So I am back to being frustrated then. :-)
What happend to the claim that if one looks closely enough at the code, then the universes in Coq actually are weak Tarskian?
I believe Peter Lumsdaine told me about this. This was at the beginning of last year, during the HoTT meeting in Bonn. Do you know what this is referring to?
No, I never understood what Peter meant by that. I’ve never looked at the source code of Coq, but to a user the universes certainly seem Russellian.
No, I never understood what Peter meant by that.
All right, I’ll try to ask Peter then.
I’ve never looked at the source code of Coq, but to a user the universes certainly seem Russellian.
If the claim is that down at the level of the kernel of Coq the universe is weak Tarskian, but then by some interfacing it is made to look strict Russelian to the user, this might just be the syntactic version of the sought-after claim (that all $\infty$-toposes have a presentation in which the object classifier interprets a strict Russelian universe).
I’ll check with Peter.
Here’s Peter Lumsdaine’s observation, with my addition for Sigma.
At first this seems to contradict Coq’s rules for subtyping. The point is that Coq lacks universe polymorphism for inductives. Amin Timani is working to fix this.
(Sorry, I cannot get the layout to work exactly as I want.)
Set Universe Polymorphism. Set Printing Universes. Set Printing All.
Section Cml_List_commute.
Section list. Universe i. Inductive myList (A : Type@{i}) : Type@{i} := | myNil : myList A | myCons (a:A) (l : myList A). End list.
Universes u0 v0.
Hypothesis A : (Type@{u0} : Type@{v0}). (* This adds the constraint [ u0 < v0 ], so Coq cannot later silently add the constraint [ u0 = v0 ]. *)
Lemma myList_commute_up (x : myList@{u0} A) : myList@{v0} A. Proof. try exact x. (* FAILS! *) induction x as [ | a l IH]. apply myNil. apply myCons; auto. Defined.
(* So Coq does not seem to validate ( cml_u^v list_{u} A ) = list_{v} (cml_u^v A) *)
End Cml_List_commute.
(* For Sigma *)
Section Cml_Sig_commute.
Universes u0 v0.
Hypothesis A : (Type@{u0} : Type@{v0}). Variable P: forall _ : A, Type@{u0}. (* This adds the constraint [ u0 < v0 ], so Coq cannot later silently add the constraint [ u0 = v0 ]. *)
Lemma mysig_commute_up (x : mysig@{u0} A P) : mysig@{v0} A P. Proof. try exact x. (* FAILS! *) induction x as [a p]. exact (myexist A P a p). Defined.
(* So Coq does not seem to commute commutativity with Sigma either. *)
Okay, so when you construct an inductive type, it matters which universe you do it in. That’s certainly something that’s true about weak Tarski universes and not true about strong Tarski universes as usually defined. However, Coq’s universes do have many other properties that are true about strong Tarski universes and not true about weak Tarski universes, such as:
Oh, I see. I thought something stronger was meant.
1 to 38 of 38