Contractible sums

[Martin Escardo]

It seems to be sort of folklore that "the right way" to say "there is
a unique x : X such that A x" is

IsContr(Σ(x : X). A x).

(For example in one of the possible definitions of equivalence.)

We know, and we exploit repeatedly, that for any X : U and x0 : X, if
we define A : X → U by

A x = (x0 = x),

then

IsContr(Σ(x : X). A x).

("There is a unique x : X such that x0 = x", logically speaking, or the
paths from x0 form a contractible space, homotopically speaking.)

If I didn't make any mistake in my (trivial) calculations (perhaps I
should have tried out my calculations in Agda, but I confess laziness
here), then the converse is true:

If we are given X : U and A : X → U such that

IsContr(Σ(x : X). A x),

then we must have

A x = (x0 = x)

for a suitable x0 : X.

I presume that this, if really correct (as I think it is), must be
well known among some of you here.

But, of course, it may be that in some practical situations one comes
up with A first only to find later, to one's joy for the application
at hand, that it must be of the form x ↦ (x0 = x). Have you come
across such a practical situation in an interesting theorem?

In any case, the trivial observation here is that the only way for the
sum Σ(x : X). A x to be contractible is that A x = (x0 = x) for a
suitable x0, which I would expect to be well known, implicitly or
explicitly.

M.

[Michael Shulman]

On Fri, Aug 1, 2014 at 1:31 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> If we are given X : U and A : X → U such that
>
> IsContr(Σ(x : X). A x),
>
> then we must have
>
> A x = (x0 = x)
>
> for a suitable x0 : X.

Yes, this is essentially Theorem 5.8.2 in the book, although it's not
observed there that (iv) already implies the existence of (in the
notation there) a0 and r0.

> But, of course, it may be that in some practical situations one comes
> up with A first only to find later, to one's joy for the application
> at hand, that it must be of the form x ↦ (x0 = x). Have you come
> across such a practical situation in an interesting theorem?

Well, this is basically how the homotopy-theoretic proof of Ω(S¹)=Z
works (section 8.1.5).

Mike

[Martin Escardo]

Thanks, Mike:

On 01/08/14 21:40, Michael Shulman wrote:
> On Fri, Aug 1, 2014 at 1:31 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> If we are given X : U and A : X → U such that
>>
>> IsContr(Σ(x : X). A x),
>>
>> then we must have
>>
>> A x = (x0 = x)
>>
>> for a suitable x0 : X.
>
> Yes, this is essentially Theorem 5.8.2 in the book, although it's not
> observed there that (iv) already implies the existence of (in the
> notation there) a0 and r0.

Right. Theorem 5.8.2, before formulating the equivalence between
(i)-(iv), starts by assuming that we already have (in the notation of
this message) x0 : X and a0 : A x0. Apart from that, the above
observation is (essentially) the equivalence between (iii) and (iv).

Now switching back to the notation of the theorem of the book, it is a
bit strange to start with a pointed (R,r0) when a0:A or r0: R(a0) are
not mentioned in one of the equivalent conditions, namely (iv). (By
the way, the theorem assumes a type A as the domain of R which becomes
clear only when one reads conditions (iii) or (iv). This should be
made explicit.)

Perhaps the theorem could be reformulated (with essentially the same
proof), as:

The following are equivalent for any A:U and R : A -> U:

(i) R can be given the structure of an identity system at a suitable
point.

(ii) ... [similar modification] ...

(iii) R can be equipped with a0:A and r0:R(a0) such that for any point
b : A, the function transport R (-,r0) : (a0 = b) -> R(b) is an
equivalence.

(iv) The type Σ(b : A). R(b) is contractible.

Currently, the theorem first posits a0:A and r0 : R(a0) before
asserting the equivalences (i)-(iv), but, as already discussed, not
only (iv) doesn't mention them, but also has what it is necessary to
produce them for the other items to use. Hence perhaps this
alternative formulation is more precise and illuminating.

Martin

[Andrej Bauer]

On Mon, Aug 4, 2014 at 1:18 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> (iii) R can be equipped with a0:A and r0:R(a0) such that for any point
> b : A, the function transport R (-,r0) : (a0 = b) -> R(b) is an
> equivalence.

I don't like the phrasing "can be equipped with'. Does that mean
"there exist" or "there merely exist"? Presumably we'd never say
things like "can be merely equipped with". I think "there exist" is
better.

[Martin Escardo]

(Fine. I don't like "merely exists" either. But please let's not discuss
terminology. The point I am making about the theorem is not a
terminological one.)

Martin

[Michael Shulman]

I think the current statement of the theorem makes the most sense
given that three of the four equivalent conditions do require the
points a0 and r0. But we could add a remark afterwards pointing out
that (iv) doesn't.

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Martin Escardo]

As you prefer.

(Regarding typos, also a0 of the first statement (i) is not
(existentially or universally) quantified. Rather, it is part of the
global assumption, of a pointed predicate (R,r0) for all statements,
which should include a mention of A and of a0:A as part of the data.)

M.

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Martin Escardo]

On 01/08/14 21:40, Michael Shulman wrote:

> On Fri, Aug 1, 2014 at 1:31 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> If we are given X : U and A : X → U such that
>>
>> IsContr(Σ(x : X). A x),
>>
>> then we must have
>>
>> A x = (x0 = x)
>>
>> for a suitable x0 : X.
>
> Yes, this is essentially Theorem 5.8.2 in the book, although it's not
> observed there that (iv) already implies the existence of (in the
> notation there) a0 and r0.

It follows that an equivalent formulation of the univalence of U is

∏(B : U). IsContr(Σ(A : U). A ≃ B).

(Where ≃ is equivalence.)

This can be seen directly from Theorem 5.8.4[(v)⇔(iv)], and could also
have been given as a corollary. (The existing two corollaries exploit
the equivalence (i)⇔(iv).)

Martin

[Michael Shulman]

I've submitted a pull request with your suggestions about 5.8.2,
https://github.com/HoTT/book/pull/700.

On Tue, Aug 5, 2014 at 2:44 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> It follows that an equivalent formulation of the univalence of U is
>
> ∏(B : U). IsContr(Σ(A : U). A ≃ B).
>
> (Where ≃ is equivalence.)
>
> This can be seen directly from Theorem 5.8.4[(v)⇔(iv)]

Hmm, that's interesting! It seems to be right --- in particular, the
proof of 5.8.4[(v)⇔(iv)] doesn't use univalence.

Mike

[Martin Escardo]

On 06/08/14 08:04, Michael Shulman wrote:
> I've submitted a pull request with your suggestions about 5.8.2,
> https://github.com/HoTT/book/pull/700.

Thanks for doing that.

> On Tue, Aug 5, 2014 at 2:44 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> It follows that an equivalent formulation of the univalence of U is
>>
>> ∏(B : U). IsContr(Σ(A : U). A ≃ B).
>>
>> (Where ≃ is equivalence.)
>>
>> This can be seen directly from Theorem 5.8.4[(v)⇔(iv)]
>
> Hmm, that's interesting! It seems to be right --- in particular, the
> proof of 5.8.4[(v)⇔(iv)] doesn't use univalence.

Shouldn't we then add this as a corollary to Theorem 5.8.4, given that
it follows directly from it?

A couple of observations follow, which everybody can safely ignore (or
publicly disagree with if they choose to read them).

- . - . - . -

Logically, "contr X" is the assertion that X is a singleton (it has a
point such that all other points are equal to it), and the (large)
type Σ(A : U). A ≃ B is that of all (small) types equivalent to
B. Then the above formulation of univalance says that for any small
type B, the large type of types A equivalent to B is a singleton,
which is precise way of saying that equivalent types are equal.

- . - . - . -

A mathematical observation here:

Let's expand equivalence "≃" in

∏(B : U). IsContr(Σ(A : U). A ≃ B),

using Vladimir's original formulation of equivalence, writing "contr"
for "IsContr" to save horizontal space:

∏(B:U). contr(Σ(A:U). Σ(f:A → B). Π(b:B). contr(Σ(a : A). f a = b)).

Recalling the definition

contr X := Σ(a : X). Π(x : X). x = a,

we see that this formulation of univalence only mentions "=", and in
particular doesn't mention J, refl, transport, ap etc.

Hence if one ever wants a precise and economic formulation of
univalence without preliminary machinery, the above is one, which only
uses "=". (I am not sure how illuminating it will be, though, but
certainly it is economic and precise and direct.)

