functions in universes

[DanGrayson]

I'm tempted to delete this sentence of Thorsten's:

Note that the universes $\UU,\UU'$ may be different, i.e.\ we can construct functions in higher or lower universes.

in the section on the recursor for Cartesian product AxB, because the recursor for making a function AxB->C seems to be more about three types A,B,C in any universe or universes, because it's types that are in universes, not functions.

[cangiuli]

It's talking about the universe in which AxB -> C lives, which depends on the universe in which C lives. I think it's worth emphasizing once that C doesn't have to live in the same universe as AxB, but maybe we can delete the part after "i.e.".

[txa]

Maybe clarifying would be better than deleting. Functions in higher universes is short for functions with types in higher or lower universes.

[andrejbauer]

I understand neither "Functions in higher universes" nor "functions with types in higher or lower universes". What is this supposed to mean?

[dlicata335]

My guess is that it means that a function type A -> B can be well-formed when A:U_i and B:U_j when i is not equal to j? In our informal a la Russell system, do we have cumulativity? If so, do we still need mixed-level functions? I.e. could we just promote the smaller of {i,j} to the bigger one?

[andrejbauer]

We explicitly state that we have commulativity. Do we explain how the universe levels work for various type formers? If not, then it seems hardly relevant to do it for one particular type former.

[txa]

We may expect that an eliminator only works within a given universe. However, this is not the case and this is quite crucial. This is a feature of our eliminators and hence it is mentioned the first time we introduce an eliminator.

[txa]

I have tried to improve the formulation. This is quite an essential feature but there aren't good examples using products. The simplest example is to prove that true != false which requires eliminating over a U_0. I mean Bool : U_0 but the function isTrue : Bool -> U_0 uses a "large elimination". Maybe we should add something in the section on Bool.

[DanGrayson]

Now the sentence reads:

"Note that the universes $\UU,\UU'$ may be different, i.e. given a product in a universe $\UU_i$ we may use the eliminator for a type or family in a different universe $\UU_j$. This is a property of all the eliminators we are going to introduce."

I still don't see the point. Let k = max(i,j). Then AxB and C are both in U_k. Thus if the eliminator had been phrased with reference to a single universe U_k, we would still be able to get a map AxB->C even if the types start out in different universes. Because universes are cumulative, we can always assume any finite collection of types lie in the same universe.

Let's go further:

I propose removing the sentence and altering the original statement of what the recursor does by replacing U' by U, and having just one universe, and the same for the other references to U' in the chapter.

[txa]

NO!!! Large elims are essential & they have nothing to do with cumulativity.

I think it is clearer if we look at the example isTrue : Bool -> U_0 isTrue true = Unit isTrue false = Empty we cannot construct this as a function of the form isTrue : Bool -> X where X : U_0 like Bool. We need to be able to eliminate for an X : U_1 (namely U_0) which is on a different universe as Bool itself.

[txa]

The fallacy it your reasoning is that you overlook that there may be functions which we can define explointing that C lives in a different (i.e. larger universe) then A,B.

[mikeshulman]

But cumulativity means that A and B also live in that larger universe! On Apr 26, 2013 6:56 AM, "Thorsten Altenkirch" notifications@github.com wrote:

The fallacy it your reasoning is that you overlook that there may be functions which we can define explointing that C lives in a different (i.e. larger universe) then A,B.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17075655 .

[dlicata335]

I actually share Dan G's confusion. You say that "we cannot construct this as a function of the form isTrue; Bool -> X where X : U_0 like bool." But why can't we construct it as a function "Bool -> X" where Bool : U_1 like X?

I think the issue may be one of a difference between eliminators and pattern-matching functions. In our informal description of pattern-matching, we don't say anything about the class of X for which you can define functions Bool -> X by pattern matching, and we definitely instantiate X with things that aren't in U_0. But I think this is justified by cumulativity. Essentially, I am proposing formal rules for pattern matching that say "a function Bool -> X can be defined by pattern-matching whenever the type Bool -> X is well-formed in some universe." In the case of isTrue, its type is in U_1.

With eliminators, I agree that the type of the eliminator needs to be universe polymorphic, and that cumulativity alone does not suffice: case : (i : ULevel) (X : U_i) -> X -> X -> Bool -> X

[txa]

