Isomorphic types are equal

[Martin Escardo]

The HoTT slogan is "isomorphic types are equal".

I think this slogan is very bad for public relations (many of you do
too). It doesn't work for public relations, and it doesn't capture
or convey what is technically intended.

I would like to cause a discussion here, not to give answers (I don't
have them).

And I don't want to take any credit or blame for anything expressed
here. There are no original ideas here.

People immediately react against the univalence axiom (sloppily)
formulated as above. And this doesn't explain what univalence is
about in practice (let alone in theory).

Many people have said to me that this is like a Browerian axiom (such
as "all functions are continuous"), which contradicts classical
mathematics. But we know that univalence doesn't contradict classical
mathematics, and, moreover, it is perfectly compatible with classical
mathematical practice (in practice). [This was cryptic remark.]

So, what's the difference?

For HoTT people, univalence is seen as a property of Martin-Lof's
identity types. An axiom about them. Identity types satisfy a certain
(postulated) property.

But, ultimately, univalence is not a property of identity types. It is
a property of properties of types: Any property of types, in MLTT, is
invariant under equivalence. This what univalance says, internally.

A logician would formulate (and prove!) this as an (external) rule (in
the empty context).

The mathematician's view is to internalize this rule. Vladimir told us
how to do this properly.

The univalance axiom internalizes something that is externally a fact:
properties of types are invariant under equivalence.

This is what the univalence axiom says.

Of course, and this is where the controversy starts: what does entitle
one to internalize something that is externally a fact (for MLTT)?

In other words, the univalance axiom internalizes (positively) the
fact that MLTT cannot distinguish equivalent types.

What is not discussed in the various intuitive explanations of
univalence is how it is useful in practice. (It is discussed
technically in the Book by elaborate examples.)

M.

[Steve Awodey]

On Jun 17, 2014, at 10:45 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

>
> The HoTT slogan is "isomorphic types are equal".
>
> I think this slogan is very bad for public relations

then why begin your post by calling it “the HoTT slogan”?!
: - )
how about instead calling it “the naive misinterpretation of UA”?

Steve

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

On 17/06/14 21:56, Steve Awodey wrote:
> On Jun 17, 2014, at 10:45 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>
>>
>> The HoTT slogan is "isomorphic types are equal".
>>
>> I think this slogan is very bad for public relations
>
> then why begin your post by calling it “the HoTT slogan”?!
> : - )
> how about instead calling it “the naive misinterpretation of UA”?

Indeed. My point is that most (intelligent) people I know take this as
the content of univalence, which it isn't.

My point is that we should do better in explaining what we mean.

I tried to explained, in my message, how the ideas are consistently
misinterpreted. And I think it is our fault.

Martin

[Michael Shulman]

I think that "any property of types is invariant under equivalence"
also does not convey the real content of univalence, and in particular
its radical nature. Most mathematicians are not familiar with Leibniz
equality, and to them this phrase could just mean that language is
restricted so that we can only talk about equivalence-invariant
properties (which was already the case in MLTT before univalence).

I've gone through many opinions on this topic, but now I think it is
okay to say that "isomorphic types are equal" as long as you
immediately clarify -- unprompted and in the same paragraph -- that
this is not because the notion of isomorphism is squashed, but because
the notion of equality is expanded.

[Gershom B]

In my experience trying to explain and popularize homotopy type theory
(largely to folks with a background more in computer science than in
mathematics), I've found that "isomorphic types are equal" might
generate a reaction of shock (which can be good, to convince people
you have something new to present) but it gets in the way of
intuition, and _especially_ so for people familiar with the old
terrain of intensional/extensional theories, etc.

Increasingly, I think the main thing to present is the idea that
homotopy type theory allows us to discuss equalities with nontrivial
computational content, and that one large class of these equalities
_happens_ to be that between equivalent types.

Propagandistically, it seems better to tell people not that anything
they know is "wrong" as such, but rather that HoTT opens up the
language of type theory to discuss a much richer class of objects,
that had been "lying next to" the objects we already discuss, but
which all along our tools had not been precise enough to discern.

If you tell people that HoTT announces all equivalences are equalities
they say "of course that will never compute!" If you tell them that it
allows equalities to carry computational content they instead say "of
course, why don't we do that already?"