- . - . - . -

The point to be made (to newcomers) is that what the univalence axiom
does is to force the notion of type equality to be determined from the
notion of point equality (in a particular, different, way from that
which the extensionality axiom in set theory relates equality of sets
to equality of elements of sets).

To make this explicit, let's use the subscript 0 for point equality
and 1 for type equality. Then univalence reads:

∏(B:U). contr₁(Σ(A:U). Σ(f:A → B). Π(b:B). contr₀(Σ(a : A). f a =₀ b)).

where

contr_i X := Σ(a : X). Π(x : X). x =_i a,

This this explains (=axiomatizes) how =₁ is determined from =₀.

- . - . - . -

Without the univalence axiom, or some other axiom (perhaps
contradicting univalence (but what would such and axiom be?)), type
equality is exceedingly underspecified, to the extent that most
statements about it are undecided.

- . - . - . -

We should be able to exploit some of the above observations further.
Given that what the univalence axiom does it to determine type
equality from point equality, one should be able to get rid of type
equality, and start from type equivalence (defined from point
equality).

Then the univalance axiom is an axiom about type equivalence, not
about type equality.

This is my prefered point of view. Theorem 5.8.4 already addresses
that. Its first corollary, not formulated in the way I would have
preferred, says that the univalence axiom amounts to a certain
induction principle for type equivalence (which is itself defined in
terms of point equality).

- . - . - . -

Thus, I repeat something that I said in a previous thread (with many
agreements and disagreements by several of you): It is wrong (both
philosophically, and, more importantly, mathematically) to say that
the univalance axiom says, precisely or imprecisely, that isomorphic
types are equal.

It doesn't say anything to that extent.

It only says that the notion of type equivalence, defined from point
equality, satisfies a certain property (an induction principle). See
Theorem 5.8.4[(i)⇔(iv)].

It is almost an accident that one can define, before type equivalence,
something (the identity type for types) that looks as if it would be
"type equality" (whatever this may mean). The univalence axiom says
that that, if it is present, is actually equivalence. But we don't
need to have "equality" of types first in order to formulate the
univalence axiom. See again Theorem 5.8.4[(i)⇔(iv)] and its first
corollary.

The univalance axiom is a stipulated property of type equivalence.

True, and I am sure Mike will say this, there is no sensible notion of
equality for types other than equivalence, and I *fully* agree. But
this doesn't mean that univalence says that equality is equivalence.

The univalance axiom is a stipulated property of type equivalence, and
this is all it is, which can be formulated before we know, or even
think, what type equality may mean, let alone have it in the language.

M.

[Michael Shulman]

On Thu, Aug 7, 2014 at 3:41 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> It is almost an accident that one can define, before type equivalence,
> something (the identity type for types) that looks as if it would be
> "type equality" (whatever this may mean). The univalence axiom says
> that that, if it is present, is actually equivalence. But we don't
> need to have "equality" of types first in order to formulate the
> univalence axiom.

I think this is exactly backwards.

It's true, as you say, that it's possible to formulate in the absence
of type equality a statement which, once we have type equality, turns
out to be equivalent to univalence. However, the majority of
applications of univalence *require* type equality, and require
moreover that it is the "same sort" of equality as all other
equalities. Specifically, they involve defining type families by
recursion on higher inductive types, and the recursion principle of a
HIT requires specifying equalities in the codomain. So I think it
would be highly misleading to refer to equivalence induction
(Corollary 5.8.5) as "the univalence axiom" in the absence of type
equality, because it would have very few of the same strong
consequences.

Mike

[Vladimir Voevodsky]

I think my old text "a very short note on homotopy lambda-calculus" may have some relevance here, but I am not sure.

V.

[Dan Licata]

> Thus, I repeat something that I said in a previous thread (with many
> agreements and disagreements by several of you): It is wrong (both
> philosophically, and, more importantly, mathematically) to say that
> the univalance axiom says, precisely or imprecisely, that isomorphic
> types are equal.
>
> It doesn't say anything to that extent.
>
> It only says that the notion of type equivalence, defined from point
> equality, satisfies a certain property (an induction principle). See
> Theorem 5.8.4[(i)⇔(iv)].
>
> It is almost an accident that one can define, before type equivalence,
> something (the identity type for types) that looks as if it would be
> "type equality" (whatever this may mean). The univalence axiom says
> that that, if it is present, is actually equivalence. But we don't
> need to have "equality" of types first in order to formulate the
> univalence axiom. See again Theorem 5.8.4[(i)⇔(iv)] and its first
> corollary.
>
> The univalance axiom is a stipulated property of type equivalence.

I haven't expanded your definitions from above, but isn't the stipulated property J + it's computation rule (propositionally) plus a uniqueness principle? That's what I understood the "equivalence induction" formulation of univalence to be.

If so, I don't really see the difference between saying "univalence says that equivalence of types is (equivalent to) equality of types" and saying "univalence says that equivalence of types obeys the universal property of equality of types".

-Dan

[Peter LeFanu Lumsdaine]

> Martin Escardo wrote: 

> The univalance axiom is a stipulated property of type equivalence.

Dan Licata <d...@cs.cmu.edu> wrote:

 

If so, I don't really see the difference between saying "univalence says that equivalence of types is (equivalent to) equality of types" and saying "univalence says that equivalence of types obeys the universal property of equality of types".

I think there is a difference, along the lines Martin suggested: the “equiv-induction” form makes sense in more generality, eg in a setting where there is *no* primitive for equality on types.

(e.g. an ambient type judgement, and a universe U, with identity types only postulated for types from U, not for arbitrary types)

However, I think the equiv-induction form is a more interesting than Martin’s super-concise form (“contractibility of the cone-of-equivalences of a type”) above, essentially for the reasons Mike gave.  The super-concise form doesn’t need much to state it, but as far as I can see, it still needs the full strength of equality on types in order to have useful consequences.  Equiv-induction doesn’t even need the existence of equality on types at all, if I remember right, to develop plenty of useful consequences.

–p.

[Steve Awodey]

the rules for the identity type A^I —> A x A (i.e. path induction) can be reformulated as:

1. transport for all (unary) predicates P —> A
2. contractibility of the fibers of the projection A^I —> A

This determines A^I up to equivalence of types (over A x A).
We know that equivalence is a relation on the universe Eq —> U x U that satisfies (1).
You are pointing out that, if we add (2) as an axiom on Eq, then it acts like an A^I.
In particular, it is then equivalent to A^I over A x A.
Yes. This is essentially the same observation as the one that Eq satisfies path induction,
but with path induciton broken down into the two components above.

The observation makes it clear that the transport condition (1), i.e. invariance of all properties with respect to equivalence,
already holds in the system without univalence, and it is the condition (2) that has the force.

I seem to recall Vladimir making this point in early presentations of UA.

Steve

[Steve Awodey]

On Aug 8, 2014, at 9:56 AM, Steve Awodey <awo...@cmu.edu> wrote:

> the rules for the identity type A^I —> A x A (i.e. path induction) can be reformulated as:
>
> 1. transport for all (unary) predicates P —> A
> 2. contractibility of the fibers of the projection A^I —> A
>
> This determines A^I up to equivalence of types (over A x A).
> We know that equivalence is a relation on the universe Eq —> U x U that satisfies (1).
> You are pointing out that, if we add (2) as an axiom on Eq, then it acts like an A^I.
> In particular, it is then equivalent to A^I over A x A.
> Yes. This is essentially the same observation as the one that

UA is equivalent to saying that

[Martin Escardo]

On 08/08/14 13:27, Peter LeFanu Lumsdaine wrote:
> > Martin Escardo wrote:
>
> > The univalance axiom is a stipulated property of type equivalence.
>
>
> Dan Licata <d...@cs.cmu.edu <mailto:d...@cs.cmu.edu>> wrote:
>
> If so, I don't really see the difference between saying "univalence
> says that equivalence of types is (equivalent to) equality of types"
> and saying "univalence says that equivalence of types obeys the
> universal property of equality of types".
>
>
> I think there is a difference, along the lines Martin suggested: the
> “equiv-induction” form makes sense in more generality, eg in a setting
> where there is *no* primitive for equality on types.
>
> (e.g. an ambient type judgement, and a universe U, with identity types
> only postulated for types from U, not for arbitrary types)

This is what I have in mind indeed.

And not this:

> However, I think the equiv-induction form is a more interesting than
> Martin’s super-concise form (“contractibility of the
> cone-of-equivalences of a type”) above, essentially for the reasons Mike
> gave. The super-concise form doesn’t need much to state it, but as far
> as I can see, it still needs the full strength of equality on types in
> order to have useful consequences. Equiv-induction doesn’t even need
> the existence of equality on types at all, if I remember right, to
> develop plenty of useful consequences.

Also, what I had in mind was that if you define ID U A B and call it
equality, it doesn't mean it is equality (for some pre-existing notion
of equality). In fact, univalence says it is equivalence.

Martin

>
> –p.

>
> --
> You received this message because you are subscribed to the Google
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to HomotopyTypeThe...@googlegroups.com

> <mailto:HomotopyTypeThe...@googlegroups.com>.

> For more options, visit https://groups.google.com/d/optout.

--

Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Michael Shulman]

It seems to me that no one is paying attention to what I said:

> the majority of applications of univalence *require* type equality,
> and require moreover that it is the "same sort" of equality as all
> other equalities. Specifically, they involve defining type families
> by recursion on higher inductive types, and the recursion principle
> of a HIT requires specifying equalities in the codomain.

As far as I can tell, equiv-induction, in the absence of a notion of
type equality, does not allow you to do this. So although it may
suffice for some applications of univalence, such as proving funext,
it can't play the role of univalence in even the most basic
homotopy-theoretic results such as pi1(S1)=Z.

In particular, as I said, it's important for these applications that
the "type equality" which is identified by univalence with equivalence
IS the pre-existing notion of equality, because the pre-existing
notion of equality is what appears in the elimination rules for HITs.

Mike

[Michael Shulman]

On Fri, Aug 8, 2014 at 10:00 AM, steve awodey <steve...@icloud.com> wrote:
> But one could in principle define type equality to be equivalence.

Yes, indeed. But it wouldn't be automatically true that such a
"defined equality" actually behaves like equality, including our
ability to eliminate into it out of HITs.

[Martin Escardo]

Mike, could you please clarify what you are saying?

If we have "Id" for U that comes with Refl and J and the (postulated)
univalence axiomn UA, or if we instead have postulated J' and Refl'
for "Eq" (equivalence), how can type theory tell the difference? Both
(Id, J, Refl, UA) and (Eq, J', Refl', UA') (where UA' is the identity
function, essentially saying that equivalent types are
equivalent). What is a context detecting the difference between the
two situations?

Both are identity systems. I don't see how one could do something with
one but not the other. But I am open see that I may be falling into a
trap, which I fail to see at the moment.

If you have term using Id, J, Refl, UA, I replace it by a term using Eq,
J', Refl', UA'.

Well, there is a potential trap. J' satisfies the "its computation
rule" only propositionally (because it is postulated).

Perhaps you have in mind a situation where the computation rule for J
is crucial. (In which case, the cubical type theory by Thierry and
coauthors would presumably suffer from the same limitation.)

Is that what you have in mind? Or is there something else going on
that I didn't spot?

Martin

[Michael Shulman]

Consider the rule for S^1-recursion:

C type
base* : C
loop* : Id_C(base,base)
---------------------------
f : S^1 -> C

The premise involves Id_C. If you let C = U, then the premise
involves Id_U. It does not involve Eq_U. So if Id_U doesn't exist,
then this rule can't be applied with C = U, even if Eq satisfies the
same induction principle of its own that Id_U would.

Mike

> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to HomotopyTypeThe...@googlegroups.com.

[Dan Licata]

On an iPhone so sorry for not being more explicit, but couldn't we consider adding a "large elim" style rule for HITs that allows you to eliminate specifically into whatever notion of type Equiv is defined for, and has Equiv instead of Id?

Sometimes when people don't have a universe they will still have a large elim eg

If(e:bool,A type,B type) type

for the type judgement.

-Dan

[Michael Shulman]

Yes, we can certainly do that. But then I would argue that we've
taken the univalence axiom and decomposed it into two pieces,
equiv-induction and large-elims-for-HITs, neither of which carries the
full strength of univalence on its own.

Note that a large elim rule for HIRTs would allow *constructing* a
universe that is univalent in the usual sense. Also, large elims for
the interval implies (at least if type equality exists) that A\simeq B
is a retract of A=B; I don't know whether it actually implies full
univalence.

[Peter LeFanu Lumsdaine]

On Fri, Aug 8, 2014 at 5:27 PM, Michael Shulman <shu...@sandiego.edu> wrote:

It seems to me that no one is paying attention to what I said:

> the majority of applications of univalence *require* type equality,
> and require moreover that it is the "same sort" of equality as all
> other equalities.  Specifically, they involve defining type families
> by recursion on higher inductive types, and the recursion principle
> of a HIT requires specifying equalities in the codomain.

[…]

 

In particular, as I said, it's important for these applications that
the "type equality" which is identified by univalence with equivalence
IS the pre-existing notion of equality, because the pre-existing
notion of equality is what appears in the elimination rules for HITs.

Ah, very good point!  Sorry, yes, I had been missing this.

So if one wants to explore the route of considering univalence independent of a primitive type equality  one needs (as Dan L mentions) “large elims” for HIT’s.  This feels a bit unnatural if we’re talking about types as elements of universes — why should a HIT have a specific induction principle into the universe? — but not so unreasonable if we’re talking about types in the global, judgemental sense; then it’s inevitable that any elimination principle into these must be a rule of its own.

If we want to consider that, though, then we also need to state univalence for types in a judgemental sense, not just types as elements of a universe — so neither equiv-induction nor Martin’s contractibility statement can be used.  However, I think it’s been mentioned here before (Mike and I and others have certainly discussed it in person) that if you posit and interval type, with a large elim including a Frobenius condition, then this acts itself as a kind of “global univalence” principle.

Are these large elims enough to prove, say, pi1(S1) and so on?  I haven’t considered quite this question before…

–p.

[Martin Escardo]

I will certainly ponder about your example, which poses an interesting
question. Nothing to say about it yet.

But the fact remains, which is the main point I am trying to make,
that *if* you *do* have ID U A B in your type theory, we have no right
to claim that this is *any kind of equality* among the "existing ones"
(whatever they may be).

The meaning of ID U A B is widely open. For example, both UA and K are
consistent with it, and we know that UA and K are contradictory.

Without UA or K (or whatever you can come up with), ID U A B is almost
meaningless (in the objective sense that very little can be proved
about it -- most statements about it are undecided).

It is for this reason that I oppose to interpret the univalence axiom
are saying "isomorphic types are equal".

If you do have ID U A B, what the univalence axion does it to make its
meaning (more) precise: it says that it means equivalence (and, on the
way, it also gives a property of equivalence that it normally doesn't
have (equivalence induction)).

But this is not the only way to make the meaning of ID U A B more
precise: we could choose e.g. K (which is a choice I wouldn't
perform).

Thus, the univalance axiom (in whatever form we prefer) is *not*
saying that two independently existing notions (equality and
isorphism) are indentified.

It is doing two things:

(i) Making more precise (or more determined) what ID U A B means
(namely equivalence).

(ii) As a collateral effect, it is postulating a property of
equivalence that is not provable (the induction principle) but
consistent.

Hence, too, univalence is deciding (in its preferred way) statements
about equivalence which are undecided without it.

In particular, the induction principle for equivalence is not provable
(because K is consistent) or refutable (because UA is consistemt).

It is for this reason that I strongly oppose to explain univalence
informally as saying that "isomorphic types are equal". This is very,
very misleading, to the extent that for many people it sounds
contradictory, or bold, or surprising.

There is nothing surprising, in retrospect, about the univalence
axiom. It is just an axiom that makes the meaning of ID U A B more
determined. It is also a flag (together with K) that ID U A B cannot
mean much intrinsically (in particular, it cannot mean equality in any
of the existing senses, until further axioms are postulated).

Martin

[Michael Shulman]

On Fri, Aug 8, 2014 at 1:07 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> Without UA or K (or whatever you can come up with), ID U A B is almost
> meaningless (in the objective sense that very little can be proved
> about it -- most statements about it are undecided).

Agreed. This is why I say that whenever we say "isomorphic types are
equal" we must follow it immediately by saying that what this means is
that we expand the notion of "equality" to mean "isomorphism". But
the fact remains that ID U A B does *exist* prior to univalence, and
(by the argument I gave) this prior existence is important in order
for univalence to have its full strength, so univalence is more than
just a definition of "type equality" along with an induction principle
for equivalences.