I guess what is happening is that we are identifying Bool:U_0 and Bool:U_1. That is to construct a function out of Bool:U_0 it is sufficient to construct one out of Bool:U1. This feels wrong. Cummulativity should only work for positive occurences not for negative ones.

[DanGrayson]

The phrase "a function out of Bool:U_i" just means "a function out of Bool".

[mikeshulman]

What does positivity have to do with it? Bool:U0 and Bool:U1 are the same type, so constructing a function out of one is the same as constructing a function out of the other. On Apr 26, 2013 7:19 AM, "Thorsten Altenkirch" notifications@github.com wrote:

I guess what is happening is that we are identifying Bool:U_0 and Bool:U_1. That is to construct a function out of Bool:U_0 it is sufficient to construct one out of Bool:U1. This feels wrong. Cummulativity should only work for positive occurences not for negative ones.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17076937 .

[txa]

Ok, I was assuming that omitting explicit lifting is just syntactic sugar. This does not seem to be the case.

I mean given a type A : Ui by "explicit cumulativity" I also get Lift(A) : U(i+1). (That is how it is implemented in Agda). Also if I have a : U_i I also get lift(a) : Lift(A).

On the other hand the types A and Lift(A) are not identified. That is I cannot in general coerce an element a:Lift(A) into one of A.

However, that doesn't matter in my example isTrue, since to construct isTrue : Bool -> U_0 I can construct one isTrue' : Lift(Bool) -> U_0 and then define isTrue b = isTrue' (lift b), even in Agda.

There is only a problem in the other direction, i.e. if I want to construct a function from the lifted type by using one on the unlifted version...

It looks like we get some extra mileage from "implicit cumulativity" which means that we don't have to be universe polymorphic when eliminating. I find this actually a bit worrying...

[DanGrayson]

If Agda has explicit lifting, then presumably it also has explicit conversion from elements of universes to types, so if A:U_i, then instead of a:A one should write a:El(A), and then El(A) and El(Lift(A)) are the same type, so one could also write a:El(Lift(A)), and there's no such thing as lift(a). Or not?

On Fri, Apr 26, 2013 at 9:44 AM, Thorsten Altenkirch < notifications@github.com> wrote:

Ok, I was assuming that omitting explicit lifting is just syntactic sugar. This does not seem to be the case.

I mean given a type A : Ui by "explicit cumulativity" I also get Lift(A) : U(i+1). (That is how it is implemented in Agda). Also if I have a : U_i I also get lift(a) : Lift(A).

On the other hand the types A and Lift(A) are not identified. That is I cannot in general coerce an element a:Lift(A) into one of A.

However, that doesn't matter in my example isTrue, since to construct isTrue : Bool -> U_0 I can construct one isTrue' : Lift(Bool) -> U_0 and then define isTrue b = isTrue' (lift b), even in Agda.

There is only a problem in the other direction, i.e. if I want to construct a function from the lifted type by using one on the unlifted version...

It looks like we get some extra mileage from "implicit cumulativity" which means that we don't have to be universe polymorphic when eliminating. I find this actually a bit worrying...

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17078536 .

[RobertHarper]

i tried to raise these issues previously, but failed to make myself understood.

first, let me say that the russellian form is what we've been using informally, and i think that is the right decision. this is what we always did in nuprl, and it coheres well with the idea that we're economizing on judgments by not having "A type" and "A=B type", and not having a special notion of "large elim". so this is all good.

second, the concept of cumulativity is trickier than you might at first think, and weaker than what you might reasonably think it is without thinking too hard. it says that if M:Ui is derivable, then M:Uj is derivable for all j bigger than or equal to i. it does not say that if M : A -> Ui then M : A -> Uj for j bigger than or equal to i, nor can that be derived. the best you can do is to say that if M : A -> Ui, then \x.Mx : A -> Uj for j bigger than or equal to i. the eta expansion witnesses a use of subtyping that is not present in type theory as we've formulated (but was present in ECC). cumulativity does not say that if M : Uj -> A then M : Ui -> A for j bigger than or equal to i. but \x.Mx : Ui -> A, the eta expansion, is in fact in Ui->A by cumulativity.