I do not know how one might present univalence to "typical"
mathematicians. The mathematicians I know have tended to say "of
course this is the case," but they come from backgrounds where people
naturally work up to equivalence or homotopy or isomorphism in any
case. What they have tended to underline as "new" to them is that this
is a setting so "nice" that one does not have to perform fibrant
replacement. Of course as sales pitches go, I suppose that hits a
rather limited audience (-:.

--Gershom

[Michael Shulman]

There are two different issues here which should not be confused:

1. How to explain (and I guess "sell") homotopy type theory, and

2. How to explain univalence.

Of course (2) may depend on how you did (1), and (1) depends on the
background of the audience. I agree that in many cases, an
appropriate choice of (1) makes univalence seem "obvious". For
instance:

- I don't have much experience telling computer scientists about HoTT,
but your suggestion of "we allow equalities to carry computational
content" for (1) makes perfect sense, and then "of course" the
computational content of an equality between types should be an
equivalence.

- When talking to category theorists, I generally say that HoTT is a
foundational theory whose basic objects are oo-groupoids. It is then
"obvious" that the morphisms in the oo-groupoid of oo-groupoids should
be equivalences of oo-groupoids, which is univalence.

- When talking to (higher) topos theorists, one can say that HoTT is
the internal language of oo-topoi. Then univalence is just the
internal incarnation of the object classifiers.

- I don't yet have a pithy one-liner for explaining HoTT to algebraic
topologists (though I do think that "you don't have to perform fibrant
replacement" is a pretty impoverished way to describe it). But once
you've explained it to them, you can say that univalence gives you a
classifying space for fibrations.

However, in some cases one has an audience lacking all of these
backgrounds, and still wants to convey some idea of what univalence
means. In that context, I think it is fine to say something like

"Univalence says that equivalent types are equal. However, it does
this not by collapsing the notion of equivalence, but rather by
expanding the notion of equality so that an equality can carry
information, such as the data of an equivalence."

It never would have occurred to me to tell people that anything they
already know is *wrong* (since it isn't). HoTT is just a new way to
do mathematics. The old ways aren't wrong; but the new one may have
advantages.

Mike

[Michael Shulman]

On Tue, Jun 17, 2014 at 1:45 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

> Many people have said to me that this is like a Browerian axiom (such
> as "all functions are continuous"), which contradicts classical
> mathematics.

I would be very curious to know, if you could ask these people, what
led them to that conclusion. Evidently they are people with some
experience in constructive mathematics, to know about and be able to
make an analogy to Browerian axioms.

Are they not familiar with type theory, or not aware that univalence
is an axiom about type theory? In this case I would expect them to be
confused at a deeper level, since even in constructive set theory one
can produce unequal isomorphic sets.

Or are they under the impression that in type theory with classical
axioms one can produce unequal isomorphic sets? That's obviously not
true in any type theory compatible with univalence. I suppose it
might conceivably be true in extensional type theory, but I would be
surprised; can't one make a set-theoretic model that is "skeletal" and
hence satisfies the naive meaning of "equivalent types are equal"?

Mike

[Thomas Streicher]

I think "isomorphic objects are equal" is fairly descriptive for
what's going on in HoTT. What causes problems to people is the
distinction between judgemental and propositional equality which
doesn't show up in ordinary mathematics.
This is not a problem in Extensional Type Theory where these two
concepts are equivalent. As Martin E. and I have shown even in
extensional type theory the universe may be indiscrete in the sense
that maps from the universe to N_2 are constant. Thus it's not easy to
prove that types are not equal. However, one may show that they are
not isomorphic as e.g. N and N^N.

Now the basic idea of HoTT is that one may interpret propositional
equality as being isomorphic. But that doesn't mean that one can
reason with isomorphism as equality since one has all the time carry
around the equality proofs. Thus, the Id-types ENFORCE on you a
discipline when reasoning up to iso which is neglected in practive of
category theory, topology, algebra and alike where the isos are swept
under the carpet.

I don't know how to prove even in Extensional Type Theory that N and
N x N are different. In set theory it's easy because 0 is not in N x N
and (0,0) is not in N. In most languages like HOL one cannot even
formulate the question whether types are equal.
It seems to me that for proving that isomorphic types are not equal
one needs a (set-theoretical) universe of all objects because for
showing A and B to be not equal one exhibits an object c which is in A
but not in B (or vice versa). But for this purpose one would have to
be able to consider judgements as propositions.

Thomas

[Andrej Bauer]

On Wed, Jun 18, 2014 at 9:58 AM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> I don't know how to prove even in Extensional Type Theory that N and
> N x N are different.

But there is no hope to prove such a thing. Because N and N x N are
isomorphic, we ought to be able to cook up a model in which N x N is
*chosen* to be the same as N. The projections pi1, pi2 may then look a
bit funny, but (N, pi1, pi2) will still have the universal property of
being the product of N and N.

Here's another reason: interpret ETT in the category of cardinal
numbers and functions between them (a skeleton of Set). There N and N
x N actually are the same.

Or is there some obstruction to "hacking" the interpretation of types
so that we change the intepretation of a particular type to an
isomorphic one?

With kind regards,

Andrej

[Thomas Streicher]

> Here's another reason: interpret ETT in the category of cardinal
> numbers and functions between them (a skeleton of Set). There N and N
> x N actually are the same.
>
> Or is there some obstruction to "hacking" the interpretation of types
> so that we change the intepretation of a particular type to an
> isomorphic one?

I think it's impossible to get the skeleton of Set split!

Thomas

[Andrej Bauer]

On Wed, Jun 18, 2014 at 10:30 AM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> I think it's impossible to get the skeleton of Set split!

Ah, I suspected you'd say something like that. How about "fixing" the
interpretation of a single type? It sounds innocent enough.

[Jason Gross]

You can prove in ETT that there are contractible types which are not equal to the unit type.  For example, if { x : bool | x = true } and { x : bool | x = false } were equal, then (true; refl) would typecheck as an inhabitant of both types, and we'd have refl : true = false.  What makes the case of N and N x N different from this case?

-Jason

[Vladimir Voevodsky]

BTW - the substitution principle for the equality i(this is what you call "extensional" equality, right?) s incompatible with univalence.

V.

[Altenkirch Thorsten]

As Thomas already pointed out I don't think there is anything wrong with
this statement.

For marketing purposes we should rather emphasize that equivalent
structures can be treated as equal, which I summarized as "Structures are
first class citizens" (stealing from FP where "Functions are 1st class
citizens"). Because by a structure we usually don't mean a particular
representation of for example a group but the object upto equivalence.

Or a bit of a insider joke for category theoreticians: "HoTT is a language
where you cannot say anything evil" :-) Yes that sounds positively
Orwellian :-)

In computer science it is important to emphaisze that HoTT gvies us what
CS people called "Abstract Data Types", an abstract data type is a data
type where we don't care about the atcual implementation but only its
behaviour. I think it is fair to say that HoTT gives us "truly abstract
data types for free".

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.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

[Peter LeFanu Lumsdaine]

It’s not quite automatic, but I think it works, at least in a classical meta-theory. 

Nat is (usually taken as) a standalone base type, not an instance of some scheme, so we can choose anything suitable as its value, no trouble.  But just that isn’t enough here — we can redefine Nat as what was previously Nat x Nat, but now Nat x Nat will become something different (the old ((Nat x Nat) x (Nat x Nat)).

So we need to re-define the product construction, and for that, we need to be a little careful not to break stability of product types under substitution.  I guess if we’re just doing the set model in a classical metatheory, we can simply say “A x B := if (A==Nat and B==Nat) then Nat, else the usual product”, and similarly for the eliminators; since this is all genuine operations on the (external) universe of sets, it’s still strictly commutative with substitution.  And the same idea should probably work in other models — certainly in groupoids and simplicial sets.

I guess the common point in these is: in all these models, types are taken to be functions into some (external, not necessarily small) universe, with decidable equality.  Without that decidable equality, I can’t see how to do this.

–p.

[Peter Aczel]

I think that a natural reaction to first seeing the univalence axiom is say that 

NxN is obviously not equal to N - so what is going on?

My initial short answer:  HoTT has judgmental/definitional equality and the above intuition about NxN

is about that equality, not `propositional equality'.  The distinction is something special to DTT

and not available in the usual set theoretic mathematics and needs to be understood.

Best wishes,

Peter

[Joyal, André]

I would like to add my grain of salt to the discussion.

I also think that the slogan "isomorphic types are equal" is bad.
This is plainly false in ordinary mathematics.
For example, the set of natural numbers has many incarnations depending
on the representation we may choose for numbers.
For example, let me write N_P for the set of Peano numbers
and N_B for the set of binary numbers.
A Peano number is a successor of 0 and
a binary number is a string of 0 and 1.
The isomorphism u:N_B to N_0
is impossible to compute in practice: just try to compute

u(100000000000000000000000000)=?

It would be wrong to assert that N_B=N_0.

We should avoid making statements that are mathematically false in practice.

Best wishes,
André

________________________________________
From: HomotopyT...@googlegroups.com [HomotopyT...@googlegroups.com] on behalf of Martin Escardo [m.es...@cs.bham.ac.uk]
Sent: Tuesday, June 17, 2014 4:45 PM
To: HomotopyT...@googlegroups.com
Subject: [HoTT] Isomorphic types are equal

M.

--

[Altenkirch Thorsten]

What do you mean by "mathematically false in practice"?

False in set theory?

What *are* the natural numbers? They are given by a representation but we
shouldn't talk about this. We can tak about representations but this is
metatheory.

T.

[Guillaume Brunerie]

I’m confused, are you saying that we shouldn’t say that the Ackermann function is computable, for instance?

[Francisco Mota]

I disagree! I think we should exploit alternative representations (via univalence) in order to achieve efficiency. 

What is u(1000000000000000000000000000)? Why, it is u(1000000000000000000000000000), of course. We don't have to convert it into its Peano normal form, because every operation over Peano numbers can be mapped onto an operation on Binary numbers, and back, via univalence.

This is a practical application of univalence. We want to reason in one type (Peano numbers) but we want the computations to happen in a more efficient type (Binary numbers).

So to say that "Peano numbers" and "Binary numbers" are practically not interconvertible is just a consequence of choosing a strict representation for Peano numbers, when univalence tells us that we can represent them differently if we so choose.

In theory, anyway.

[Michael Shulman]

On Wed, Jun 18, 2014 at 1:30 AM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> I think it's impossible to get the skeleton of Set split!

I don't see why it should be. All the constructions of splittings are
category-theoretic in the base category, so they should work just as
well with Set replaced by any equivalent copy of it (by univalence, if
you like).

But a splitting of the fundamental fibration of a skeleton of Set
isn't what we want anyway -- what we want is a splitting of the
fundamental fibration of Set (or some equivalent copy of it) whose
*fibers* are skeletal. It seems to me that we should be able to get
that by using the set of (small) cardinal numbers as a universe.

Mike

[Michael Shulman]

On Wed, Jun 18, 2014 at 1:58 AM, Jason Gross <jason...@gmail.com> wrote:
> You can prove in ETT that there are contractible types which are not equal
> to the unit type. For example, if { x : bool | x = true } and { x : bool |
> x = false } were equal, then (true; refl) would typecheck as an inhabitant
> of both types, and we'd have refl : true = false.

I'm not convinced by this. You're arguing that since

(true; refl) : { x : bool | x = false }

we have

pr2 (true; refl) : pr1 (true; refl) = false

and pr1 (true; refl) = true, so true = false. But the pair
constructor (-;-) actually has the type

forall {A : Type} {B : A -> Type} (a : A) (b : B a), { x : A | B x }

and similarly pr1 has the type

forall {A : Type} {B : A -> Type}, { x : A | B x } -> A.

But here you are trying to compare them with different values of B!
The constructor (true; refl) is applied with B x := (x = true), while
the pr1 in question is applied with B x := (x = false). So I don't
think you should be able to beta-reduce them to get pr1 (true; refl) =
true (or pr2 (true; refl) = refl).

I suppose one might imagine a sort of ETT in which the notion of
reduction is untyped and sees only the syntaxes "(-;-)" and "pr1" with
implicit arguments omitted. I suppose such a thing might even have a
set-theoretic model, although I haven't checked the details. But I
think it would be *much* harder to construct any nontrivial
category-theoretic model: you'd need to ensure somehow that A x B is
never equal to C x D, even by accident, unless A = C and B = D (and
similarly for all other type constructors).

Mike

[Thomas Streicher]

> But a splitting of the fundamental fibration of a skeleton of Set
> isn't what we want anyway -- what we want is a splitting of the
> fundamental fibration of Set (or some equivalent copy of it) whose
> *fibers* are skeletal. It seems to me that we should be able to get
> that by using the set of (small) cardinal numbers as a universe.

Well, if Sk is the full subcat of Set on cardinals then in it all
types are equal. Using choice a lot one can turn (one of) the (usual)
splitting(s) of the fundamental fibration of Sk into a model of type
theory. But, the fibre over 1 can be arranged to be skeletal and that
enough for getting N \cong N x N or any other equality of isomorphics
types.

Thomas

[Jonathan Sterling]

Mike,

In Nuprl (the only ETT implementation I am familiar with), reduction
*is* untyped and the terms are not "proof terms" in the sense of ITT,
but rather computational realizers; I am not aware that full ETT can be
nicely done in any other way than this, but that might be merely my own
ignorance. I do not have a working installation of Nuprl at hand, but
perhaps someone who does can verify that Jason is indeed correct that
ETT refutes the equation ({x:bool | x = false} = {x:bool | x = true} in
U). It certainly feels "intuitively true" to me, but ETT can be pretty
tricky and often trips me up.

My best,
Jon

>
> Mike

[Jason Gross]

I also plan on trying this in brazil, unless someone else does first.  (My suspicion is that, at least with sigmas axiomatized as inductive types, Mike is correct.)

Andrej, is reduction of the new record projections in brazil typed or untyped?

-Jason

[Joyal, André]

Dear Thorsten,

This discussion is about communicating type theory to non-type theorists.

The number systems N_P and N_B are isomorphic but not *identical*.
We should stop calling the identity type Id_A(x,y) the *identity* type.
For the sake of the discussion, let me call the identity type Id_A(x,y)
the *equivalence* type Eq_A(x,y). It would be perfectly ok to say that the
number systems N_P and N_B are *equivalent* since they are isomorphic.

A.

________________________________________
From: HomotopyT...@googlegroups.com [HomotopyT...@googlegroups.com] on behalf of Altenkirch Thorsten [psz...@exmail.nottingham.ac.uk]
Sent: Wednesday, June 18, 2014 6:25 AM
To: Joyal, André; Martin Escardo; HomotopyT...@googlegroups.com
Subject: Re: [HoTT] Isomorphic types are equal

[Martin Escardo]

On 18/06/14 08:58, Thomas Streicher wrote:
> As Martin E. and I have shown even in extensional type theory the
> universe may be indiscrete in the sense that maps from the universe
> to N_2 are constant. Thus it's not easy to prove that types are not
> equal.

This is a sticky point. For similar reasons, it is not easy to prove
that points of types more mundane than the universe are different.

As in the joint paper with you, and as I explained in my IHP talk last
week, one can easily construct a type X with two different points x0
and x1 such that "there is no map X->2 with p x0 = 0 and p x1 = 1".

(The example in my talk was the one-point compactification of N (the
type of decreasing binary sequences), with the point at infinity \i.1
exploded in two copies x0 and x1, to negatively answer a question by
Altenkirch et al.)

I put this in quotes because it is not true. What is true is that the
statement "there is a map X->2 with p x0 = 0 and p x1 = 1" implies
WLPO (rather than the empty type). Here WLPO is the "contructive
taboo" that any infinite binary sequence is either constantly zero or
not (a morally empty type for constructive mathematicians, but whose
emptiness/inhabitedness is left deliberately undecided by (most of) them).

This construction of X,x0,x1 is in Section 2.3 of our paper
http://www.cs.bham.ac.uk/~mhe/papers/universe-indiscrete.pdf

The points x0 and x1 *are* different, but this cannot be established
by exhibiting a map p:X->2 with p x0 = 0 and p x1 = 1 (where "cannot"
means that if we could then we would get the WLPO taboo).

We instead define a map p:X->U such that

p x0 = 0 (the initial type)
p x1 = 1 (the terminal type)

to distinguish x0 and x1. This doesn't rely on taboos. It is just a
fact.

Martin

[Martin Escardo]

On 18/06/14 23:29, Joyal, André wrote:
> Dear Thorsten,

(And everybody else.)

> This discussion is about communicating type theory to non-type theorists.

Yes, this is what I intended.

We all here know precisely what we are talking about, and we are not
confused. The point is what is the most concise way (perhaps omitting
part of the truth, but not distorting it too much) of conveying what
we mean.

M.

[Peter LeFanu Lumsdaine]

On Wed, Jun 18, 2014 at 10:11 PM, Thomas Streicher <stre...@mathematik.tu-darmstadt.de> wrote:

> But a splitting of the fundamental fibration of a skeleton of Set
> isn't what we want anyway -- what we want is a splitting of the
> fundamental fibration of Set (or some equivalent copy of it) whose
> *fibers* are skeletal.  It seems to me that we should be able to get
> that by using the set of (small) cardinal numbers as a universe.

Well, if Sk is the full subcat of Set on cardinals then in it all
types are equal. Using choice a lot one can turn (one of) the (usual)
splitting(s) of the fundamental fibration of Sk into a model of type
theory.

Can one?  How does that work?

–p.

 

But, the fibre over 1 can be arranged to be skeletal and that
enough for getting N \cong N x N or any other equality of isomorphics
types.

Thomas

[Thomas Streicher]

> The number systems N_P and N_B are isomorphic but not *identical*.
> We should stop calling the identity type Id_A(x,y) the *identity* type.
> For the sake of the discussion, let me call the identity type Id_A(x,y)
> the *equivalence* type Eq_A(x,y). It would be perfectly ok to say that the
> number systems N_P and N_B are *equivalent* since they are isomorphic.

Maybe the right way of putting it is that equality is hidden and
"misinterpreted" as isomorphism. Of course, for discrete types equality
and isomorphism coincide. The role of univalenc is to turn potentially
"evil" (equality of types) into "good" (isomorphism of types).
But being non-evil all the time can be a bit tiring and thus "bad
language" is reintroduced in Brazil.
This tries to pinpoint what's going on rather to find the right slogan
for promotion.

As to the discussion whether isomorphic types can be proven to be not
equal (as e.g. N and NxN) it is a metamathematical consequence of the
consistency of UA that the negation of their equality is inconsistent
with extensional type theory.
But models of extensional type theory as e.g. realizability models and
sheaf models do validate that e.g. N and N x N are not not isomorphic.

Since these models are quite natural I find it problematic to say that
UA is the right option. It's just a very interesting possible one
though a bit extremist in identifing equality and isomorphism.

I, personally, find that one should inform "customers" about the
features of certain "products" rather than saying that it's better
than the competing ones.

Thomas

[Martin Escardo]

On 19/06/14 08:46, Thomas Streicher wrote:
>[...]

> This tries to pinpoint what's going on rather to find the right slogan
> for promotion.

I don't want a slogan. I want to get rid of an existing one.

> I, personally, find that one should inform "customers" about the
> features of certain "products" rather than saying that it's better
> than the competing ones.

That's precisely the idea.

Best,
Martin

[Thomas Streicher]

Well, Sk is lcc with a nno. It can be split via one of the usual techniques.

Thomas

[Thomas Streicher]

> > This tries to pinpoint what's going on rather to find the right slogan
> > for promotion.
>
> I don't want a slogan. I want to get rid of an existing one.
>
> > I, personally, find that one should inform "customers" about the
> > features of certain "products" rather than saying that it's better
> > than the competing ones.
>
> That's precisely the idea.

so why not say

"Isomorphic types may be equal"

Thomas

[Steve Awodey]

How about calling the identity type the type of *homotopies*?

Two points are homotopic if they are connected by a path, two functions are homotopic if their respective values are connected by paths, two objects in a universe are homotopic if they are connected by a path in the universe.

The univalence axiom says that two objects in the universe are homotopic if they are homotopy equivalent: i.e. the paths in the universe are homotopy equivalences.

The fact that it is the usual *Identity* type that is being reinterpreted means that everything that can be said in the system is invariant under homotopy — because everything is invariant under identity.

Steve

[Thierry Coquand]

Dear André,

The notation

Eq_A(x,y)

instead of Id_A(x,y) seems indeed much better.
We should avoid to mention "identical"

and Eq_A(x,y) can also be read as "x and y are equal"

Thierry

PS: This also fits with Bishop's informal way to introduce equality
"Each set will be endowed with a relation = of equality. This relation is
a matter of convention, except that it must be an -equivalence relation-"
This is generalized to "higher level" equivalence relations.

[Andrej Bauer]

My experience with explaining HoTT has been as follows.

1. It is a very bad idea to utter any suprising statements such as
"equivalence is equality" or "equivalence is equivalent to equality".

2. It is a bad idea to try to explain the difference between
judgmental and propositional identity in terms of there being two
kinds of equality. I might as well say that all equalities are equal
but some are more equal than others.

3. Geometric/homotopical explanations work pretty well. People *do*
understand the idea that two things may be "equal up to homotopy" or
that "they're not equal but there is a path between them so they're
kind of equal". That's just the usual stuff from homotopy theory and
topology. Building on that, it's not hard to introduce Id_A(x,y), as
long as I call it "path" space and never ever say "identity".

4. People (by which I mean topologists) easily accept the idea that
every construction in type theory is "homotopy invariant". They're not
quite aware of the consequences though. For instance, after defining
the interval as a hit someone noticed that the square satisfies the
axioms (with endpoints being opposite vertices) -- and that was very
suprising to everyone. But that's exactly the sort of thing I want
them to notice.

4.5. People are not impressed by the fact that type theory is
"homotopy invariant". They will point out that what they do in
practice is already homotopy invariant, so what's the point? Then if I
start explaining how it is *possible* to make non-invariant statements
in set theory, they will just think I am being difficult. The natural
reply is "don't make such statements". They do not see a problem, and
thus HoTT is not a solution to anything. A discussion about how
"sometimes you have to look under the hood" isn't productive either --
because it argues in favor of set theory!

5. It is confusing that a fibration p : E -> Y can be given as a
family of fibers y : Y |- E_y because people do not see where the
information for "gluing the fibers E_y back into E" comes from. It
seems to be somehow mysteriously available. I blame this confusion on
set theory.

6. The best way to understand univalence is via the question "what is
a path in the universe?"

We do not need a slogan. We need a method for explaining HoTT by
drawing on pre-existing intuitions that people might have.

[Steve Awodey]

I think this is an important point:

Foundations should not introduce anything controversial, anything that’s not already accepted in everyday math.
That working in such a way that everything is invariant is already common-place and uninteresting means that it’s OK to put that into a system of foundations. That set theory does not support such reasoning is maybe one reason why no one really uses set theoretic foundations in practice. That HoTT does allow it, and even allows one to do it in a more precise and systematic way, could make it actually useful for everyday math.
So we shouldn’t say that UA introduces a "powerful new principle of reasoning” (although I do think that is true for some kinds of applications involving higher n-types), but rather that it formalizes a common practice of everyday math that is not permitted by set theory.

So the problem that’s being solved by HoTT is not "how to do mathematics invariantly", it’s "how to get a system of foundations that agrees more closely with how people actually do mathematics".

Steve

>
> 5. It is confusing that a fibration p : E -> Y can be given as a
> family of fibers y : Y |- E_y because people do not see where the
> information for "gluing the fibers E_y back into E" comes from. It
> seems to be somehow mysteriously available. I blame this confusion on
> set theory.
>
> 6. The best way to understand univalence is via the question "what is
> a path in the universe?"
>
> We do not need a slogan. We need a method for explaining HoTT by
> drawing on pre-existing intuitions that people might have.
>

[Andrew Polonsky]

Dear Andre,

I think the mismatch between the concepts of "identity" and "equality" which you have pronounced is due to the different ways that the identity type is interpreted semantically.

In the standard, set-theoretic model of type theory, the natural interpretation of the identity type is set-theoretic equality.  This interpretation also validates the propositional-reflection rule of extensional type theory. Also, the classical (non-homotopic) categorical models validate this rule, leading some prominent persons to take the view that the extensional type theory is "the real thing", and intensional type theory is a compromise with the syntax, forced by the desire to keep type-checking decidable.

However, extensional type theory is incompatible with the univalence axiom, precisely because the latter insists that the identity type be interpreted by univalent/path equality, and not exact/strict equality.  Both propositional reflection and UA therefore act as kind of "regulatory principles", restricting the way the language is interpreted, and these two principles are incompatible.

A possible way to reconcile the two views is to have two notions of equality on the level of syntax already, which can be then be interpreted differently. Among type theorists, there is wide agreement that there should be a native notion of "extensional equality", which is not the identity type Id_A(x,y), but is defined by induction on type structure.  For example, in this definition, two functions of type A->B would be equal iff they send equal elements to equal elements -- and this would be a definition, not a consequence of other principles.

In discussions, Per Martin-Loef suggested to use the notation Eq_A(x,y) for this as-yet-undefined notion of "extensional equality", which is to be interpreted by path equality in the models with homotopy structure.  This notation is very appealing, since the concept indeed corresponds to the "book equality" of traditional mathematics, whereas the "identity type" Id_A(x,y) is conceptually akin to the formalist native equality of first-order logic.  It can be interpreted by exact equality in the model.

Finally, having such a native type-theoretic notion of "extensional equality" would also help resolve a certain counter-intuitive feature of the univalence axiom: that, on the surface, it is merely a statement about equality in the universe, but the adoption of this statement forces new equalities between objects as well.  If we had a well-behaved equality type Eq_A(x,y), and the univalence axiom was formulated for this type, rather than the intensional identity type, then all of the equalities between objects would already be there, and the content of the axiom would merely fix the interpretation of equality between types.

Cheers,

Andrew

P.S.  The difficulty with exhibiting Eq_A(x,y) as a type constructor is that extensional equality is an "external" concept, and getting it into the language of type theory requires one to internalize the logical relation defined by induction on type structure, into that very type structure.

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

>For more options, visit https://groups.google.com/d/optout.
>
>--
>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.

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

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

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

[Steve Awodey]

Andrew,

I think it is very confusing to use the terms “intensional” and “extensional” equality like this, because everyone means something different by them.  Can you please try to restate your proposal without referring to “intensional" and “extensional” equality?

Thanks,

Steve

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

[Andrew Polonsky]

Steve,

One could consider the tentative type Eq_A(x,y) to answer the name of
"observational equality" or "behavioral equality", since the way it is
defined fits the following pattern:

Two objects are equal at type A, if, whenever they are used in the
same way, they yield the same results. More precisely, a is A-equal
to a' if, for every elimination form for type A, applying that form
with equal arguments to a and a' yields equal outcomes. Thus,

- two functions f,f' : A -> B are equal if the application of f,f' to
A-equal a,a' gives B-equal fa,f'a';
- two pairs p,p' : A x B are equal if the first projection of p is
A-equal to the first projection of p', and the second projection of p
is B-equal to the second projection of p',
etc.

That said, I find the term "extensional equality" to be quite
appropriate for this concept, because it coincides with the principle:
"Two objects are equal if they have the same extension."

In particular, two functions are equal if they map every input to the
same value.

Cheers,
Andrew

>> >email to HomotopyTypeThe...@googlegroups.com.
>> >For more options, visit https://groups.google.com/d/optout.
>> >
>> >--
>> >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.
>>

>> This message and any attachment are intended solely for the addressee and
>> may contain confidential information. If you have received this message in
>> error, please send it back to me, and immediately delete it. Please do not
>> use, copy or disclose the information contained in this message or in any
>> attachment. Any views or opinions expressed by the author of this email do
>> not necessarily reflect the views of the University of Nottingham.
>>
>> This message has been checked for viruses but the contents of an
>> attachment
>> may still contain software viruses which could damage your computer
>> system, you are advised to perform your own checks. Email communications
>> with the University of Nottingham may be monitored as permitted by UK
>> legislation.
>>
>>
>>
>> --
>> 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

[Bas Spitters]

> 4.5. Then if I start explaining how it is *possible* to make non-invariant statements

in set theory, they will just think I am being difficult.

This is an old point, going back to deBruijn at least. When I write
pi \in sin
this is a well-typed statement in set theory. However, I probably made a typo.
The proof assistant should give me an early warning at this point.

[Michael Shulman]

On Thu, Jun 19, 2014 at 12:46 AM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> As to the discussion whether isomorphic types can be proven to be not
> equal (as e.g. N and NxN) it is a metamathematical consequence of the
> consistency of UA that the negation of their equality is inconsistent
> with extensional type theory.

I don't think so, because UA is not consistent with extensional type theory.

> But models of extensional type theory as e.g. realizability models and
> sheaf models do validate that e.g. N and N x N are not not isomorphic.

I thought the bijection between them was constructive, so that they
are always isomorphic. What goes wrong?

> Since these models are quite natural I find it problematic to say that
> UA is the right option.

Well, sheaf models, at least, sit inside stack models that do validate
UA. Probably the same is true of realizability models.

Mike

[Michael Shulman]

On Thu, Jun 19, 2014 at 1:06 AM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> Well, Sk is lcc with a nno. It can be split via one of the usual techniques.

I think Peter's question was not about the splitting, but about
modeling type theory in the resulting split fibration.

[Michael Shulman]

On Thu, Jun 19, 2014 at 1:14 AM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> so why not say
>
> "Isomorphic types may be equal"

But in the world of homotopy type theory, isomorphic types *are*
equal. No one is saying (I hope) that we should go around telling
people that isomorphic types are equal in set theory! We're just
talking about how to describe what UA says *inside* HoTT.

[Michael Shulman]

On Thu, Jun 19, 2014 at 1:20 AM, Thierry Coquand
<Thierry...@cse.gu.se> wrote:
> The notation
>
> Eq_A(x,y)
>
> instead of Id_A(x,y) seems indeed much better.
> We should avoid to mention "identical"

One nice thing about "Id(x,y)" is that it can be read as "the type of
identifications between x and y". The similar reading of "Eq(x,y)" as
"the type of equalities between x and y" doesn't have quite the same
implication; I think it's easier to understand that an
"identification" can carry data than that an "equality" can.

[Vladimir Voevodsky]

You are going to go in circles forever if you do not accept that in the UF there are two notions of "equality" - the univalent equivalence which is "canonical" and substitutional (strict) equality which for most types is not canonical and depends on conventions.

V.

[Michael Shulman]

On Thu, Jun 19, 2014 at 9:33 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> You are going to go in circles forever if you do not accept that in the UF there are two notions of "equality" - the univalent equivalence which is "canonical" and substitutional (strict) equality which for most types is not canonical and depends on conventions.

That's a very bold statement. I have not observed myself going in any
circles yet. (-:

But the present discussion is only about terminology, and I don't see
that calling the fibrant equality "equality" precludes also having a
stricter kind of equality.

[Martin Escardo]

On 19/06/14 17:52, Michael Shulman wrote:
> On Thu, Jun 19, 2014 at 9:33 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>> You are going to go in circles forever if you do not accept that in the UF there are two notions of "equality" - the univalent equivalence which is "canonical" and substitutional (strict) equality which for most types is not canonical and depends on conventions.
>
> That's a very bold statement. I have not observed myself going in any
> circles yet. (-:
>
> But the present discussion is only about terminology,

I thought it was about explaining (homotopy) type theory to
set-theory-founded mathematicians.

M.

[Michael Shulman]

On Thu, Jun 19, 2014 at 9:55 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> I thought it was about explaining (homotopy) type theory to
> set-theory-founded mathematicians.

Right. It meandered a bit into terminology too. But the point I was
making is that it's not about whether there should be two kinds of
equality.

[Michael Shulman]

On Thu, Jun 19, 2014 at 2:04 AM, Andrej Bauer <andrej...@andrej.com> wrote:
> We do not need a slogan. We need a method for explaining HoTT by
> drawing on pre-existing intuitions that people might have.

I don't think we need a one-size-fits-all solution. In a previous
message in this thread I mentioned a bunch of different methods that
apply depending on the pre-existing intuitions that a particular
audience may have.

[Michael Shulman]

On Thu, Jun 19, 2014 at 2:43 AM, Steve Awodey <awo...@cmu.edu> wrote:
> So we shouldn't say that UA introduces a "powerful new principle of reasoning" (although I do think that is true for some kinds of applications involving higher n-types), but rather that it formalizes a common practice of everyday math that is not permitted by set theory.
>
> So the problem that's being solved by HoTT is not "how to do mathematics invariantly", it's "how to get a system of foundations that agrees more closely with how people actually do mathematics".

But if that's all there is to it, then given that the working
mathematician doesn't generally bother to translate their work into
foundations anyway, why should they care about HoTT?

[Vladimir Voevodsky]

The point about two kinds of equality is that this is what one should start any explanation of HoTT to set-theoretically minded mathematicians with.

V.

PS This applies to any kind of foundations based on type theory where there is another notion of equality in addition to the substitutional equality.

[Vladimir Voevodsky]

Because it opens for them a way to use proof assistants in their work.

V.

[Michael Shulman]

On Thu, Jun 19, 2014 at 10:36 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> The point about two kinds of equality is that this is what one should start any explanation of HoTT to set-theoretically minded mathematicians with.

I think that will only confuse them more.

[Michael Shulman]

On Thu, Jun 19, 2014 at 10:38 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>> But if that's all there is to it, then given that the working
>> mathematician doesn't generally bother to translate their work into
>> foundations anyway, why should they care about HoTT?
>
> Because it opens for them a way to use proof assistants in their work.

I think it would be really sad if the exciting promise of HoTT were
reduced to something as banal as making it easier for mathematicians
to use proof assistants. I don't think HoTT on its own really makes a
huge difference in the usability of proof assistants anyway; it has
the potential to make a few things easier, but the hard problems that
have to be solved are software engineering ones.

Steve said:

> Foundations should not introduce anything controversial, anything that's not already accepted in everyday math.

but I'm not convinced by that. Certainly, any new foundation should
be able to represent everything that's already accepted in everyday
math, but why can't it also make new things possible?

Mike

[Joyal, André]

Michael Shulman wrote:

>I think it would be really sad if the exciting promise of HoTT were
>reduced to something as banal as making it easier for mathematicians
>to use proof assistants.

The idea of creating a user-friendly proof assistant for
mathematicians is exciting. It should be compatible with Hott.
Coq is a good start. Tex is an example of software that
was universally adopted by the mathematical community.
Typing with Tex has become banal and this is a measure
of its success.

André

________________________________________
From: HomotopyT...@googlegroups.com [HomotopyT...@googlegroups.com] on behalf of Michael Shulman [shu...@sandiego.edu]
Sent: Thursday, June 19, 2014 3:34 PM
To: Vladimir Voevodsky
Cc: Steve Awodey; Andrej Bauer; HomotopyT...@googlegroups.com

Subject: Re: [HoTT] Isomorphic types are equal

On Thu, Jun 19, 2014 at 10:38 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

Steve said:

Mike

--

[Michael Shulman]

Of course, all of that is true. I was just saying that HoTT is much
*more* than that.

[Martin Escardo]

On 19/06/14 21:04, Joyal, André wrote:
> Typing with Tex has become banal and this is a measure
> of its success.

I believe that in sufficiently many years (soon, but I don't know how
soon), mathematicians will be more tempted to do difficult calculations
in the computer rather than on paper and blackboards as we do now.

And by this I don't mean proving theorems, but rather experimenting with
ideas as we do everyday on paper and blackboards, before we know that
they will work.

Martin

[Martin Escardo]

Let me make this explicit.

Proof assistants are nice (e.g. Coq and Agda).

But what we really need is e-blackboards, to easily experiment with
mathematical ideas, before we even try to prove a theorem, and before
we have figured out what it is that we are trying to prove, which is
how mathematical practice often works.

Martin

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

[Jacques Carette]

Changing the title, since this thread has seriously veered.

Various people have been toiling away at this for years. One really
wants the computational ease of Maple/Mathematica/Sage, the semantics
and certainty of Agda/Coq, and the breadth of mathematics of LaTeX (or
MathML for that matter).

The problem of course is that neither LaTeX nor Maple have semantics,
the computational capabilities of Agda/Coq are risible, and the display
richness of the CASes and the provers is far far below LaTeX.

Joining computational ease and semantics has been 'figured out' in
theory a long time ago via so-called "biform theories". In practice,
the lack of semantics for CAS computations has made things difficult to
implement. But it turns out that HoTT brings a lot here: another big
hurdle is that no one quite knew why the 'theory morphisms' between
various isomophic theories were so difficult. In HoTT, the reason is
clear: those isomophism had quite a lot of computational content in
them. [The most famous example was given previously: N_P and N_B, aka
Peano and Binary naturals].

Although I am extremely fluent in Maple [I used to be one of its
developers, and I helped fix a bug in it this morning] and now Agda too
[I was using this afternoon to make sure what I claimed was a groupoid
was indeed a groupoid], when I had to 'prove' yesterday that a certain
probability distribution was equivalent to another in a different form,
I still did it on paper. Why? Neither Agda (nor Coq) have the
libraries needed to express the underlying mathematics I needed; and
Maple cannot 'prove' anything, even though it can represent the
mathematics I was doing perfectly well.

As was said in another message: even though HoTT presents a significant
foundational advantage, there remains enormous software engineering
hurdles to overcome to properly capture all the 'computational content'
of something like Maple, all the 'reasoning content' of large proof
libraries, in a setting where semantics and 'pretty math' coexist
peacefully.

But I'm not complaining, it's keeping me well-fed with interesting
research problems!

Jacques

[Altenkirch Thorsten]

Dear Andre,

>This discussion is about communicating type theory to non-type theorists.

Indeed. We should make clear that type theory is different from set theory.

E.g. we cannot express any property which distinguishes equivalent types.
In HoTT we go one step further and identify equivalent types.

This is not possible in set theory which is much more intensional and
allows us to express properties which distinguish isomorphic sets.
Extensionality is essential for abstraction and reuse which in turn is
esssential for developing computer based libraries of Mathematics.

>
>The number systems N_P and N_B are isomorphic but not *identical*.
>We should stop calling the identity type Id_A(x,y) the *identity* type.

Ok, I prefer equality type anyway.

>For the sake of the discussion, let me call the identity type Id_A(x,y)
>the *equivalence* type Eq_A(x,y). It would be perfectly ok to say that the
>number systems N_P and N_B are *equivalent* since they are isomorphic.

The point is that they are equal in the sense that they can be substituted
in all contexts.

T.


>
>A.
>
>
>
>
>
>________________________________________
>From: HomotopyT...@googlegroups.com

>[HomotopyT...@googlegroups.com] on behalf of Altenkirch Thorsten
>[psz...@exmail.nottingham.ac.uk]
>Sent: Wednesday, June 18, 2014 6:25 AM

>To: Joyal, André; Martin Escardo; HomotopyT...@googlegroups.com

>Subject: Re: [HoTT] Isomorphic types are equal
>

>What do you mean by "mathematically false in practice"?
>
>False in set theory?
>
>What *are* the natural numbers? They are given by a representation but we
>shouldn't talk about this. We can tak about representations but this is
>metatheory.
>
>T.
>
>On 18/06/2014 11:16, "Joyal, André" <joyal...@uqam.ca> wrote:
>
>>I would like to add my grain of salt to the discussion.
>>
>>I also think that the slogan "isomorphic types are equal" is bad.
>>This is plainly false in ordinary mathematics.
>>For example, the set of natural numbers has many incarnations depending
>>on the representation we may choose for numbers.
>>For example, let me write N_P for the set of Peano numbers
>>and N_B for the set of binary numbers.
>>A Peano number is a successor of 0 and
>>a binary number is a string of 0 and 1.
>>The isomorphism u:N_B to N_0
>>is impossible to compute in practice: just try to compute
>>
>>u(100000000000000000000000000)=?
>>
>>It would be wrong to assert that N_B=N_0.
>>
>>We should avoid making statements that are mathematically false in
>>practice.
>>
>>
>>Best wishes,

>>André
>>
>>
>>
>>
>>________________________________________
>>From: HomotopyT...@googlegroups.com

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

>This message and any attachment are intended solely for the addressee and
>may contain confidential information. If you have received this message
>in error, please send it back to me, and immediately delete it. Please
>do not use, copy or disclose the information contained in this message or
>in any attachment. Any views or opinions expressed by the author of this
>email do not necessarily reflect the views of the University of
>Nottingham.
>
>This message has been checked for viruses but the contents of an
>attachment
>may still contain software viruses which could damage your computer
>system, you are advised to perform your own checks. Email communications
>with the University of Nottingham may be monitored as permitted by UK
>legislation.
>
>
>
>

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

Dear Thomas,

I deliberately asked you this personally today before asking it in
public:

On 19/06/14 08:46, Thomas Streicher wrote:
> models of extensional type theory as e.g. realizability models and
> sheaf models do validate that e.g. N and N x N are not not isomorphic.
>

> Since these models are quite natural I find it problematic to say that

> UA is the right option. It's just a very interesting possible one
> though a bit extremist in identifing equality and isomorphism.

But what is this (non-univalent, propositional) equality good for?

More importantly, without univalence, propositional type equality is
useless: there is nothing we can say about it, and there is nothing
interesting we can do with it.

Is there a principle for propositional type equality that comes from
realizability models that makes it useful in practice (in a different
direction than univalance)?

Best,
Martin

[Steve Awodey]

On Jun 19, 2014, at 7:23 PM, Michael Shulman <shu...@sandiego.edu> wrote:

maybe because a system that does handle things like applications of univalence in a rigorous and systematic way will make it worthwhile to translate (at least some kinds of) work into foundations.

[Martin Escardo]

Andrej,

I agree with everything except point 4.5:

On 19/06/14 10:04, Andrej Bauer wrote:
> 4.5. People are not impressed by the fact that
> type theory is
> "homotopy invariant".

But they should.

> They will point out that what they do in
> practice is already homotopy invariant, so what's the point?

That's a bit like saying (which is true) that all definable functions
are 2^N->N are uniformly continuous.

It is a big stretch to go from this to the internal axiom that all
(hypothetical) functions 2^N->N are uniformly continuous. Once you have
this axiom, you can prove things that don't follow from the uniform
continuity rule (such as 2^N satisfies the principle of omniscience).

The point is that if you internalize "what they do in
practice is already homotopy invariant", you get to prove things that
you were not able to before (in type theory, such as the fundamental
group of S^1 is Z (and this won't impress them)).

I repeat something I said in a previous message: with univalence (or
something contrdicting) univalence, the propositional equality of types
is useless for any practical purposes. There is nothing we can prove
about it, and there is nothing we can do with it. It is clear to me that
one univalence is postulated, propositional type equality becomes
interesting and useful.

It is not clear to me (Thomas' message), that there is useful
anti-univalence axiom coming from realizability models that makes type
equality useful from a perspective different than that of HoTT.

Martin

> if I
> start explaining how it is *possible* to make non-invariant statements
> in set theory, they will just think I am being difficult. The natural
> reply is "don't make such statements". They do not see a problem, and
> thus HoTT is not a solution to anything. A discussion about how
> "sometimes you have to look under the hood" isn't productive either --
> because it argues in favor of set theory!

E.g., in type theory, the continuity rule for functions N^N->N holds,
but the continuity axion is undecided (intuitively, all definable
functions are continuous, but we are not entitled to say that all
hypothetical functions are continuous).

[Piyush P Kurur]

On Thu, Jun 19, 2014 at 01:09:47PM -0700, Michael Shulman wrote:
> Of course, all of that is true. I was just saying that HoTT is much
> *more* than that.
>

While univalence is very interesting, for a functional programmer the
other contribution of HoTT namely HIT is a brand new "toy" to play
with. In particular, stuff like Dan Licata's formalisation of Darcs
patch theory in terms of HITs looks like a nice starting point in the
"application" side of HoTT.

Regards

ppk

[Andrej Bauer]

On Thu, Jun 19, 2014 at 9:34 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> I think it would be really sad if the exciting promise of HoTT were
> reduced to something as banal as making it easier for mathematicians
> to use proof assistants.

If mathematical pratice moved from paper to proof assistants that
would be the most profound change in mathematics ever since that Roman
soldier killled that mathematician who was using sand instead of paper
to do math.

I would say that e-mail and TeX contributed far more to development of
mathematics than any particular theorem, or even any particular
theory.

With kind regards,

Andrej

[Thomas Streicher]

> > But models of extensional type theory as e.g. realizability models and
> > sheaf models do validate that e.g. N and N x N are not not isomorphic.
>
> I thought the bijection between them was constructive, so that they
> are always isomorphic. What goes wrong?

I meant equal. So if types are isomorphic in ITT but not equal in some
model of ETT then neiter their propositional equality nor its negation
are provable.

Thomas

[Thomas Streicher]

Something like Church's Thesis or Continuity Principles are modeled by
realizability models but not by known models of HoTT. Or Synthetic
Domain Theory or Syntehtic topology etc.

Thomas

[Thierry Coquand]

So

Id_A(x,y)

should be read as "x and y are identified" and not as "x and y are identical".

Another motivation for avoiding the notation

Id_A(x,y)

is that it is already used by Martin-Löf, with a precise meaning (inductively defined
type with reflexivity as the only constructor) which is different to (and incompatible with) the
"equality/identification type" with the axiom of univalence.

Thierry

[Urs Schreiber]

> I would say that email an TeX
> contributed far more to the
> development of mathematics than
> any particular theorem.

In this vein also the contribution of central heating to mathematics is enormous. This engineering feat however is not itself  mathematics. What would indeed be sad is if the exciting promise of HoTT as a topic in mathematics were reduced to a contribution in software engineering.

Andrej Bauer wrote:

>On Thu, Jun 19, 2014 at 9:34 PM, Michael Shulman wrote: >> I think it would be really sad if the exciting promise of HoTT were >> reduced to something as banal as making it easier for mathematicians >> to use proof assistants. > >If mathematical pratice moved from paper to proof assistants that >would be the most profound change in mathematics ever since that Roman >soldier killled that mathematician who was using sand instead of paper >to do math. > >I would say that e-mail and TeX contributed far more to development of >mathematics than any particular theorem, or even any particular >theory. > >With kind regards, > >Andrej > >-- >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.

[Steve Awodey]

On Jun 20, 2014, at 10:55 AM, Thierry Coquand <Thierry...@cse.gu.se> wrote:

>
> So
>
> Id_A(x,y)
>
> should be read as "x and y are identified" and not as "x and y are identical".
>
> Another motivation for avoiding the notation
>
> Id_A(x,y)
>
> is that it is already used by Martin-Löf, with a precise meaning (inductively defined
> type with reflexivity as the only constructor) which is different to (and incompatible with) the
> "equality/identification type" with the axiom of univalence.

is it?
it is still defined as the inductive family generated by refl.
if that understanding is incompatible with UA, then we have to rethink all other inductive types, too.

Steve

>
> Thierry
>
>
>
> On Jun 19, 2014, at 6:29 PM, Michael Shulman wrote:
>
>> On Thu, Jun 19, 2014 at 1:20 AM, Thierry Coquand
>> <Thierry...@cse.gu.se> wrote:
>>> The notation
>>>
>>> Eq_A(x,y)
>>>
>>> instead of Id_A(x,y) seems indeed much better.
>>> We should avoid to mention "identical"
>>
>> One nice thing about "Id(x,y)" is that it can be read as "the type of
>> identifications between x and y". The similar reading of "Eq(x,y)" as
>> "the type of equalities between x and y" doesn't have quite the same
>> implication; I think it's easier to understand that an
>> "identification" can carry data than that an "equality" can.
>

[Vladimir Voevodsky]

I suggest we try and see what happens.

V.

[Michael Shulman]

On Fri, Jun 20, 2014 at 2:10 AM, Steve Awodey <awo...@cmu.edu> wrote:
>> Another motivation for avoiding the notation
>>
>> Id_A(x,y)
>>
>> is that it is already used by Martin-Löf, with a precise meaning (inductively defined
>> type with reflexivity as the only constructor) which is different to (and incompatible with) the
>> "equality/identification type" with the axiom of univalence.
>
> is it?
> it is still defined as the inductive family generated by refl.
> if that understanding is incompatible with UA, then we have to rethink all other inductive types, too.

Yeah, that's exactly how we've been using it all this time, and it
makes perfect sense.

One can alternatively view UA as a "definition" of the identity type
of the universe as part of a type-directed definition of all identity
types, with the induction principle then being provable. This might
be more convenient (although I don't think anyone has yet done it for
the untruncated theory), but the other way isn't wrong.

Mike

[Joyal, André]

Jacques Carette wrote:

>The problem of course is that neither LaTeX nor Maple have semantics,
>the computational capabilities of Agda/Coq are risible, and the display
richness of the CASes and the provers is far far below LaTeX.

>As was said in another message: even though HoTT presents a significant

>foundational advantage, there remains enormous software engineering
>hurdles to overcome to properly capture all the 'computational content'
>of something like Maple, all the 'reasoning content' of large proof
>libraries, in a setting where semantics and 'pretty math' coexist peacefully.

I am not an expert on things technological, so my opinion should be taken with a grain of salt.

There seems to be two patterns here.
One idea is to develop a super-math software for professional mathematicians
that would combine a proof assistant like Coq with the computational power of Maple.
This will be expensive and difficult to realise; it will take a lot of time and will be risky.
Another idea is to develop things incrementally, starting with something simpler
that could be used by many peoples to learn basic logic and proofs.
It may have low computational power but it should be user-friendly and fun to play with.
It could be specialised in elementary euclidian geometry or elementary arithmetic.
If it is done well enough, it will open a "market" that could sustain future developpements.

-André

________________________________________
From: Jacques Carette [jacques...@gmail.com]
Sent: Thursday, June 19, 2014 5:08 PM
To: Martin Escardo; Joyal, André; Michael Shulman; Vladimir Voevodsky

Cc: Steve Awodey; Andrej Bauer; HomotopyT...@googlegroups.com

Subject: Mechanized mathematics

[Jason Gross]

In Brazil, whether or not { x | x = true} == { x | x = false } is admissible depends on whether we define sigma types via records or via axiomatization, currently: https://github.com/andrejbauer/tt/issues/39.  Brazilians are apparently performing untyped reduction of record projections, but get stuck on the expected type error in the axiomatization:

Typing error: sig.br:122:34: expression

  snd bool (fun (b : bool) => b = false)

  (rewrite reflect in contr_true_inhab) has type

  fst bool (fun (b : bool) => b = false)

  (rewrite reflect in contr_true_inhab)

    =

    false but should have type true = false

(it's saying that it can't reduce @pr1 bool (fun b => b = false) ((true; idpath) :: { x | x = false }) to true.)

-Jason

On Wed, Jun 18, 2014 at 10:51 PM, Jason Gross <jason...@gmail.com> wrote:

I also plan on trying this in brazil, unless someone else does first.  (My suspicion is that, at least with sigmas axiomatized as inductive types, Mike is correct.)

Andrej, is reduction of the new record projections in brazil typed or untyped?

-Jason

On Wed, Jun 18, 2014 at 10:07 PM, Jonathan Sterling <j...@jonmsterling.com> wrote:

Mike,

On Wed, Jun 18, 2014, at 07:32 AM, Michael Shulman wrote:
> On Wed, Jun 18, 2014 at 1:58 AM, Jason Gross <jason...@gmail.com>
> wrote:
> > You can prove in ETT that there are contractible types which are not equal
> > to the unit type.  For example, if { x : bool | x = true } and { x : bool |
> > x = false } were equal, then (true; refl) would typecheck as an inhabitant
> > of both types, and we'd have refl : true = false.
>
> I'm not convinced by this.  You're arguing that since
>
> (true; refl) : { x : bool | x = false }
>
> we have
>
> pr2 (true; refl) : pr1 (true; refl) = false
>
> and pr1 (true; refl) = true, so true = false.  But the pair
> constructor (-;-) actually has the type
>
> forall {A : Type} {B : A -> Type} (a : A) (b : B a), { x : A | B x }
>
> and similarly pr1 has the type
>
> forall {A : Type} {B : A -> Type}, { x : A | B x } -> A.
>
> But here you are trying to compare them with different values of B!
> The constructor (true; refl) is applied with B x := (x = true), while
> the pr1 in question is applied with B x := (x = false).  So I don't
> think you should be able to beta-reduce them to get pr1 (true; refl) =
> true (or pr2 (true; refl) = refl).
>

> I suppose one might imagine a sort of ETT in which the notion of
> reduction is untyped and sees only the syntaxes "(-;-)" and "pr1" with
> implicit arguments omitted.  I suppose such a thing might even have a
> set-theoretic model, although I haven't checked the details.  But I
> think it would be *much* harder to construct any nontrivial
> category-theoretic model: you'd need to ensure somehow that A x B is
> never equal to C x D, even by accident, unless A = C and B = D (and
> similarly for all other type constructors).

In Nuprl (the only ETT implementation I am familiar with), reduction
*is* untyped and the terms are not "proof terms" in the sense of ITT,
but rather computational realizers; I am not aware that full ETT can be
nicely done in any other way than this, but that might be merely my own
ignorance. I do not have a working installation of Nuprl at hand, but
perhaps someone who does can verify that Jason is indeed correct that
ETT refutes the equation ({x:bool | x = false} = {x:bool | x = true} in
U). It certainly feels "intuitively true" to me, but ETT can be pretty
tricky and often trips me up.

My best,
Jon

>
> Mike

[Michael Shulman]

Maybe Brazilians ought to rethink their handling of records, then.

[Andrej Bauer]

The Brazilians are still just experimenting with the record types.
They certainly do not intend to perform any untyped reductions. If you
find them, please report to the authorities.

[Martin Escardo]

(Minor remark: there is a Brazilian (and possibly more than one, but
this is unknown to me) in this list who doesn't necessarily subscribe
to this (but who also in principle is just watching to see what comes
out of this effort, and open so see and acknowledge a good
outcome). May I suggest that this be renamed to Slovene type theory?
After all, if you are a Brazilian, as I am, something such as Slovenia
is definitely faraway, whereas Brazil would be close to me (at least
at heart, given that I live in the UK.))

M.

[Martin Escardo]

(NB. I forgot to say that am not offended. I am never offended. I just
wanted to point out that you may be saying what you didn't mean.)

[Michael Shulman]

Maybe we should call them Martians. Are there any Martians on the list?

[Martin Escardo]

Good point:

On 25/06/14 22:40, Michael Shulman wrote:
> Maybe we should call them Martians. Are there any Martians on the list?

In which case I am still included:

http://en.wikipedia.org/wiki/Martin_%28name%29

"The meaning is usually rendered in reference to the god as "of Mars",
or "of war/warlike" ("martial")."

:-)

I hesitate to sign "Martin" here:

M.

[Andrej Bauer]

I was also thinking of renaming it. I could just go back to "tt", or
use a planet. But not Mars, I was rather thinking Saturn or Jupiter.
What are the inhabitants of Jupiter called?

[Francisco Mota]

"Jovian", apparently.

http://en.wikipedia.org/wiki/Jovian :

Jovian is the adjectival form of the god Jupiter, or the planet Jupiter. Its archaic form is Jovial.

http://en.wikipedia.org/wiki/Jovian_(fiction) :

In science fiction, a Jovian is an inhabitant of the planet Jupiter.

[Martin Escardo]

You should go for Andromeda (no pun intended), just in case.

[Vladimir Voevodsky]

Maybe "brazilians" with a small "b"?
V.

[Vladimir Voevodsky]

Jovians.

Jovian |ˈjōvēən|adjective1 (in Roman mythology) of or like the god Jove (or Jupiter).2 of or relating to the planet Jupiter or the class of giant planets to which Jupiter belongs.nouna hypothetical or fictional inhabitant of the planet Jupiter.

[Benno van den Berg]

Tropical type theory?

http://en.wikipedia.org/wiki/Tropical_geometry

Best,

Benno

--

[Marc Bezem]

Titanic type theory?

Offers maximal alliteration, plus handy connotations for various scenarios, including inconsistency.

Marc

[Egbert Rijke]

How about calling it Vulcan? Vulcans are noted for their attempt to live by reason and logic with no inference from emotion (so says wikipedia). Vulcan is their planet, so sending our proofs to Vulcan and let them figure out whether it's correct seems a right alternative to sending them to Brazil. Are there any Vulcans among us?

[Joyal, André]

Let us stay on earth, I do not wish to learn Klingon.
Here is a sample:

http://www.cs.ru.nl/~freek/comparison/comparison.pdf

Wizard? Gee-Whiz?

-André

---

From: HomotopyT...@googlegroups.com [HomotopyT...@googlegroups.com] on behalf of Egbert Rijke [e.m....@gmail.com]
Sent: Thursday, June 26, 2014 4:53 PM
To: Marc Bezem
Cc: HomotopyT...@googlegroups.com
Subject: Re: [HoTT] Isomorphic types are equal

[Vladimir Voevodsky]

On Jun 26, 2014, at 10:53 PM, Egbert Rijke <e.m....@gmail.com> wrote:

> How about calling it Vulcan? Vulcans are noted for their attempt to live by reason and logic with no inference from emotion (so says wikipedia). Vulcan is their planet, so sending our proofs to Vulcan and let them figure out whether it's correct seems a right alternative to sending them to Brazil. Are there any Vulcans among us?

The idea was that in Brazil (actually it was originally Bolivia) they may have some other measures of correctness and rationality than we do. The format of formal proofs however should be so well and so completely documented than even then they should be able to write their own proof checker (in their own weird Brazilian programming language).

V.