Mike

[Steve Awodey]

I disagree with your claim that, without UA, type equality as given by the usual ("path induction") rule for Id_U is “practiaclally meaningless”.

These rules are essentially Lawvere’s rules for equality in a hyperdoctrine — with proof-relevance — and they determine a perfectly sensible notion of type equality, 

Indeed, arguably, the most natural one.  In particular, path induction says that equality is the least reflexive relation, and that every other relation respects it. 

This is a good notion of equality: it implies Leibniz’s law, and it endows each type with the structure of a (higher) groupoid.

That the identity on the universe admits further specification is no surprise: the same is true for Sigma and Pi types, which e.g. can be assumed to have further eta rules or not, function extensionality, etc.  This is just saying that the choice of identity is not entirely determined by the type, but also is sensitive to the way the type is related to other ones.

The formulation: "equivalent types are equal" is not misleading, but completely accurate, given this reasonable notion of equality.  It’s like declaring that “lower sets are open” in making a space from a poset.  What is misleading is the “absolute” conception of equality as an intrinsic feature of a type, unrelated to the rest of the system.  Once we regard equality instead from a more “relative” point of view, the idea that equivalence can play the role of equality is not so shocking.

Steve

[Steve Awodey]

On Aug 8, 2014, at 5:07 PM, Steve Awodey <awo...@cmu.edu> wrote:

I disagree with your claim that, without UA, type equality as given by the usual ("path induction") rule for Id_U is “practiaclally meaningless”.

“almost meaningless”

[Michael Shulman]

Maybe what Martin meant to say (certainly what I took him to be
saying) is "almost completely undetermined" rather than "almost
meaningless".

[Steve Awodey]

what he said was:

> Without UA or K (or whatever you can come up with), ID U A B is almost
> meaningless (in the objective sense that very little can be proved
> about it -- most statements about it are undecided).

[Martin Escardo]

On 08/08/14 22:17, Michael Shulman wrote:
> Maybe what Martin meant to say (certainly what I took him to be
> saying) is "almost completely undetermined" rather than "almost
> meaningless".

Yes, this is what I mean.

Also:

> On Fri, Aug 8, 2014 at 2:07 PM, Steve Awodey <awo...@cmu.edu> wrote:
>> I disagree with your claim that, without UA,

I didn't say without UA. I said "without UA or K (or whatever you can
come up with)".

I know of *no* interesting (=non-trivial?) theorem about ID U A B
without further axioms.

I do stand by my claim that without further axioms, ID U A B is
meaningless in the objective sense I proposed (most statements about it
are undecided (in the formal system of type theorem)).

Martin

[Steve Awodey]

On Aug 8, 2014, at 5:21 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

On 08/08/14 22:17, Michael Shulman wrote:

Maybe what Martin meant to say (certainly what I took him to be
saying) is "almost completely undetermined" rather than "almost
meaningless".

Yes, this is what I mean.

Also:

On Fri, Aug 8, 2014 at 2:07 PM, Steve Awodey <awo...@cmu.edu> wrote:

I disagree with your claim that, without UA,

I didn't say without UA. I said "without UA or K (or whatever you can come up with)".

I know of *no* interesting (=non-trivial?) theorem about ID U A B without further axioms.

it makes U into a weak nifty-groupoid.

[Martin Escardo]

On 08/08/14 22:24, Steve Awodey wrote:
> it makes U into a weak nifty-groupoid.

I think this is a nice summary.

Martin

[Martin Escardo]

Nice to see that we agree technically, even though we don't seem to
completely agree pedagogically.

For me, personally, it is important to understand that the univalence
axiom (or the K axiom for that matter), is not saying that two
existing notions of equality agree, but rather as making (more)
precise what the identity type for the universe is. It is also
important to understand that the identity type for the universe,
without further axioms, may be saying something interesting about
equality in general, but virtually nothing about it in particular.

On the positive side, it is interesting to have a minimal notion of
type equality, given by identity types (however underspecified), which
is compatible with both UA and K.

Perhaps this is what Steve had in mind: the identity type doesn't say
what equality is, but it merely constraints what it may be.

Also, I like the view that univalence is an axiom about equivalence,
which can be formulated in the absence of of identity types, pace your
objection regarding HIT's, which I still have to analyse.

Martin

[Vladimir Voevodsky]

Just a comment - in my view of things "large-elims" i.e. eliminators which are quantifier in the sense that they bind variables are a good thing.

1. This separates elimination from the universe hierarchies. In theories where types and objects of universes are not the same this is the only way to go.

2. One can have a modular description of type theory in which elimination for inductive types is separated from the dependent product. This is a good thing too.

V.








Using such elims one can

[Michael Shulman]

I agree that there are some nice things about separating large elims
from universes. However, I still maintain that large elims for HITs
should be regarded as an aspect of univalence, which merely happens to
be expressible without a universe.

In particular, HITs make perfect sense in extensional type theory, and
exist in models such as Set, but they do not have large elims there
(except perhaps into hProp). So large elims shouldn't be thought of
as an intrinsic aspect of the notion of HIT; rather, they're a
consequence (or, perhaps better, an expression) of the fact that the
ambient type theory is "univalent" in some sense.

Semantically, this is closely analogous to the fact that an
(oo,1)-topos can be defined either by the existence of "object
classifiers" or by the fact that colimits satisfy "descent". The
former is like having univalent universes; the latter is like having
large elims for HITs. Descent is likewise not intrinsic to the notion
of colimit; it expresses a stronger property of the ambient category.

[Steve Awodey]

On Aug 9, 2014, at 11:02 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> I agree that there are some nice things about separating large elims
> from universes. However, I still maintain that large elims for HITs
> should be regarded as an aspect of univalence, which merely happens to
> be expressible without a universe.
>
> In particular, HITs make perfect sense in extensional type theory, and
> exist in models such as Set, but they do not have large elims there
> (except perhaps into hProp). So large elims shouldn't be thought of
> as an intrinsic aspect of the notion of HIT; rather, they're a
> consequence (or, perhaps better, an expression) of the fact that the
> ambient type theory is "univalent" in some sense.

Mike, I think this point is indeed an important one, but one that deserves to be explained further — could you please elaborate a bit on this?

Thanks,

Steve

[Vladimir Voevodsky]

On Aug 10, 2014, at 11:02 AM, Michael Shulman <shu...@sandiego.edu> wrote:

Semantically, this is closely analogous to the fact that an
(oo,1)-topos can be defined either by the existence of "object
classifiers" or by the fact that colimits satisfy "descent".  The
former is like having univalent universes; the latter is like having
large elims for HITs.  Descent is likewise not intrinsic to the notion
of colimit; it expresses a stronger property of the ambient category.

This sounds like an interesting arguments for looking at things in both ways.

Vladimir.

[Vladimir Voevodsky]

On Aug 10, 2014, at 11:02 AM, Michael Shulman <shu...@sandiego.edu> wrote:

I agree that there are some nice things about separating large elims
from universes.  However, I still maintain that large elims for HITs
should be regarded as an aspect of univalence, which merely happens to
be expressible without a universe.

... and yes, now that you have pointed out the connection with two ways of formulating the (infty,1)-topos condition I better understand what you have been saying earlier in this discussion.

V.

[Peter LeFanu Lumsdaine]

On Sun, Aug 10, 2014 at 4:02 AM, Michael Shulman <shu...@sandiego.edu> wrote:

I agree that there are some nice things about separating large elims
from universes.  However, I still maintain that large elims for HITs
should be regarded as an aspect of univalence, which merely happens to
be expressible without a universe.

[…]

 

Semantically, this is closely analogous to the fact that an
(oo,1)-topos can be defined either by the existence of "object
classifiers" or by the fact that colimits satisfy "descent".  The
former is like having univalent universes; the latter is like having
large elims for HITs.  Descent is likewise not intrinsic to the notion
of colimit; it expresses a stronger property of the ambient category.

This made me think: are there any natural (classes of) categories that have a large class of colimits, but have descent only for some subclass of them?

E.g. (finitary) extensive categories have descent just for finite colimits — but those are the only colimits they are assumed to have.