third, although i do not propose this, we can "build in" the eta expansions by defining a subtyping relation A <: B generated by Ui <: Uj for j biger than or equal to i and closed under appropriate co- and contra-variance rules. this is a strictly stronger theory than one with only cumulativity. this idea was introduced in ECC, in part to avoid the evident fact (from the above remarks) that the cumulativity-only version does not preserve eta reduction. i think there are stronger arguments than this, but this was the original reason afaik.

fourth, do not build in "max(i,j)" calculations into the rules. this is excessively algorithmic. rather, just rely on available cumulativity to shift the premises upwards as necessary to make the rule apply. long experience here suggests that this is the right way to do things. i can elaborate if this is not obvious.

bob

Sent from tablet

On Apr 26, 2013, at 11:09, "Daniel R. Grayson" notifications@github.com wrote:

If Agda has explicit lifting, then presumably it also has explicit conversion from elements of universes to types, so if A:U_i, then instead of a:A one should write a:El(A), and then El(A) and El(Lift(A)) are the same type, so one could also write a:El(Lift(A)), and there's no such thing as lift(a). Or not?

On Fri, Apr 26, 2013 at 9:44 AM, Thorsten Altenkirch < notifications@github.com> wrote:

Ok, I was assuming that omitting explicit lifting is just syntactic sugar. This does not seem to be the case.

I mean given a type A : Ui by "explicit cumulativity" I also get Lift(A) : U(i+1). (That is how it is implemented in Agda). Also if I have a : U_i I also get lift(a) : Lift(A).

On the other hand the types A and Lift(A) are not identified. That is I cannot in general coerce an element a:Lift(A) into one of A.

However, that doesn't matter in my example isTrue, since to construct isTrue : Bool -> U_0 I can construct one isTrue' : Lift(Bool) -> U_0 and then define isTrue b = isTrue' (lift b), even in Agda.

There is only a problem in the other direction, i.e. if I want to construct a function from the lifted type by using one on the unlifted version...

It looks like we get some extra mileage from "implicit cumulativity" which means that we don't have to be universe polymorphic when eliminating. I find this actually a bit worrying...

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17078536 .

— Reply to this email directly or view it on GitHub.

[dlicata335]

@DanGrayson no, Agda is not like Vladimir's design. In Agda, there are universes U_1, U_2, ... and every classifier has type U_i for some i. There is no separate notion of type. If A : Ui then you can define a type Lift(A) : U{i+1} with lift : A -> Lift(A) (you define this as a datatype or a record, with lift as a constructor).

[andrejbauer]

The question for Bob then is: how much trouble are we in? (Note that we assume judgmental eta.)

[txa]

In an attempt to summarize: In Type Theory we allow eliminators to eliminate into any universe. This is important. It seems that in the presence of cumulativity ala Russell, this flexibility isn't really necessary. Thanks to Dan G. for noticing this. This also highlights that there could be semantical issues with this form of cumulativity because semantically we understand explicit (Frege style) cumulativity and in general it is not clear how to translate one into the other (c.f. bob's post). I suggest that we keep the flexibility of the eliminators but think more about implicit vs. explicit cumulativity.

[andrejbauer]

We can think of course, but what, if anything, should be write in the book?

[DanGrayson]

What if I go ahead and rewrite it as I proposed, collapsing U and U' to U? Then you can all take a look.

On Fri, Apr 26, 2013 at 11:17 AM, Andrej Bauer notifications@github.comwrote:

We can think of course, but what, if anything, should be write in the book?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17084319 .

[DanGrayson]

A further type of simplifying change would be to replace such things as