This fact — that there don’t seem to be any definitions along the lines of eg “a(n) (∞-)category with all finite colimits, and descent for finite coproducts” — seems to support Mike’s point of view that descent is really a property of the ambient category, not of the specific colimits; correspondingly, that large elims for HIT’s should be seen as “univalence of the ambient type theory”, not as strengthenings of the specific HIT’s.

–p. 

[Michael Shulman]

On Sun, Aug 10, 2014 at 8:53 AM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> This made me think: are there any natural (classes of) categories that have
> a large class of colimits, but have descent only for some subclass of them?

Well, Grothendieck 1-toposes (like Set) have all colimits, but only
descent for some of them. One might, I suppose, argue that this is an
"accident", because one can construct all colimits out of the ones for
which they have descent.

I'm not sure there's much meaning in asking whether descent is "a
property of the particular colimits" or "a property of the ambient
category" -- I was just saying that it's not a part of the *notion* of
"colimit", but rather an extra condition on top of the existence of
colimits.

[Michael Shulman]

There are three statements under consideration:


1. Univalence, as originally stated by Vladimir: the map Id_U(A,B) ->
Equiv(A,B) is an equivalence for all A,B:U.

2. Equiv-induction: if C is a type family dependent on two types and
an equivalence between them, and we have c_A:C(A,A,id) for all A, then
we have C(A,B,e) for all (A,B,e).

3. Large elims for HITs: Given any HIT, in addition to its usual
induction principle, we have a large elim principle for defining type
families over it, obtained by replacing Ids with Equivs in the
premises. Let's give it judgmental computation rules for
point-constructors.


In the usual MLTT, where in particular the universe U has an identity
type Id_U (which is necessary to even state (1)), the three are all
equivalent.

(1)<=>(2) is Corollary 5.8.5 in the book.

(1)=>(3) is easy and we use it all the time starting in Chapter 8.

I never noticed that (3)=>(1) completely before, but it's pretty easy,
and requires only the HIT interval. Given e:Equiv(A,B), large I-elim
gives E : I -> U, whence ap_E(seg) : Id_U(A,B), and the computation
rule for large I-elim gives coe(ap_E(seg)) = e. Thus, Equiv(A,B) is a
retract of Id_U(A,B). But then Sum(B:U) Equiv(A,B) is also a retract
of Sum(B:U) Id_U(A,B), and the latter is contractible, hence so is the
former; so by Martin's observation last week, U is univalent.


However, we can also consider a weaker theory where, say, Id_U does
not exist. Unlike (1), (3) can be stated even without a universe
existing, while (2) requires only some sort of polymorphism (a
universe suffices).

I claim that without Id_U, we still have (3)=>(2), again using only
the HIT interval. Suppose C and c as in (2), and e:Equiv(A,B). Large
I-elim on e gives E : I -> U, and we also have the constant family
lam(x:I).A : I -> U. Ordinary I-induction shows Prod(x:I)
Equiv(A,E(x)), using id_A when x=zero and e when x=one. Rearranging E
and lam(x:I).A, we have I -> Sum(X:U)(Y:U) Equiv(X,Y), which composed
with C gives D : I -> U such that D(zero) = C(A,A,id_A) and D(one) =
C(A,B,e) (judgmentally). Thus, transport(D,seg,c_A) : C(A,B,e).
Showing that when e=id_A we get back c_A (propositionally) is left as
an exercise.

I also claim that (2) does *not* imply (3) without Id_U; at least, not
for all HITs. Start from ordinary type theory with univalence (1),
let U be a universe of hsets, and forget about Id_U and all other
universes. Then (2) holds because U is univalent in the original type
theory. Moreover, HITs do exist in U, obtained from HITs in the
original type theory by adding a 0-truncation constructor. This
doesn't bother elimination into other types in U, though it prevents
elimination into U (which we can't actually even ask about in the
absence of Id_U). And these HITs can't admit large elims, since
otherwise we could prove Omega(S^1)=Z as usual, whereas the "S^1" in U
is a set.

If these arguments are correct (I have not formalized them), then
while (1), (2), and (3) are equivalent in the presence of Id_U, in its
absence, (3) is strictly stronger than (2) (and (1) can't even be
stated). This suggests to me that (2) does not capture the whole
meaning of univalence, whereas (3) might. I hesitate to claim
definitely that it *does*, but it's worth noting that from HIRTs with
large elims we can *construct* a universe that is univalent (1).