\rec{A\times B} : \prd{C:\UU'}(A \to B \to C) \to A \times B \to C

by

\rec{A\times B,C} :(A \to B \to C) \to A \times B \to C

On Fri, Apr 26, 2013 at 11:27 AM, Daniel R. Grayson dan@math.uiuc.eduwrote:

What if I go ahead and rewrite it as I proposed, collapsing U and U' to U? Then you can all take a look.

On Fri, Apr 26, 2013 at 11:17 AM, Andrej Bauer notifications@github.comwrote:

We can think of course, but what, if anything, should be write in the book?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17084319 .

[DanGrayson]

But since we admit eta-conversion, M is judgmentally equal to \x.Mx, so by conversion, M : A->Uj can actually be derived.

On Fri, Apr 26, 2013 at 10:42 AM, Robert Harper notifications@github.comwrote:

... second, the concept of cumulativity is trickier than you might at first think, and weaker than what you might reasonably think it is without thinking too hard. it says that if M:Ui is derivable, then M:Uj is derivable for all j bigger than or equal to i. it does not say that if M : A -> Ui then M : A -> Uj for j bigger than or equal to i, nor can that be derived. the best you can do is to say that if M : A -> Ui, then \x.Mx : A -> Uj for j bigger than or equal to i.

[DanGrayson]

Oh, thanks!

On Fri, Apr 26, 2013 at 10:44 AM, Dan Licata notifications@github.comwrote:

@DanGrayson https://github.com/DanGrayson no, Agda is not like Vladimir's design. In Agda, there are universes U_1, U_2, ... and every classifier has type U_i for some i. There is no separate notion of type. If A : Ui then you can define a type Lift(A) : U{i+1} with lift : A -> Lift(A) (you define this as a datatype or a record, with lift as a constructor).

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17082312 .

[RobertHarper]

Not in this sense: it is not permissible to type M by typing \lambda x.Mx instead. This is what sub typing adds to type theory as we've formulated it.

(sent from handheld)

On Apr 26, 2013, at 12:35, "Daniel R. Grayson" notifications@github.com wrote:

But since we admit eta-conversion, M is judgmentally equal to \x.Mx, so by conversion, M : A->Uj can actually be derived.

On Fri, Apr 26, 2013 at 10:42 AM, Robert Harper notifications@github.comwrote:

... second, the concept of cumulativity is trickier than you might at first think, and weaker than what you might reasonably think it is without thinking too hard. it says that if M:Ui is derivable, then M:Uj is derivable for all j bigger than or equal to i. it does not say that if M : A -> Ui then M : A -> Uj for j bigger than or equal to i, nor can that be derived. the best you can do is to say that if M : A -> Ui, then \x.Mx : A -> Uj for j bigger than or equal to i.

— Reply to this email directly or view it on GitHub.

[DanGrayson]

Oh, I see, thank you.

On Fri, Apr 26, 2013 at 11:39 AM, Robert Harper notifications@github.comwrote:

Not in this sense: it is not permissible to type M by typing \lambda x.Mx instead. This is what sub typing adds to type theory as we've formulated it.

(sent from handheld)

On Apr 26, 2013, at 12:35, "Daniel R. Grayson" notifications@github.com wrote:

But since we admit eta-conversion, M is judgmentally equal to \x.Mx, so by conversion, M : A->Uj can actually be derived.

On Fri, Apr 26, 2013 at 10:42 AM, Robert Harper < notifications@github.com>wrote:

... second, the concept of cumulativity is trickier than you might at first think, and weaker than what you might reasonably think it is without thinking too hard. it says that if M:Ui is derivable, then M:Uj is derivable for all j bigger than or equal to i. it does not say that if M : A -> Ui then M : A -> Uj for j bigger than or equal to i, nor can that be derived. the best you can do is to say that if M : A -> Ui, then \x.Mx : A -> Uj for j bigger than or equal to i.

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17085550 .

[mikeshulman]

Bob, when you say that type theory with a subtyping relation generated by cumulativity is "strictly stronger" than one without, what exactly does that mean? Is it stronger proof-theoretically, or just allows more typing judgments? Offhand, it seems to me like this is something we would want -- a mathematician is going to be surprised if every element of Ui is also an element of Uj, but not every function into Ui is also a function into Uj. It seems to me that it would also be validated by almost any model construction (e.g. simplicial sets) that can be tweaked to validate cumulativity.

[DanGrayson]

Bob's remark implies that there is a problem with my proposal to replace every U' in chapter 1 by U, because sometimes U' is there because it's the target of a dependent type. For example, in the section on dependent pair types, we start with

A : U

B : A -> U

C : Sigma_x:A B(x) -> U'

If we want to phrase it in terms of one universe, then there is a problem, because if we let U''' = max(U,U'), then we can't conclude that

B : A -> U'''

nor that

C : Sigma_x:A B(x) -> U'''

Indeed, it appears there is already a problem of not being general enough in the original text, because it's unclear how to cover the case where we start with three different universes and reduce it to two:

A : U

B : A -> U'

C : Sigma_x:A B(x) -> U''

This difficulty goes away completely in the appendix, where type families have their parameters in the context, see A.2.5. Bob's remark about eta-expansion also makes the difficulty go away, as we could imagine replacing B and C by their eta-expansions.

Even if there is a problem with replacing U' by U in chapter 1, it's just one of lack of generality, and we're talking about chapter 1, and the presentation chosen is already not as general as possible, and the problem goes away when viewed from the perspective of the formal type theory in the appendix. --- So, it still seems best to replace U' by U in chapter 1, since it's good to reveal only those technical difficulties that represent something really real.

On Fri, Apr 26, 2013 at 11:39 AM, Robert Harper notifications@github.comwrote:

Not in this sense: it is not permissible to type M by typing \lambda x.Mx instead. This is what sub typing adds to type theory as we've formulated it.

(sent from handheld)

On Apr 26, 2013, at 12:35, "Daniel R. Grayson" notifications@github.com wrote:

But since we admit eta-conversion, M is judgmentally equal to \x.Mx, so by conversion, M : A->Uj can actually be derived.

On Fri, Apr 26, 2013 at 10:42 AM, Robert Harper < notifications@github.com>wrote:

... second, the concept of cumulativity is trickier than you might at first think, and weaker than what you might reasonably think it is without thinking too hard. it says that if M:Ui is derivable, then M:Uj is derivable for all j bigger than or equal to i. it does not say that if M : A -> Ui then M : A -> Uj for j bigger than or equal to i, nor can that be derived. the best you can do is to say that if M : A -> Ui, then \x.Mx : A -> Uj for j bigger than or equal to i.

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17085550 .

[RobertHarper]

hi mike,

there are two formulations of "cumulativity" in type theory that i know about. the first is simply to stipulate a rule that if M : Ui and M : Uj for larger j. this is the most common meaning of a "cumulative hierarchy of universes" in my experience. the second way is to start with this, but to also add subtyping defined by these two principles:

if M : A and A <: B, then M : B   [subsumption]
A <: B if x:A |- eta_B(x) : B         [structural subtyping]

where eta_B(M) is the eta expansion of M at type B. adding these rules strengthens the theory relative to the first formulation because, for example, if x : A -> U1 is a variable, the x : A -> U2 is derivable because A -> U1 <: A -> U2 by the structural subtyping principal and subsumption. similarly, if x : U2 -> A, then x : U1 -> A for similar reasons.

however, i would add that it's not all a matter of eta-expanstion for function types, but also for products and other types as well. for example, to ensure that AxB <: A'xB', when A <: A' and B <: B', we need to define the eta expansion of terms of product type so that M expands to , and so on for all other types.

adding such subtyping principles allows us to type more terms, and is arguably more natural in some respects, but it greatly complicates the proof theory. unicity of types is lost, type checking algorithms now have to account for subtyping, you have to prove decidability of subtyping, and so forth. it's quite a mess, really, which is why, i think, few people have taken it up seriously. i don't think coq or agda supports it, to my knowledge.

a deficiency of "plain cumulativity" (without subtyping) is that subject reduction fails for eta reduction, for exactly the reasons that motivate the passage to subtyping: you may have \x.Mx : A, but not M : A for certain choices of A. i mentioned this a few weeks ago, but it was dismissed as irrelevant for our purposes. but i should have stressed that this is not the only issue involving eta, it interacts with cumulativity and, more generally, structural subtyping.

bob

On Apr 26, 2013, at 2:22 PM, Mike Shulman wrote:

Bob, when you say that type theory with a subtyping relation generated by cumulativity is "strictly stronger" than one without, what exactly does that mean? Is it stronger proof-theoretically, or just allows more typing judgments? Offhand, it seems to me like this is something we would want -- a mathematician is going to be surprised if every element of Ui is also an element of Uj, but not every function into Ui is also a function into Uj. It seems to me that it would also be validated by almost any model construction (e.g. simplicial sets) that can be tweaked to validate cumulativity.

— Reply to this email directly or view it on GitHub.

[mikeshulman]

Okay, so it sounds like "stronger" just means "can type more terms"; that's all I was asking.

What would we think about quietly using cumulativity with subtyping in the informal text, but mentioning in the Notes and in Appendix A that it is formally problematic, so that when formalizing things we usually do it differently?

[awodey]

what would be the difference between informal cumulativity with or without subtyping?

On Apr 26, 2013, at 9:37 PM, Mike Shulman notifications@github.com wrote:

Okay, so it sounds like "stronger" just means "can type more terms"; that's all I was asking.

What would we think about quietly using cumulativity with subtyping in the informal text, but mentioning in the Notes and in Appendix A that it is formally problematic, so that when formalizing things we usually do it differently?

— Reply to this email directly or view it on GitHub.

[mikeshulman]

If I understand correctly, if we did it without subtyping, then a type family B : A -> U could not also be regarded as a family A -> U' for some larger universe, without inserting an eta-expansion.

[DanGrayson]

Typical ambiguity also resolves the original issue nicely, so I've checked in a change that replaces U' by U and removes the original sentence, for your perusal, in 25eeefafc1b38bc639415adf0a9df712dade8c42

On Fri, Apr 26, 2013 at 4:13 PM, Mike Shulman notifications@github.comwrote:

If I understand correctly, if we did it without subtyping, then a type family B : A -> U could not also be regarded as a family A -> U' for some larger universe, without inserting an eta-expansion.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17100319 .

[RobertHarper]

yes, but we were previously forbidden from using the terms "typical ambiguity" and "universe polymorphism".

On Apr 26, 2013, at 5:20 PM, Daniel R. Grayson wrote:

Typical ambiguity also resolves the original issue nicely, so I've checked in a change that replaces U' by U and removes the original sentence, for your perusal, in 25eeefafc1b38bc639415adf0a9df712dade8c42

On Fri, Apr 26, 2013 at 4:13 PM, Mike Shulman notifications@github.comwrote:

If I understand correctly, if we did it without subtyping, then a type family B : A -> U could not also be regarded as a family A -> U' for some larger universe, without inserting an eta-expansion.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17100319 .

— Reply to this email directly or view it on GitHub.

[RobertHarper]

not in general, eg if the type family were a variable.

bob

On Apr 26, 2013, at 5:13 PM, Mike Shulman wrote:

If I understand correctly, if we did it without subtyping, then a type family B : A -> U could not also be regarded as a family A -> U' for some larger universe, without inserting an eta-expansion.

— Reply to this email directly or view it on GitHub.

[awodey]

On Apr 26, 2013, at 11:28 PM, Robert Harper notifications@github.com wrote:

yes, but we were previously forbidden from using the terms "typical ambiguity" and "universe polymorphism".

what was forbidden was using both at the same time without explanation.

On Apr 26, 2013, at 5:20 PM, Daniel R. Grayson wrote:

Typical ambiguity also resolves the original issue nicely, so I've checked in a change that replaces U' by U and removes the original sentence, for your perusal, in 25eeefafc1b38bc639415adf0a9df712dade8c42

On Fri, Apr 26, 2013 at 4:13 PM, Mike Shulman notifications@github.comwrote:

If I understand correctly, if we did it without subtyping, then a type family B : A -> U could not also be regarded as a family A -> U' for some larger universe, without inserting an eta-expansion.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17100319 .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub.

[DanGrayson]

I didn't even use either of the terms: any use of "U" is typically ambiguous, so simply changing U' to U restores ambiguity.

On Fri, Apr 26, 2013 at 4:28 PM, Robert Harper notifications@github.comwrote:

yes, but we were previously forbidden from using the terms "typical ambiguity" and "universe polymorphism".

On Apr 26, 2013, at 5:20 PM, Daniel R. Grayson wrote:

Typical ambiguity also resolves the original issue nicely, so I've checked in a change that replaces U' by U and removes the original sentence, for your perusal, in 25eeefafc1b38bc639415adf0a9df712dade8c42

On Fri, Apr 26, 2013 at 4:13 PM, Mike Shulman notifications@github.comwrote:

If I understand correctly, if we did it without subtyping, then a type family B : A -> U could not also be regarded as a family A -> U' for some larger universe, without inserting an eta-expansion.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/174#issuecomment-17100319> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/174#issuecomment-17100932 .

[mikeshulman]

I added some discussion of this issue and the choices we could make. Feel free to reopen if you are unhappy.

[dlicata335]

looks good