What about "descent"? A colimit in a category (or (oo,1)-category) C
is said to (be universal and) satisfy descent
(http://ncatlab.org/nlab/show/van+Kampen+colimit) if it is preserved
by the contravariant functor X |-> C/X, i.e. taken to a limit. That
means if we have Y_i \in C/F(i) for all objects F(i) in the diagram,
where Y_j pulls back along F(i->j) to Y_i coherently, then colim(Y_i)
\in C/colim(F) pulls back to the Y_i. Thus objects of slice
categories "descend" along the colimit.

It turns out to be sufficient to consider X |-> Core(C/X) instead,
where Core means the maximal sub-(oo-)groupoid. In particular, *all*
colimits in C satisfy descent just when this functor is continuous.
By AFT, continuous functors are "almost the same" as representable
ones, modulo a size condition. And a representing object for (some
small version of) this functor is an (oo,1)-categorical universe (or
"object classifier"). Being more careful, we get with the Rezk-Lurie
theorem that a locally presentable (oo,1)-category has descent for all
colimits if and only if it has object classifiers -- and if and only
if it is an (oo,1)-topos.

Ordinary 1-categories basically never satisfy descent for *all*
colimits. The ones that come closest are the Grothendieck 1-toposes,
which satisfy descent for a lot of colimits like coproducts
("extensivity"), quotients of equivalence relations
("Barr-exactness"), pushouts of monomorphisms ("adhesivity"),
sequentian colimits of monomorphisms ("exhaustivity"), etc.

But general coequalizers or pushouts don't satisfy descent, even in
Set. For instance, the coequalizer of two copies of the identity map
of the terminal set 1 is again 1. But if we let each Y_i be the
integers Z, with the two maps being the identity and the successor,
then descent would imply that the coequalizer of these maps -- which
is again 1 -- pulls back along id_1 to Z, which is absurd. (This is a
category-theoretic version of the HoTT proof that Omega(S^1)=Z: the
above coequalizer is essentially the HIT S^1.)

Now univalent (1) universes are closely related to object classifiers,
while large elims for HITs (3) are closely related to colimits
satisfying descent. For a non-recursive HIT that constructs a
colimit, the premises of its large elim are exactly the Y_i and the
equivalences between their pullbacks, its conclusion is their colimit
Y (by the flattening lemma), the computation rules say that Y pulls
back to each Y_i, and so on. So (1)=>(3) is an internalization of the
fact that object classifiers imply descent, while the construction of
a univalent (1) universe from a HIRT with a large elim (3) is an
internalization of the converse.

By contrast, (2) seems to be mainly an expression of "invariance" (or,
to use the controversial terminology "non-evil"): it says that all
constructions we can perform in type theory are invariant under
equivalence. This is an important part of univalence, but it's not
all of it.

Mike

[Steve Awodey]

Thanks Mike — that’s very helpful indeed!
I think this would even make a good blog post as is.

Just one question: when we talk about preservation of (co)limits in the descent condition,
there is a shift of dimension from C to Cat (or whatever) in the domain and codomains of the functor X |-> C/X.
So e.g. in the 1-categorical case, the colimit in C goes to a *pseudo*-limit in Cat.
In the general case when C is an (oo,1)-cat, I guess the idea is that the shift falls away because the codomain of the functor C/(-) is also an (oo,1)-cat?
Or do we consider the condition as applying uniformly to (oo,1)-cats, and in the 1-cat case the domain and codomain of C/(-) just happen to be truncated at different levels?

Thanks,

Steve

[Michael Shulman]

On Tue, Aug 12, 2014 at 11:59 AM, Steve Awodey <awo...@cmu.edu> wrote:
> I think this would even make a good blog post as is.

Yeah, I considered it, but I was too lazy/busy. Maybe I'll find the time. (-:

> Just one question: when we talk about preservation of (co)limits in the descent condition,
> there is a shift of dimension from C to Cat (or whatever) in the domain and codomains of the functor X |-> C/X.
> So e.g. in the 1-categorical case, the colimit in C goes to a *pseudo*-limit in Cat.

Yeah, that's right.

> In the general case when C is an (oo,1)-cat, I guess the idea is that the shift falls away because the codomain of the functor C/(-) is also an (oo,1)-cat?
> Or do we consider the condition as applying uniformly to (oo,1)-cats, and in the 1-cat case the domain and codomain of C/(-) just happen to be truncated at different levels?

I don't think there's really much difference between those two
statements, so you can pick whichever you prefer. (-:

[Steve Awodey]

check!

[Martin Escardo]

Mike,

On 12/08/14 05:20, Michael Shulman wrote:
> There are three statements under consideration:
>
>
> 1. Univalence, as originally stated by Vladimir: the map Id_U(A,B) ->
> Equiv(A,B) is an equivalence for all A,B:U.
>
> 2. Equiv-induction: if C is a type family dependent on two types and
> an equivalence between them, and we have c_A:C(A,A,id) for all A, then
> we have C(A,B,e) for all (A,B,e).
>
> 3. Large elims for HITs: Given any HIT, in addition to its usual
> induction principle, we have a large elim principle for defining type
> families over it, obtained by replacing Ids with Equivs in the
> premises. Let's give it judgmental computation rules for
> point-constructors.

Nice. Including the fact that you made use of my observation last week
to prove this. :-)

> Now univalent (1) universes are closely related to object classifiers,
> while large elims for HITs (3) are closely related to colimits
> satisfying descent. For a non-recursive HIT that constructs a
> colimit, the premises of its large elim are exactly the Y_i and the
> equivalences between their pullbacks, its conclusion is their colimit
> Y (by the flattening lemma), the computation rules say that Y pulls
> back to each Y_i, and so on. So (1)=>(3) is an internalization of the
> fact that object classifiers imply descent, while the construction of
> a univalent (1) universe from a HIRT with a large elim (3) is an
> internalization of the converse.

Interesting.

> By contrast, (2) seems to be mainly an expression of "invariance" (or,
> to use the controversial terminology "non-evil"): it says that all
> constructions we can perform in type theory are invariant under
> equivalence. This is an important part of univalence, but it's not
> all of it.

Regarding this last remark: The invariance under equivalence is much
weaker than (2). We know that J is equivalent to transport + the
contractibility of "singletons" (the Sigma types of paths from a given
point). But invariance under equivalence is only the transport part.

Martin

[Michael Shulman]

On Aug 13, 2014 2:43 AM, "Martin Escardo" <m.es...@cs.bham.ac.uk> wrote:
> The invariance under equivalence is much
> weaker than (2). We know that J is equivalent to transport + the
> contractibility of "singletons" (the Sigma types of paths from a given
> point). But invariance under equivalence is only the transport part.

I think it depends on what you mean by "invariance". It seems to me that J is itself a stronger sort of invariance, which is entirely reasonable to ask for in the case of equivalences.

[Martin Escardo]

If J is your definition of invariance, I agree. But then your claim that
(2) is nothing but invariance is tautological, because (2) says that
equivalence satisfies the J axiom.

M.

[Michael Shulman]

On Wed, Aug 13, 2014 at 8:07 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> If J is your definition of invariance, I agree. But then your claim that (2)
> is nothing but invariance is tautological, because (2) says that equivalence
> satisfies the J axiom.

My remark (which I probably wouldn't elevate to the status of a
"claim") was that

> By contrast, (2) *seems* to be *mainly* an expression of "invariance"

(emphasis added).

I was not using any particular "definition" of "invariance", but
rather an informal meaning of the word which could refer to J. I
agree that this is rather tautological; the point is that in the
absence of Id_U, (2) doesn't seem to imply any *more* than
invariance/J, in contrast to (3) which also includes descent.

Mike

[Martin Escardo]

Mike,

I don't see any fundamental disagreement in this thread.

However, the following annoys me a little bit:

My problem is sentence "(2) doesn't seem to imply any *more* than
invariance/J".

(Emphasis *not* added.)

We have that (2) is *literally* invariance/J, as we have already
agreed.

Then, of course, (2) can't imply any more than itself.

> in contrast to (3) which also includes descent.

Regardless of whether (2) implies descent (let me believe your (very
plausible) argument, without any reservation, that it doesn't), what
is the sentence "(2) doesn't seem to imply any *more* than
invariance/J" meant to mean?

You have *not* argued that (2) doesn't imply anything interesting that
is "missing" in the absence of (2).

Martin

[Michael Shulman]

Ok, I guess you're right. I'm no longer sure what I was thinking when
I wrote that sentence, but right now I can't think of anything true
for it to mean. For instance, if I recall correctly, (2) suffices to
prove function extensionality. So I withdraw that sentence: (2) is a
statement of invariance/J, from which other useful things may follow,
but (I claim) not descent.

On Wed, Aug 13, 2014 at 12:58 PM, Martin Escardo
<m.es...@cs.bham.ac.uk> wrote:
> Mike,
>

> I don't see any fundamental disagreement in this thread.
>
> However, the following annoys me a little bit:
>
> On 13/08/14 16:17, Michael Shulman wrote:

> My problem is sentence "(2) doesn't seem to imply any *more* than
> invariance/J".
>
> (Emphasis *not* added.)
>
> We have that (2) is *literally* invariance/J, as we have already
> agreed.
>
> Then, of course, (2) can't imply any more than itself.
>

>> in contrast to (3) which also includes descent.
>

[Martin Escardo]

On 13/08/14 20:58, Martin Escardo wrote:
> You have *not* argued that (2) doesn't imply anything interesting that
> is "missing" in the absence of (2).

Therefore I shall argue myself, relying on the work of Nicolai Kraus
and Christian Sattler,

http://arxiv.org/abs/1311.4002

that (2) actually does prove something that cannot be known in the
absence of (2) (because the MLTT-consistent K axiom precludes their
conclusion).

They only use univalance on top of MLTT, and not HIT's, until section
5, after the main theorem is proved, namely Theorem 4.10.

I claim that the (2)-formulation of univalence is all they need to
prove Theorem 4.10.

Martin

[Michael Shulman]

On Wed, Aug 13, 2014 at 1:52 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> I claim that the (2)-formulation of univalence is all they need to
> prove Theorem 4.10.

Well, but they also use Id_U, in the presence of which (1), (2), and
(3) are all equivalent.

[Martin Escardo]

Of course my point is that they don't need to.

[Martin Escardo]

On 13/08/14 21:52, Michael Shulman wrote:
> Ok, I guess you're right. I'm no longer sure what I was thinking when
> I wrote that sentence, but right now I can't think of anything true
> for it to mean. For instance, if I recall correctly, (2) suffices to
> prove function extensionality. So I withdraw that sentence: (2) is a
> statement of invariance/J, from which other useful things may follow,

Ok, your example is even better than mine.

> but (I claim) not descent.

(Which I already accepted. (But it will be nice to see a more precise
formulation and proof, although I am not using this against you.))

I emphasize again:

> On Wed, Aug 13, 2014 at 12:58 PM, Martin Escardo

>> I don't see any fundamental disagreement in this thread.

In any case, I think the lessons are interesting. (At least for me.)

Martin

[Michael Shulman]

It seems to me that even asking the *question* of whether U_n is an
n-type requires Id_U. Am I confused?

[Martin Escardo]

Sorry it took so long to respond.

On 13/08/14 23:13, Michael Shulman wrote:
> It seems to me that even asking the *question* of whether U_n is an
> n-type requires Id_U. Am I confused?

I can't say conclusively, and hence I prefer to rely on your own
example that J for equivalence in U gives function extensionality for
types in U.

However, I have read their paper more carefully, and also their Agda
code. In fact, they find in more convenient to work "as much as
possible with equivalence rather than identity types Id U" in the code
(in the paper they work with identity types).

It seems (but I don't promise without further analysis) that there is
no problem in defining n-type using equivalence rather than Id U.

But there is something interesting that is potentially problematic in
my claim that what they do can be done without invoking Id U: the use
of pointed types. To define equality/equivalence of pointed types, one
needs both equality/equivalence on types, and equality on points of
types. In fact, they explicitly define their own pointed-type
equality, using equivalence of types and equality of points. It is not
clear to me whether (or not) univalence holds automatically for this
(mixed) notion of equality (or whether they need it).

Nicolai, any insight in this respect?

I would be surprised if you really do need identity types Id U, but I
am of course open to such surprises.

Martin

[Michael Shulman]

On Aug 15, 2014 10:37 AM, "Martin Escardo" <m.es...@cs.bham.ac.uk> wrote:
> It seems (but I don't promise without further analysis) that there is
> no problem in defining n-type using equivalence rather than Id U.

Well, you could define the statement "U is an n-type" using equivalence instead of Id U, but then it won't be an instance of the general notion of "n-type" any more, so you won't be proving the same theorem.

[Christian Sattler]

Just a side remark: as mentioned several times in the Agda code (esp.
Universe.Hierarchy), our reason for working explicitly with (pointed)
equivalences rather than (pointed) type equalities in the Agda code is
an ugly technicality --- the lack of universe cumulativity in Agda. We
are unable to even state the univalence axiom as an equality (without
cluttering everything with liftings and having redundant noise of how
explicit liftings interact with type formers). If Agda had universe
cumulativity, we would have used equality more liberally: lemmata like
'equiv-Π•' or 'equiv-Ω^' (expressing invariance under pointed
equivalences) would be eliminated (we do not care about computing the
equivalence here), replaced simply by instances of 'ap'.

Christian

PS: Equivalence of pointed types ("pointed type equality") and its
equivalence to equality of pointed types Martin attributes to us are
hardly our own invention, I think the HoTT Book has the exact same notions.

[Martin Escardo]

On 15/08/14 19:30, Michael Shulman wrote:
>
> On Aug 15, 2014 10:37 AM, "Martin Escardo" <m.es...@cs.bham.ac.uk

I think this sort problem already occurs in the absence of identity
types, disregarding whether we want to define the "equality" type of U
to be Martin-Loef's Id U, or the type Eq U of equivalences in U.

For example, for the natural numbers (with cumulativity (Coq) or not
(Agda)). We think that there is only *one* elimination rule for the
natural numbers (induction/recursion).

However, because we have a sequence U_i of universes indexed by *meta
language* natural numbers i (as emphasized in the HoTT book), in
reality we have countably many elimination rules for the natural
numbers, one for each universe. They all look the same, to the extent
that both Agda and Coq can fake the impression that there is only
one elimination rules. But they "are the same" only meta-linguistically.
We have an elimination *scheme* in the terminology of mathematical
logic.

Going back to equality in universes, if we *define* Id U to be Eq U,
we could also have Agda and Coq to trick the user to think that there
is a uniform definition of Id.

I think both Agda and Coq add to the confusion, in different
ways. Agda by faking a "type" of universe levels, and Coq by adopting
"typical ambiguity". Also the writing of the HoTT book may contribute
to the confusion (although it explicitly very often tries to point out
potential pitfalls).

Another source of confusion is the good thing that we have many
interesting models (satisfying univalence or not). In many such models,
e.g. the natural numbers have only one universal property. But this
doesn't show in the syntax of type theory (with univalence or not).
In the syntax, we do have countably many elimination rules.

Martin

[Martin Escardo]

(Another way to fake the uniformity is to use --type-in-type in Agda,
which ammounts to U:U, and "making sure we use it properly" (although
nobody seems to have given a definition of what this amounts to, as
far as I know, (but this should be possible.)). M.

[Dan Doel]

When working in Martin-loef type theory, there should be a single induction schema that captures all the cases. Something like:

    G, n:Nat |- T(n) type
    G |- z : T(0)
    G |- s : (n:Nat) -> (x:T(n)) -> T(suc n)

    G |- m : Nat

    ----

    G |- elim(z, s, m) : T(m)

Having to define one of these for each universe would be an artifact of using T(n) : U_i instead of a type judgment. The above is of course a schema and stands in for infinitely many instantiations, but it's at least not infinitely many schemas.

Also, in Agda, you can define a single eliminator using universe polymorphism that will cover all the natural-indexed universes.

    elim : (i : Level) -> (T : Nat -> Set i) -> T 0 -> ((n : Nat) -> (x : T n) -> T (suc n)) -> (m : Nat) -> T m

  

-- Dan

[Nicolai Kraus]

Hi Martin (and everyone),

On 15/08/14 18:37, Martin Escardo wrote:
> However, I have read their paper more carefully, and also their Agda
> code. In fact, they find in more convenient to work "as much as
> possible with equivalence rather than identity types Id U" in the code
> (in the paper they work with identity types).

As Christian said, the reason why equivalences are more convenient is
simply that Agda does not have cumulative universes. In Agda, if A and B
live in universes of different index, you can write "A ~ B" (where ~
means equivalence) but you cannot write "A == B" (where == is
propositional equality), even though both is fine in HoTT.

> It seems (but I don't promise without further analysis) that there is
> no problem in defining n-type using equivalence rather than Id U.

Ok, but not sure if you can do this in a way that you will find satisfying.

Yes, you could use that
is-n-type(U)
can, by [book, Thm 7.2.9] be written as
Pi (A:U). isContr(Omega^{n+1}(U,A))
which (for n>0) is by [lemma 4.2 in the article you mentioned] equivalent to
Pi (A:U). Pi (a:A). isContr(Omega^n(A,a)).

The last expression does not involve Id U any more (it is not quite
right for n<1, but let's forget this case).
With this translation, I guess you can prove that "Universe n is not an
n-type" in a theory without "Id U" and an alternative formulation of the
univalence axiom as discussed in this thread.

But, as Mike says, that would be another theorem.

> But there is something interesting that is potentially problematic in
> my claim that what they do can be done without invoking Id U: the use
> of pointed types. To define equality/equivalence of pointed types, one
> needs both equality/equivalence on types, and equality on points of
> types. In fact, they explicitly define their own pointed-type
> equality, using equivalence of types and equality of points. It is not
> clear to me whether (or not) univalence holds automatically for this
> (mixed) notion of equality (or whether they need it).

The type of pointed types is just "Sigma (A:U). A", so its identity
types are given by the usual principle for dependent pairs. (A,a) =
(B,b) is equivalent to Sigma (p : A=B). p_*(a) = b.
If you exchange A=B by equivalences, the transport becomes just
application. There is no "additional" version of univalence assumed in
any way.

> Nicolai, any insight in this respect?
>
> I would be surprised if you really do need identity types Id U, but I
> am of course open to such surprises.

If you mean something in the direction of what I did above, you might be
able to do it without Id U.
But it would look very different from the original formulation.

Nicolai

[Martin Escardo]

Hi Nicolai,

Thanks for the clarification.

My implicit proposal in this discussion was to define (for your
definitions and theorems, and more generally for any definition and
theorem):

Id(0) = the usual Martin-Loef type ("on points" of types X:U0).

Id(n+1) = Eq (on types, defined from Id(n) in the usual way).

Then we postulate univalence, in the form of J-induction for all
Id(n+1). (For Id(0) we don't need to, by definition of Martin-Loef
identity).

Then the *definition* of n-truncatedness is *the same*. It is just
that I changed what I mean by Id(n) for n>0.

So the theorem *is* (or should be) the same, and indeed with the same
proof. The only difference is that we adopted a different identity
system (but any two identity systems are equivalent, and the
univalence axiom is just saying that equivalence is an identity
system).

This is what I had in mind all along.

Martin

[Vladimir Voevodsky]

I probably missed something. How do you define what equivalence is without Id on types?

V.

[Vladimir Voevodsky]

Would you troubles related to cumulativity disappear if lifting "computed" i.e. if the lifting of a type constructor was definitionally equal to the type constructor of the liftings?

V.

[Christian Sattler]

Certainly, yes.

[Michael Shulman]

On Fri, Aug 15, 2014 at 6:16 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> I probably missed something. How do you define what equivalence is without
> Id on types?

None of the definitions of equivalence use Id on types, only Id on
*elements* of types.

[Michael Shulman]

On Fri, Aug 15, 2014 at 2:19 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> My implicit proposal in this discussion

Well, thank you for finally making it explicit; I had no idea this was
what you had in mind.

It sounds like the point you're making is not really particular to
"U_n is not an n-type"; it's just that if you postulate equivalence
induction, you can then define "Id_U" to be "Eq" and obtain a roughly
equivalent system to if you had Id_U to begin with and postulated that
it was equivalent to Eq.

I do feel that this undercuts the objection to expressing univalence
as "equivalent types are equal". In fact, it seems to be exactly what
I've been saying, that equivalent types are equal *because* we expand
the meaning of "equal" for types to mean "equivalent".

Mike

[Martin Escardo]

On 16/08/14 08:03, Michael Shulman wrote:
> On Fri, Aug 15, 2014 at 2:19 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> My implicit proposal in this discussion
>
> Well, thank you for finally making it explicit; I had no idea this was
> what you had in mind.

I always said that instead of working with equality on U one should work
with equivalence on U to define univalence. When you unravel this to
countably many universes, this is unvaoidably what you get.


Martin

>
> It sounds like the point you're making is not really particular to
> "U_n is not an n-type"; it's just that if you postulate equivalence
> induction, you can then define "Id_U" to be "Eq" and obtain a roughly
> equivalent system to if you had Id_U to begin with and postulated that
> it was equivalent to Eq.
>
> I do feel that this undercuts the objection to expressing univalence
> as "equivalent types are equal". In fact, it seems to be exactly what
> I've been saying, that equivalent types are equal *because* we expand
> the meaning of "equal" for types to mean "equivalent".
>
> Mike
>

[Michael Shulman]

I feel that there is a difference between "instead of working with
equality on U one should work with equivalence on U" and "we define
equality on U to mean equivalence on U". In fact, this is precisely
the point.

[Martin Hotzel Escardo]

My point of view is that univalence doesn't say that equivalent types are equal. Sure, that's one possible formal formulation of univalance, which requires identity types for universes to be present. You first define what you mean by (sic) "type equality" via identity types, then you define what you mean by equivalence, and then you say that the two are equivalent (in a suitably precise way). But I think, as I said, it is conceptually better to see univalence as a property of equivalence. Then, if you do have identity types for universes,  it follows (as a theorem) that equivalence is equivalent to identity. From the proof engineering point of view, I do agree that it is useful to have identity types. However, then I see univalence as saying that what identity types really capture is equivalence (and not as saying that "isomorphic types are equal"). However, we have already discussed this endlessly in this thread and a previous thread. WIthout univalence or K (which contradicts univalence), identity types for universes are fairly neutral  as to which notion of type equality they are axiomatizing. Hence another point of view is that univalence is making (more precise) which notion of equality we intend identity types for types to capture.
 

[Martin Escardo]

I should probably refrain from making further comments in this
thread. But here we go.

There are many statements and proofs of HoTT that, when expressed
informally but rigorously, make perfect sense in other mathematical
theories, such as ZFC and various flavours of constructive and
non-constructive mathematics.

For example, the statement and proof that there are infinitely many
prime numbers look the same in HoTT and in any other mathematical
theory.

However, a statement such as "isomorphic types are equal", as an
informal rendering of univalence, is false in "competing" mathematical
theories.

It is false, say in ZFC, IZF, CZF.

***BUT*** it is (not even) wrong to say that univalence fails in such
theories.

There is *no way* to formulate univalence in ZFC, IZF, CZF. There is
no univalence statement (among the several we have considered in this
discussion) that makes sense in these theories.

Hence it is wrong to say that univalence fails (or holds) in ZFC, IZF,
CZF. It can't even be formulated in these theories.

HoTT already needs to start from a different base (Martin-Loef type
theory with or without identity types for universes) in order to be
able to *say* what the univalence axiom is.

The informal formulation "isomorphic types are equal" gives the
impression that one would be able to formulate univalence in ZFC, and
then immediately prove it false.

However, the univalence axiom cannot even be formulated in ZFC,

Martin

[Michael Shulman]

What would you think about

"Isomorphic types are equal, by definition"

? This is a conciser version of what I've been trying to say all
along that the slogan should be, and it seems to me to be the same
thing that you are saying.

[Martin Escardo]

On 17/08/14 23:30, Michael Shulman wrote:
> What would you think about
>
> "Isomorphic types are equal, by definition"

(Clever) people want to know what the univalence axiom says. A number
of them have asked me that, and this is partly why I am discussing
this.

If one thinks of a slogan not as propaganda but as a first
approximation of a subtle notion, one should not choose that
approximation to be something that violates intuition.

Any violation of intuition should be left for the second
approximation, and preferably should come as a theorem and not as an
axiom. Mathematicians can cope very well with theorems that violate
intuitions, and this happens all the time, provided they believe the
axioms.

We need a believable, even if provocative, first approximation to the
univalence axiom.

Unfortunately, it is not enough to explain the axiom itself: to
explain it, we need to say at least a little bit about the
mathematical theory that allows its formulation.

Perhaps a first approximation would say not something about
univalence, but something about Martin-Loef type theory itself: it is
a theory that is compatible with the principle that, both in theorems
and proofs, objects can be replaced by isomorphic copies.

Then the univalence axiom itself is, as a first approximation, the
statement that this principle holds.

Then better approximations of the formulation of univalence (using
equivalence, identity types, or what-you-have), followed/accompanied
by theorems, should follow that. In particular, not only useful
theorems should be given immediately, but also surprising ones should
be given as soon as possible,.

Martin

[Michael Shulman]

On Sun, Aug 17, 2014 at 4:24 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> Unfortunately, it is not enough to explain the axiom itself: to
> explain it, we need to say at least a little bit about the
> mathematical theory that allows its formulation.

I agree entirely. If someone asks me what univalence is and is
expecting an answer that makes sense in set theory, then I had better
start by correcting that expectation; otherwise anything I say is
going to be misleading or counterintuitive or both.

I don't think I have any more to add to what I said 2 months ago:
https://groups.google.com/d/msg/homotopytypetheory/yJm1aFPgjME/okKuZQsTWUIJ

Mike

[Vladimir Voevodsky]

It is impossible to explain Univalence Axiom mathematically without starting by explaining that there are two equalities in MLTT:

Substitutional equality which is designed to be decidable and which is "locked" from the user so that it can only be checked but can not be assumed (as an axiom or as an inductive assumption) or proved.

...and

Propositional equality which can be assumed and proved but can not be used to syntactically substitute equal for equal. Instead a choice of proof of a propositional equality is required to perform the "transport" which replaces substitution for propositional equality.

The univalence axiom associates a proof of propositional equality to an equivalence.

Vladimir.

[Thomas Streicher]

Dear Martin,

I think there is a problem with your suggestion. You may define Id on
universes as equivalence but what about types in universes. For U(0)
you say you take the usual Id of Martin-Loef. But what about types in
some U(n+1), e.g. what is the equality on N -> U(0)?

Possibly, what you have in mind is dispensing with Id at all and
instead define Id by recursion on the structure of types as some
people do suggest?

Thomas

[Robert Harper]

if one embeds type theory within an ambient logical framework, then it is entirely possible to formulate and use judgmental equality hypotheses; in fact, one can define types in this manner as theories within the framework.  the delicate part is to characterize the (framework) contexts that ensure sensibility (adequacy) of the theory it formulates; it is by no means given that it is necessarily sensible/meaningful/consistent.  but from this perspective one can certainly consider hypothetical judgments of this form, and so can hypothesize judgmental equalities.

i have sometimes wondered, without pursuing it, whether such an approach might help with your suggestions about "exact equality" or similar thoughts that have been raised now and again.

bob

>>> email to HomotopyTypeTheory+unsub...@googlegroups.com.

>>> For more options, visit https://groups.google.com/d/optout.
>>
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.

[Martin Escardo]

On 18/08/14 12:02, Thomas Streicher wrote:
> Dear Martin,
>
> I think there is a problem with your suggestion. You may define Id on
> universes as equivalence but what about types in universes. For U(0)
> you say you take the usual Id of Martin-Loef. But what about types in
> some U(n+1), e.g. what is the equality on N -> U(0)?
>
> Possibly, what you have in mind is dispensing with Id at all and
> instead define Id by recursion on the structure of types as some
> people do suggest?

I haven't made up my mind whether one should or should not have
identity types for universes as primitive notions, but if we don't,
we have to do as you say.

The point I was trying to make is that I prefer to see univalence as a
postulate about equivalence, at least for the purposes of explaining
concisely what univalence is, avoiding anything to the extent
"isomorphic types are equal" in such an explanation. Then if one does
have identity types for the universe, universe identity types are
equivalent to equivalence (theorem), which says that what identity
types capture is equivalence (in the presence of univalence).

But, as Mike said, we seem to be able to get more if we do have
identity types for universes. But we don't need to invoke
them while explaining what univalence is.

Martin

>
> Thomas
>
>> My implicit proposal in this discussion was to define (for your
>> definitions and theorems, and more generally for any definition and
>> theorem):
>>
>> Id(0) = the usual Martin-Loef type ("on points" of types X:U0).
>>
>> Id(n+1) = Eq (on types, defined from Id(n) in the usual way).