Sigma Oddity

[Martin Escardo]

The Sigma type constructor in MLTT of course has many uses. Under the
CH interpretation, it expresses a (strong) form of existence.

But also, it is said, Sigma types can be used to define subtypes, e.g.

Odds = Sigma(n:N). isOdd(n).
Evens = Sigma(n:N). isEven(n).

These types are isomorphic. Most people, perhaps based on the standard
set-theoretical interpretation of MLTT, would consider these two types
to be different.

However, even if the equality-reflection rule for the universe U in
which the types Odds and Evens live, producing an equality of type

Id U X Y

from any given judgemental equality

X=Y,

were added to MLTT, to get so-called extensional MLTT, one still
wouldn't be able to prove/inhabit the negated type

Id U Odds Evens -> 0. [Not provable, even in extensional MLTT.]

So, although extensional MLTT somehow refuses to accept that
isomorphic types are equal, it can't prove that they are not. Let's be
more precise.

This "oddity" arises much before we think of univalance, and, indeed,
is present in extensional MLTT, which is incompatible with
univalence, as we have just discussed.

In fact, it is much easier to reconcile intensional MLTT than
extensional MLTT with the above phenomenon: the univalence axiom UA is
consistent with intensional MLTT. So, even if we don't postulate UA,
its consistency explains this phenomenon: nothing prevents the type
Odds from being equal to Evens, in intensional MLTT. Moreover,
anything we can prove about one of these two types can be proved about
the other.

But how does one reconcile this phenomenon with extensional MLTT? On
the one hand, if we were to have an inhabitant of the type

Id U Odds Even,

in extensional MLTT, it would have to be unique, and so equality can't
amount to isomorphism in this case. On the other hand, it is
consistent that the type

Id U Odds Even

has an inhabitant. But what would this inhabitant be, if it happens to
exist? It is necessarily contingent: it would have to be a unique
isomorphism, but of course there isn't a canonical choice of an
isomorphism.

I think that this illustrates that it is difficult to deny the
inevitability of the univalence axiom on the grounds of some presumed
"naturality" of the equality reflection rule (as I heard some people
arguing). My contention is that the above argument shows that the
equality reflection rule for the elements of U is rather unnatural,
not because it contradicts univalence, but because it fails to
precisely determine the type Id U X Y in any useful (mathematical,
philosophical or practical) way.

Another type that arises in the above way is the fiber, or inverse
image of a point y:Y, under a function f:X->Y,

fiber f y = Sigma(x:X). f(x)=y.

One can read this as "the type of x's that are mapped to y by f".

But I think that this reading is problematic if taken too literally in
the set-theoretic sense (although it makes perfect sense in all models
of MLTT we currently have in mind, univalent or not).

For instance, consider the parity function f:N->2 that maps even
numbers to 0 and odd numbers to 1. Then its two fibers are
manifestations of the types Evens and Odds, intuitively, but this
cannot be expressed formally: there is no internal distinction between
these four types, and no particular fiber can be claimed to be a
manifestation of the type Evens, as opposed to the type Odds, for
instance, although an intuition guided by sets leads us to see the
type fiber f 0 as the same thing as the type Evens, but not
necessarily the type Odds.

QUESTION (to try to emphasize my point). Is there any sensible axiom
for MLTT (even if we didn't want to adopt it) that, in the presence of
the equality-reflection rule (or not), allows to prove the negation of

Id U Even Odds?

For example, certainly the K axiom is not such an axiom, even though
it denies univalence.

Martin

[Martin Escardo]

Of course I wrote the equality reflection rule the other way round in
the message below. :-) Martin

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

[Dan Licata]

On Oct 1, 2015, at 6:12 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

> QUESTION (to try to emphasize my point). Is there any sensible axiom
> for MLTT (even if we didn't want to adopt it) that, in the presence of
> the equality-reflection rule (or not), allows to prove the negation of
>
> Id U Even Odds?

I think intensional type analysis (typecase) is such an axiom/principle. If you can inspect the structure of types internally, then it is inconsistent to equate Evens and Odds.

Here is a simplified example in Agda:
https://github.com/dlicata335/hott-agda/blob/master/misc/Typecase.agda

Code is an inductive-recursive type containing codes for some finite types and Sigmas. If you had intensional type analysis for U, then you would use U where I use Codes in the file.

My simplified example is

IsTrue : Bool → U
IsTrue True = Unit
IsTrue False = Void

IsFalse : Bool → U
IsFalse True = Void
IsFalse False = Unit

Then we can prove the negation of

Σ (x : Bool). IsTrue x = Σ (x : Bool) IsFalse x

by defining a function

inspect : U → U
inspect (Σ Bool f) = f True
inspect _ = Unit

because then applying inspect to both sides of the assumed equality gives Unit = Void.

The same thing should work for your example, just use Nat and apply f to 0 instead.

-Dan

[Matt Oliveri]

Nuprl, can prove that, I'm pretty sure. The difference is not actually the presence of an additional axiom, but the absence of type annotations:

(0,*) in Evens (isEven 0 is unit, so use unit intro and sigma intro)
(0,*) in Odds (equality reflection)
* in empty (2nd projection, and isOdd 0 is empty)

In extensional type theory, the projections get stuck on type annotations, so the thing we prove doesn't equal empty.

I've been hung up on this since I learned about it from Andrej's Andromeda slides. But I'm on Nuprl's side, I'm OK with Evens and Odds being different. ETT seems strange to me too. What I can't figure out is why, intuitively, having type annotations protects you from ad-hoc isomorphisms. Are there actually different "implementations" of the projections at different types? I guess so; some of them need to silently apply the isomorphism. (But ETT's rules don't know that, so they just get stuck.)

[Michael Shulman]

I would say it's not that type annotations protect you from ad-hoc
isomorphisms, but that they prevent you from writing nonsense. It
seems to me that a type theory without type annotations is really only
half a type theory and half more like an untyped set theory. In set
theory, an ordered pair is "intrinsically" an ordered pair and you can
always extract its two components, regardless of what set your ordered
pair might itself be an element of. But in a fully typed type theory,
you can't take an element of a Sigma-type, forget that it was an
element of a particular Sigma-type, and still claim that it's somehow
"intrinsically" an ordered pair that you can extract the components of
(perhaps along the way claiming that it's also an element of some
other Sigma-type).

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

[Matt Oliveri]

I basically agree with that, just that:
- Nuprl is half untyped functional programming language, not half untyped set theory.
- "Nonsense" is a matter of perspective. Nuprl's types don't need to prevent you from dealing with untyped objects because untyped objects are not considered nonsensical in Nuprl.
- Since ETT embeds into Nuprl, one can interpret ETT using Nuprl's semantics, but this does not explain how ad-hoc isomorphisms are consistent with ETT. I was trying to understand that, coming from this direction.

How about structural set theories? If they have equality of sets (which, I guess, they may well not), then it seems like they might have the same "oddity" as ETT.

[Michael Shulman]

One doesn't generally use equality of sets in a structural set theory,
but it can certainly be included. I don't think this is particularly
odd from the structural-categorical point of view; the point there is
just that category theory in its usual formulation is agnostic about
equality of objects. It might be that there is a notion of equality
of objects that's stricter than isomorphism; it might even be that our
category is skeletal, so that isomorphic objects are equal (in a
non-univalent sense). Or it might not. Category theory doesn't
generally care.

[Andrej Bauer]

On Fri, Oct 2, 2015 at 12:12 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> QUESTION (to try to emphasize my point). Is there any sensible axiom
> for MLTT (even if we didn't want to adopt it) that, in the presence of
> the equality-reflection rule (or not), allows to prove the negation of
>
> Id U Even Odds?

Assuming equality reflection, an axiom you can add is that type
constructors are injective, for instance

Id A x y ≡ Id B u v
------------------------------
A ≡ B x ≡ u y ≡ v

and similarly for Σ (I am omitting some contexts here, we need to pay
attention to bound variables):

Σ (x:A) B ≡ Σ (y:C) D
---------------------------
A ≡ C B ≡ C[x/y]

If the type Id U Even Odds is inhabited then Even ≡ Odds, which would
give us isOdd(n) ≡ isEven(n), i.e.,

Σ (m:N) Id N n (2 * m + 1) ≡ Σ (m:N) Id N n (2 * m)

and by injectivity

2 * m ≡ 2 * m + 1.

I think this is quite similar to what Dan suggested. That is, his
assumptions imply injectivity of type constructors, right?

With kind regards,

Andrej

[Thorsten Altenkirch]

A well known addition would be to allow universe recursion which allows us
to access the representation of a type in U.
This also allows us to prove that type constructors are injective because
they are just constructors.

However, this conflates the idea of a type and a type code. Similar the
rejection of functional extensionality confuses functions and function
codes.

Vanilla ITT doesn’t introduce any primitives which allow us to observe the
intensional structure of infinite objects like functions or types. This is
sensible because these objects should be viewed extensionally, i.e. as
given by their behaviour and not the way they are constructed. However,
ITT is fundamentally incomplete because while it doesn’t provide any
intensional observations it falls short of identifying extensional equal
objects. HoTT overcomes this conceptual incompleteness.

So called “Extensional Type Theory” is actually in a sense
anti-extesnional because it is inconsistent with univalence i.e.
extensionality of types.

Btw, even in HoTT we can introduce the concept of a function code or a
universe of types code. However, if extensionality is not in some way
built into our theory there is no way to recover it.

Thorsten

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

[Dan Licata]

On Oct 2, 2015, at 4:07 AM, Andrej Bauer <andrej...@andrej.com> wrote:

> I think this is quite similar to what Dan suggested. That is, his
> assumptions imply injectivity of type constructors, right?

I think that with typecase you can prove injectivity, just as with listcase you can prove that :: is injective.

-Dan

[Martin Escardo]

Ok. But what does it *mean*? It all models I know, this seems to fail.

For example, it fails in the set-theoretical model, in realizability
models (and of course, in univalent models).

Let's write Id X x y as x=y now.

Consider the 0-univalence axiom: any two empty types are equal,

Pi(X:U).(X->0)->(Y->0)->X=Y.

Equivalently, any empty type is equal to the (canonical) empty type:

Pi(X:U).(X->0)->X=0.

This holds in the models mentioned above.

But now 0-univalence implies

(0 * 0) = (1 * 0)

and hence 0=1 by injectivity of constructors.

This shows that constructor-injectivity negates 0-univalence, and in
particular doesn't hold in the models mentioned above.

Perhaps I should reformulate the question. I have a sense that the
proponents of the equality-reflection rule have in mind the
set-theoretical model and similar models:

Question. Is there an axiom for Id-equality in MLTT such that
Id-equality of types (in a universe) turns out to be equality in the
set-theoretical interpretation (and related interpretations)?

(I don't think so.)

A related question, given Dan's answer on which Andrej's answer builds
in this.

Question. Suppose you work in a universe a la Tarski as Dan does. Is
there an axiom that only mentions the extensions [ c ] of the Codes c
and allows to prove that Even /= Odds?

(I don't think so either.)

(I think what I am trying to argue is that so-called extensional MLTT
is actually anti-extensional, like Thorsten said, but trying to invoke
mathematics rather than ideology to make this explicit. But I would
like to avoid a flame war in this discussion, and purely concentrate
on the mathematical facts/questions.)

Martin

[Jules Jacobs]

You could define the identity on sigma types as follows:

Id U (Sigma(a:A). f a) (Sigma(b:B). g b) = Id A B /\ Id f g

This would make Odds /= Evens, but it would make Odds = Sigma(n:N). isDivisibleByFour n \/ isDivisibleByFour (n+2).

[Jules Jacobs]

Sorry, should be Evens of course.

[Jules Jacobs]

If you want all empty types to be equal, then I think this might work:

Id U A B = (IsEmpty A * IsEmpty B) + EqU A B

EqU (A*B) (C*D) = Id U A C * Id U B D

etc.

One would have to check that all type constructors respect such an equality, but I think they do. It's a strange system though, trying to be like set theory in that empty sets at different types are equal, but non-empty sets of the same cardinality aren't.

[Martin Escardo]

What makes any notion of equality, in any mathematical theory, to
really be equality? The fact that we can replace equals for equals.

In MLTT, this is "transport" (old terminology: "cong"). This is
actually the recursion principle for the identity type (the induction
principle is J).

In set theory, the situation is similar. We have an axiom scheme
(meaning: countably many axioms, one for each syntactical
proposition), saying that we can replace equals for equals.

Operationally, these axioms are very useful, in both
theories. However, they don't tell us how to get any non-trivial
(non-tautological) equality to start with.

Let's consider set theory first: It is certainly the case that if two
sets are equal then they have the same elements:

forall(x,y). x=y -> forall(z). z in x iff z in y.

The extensionality axiom says that this implication is a (logical)
equivalence.

We are very used to this: if two sets have the same elements then they
are equal. But this doesn't follow from the definition of equality,
namely that we can substitute equals for equals (Leibniz
principle). It is really a postulate (the extensionality axiom).

I wouldn't say that this postulate is asserting some truth. I would
instead say that it is determining the nature of sets.

Let's abbreviate

forall(z). z in x iff z in y
by
Eq x y

so that we have the fact

forall(x,y). x=y -> Eq x y,

and so that the set-theoretic extensionality axiom says that this
implication is an equivalence.

You can see two things from this discussion: (1) The set-theoretical
axiom of extensionality has the same shape as the univalence axiom.
(2) There is nothing intrinsic to the notion of equality that would
require that two collections are equal if they have the same elements or
instead that they are isormorphic.

However, the way collections are set-up in MLTT makes it impossible,
by construction, to even formulate the question of whether two
collections have the same elements.

Intensional MLTT is "incomplete" in the sense that it fails to fully
specify the nature of equality, particularly in a universe of types.

Extensional MLTT specializes the notion of equality in an odd way so
as to prevent any reasonable resolution of the notion of equality in
the universe: neither the notion of "equal as having the same
elements" or "equal as being isomorphic" make any sense for
(so-called) extensional MLTT.

Martin

[Jules Jacobs]

However, the way collections are set-up in MLTT makes it impossible, 
by construction, to even formulate the question of whether two 
collections have the same elements. 

What if one added the following type to reflect x:A into the system:

A:Type, B:Type, x:B

-------------------

(x::A) : Type

With introduction rule:

A:Type, x:A

--------------

judge : (x::A)

And this rule:

p : (x::A)

----------

x : A

Then one could define equality on the universe as:

Id U A B = (forall b:B. (b::A)) * (forall a:A. (a::B))

It would automatically be the case that (0 * 1) = (0 * 0), Evens /= Odds, and it would allow you to prove that if there's no bijection between A and B then A /= B. Wouldn't say anything about (A,A) vs Bool -> A on its own, but could have additional rules that make them either equal or inequal.

Would be weird since it allows you to hypothesize 3::Bool, although any function that hypothesizes this can't be called since 3::Bool can't be proved.

Jules

[Jon Sterling]

Martin,

Thanks for the interesting & thoughtful note. A few remarks between the
lines...

On Fri, Oct 2, 2015, at 02:35 PM, Martin Escardo wrote:
>
> What makes any notion of equality, in any mathematical theory, to
> really be equality? The fact that we can replace equals for equals.
>
> In MLTT, this is "transport" (old terminology: "cong"). This is
> actually the recursion principle for the identity type (the induction
> principle is J).

I thought that "cong" was the old terminology for what is now often
called "ap"; "transport" is new terminology for what was frequently
called "subst".

Why doesn't it make sense to consider "equal as having the same
elements" in ETT? Yes, that exact interpretation is quite impossible,
but if we amend this to "equal as having the same elements & the same
equivalence relation", then this is *exactly* the definition of equality
of types in ETT (or, at least, MLTT 1979-1984). You may choose to have a
more intensional equality for the universe itself (that is, membership
in a universe vs typehood, which are two separate concepts in MLTT), but
this is by no means required (or ruled out). But this is a conversation
that has already been had on this list, so I won't re-hash it. [I also
am not trying to say, "This is the right way to do it, listen!", or
provoke any kind of flamewar; my remarks tonight are meant to emphasize
a position of pluralism within the design spectrum for type theory, and
note the usefulness of many different versions of equality.]

In MLTT 1979, you are right that you cannot express the question of
whether two types have the same elements/equivalence relations
*internally* in the direct way, but you can do so indirectly using the
identity type, which reflects exactly the judgmental equality, and
thence suffices to express that two types have the same equivalence
relation, if you have arranged the equality in the universe to coincide
with the equality of types/sets. In Nuprl, which is not ETT (but
contains it), you can even express this question internally as a
type/proposition; Nuprl extends ETT with (among other things) a kind of
"mathematics of the third order", where you can reason about terms &
computation.

By the way, I also agree with you that there is nothing about equality
(as a concept) that forces either of those interpretations... In some
sense, as you and Thorsten have noted, choosing isomorphism as the
equality of types is perhaps the most extensional option of all, but I
echo Matt in noting that the design continuum between ETT and Nuprl
(i.e. varying degrees of ability to talk about raw terms separately from
their types) can be extremely useful in practice, and is perfectly
justified intuitively; this doesn't mean that isomorphism as equality
wouldn't be useful, but let's just remember that nobody as yet has a
satisfactory meaning explanation for it, so it is certainly not yet
intuitionistically valid.

[By the way, for the reasons that Thorsten has so convincingly stated in
his lectures on cubical type theory, and elsewhere, I think it may have
been a mistake to have used the terminology "extensional" at all in the
context of type theory, since there are so many fine-grained
distinctions that can be lost. In particular, there is an inherent
conflict between "extensional" in the set-theoretic sense and
"extensional" in the "respects equality" sense; also, the use of the
term "extensionality" in relation to consequence and hypothetical
judgment tends to evoke for most people the idea of the classical
material consequence (a coincidence of truth values), as opposed to the
intuitionistic material consequence, which involves an effective
transformation of mathematical acts.]

Coming from a position of mathematical pluralism within the
intuitionistic framework, I think that trying to find the "correct /
real notion" of equality for type theory is perhaps not a super useful
thing to do, and I would like to avoid statements like "prevent any
reasonable resolution of the notion of equality in the universe", which
are highly questionable and perhaps less than constructive.

I don't think there is anything definitive at all about type theory such
that the particular way we have chosen to axiomatize equality should
require any kind of philosophical commitment on our parts; I won't take
a particular choice personally, since a given type theory is not a
definition of mathematical activity, but merely a reflection of some
portion of it. Type theory is *mathematics of the second order*, in
Brouwer's terminology, and is not definitive of mathematics of the first
order, and so we may simply choose any notion of equality which we find
useful, and that can be justified intuitively (i.e. via a meaning
explanation); thence many different type theories may flourish and be
used for different purposes, as we have seen with the three successful
(but profoundly different) lines of type-theoretic development (Swedish,
Ithacan and LF).

My message is, then—so long as we have in place a meaning explanation
for it, the particular choice of equality that we make does not affect
its worth or validity as defining a theory of types, but rather allows
us to vary the (idealized) mathematical activity that we have chosen to
reflect / simulate.

Best wishes,
Jon

[Andrej Bauer]

On Fri, Oct 2, 2015 at 8:25 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> Ok. But what does it *mean*? It all models I know, this seems to fail.
>
> For example, it fails in the set-theoretical model, in realizability
> models (and of course, in univalent models).

Well, you asked for some axioms and you got an answer.

Frankly, I am not really sure anymore what your asking "what does it
*mean*" means :-) As far as I can tell you'd like to internalize (in a
psychological sense) a formal concept, and I sympathize with that
because that's what I do as well (doesn't everyone?). But at least for
me more often than not the fuzzy feeling of "really knowing" a
mathematical concept comes only after I have struggled with using it
by rote, formally, and with little understanding of what it's for. I
distinctly remember that this was the case for "topology", "compact
space", "adjoint functor" and "cartesian closed category", to name a
few. I don't think lengthy semi-philosophical explanations helped
much, altough I liked to indulge in them.

Be that as it may, here is an explanation of the axiom of injective
constructors. Quite generally in mathematics we often think of
representing one kind of objects with another, for instance:

* words represent the elements of a group (for a given group presentation)
* lists represent finite sets
* Haskell programs represent computable maps
* measurable square-integrable maps [0,1] → R represent the elements
of the space L^2([0,1])
* etc.

Diagramatically, we have a quotient map

Represenatation → Objects

The representation may be more or less "free". When representing a
group with words the representation by arbitrary words is "more free"
than a representation by only the reduced words.

Logicians can recognize in this just the usual representation of
objects by language, in other words *interpretation*:

Language → Objects

and specifically

Type theory → Objects

It is important here *not* to view "Language" and "Type theory" as
"just syntactic stuff", Lawvere taught as the benefits of including
"just syntax" into the happy family of "truly mathematical" objects.

The axiom of injective constructors says that type theory is a "very
free" represenation of mathematical objects (whatever they are). It is
like words in the represenation of a group: one can discern how an
element of the group is built from the generators by looking at a
word. If we had type theory in which only normal-form terms were
allowed to appear that would be a bit like using only the reduced
words in a group presentation. These are of course just analogies, but
perhaps they can give someone some ideas on how things connect.

There is nothing wrong with having a "very syntactic" type theory (I
would prefer to say "very free"), just like there is nothing wrong
with having free groups. The "freeness" has one major advantage for
the working mathematicians: it let's us *calculate* and *manipulate*
constructions.

When one wants to understand type theory on its own terms, as a
fundation, as "starting from scratch", then the representation picture
above is not satisfactory and one is left with a simpler diagram:

Type theory

This is the "anti-model-theoretic" view of type theory. I have not
much to say about it, except that it really now becomes a problem in
"design of mathematics": what would you like type theory to stand for,
and what would you like to do with it? If the purpose is to provide a
foundation for mathematics, then I agree that the axiom of injective
constructors is a lousy one. If you're implementing a proof assistant
then it is a very tempting, if you can afford it.

With kind regards,

Andrej

[Egbert Rijke]

> If the purpose is to provide a

foundation for mathematics, then I agree that the axiom of injective
constructors is a lousy one. If you're implementing a proof assistant
then it is a very tempting, if you can afford it.

Why are the interests of 'providing a foundation for mathematics' and 'writing a proof assistant' at odds with each other?

 

With kind regards,

Andrej

[Andrej Bauer]

On Sat, Oct 3, 2015 at 9:08 PM, Egbert Rijke <e.m....@gmail.com> wrote:
> Why are the interests of 'providing a foundation for mathematics' and
> 'writing a proof assistant' at odds with each other?

They are not "at odds at each other" but they have different emphasis.

A human prefers a conceptually clean formulation of type theory, what
we might call "declarative" formulation.

A proof assistant prefers an algorithmic formulation, even at the
expense of conceptual minimality.

For instance, a common technique used in proof assistants is to have 3
different judgmental equalities:

1. Equality of terms a and b at type A.
2. Equality of terms a and b at a weak head-normal type A.
3. Equality of weak head-normal form terms a and b, at a type which is
either a variable or a weak head-normal form application.

Good luck selling something like this to a mathematician.

A proof assistant *always* works with a version of type theory that is
an elaboration (has more details) of what the human user perceives it
to be. That is, we have a representation

Proof assistant type theory → Human type theory.

The sort of extra details that are part of the proof assistant type
theory but not of human type theory are:

1) terms are tagged with locations in the source code (completely
irrelevant for mathematical aspects of type theory)
2) explicit universe indices which humans can't be bothered to write
down (and so they need to be reconstructed and inserted)
3) keeping track on which pieces of the context a term actually depends on
4) keeping a graph of dependencies between the variables in the
context (because saying that the context is a list is an
over-simplification of what is actually going on and what is actually
needed in some situations)
5) keeping track of "meta-variables" and their instantiations
6) keeping track of what would be a good concrete name for a given de
Bruijn index, so that we can print things in a reasonable way

The proof assistant type theory is "more free" than the human type
theory so that the proof assistant can more easily compute with it. It
is easier to compute with a type theory which has injective type
construtors, as that simplifies equality checking. However, if the
proof assistant type theory has injective constructors but the human
version does not, then the proof assistant will fail to recognize
human-equal types as equal, and that can be annoying.

Does this answer your question?

With kind regards,

Andrej

[Martin Escardo]

On 03/10/15 11:05, Andrej Bauer wrote:
> This is the "anti-model-theoretic" view of type theory.

I agree that type theory can be understood on it own sort of
"axiomatically" like set theory or Euclidean geometry (although, of
course, there are no axioms in the sense of 1st order logic).

> I have not much to say about it, except that it really now becomes a
> problem in "design of mathematics": what would you like type theory
> to stand for, and what would you like to do with it? If the purpose
> is to provide a foundation for mathematics, then I agree that the
> axiom of injective constructors is a lousy one.

OK, given this assertion, can we add a non-lousy axiom that proves
Odd/=Even, if I want it to be a foundation of mathematics (and have a
proof assistant)?

Best,
Martin

[Matt Oliveri]

Probably, if you consider axioms based on PER or set semantics to be sufficiently non-lousy.

[Peter Aczel]

Matt Oliveri wrote:

OK, given this assertion, can we add a non-lousy axiom that proves 
Odd/=Even, if I want it to be a foundation of mathematics (and have a 
proof assistant)?

I assume that  `Odd/=Even' is an abbreviation for Id(U, Odd, Even)->0, which depends on the universe U.  Presumably one can consistently have distinct universes U1, U2 in which both Id(U1, Odd, Even) and Id(U2, Odd, Even)->0 are inhabited.

But this is thinking of universes a la Tarski.  Maybe things are more subtle a la Russell, where Odd and Even are names of types which may be distinct in U1 and U2?

Peter A

--

[Martin Escardo]

"lousy" was Andrej's terminology, and I couldn't resist answering to him
with his own adjective. It was not meant to offend anyone: only to tease
him.

We can certainly talk about the NuPrl type theory, if we wish, but it is
significantly different from Martin-Loef type theories, in particular by
being based in an untyped universe of things, out of which every NuPrl
type is constructed by carving a subset, very much in the spirit of set
theory, as far as I understand.

You should not extrapolate any claim I make about Martin-Loef type
theories to NuPrl. In fact, I am not qualified to make any claim about
NuPrl, because I haven't studied it (and perhaps even the last sentence
of the previous paragraph is wrong).

All I am saying is this: While it may (or may not) make sense to add the
equality reflection rule to the first layer of types in MLTT (e.g. for
natural numbers N, for function types N->N etc.), adding the equality
reflection for the universe itself seems much more dubious to me.

Why? Well, because at the same time (1) you prevent equality from being
isomorphism (or equivalence to be precise) but (2) you still leave
equality in U largely undetermined (to the extent that the inhabitedness
of Id U Evens Odds is undecided).

Even with equality reflection, the nature of the type Id U X Y is
underspecified. So, although equality reflection rules out that this is
a type of isomorphisms, it doesn't, in particular, say that this is a
type of "pointwise equalities" (if we knew how to say pointwise equality
for two given hypothetical types, which, in my view, probably doesn't
make sense in MLTT).

I asked (and this was a genuine question) what "axioms" one can add to
such an equality-reflecting MLTT so that the meaning of Id U Evens Odds
is resolved.

Dan and Andrej gave related answers.

I think these answers are not (mathematically) satisfying, because it
relies on a syntactical view of the universe.

To make a comparison: we could also reflect induction principles for the
formation of elements of other types, such as, say, N->N, so that
equality becomes "equality of programs". (Or: add so-called Church's
Thesis as an axiom for MLTT, which is very much like LISP's quote.)

I see the type codes precisely as that: as codes. But when I speak of a
type, I don't mean a code c of the type but its extension [ c ] (using
Dan's notation).

I would regard a reasonable axiom for making Id U X Y empty as one that
refers to the extensions of X and Y, and not to codes. (Whatever
extension means, which would be affected by such an axiom.)

Martin

[Gabriel Scherer]

On Mon, Oct 5, 2015 at 8:16 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> OK, given this assertion, can we add a non-lousy axiom that proves
> Odd/=Even, if I want it to be a foundation of mathematics (and have a
> proof assistant)?

The intuitive proof of (Evens /= Odds) we all have in mind, drafted in
NuPRL by Matt Oliveri above, is something like
0 is even, so it is the first component of a pair in Evens.
If Evens = Odds, then this pair is also in Odds.
But the first component of the pair is 0, so 0 is odd.
0 is not odd: contradiction.

The third line in the informal reasoning above assumes that the first
projection of the same value seen at *distinct* sigma-types are equal
-- transport has not affected them.

You can formalize this, in Coq for example, as a "parametricity" axiom
on the first projection:

Axiom projT1_parametric : forall {A} (P1 P2 : A -> Type) (x : sigT P1)
(y : sigT P2),
JMeq x y -> projT1 x = projT1 y.

sigT (P : A -> Type) is Coq's notation for (Sigma(x:A). P A), with
projections projT1 and projT2.

JMeq is Conor Mcbride's heterogeneous equality: x and y live in
distinct sigma types (with a common first component). JMeq is defined
as an inductive that can only be inhabited when the two types are
equal and the two values are equal:
https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.JMeq.html

You could also reformulate this without using JMeq at all, which is
useful for those that don't trust Coq inductives.
The axiom would then be:
if w:(sigT P1 = sigT P2) and x:(sigT P1), then (projT1 x = projT1
(transport w x)).

A proof that (Evens /= Odds) using (only) this axiom is given below.

Fixpoint isEven n : Prop :=
match n with
| 0 => True
| 1 => False
| S (S n) => isEven n
end.

Definition isOdd n := not (isEven n).

Definition Evens := sigT isEven.
Definition Odds := sigT isOdd.

Print sigT.

Definition Even0 : Evens := existT _ 0 I.

Require Import JMeq.

Check eq_rect.

Axiom projT1_parametric : forall {A} (P1 P2 : A -> Type) (x : sigT P1)
(y : sigT P2),
JMeq x y -> projT1 x = projT1 y.

Goal not (Evens = Odds).
Proof.
intro HEO.
(* We call Odd0 the image of Even0 by transport from Evens to Odds *)
assert (exists (Odd0 : Odds), JMeq Even0 Odd0) as [ Odd0 HO ].
{ rewrite <- HEO. exists Even0. auto. }

(* we need parametricity for Odd0 to project to 0 *)
assert (projT1 Odd0 = 0) as H0.
{ replace 0 with (projT1 Even0); auto.
apply projT1_parametric; auto. }

assert (isOdd 0) as isOdd_0.
{ rewrite <- H0. apply projT2. }

contradiction isOdd_0.
{ constructor. }
Qed.

[Matt Oliveri]

On Monday, October 5, 2015 at 5:34:31 AM UTC-4, Martín Escardó wrote:

On 05/10/15 09:55, Matt Oliveri wrote:
> On Monday, October 5, 2015 at 2:16:03 AM UTC-4, Martín Escardó wrote:
>> OK, given this assertion, can we add a non-lousy axiom that proves
>> Odd/=Even, if I want it to be a foundation of mathematics (and have a
>> proof assistant)?
>
> Probably, if you consider axioms based on PER or set semantics to be
> sufficiently non-lousy.

"lousy" was Andrej's terminology, and I couldn't resist answering to him
with his own adjective. It was not meant to offend anyone: only to tease
him.

I had to refer to your requirements for an axiom somehow. :)

We can certainly talk about the NuPrl type theory, if we wish, but it is
significantly different from Martin-Loef type theories, in particular by
being based in an untyped universe of things, out of which every NuPrl
type is constructed by carving a subset, very much in the spirit of set
theory, as far as I understand.

You should not extrapolate any claim I make about Martin-Loef type
theories to NuPrl. In fact, I am not qualified to make any claim about
NuPrl, because I haven't studied it (and perhaps even the last sentence
of the previous paragraph is wrong).

(It's morally right, though not technically. After you carve a subset, you give an equivalence relation to use as the equality in the type. This is equivalent to giving a PER on the untyped universe. So a PER is like a subset combined with a setoid.)
I figured you are asking about MLTT, not Nuprl. I was suggesting that there could be axioms for MLTT that expose more of a Nuprl-style semantics without adopting a Nuprl-style syntax. But Gabriel Scherer's idea sounds less draconian.

All I am saying is this: While it may (or may not) make sense to add the
equality reflection rule to the first layer of types in MLTT (e.g. for
natural numbers N, for function types N->N etc.), adding the equality
reflection for the universe itself seems much more dubious to me.

Why? Well, because at the same time (1) you prevent equality from being
isomorphism (or equivalence to be precise) but (2) you still leave
equality in U largely undetermined (to the extent that the inhabitedness
of Id U Evens Odds is undecided).

Oh, is that what you were saying? (2) is what you're asking about. Regarding (1), the nice thing about unique proofs of equality in universes is that it lets type theory eat itself. Maybe there are other (good) ways to get type theory to eat itself, but we don't know any, right?

I asked (and this was a genuine question) what "axioms" one can add to
such an equality-reflecting MLTT so that the meaning of Id U Evens Odds
is resolved.

My proposal to try and axiomatize more of Nuprl or set theory's semantics in MLTT was also genuine. Just not very good: it would be a hack, since it makes the objects fundamentally untyped, even though the syntax tries to hide it. Gabriel's idea sounds good.

[Matt Oliveri]

Neat!
Is there a similar axiom to prove (nat->nat) /= (nat->bool)?

In Nuprl intuition, they're not equal because:
- You can wrap (x : T) into (fun _:nat => x : nat->T), and unwrap it with (f 0). unwrap o wrap = id.
- So if (nat->nat) = (nat->bool), you can wrap at one type and unwrap at the other, so the identity function is an isomorphism nat ~= bool.
- But there can be no such isomorphism.

[Gabriel Scherer]

I have re-done the proof that (Evens /= Odds) with an explicit
transport instead of JMeq, and it is slightly shorter. It is included
at the end of this e-mail.

> Is there a similar axiom to prove (nat->nat) /= (nat->bool)?

I have ran out of reflexion time, so I don't know.
The "parametricity" idea cannot be easily adapted to this case,
because the direct adaptation would require saying that the image and
the image in the transport are equal, and the images are of different
types.

I tried another approach which is to remark that there does not exist
three distinct values in bool. This suffices to prove (nat /= bool),
using injectivity of transport. But then lifting this to (nat -> nat)
and (nat -> bool), because instead of deriving a contradiction from
(transport w 0 = transport w 1), one need to derive a contradiction
from (transport w id 0 = transport w id 1); the axiom needed here
would be that (transport id) is injective, which feels arbitrary.
On the other hand, this proof technique allows to prove that the set
of injective functions from nat to bool is distinct from the set of
injective functions from nat to nat, without any axiom.

Parametric first projections, using transport and a parametricity axiom:

Definition transport {A B : Type} (w : A = B) (x : A) : B.
rewrite <- w. exact x.
Defined.

Axiom projT1_parametric :
forall {A} (P1 P2 : A -> Type) (w : sigT P1 = sigT P2),
forall (x : sigT P1), projT1 x = projT1 (transport w x).

Goal not (Evens = Odds).
Proof.
intro HEO.

pose (Odd0 := transport HEO Even0).

(* we need parametricity for Odd0 to project to 0 *)

assert (0 = projT1 Odd0) as H0.

{ replace 0 with (projT1 Even0); auto.
apply projT1_parametric; auto. }

assert (isOdd 0) as isOdd_0.

{ rewrite H0. apply projT2. }

contradiction isOdd_0.
{ constructor. }
Qed.

Proof of (injections nat nat) <> (injections nat bool), without axiom:

Definition three_diff {A} (x y z : A) := (x <> y) /\ (x <> z) /\ (y <> z).

Lemma no_three_bools : forall (x y z : bool), not (three_diff x y z).
Proof.
intros x y z.
destruct x; destruct y; destruct z; unfold three_diff; intuition.
Qed.

Lemma transport_inj : forall {A B : Type} (w : A = B) x y,
(transport w x = transport w y) -> x = y.
Proof.
intros A B w x y H.
unfold transport in H.
destruct w.
apply H.
Qed.

Definition injective {A B : Type} (f : A -> B) := forall x y, f x =
f y -> x = y.
Definition injections A B := sigT (fun (f : A -> B) => injective f).

Definition ternary_inj {A} (inj : injections nat A) :=
let (f, _) := inj in
three_diff (f 0) (f 1) (f 2).

Lemma no_ternary_bool : not (exists (f : injections nat bool), ternary_inj f).
unfold ternary_inj.
intros [[f Hinj] Hf]. generalize Hf. apply no_three_bools.
Qed.

Lemma ternary_nat : exists (f : injections nat nat), ternary_inj f.
assert (injective (fun (n : nat) => n)) as Hinj.
{ unfold injective. intuition. }
exists (existT _ (fun n => n) Hinj). unfold ternary_inj. unfold
three_diff. auto.
Qed.

Goal (injections nat nat <> injections nat bool).
intro H.
apply no_ternary_bool.
unfold ternary_inj. unfold three_diff.
destruct ternary_nat as [f Hf].
exists (transport H f).
destruct (transport H f) as [tf Hinj].
split; [ | split ]; intro Hab; apply Hinj in Hab; discriminate.
Qed.

[Andrej Bauer]

On Mon, Oct 5, 2015 at 3:00 PM, Gabriel Scherer
<gabriel...@gmail.com> wrote:
>> Is there a similar axiom to prove (nat->nat) /= (nat->bool)?
>
> I have ran out of reflexion time, so I don't know.

There is no such proof because it is consistent to assume that nat →
nat ≡ nat → bool.

Consider the model of type theory in which the types are cardinals and
the morphisms are all functions between cardinals. This is a skeleton
of the category of sets. Because nat → nat and nat → bool have the
same cardinality they are interpreted by the same cardinal, namely
2^ℵ₀.

> On the other hand, this proof technique allows to prove that the set
> of injective functions from nat to bool is distinct from the set of
> injective functions from nat to nat, without any axiom.

This is not much of a revelation since there are no injective
functions from natural numbers to booleans, quite obviously, and
uncountably many injective functions from natural numbers to natural
numbers.

With kind regards,

Andrej

[Gabriel Scherer]

In this cardinality model, it is also the case that (Evens = Odds). I
understood Matt's question as "what is a natural axiom allowing to
disprove (nat->nat = nat->bool), that would be weaker than injectivity
of pi-types?", as a variant of Martin question ("is there a natural
axiom allowing to disprove (Evens = Odds), weaker than injectivity of
sigma-types?").

(Fully agreed on the triviality of the result on injections. It was an
exploration of what can or cannot do with transport, hoping to find a
reasonable axiom, rather than for the value of the result itself.)

[Martin Escardo]

Interesting, Gabriel. And you don't use equality reflection.

However, parametricity is anti-classical, as is well known. A general
foundation of maths should be compatible with both classical mathematics
and constructive mathematics, which MLTT type theories seem to be.

One question I asked before was whether there is an axiom for

Id-equality in MLTT such that Id-equality of types (in a universe

[interpreted as a Grothendieck universe]) turns out to be equality in
the [constructive or classical] set-theoretical interpretation.

The reason I emphasize this is that people said to me privately that one
reason to add equality reflection is to make Id-types closer to "usual"
equality in mathematics. But if this is the case, then equality
reflection is far from enough.

Martin

[Andrej Bauer]

On Mon, Oct 5, 2015 at 3:38 PM, Gabriel Scherer
<gabriel...@gmail.com> wrote:
> In this cardinality model, it is also the case that (Evens = Odds).

Sorry, I didn't realize we also wanted Evens ≠ Odds at the same time
as Nat → Nat ≡ Nat → Bool. Here's a model which has Evens ≠ Odds and
Nat → Nat ≡ Nat → Bool at the same time.

I will first explain the semantic idea. Suppose we have a cartesian
closed category with a chosen exponential operation Exp that takes two
objects and produces their exponent Exp(A,B) = (B^A, ev_{A,B} : B^A ×
A → B). Suppose that for two fixed objects X and Y we have a
different, preferred exponent (Z, e : Z × X → Y). We can define a new
chosen exponential operation Exp' which is just like Exp, except at B
and A where we change it to Z:

Exp'(A,B) =
if A = X and B = Y then (Z, e) else Exp(A,B)

The new Exp' still gives us the cartesian closed structure. A slightly
more involved version of this ought to allow us to change dependent
products. The definition of Exp' uses excluded middle.

So, consider the category of sets, as usual. Because Exp(Nat, Bool) is
isomorphic to Exp(Nat, Nat), we can assume by the above trick that
Exp(Nat, Bool) actually equals Exp(Nat, Nat). So far I have done no
type theory at all.

Now interpret type theory in classical sets, with the Exp operation
(or its dependent version) which gives equality of Exp(Nat, Bool) and
Exp(Nat, Nat). This guarantees that Nat → Nat ≡ Nat → Bool will be
valid in the model. And unless we're playing strange tricks, it will
also turn out that Odds are interpreted as {1, 3, 5, 7, ...} and Evens
as {0, 2, 4, 6, ...}, and so they are different.

I think these ideas show that one can probably manipulate equality of
types quite arbitrarily.

With kind regards,

Andrej

[Andrej Bauer]

> Exp' which is just like Exp, except at B and A where we change it to Z:

"except at Y and X we change it to Z", of course.

[Andrea Vezzosi]

On Mon, Oct 5, 2015 at 11:59 AM, Gabriel Scherer
<gabriel...@gmail.com> wrote:
> On Mon, Oct 5, 2015 at 8:16 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> OK, given this assertion, can we add a non-lousy axiom that proves
>> Odd/=Even, if I want it to be a foundation of mathematics (and have a
>> proof assistant)?
>
> The intuitive proof of (Evens /= Odds) we all have in mind, drafted in
> NuPRL by Matt Oliveri above, is something like
> 0 is even, so it is the first component of a pair in Evens.
> If Evens = Odds, then this pair is also in Odds.
> But the first component of the pair is 0, so 0 is odd.
> 0 is not odd: contradiction.
>
> The third line in the informal reasoning above assumes that the first
> projection of the same value seen at *distinct* sigma-types are equal
> -- transport has not affected them.
>
> You can formalize this, in Coq for example, as a "parametricity" axiom
> on the first projection:
>
> Axiom projT1_parametric : forall {A} (P1 P2 : A -> Type) (x : sigT P1)
> (y : sigT P2),
> JMeq x y -> projT1 x = projT1 y.

Do you have some specific formulation of "parametricity" in mind that
inspires this axiom?

[Matt Oliveri]

On Monday, October 5, 2015 at 11:24:24 AM UTC-4, Martín Escardó wrote:

Interesting, Gabriel. And you don't use equality reflection.

However, parametricity is anti-classical, as is well known. A general
foundation of maths should be compatible with both classical mathematics
and constructive mathematics, which MLTT type theories seem to be.

But Gabriel's specific axiom doesn't seem anti-classical. It seems true in the classical set theory interpretation. There, transport is the identity function, so the axiom just says that the first projection functions out of two disjoint unions are the same when those disjoint unions are in fact the same.

One question I asked before was whether there is an axiom for
Id-equality in MLTT such that Id-equality of types (in a universe
[interpreted as a Grothendieck universe]) turns out to be equality in
the [constructive or classical] set-theoretical interpretation.

I would only know how to do that once you allow reasoning about type membership. That's more natural in a Nuprl-like system than MLTT, but still probably possible, by thinking of the typed terms as representatives of untyped objects, and exposing a way to say that terms of different types represent the same untyped object. Then you could have a proposition/type saying that [the untyped object represented by] a term of one type is a member of another type.

But this does not seem necessary for proving any of the disequalities so far: you just need untyped beta/computation rules.

(All of this seems completely antithetical to HoTT and structuralism.)

[Gabriel Scherer]

On Mon, Oct 5, 2015 at 5:55 PM, Andrea Vezzosi <sanz...@gmail.com> wrote:

Do you have some specific formulation of "parametricity" in mind that
inspires this axiom?

I think the name was not well-chosen. The intuition comes from the fact that, at first reading, what goes wrong (without the axiom) in the (Evens /= Odds) proof attempt seems to be the fact that the first projection does something different when at type Evens and at type Odds. (In fact, what matters is the interaction between the first projection and transport, but that is less immediate in the evil set-theoretic model where transport is the identity); the intuition for the formulation was to say that projT1, as an untyped counterpart, would return the same first-component at all pair types -- with the extra transport sprinkled in for type-checking purposes. So that would be parametricity in the ML sense "types can be erased".

In retrospect what the axiom really talks about is the relation between transport and projection, and that is even clearer with the following reformulation, that still allows to prove (Evens /= Odd):

Axiom transport_projT1 :
  forall {A1 A2} (P1 : A1 -> Type) (P2 : A2 -> Type)
         (wA : A1 = A2) (wS : sigT P1 = sigT P2),
    forall (x : sigT P1), transport wA (projT1 x) = projT1 (transport wS x).

(Apologies for any confusion caused by the relatively improper use of "parametricity" here.)

[Martin Escardo]

On 05/10/15 23:06, Matt Oliveri wrote:
> (All of this seems completely antithetical to HoTT and structuralism.)

:-)

Yes. But even before you consider HoTT axioms, MLT theories, with or
without equality reflection, but without induction on the universe (i.e.
with an open-ended universe a la Russell), can't distinguish equivalent
types, as the structuralist view has (and to which I subscribe).

If you want to talk about subsets of N, and distinguish them, you can: a
subset of N is simply a map N->Prop (where Prop is the type of
subsingletons), and we do have that even,odd:N->Prop are different
subsets of N. However, when you Sigma them, they become
undistinguishable. This may be counter-intuitive, if one's intuition
comes from an untyped, set-theoretical background, but this is, from a
structuralist point of view, the wrong intuition. Of course, it is an
entirely different matter whether people choose to be structuralist or
not, but MLTT is compatible with this point of view, at least with
open-ended universes a la Russell, and the univalence axiom makes this good.

Martin

[Thorsten Altenkirch]

Just to blow into the same horn.

Given oddP,evenP : Nat -> Prop
There is a property P :(Nat -> Prop) -> Prop which distinguishes them,
namely
P(Q) = Q 0

But given Odd = Sigma n:Nat.oddP n, Even = Sigma n:Nat.evenP n with
Odd,Even : Type
There is no P : Type -> Prop which distinguishes them.

Unless you assume that you can look into the structure of a type.

I know that the evening star and the morning star are the same. But I was
asking wether the name of the star starts wit ³E².
:-)

Thorsten

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

[Gabriel Scherer]

A few extra remarks.

(1) I have thought more about Matt's question of how to internalize in MLTT the "untyped reasoning" in general. I think that an interesting answer is injectivity of type constructors.

Injectivity is a consequence of the "untyped" or "naive set-theoretic" view that types are sets of values (living independently from their types, hence "untyped"), and that equality of types has the rather evil (in category-theory sense) meaning that the sets have the exact same elements (by opposition to: modulo isomorphism). If two sigma-types have "exactly" the same pairs, then in particular the domains of the first components are equal, and for a fixed first component the domains of the second are equal. Note that (propositional) injectivity of dependent type connectives is less disturbing than injectivity of non-dependent products and functions, as it is compatible with identifying all Sigma(x : 0).A, and identifying all Pi(x : 0).A --- but not Sigma(x : A).0 or Pi(x : A).1.

Conversely, injectivity can also be seen as *claiming* that this evil set-theoretic notion of equality is the right one: if all base types satisfy the fact that only same-elements types are equal, then injectivity extends this property to all types.

(2) I am not sure that the projT1/transport axioms proposed above are weaker than injectivity -- it would be interesting. In particular, it now appear to me that the second as transport_projT1 implies a property I find much too strong, which is that transporting along a endo-equality (A = A) is the identity:

Lemma transport_trivial : forall {A} x (w : A = A), transport w x = x.
Proof.
  intros A x wA.
  pose (triv := fun (_ : A) => True).
  pose (b := existT triv x I).
  assert (x = projT1 b) as Hx1 by auto.
  assert (x = projT1 (transport eq_refl b)) as Hx2 by auto.
  rewrite Hx1 at 1. rewrite Hx2.
  apply transport_projT1.
Qed.

[Matt Oliveri]

(1) I don't agree that injectivity of type constructors properly captures untyped reasoning. But first...

(2)
I think your projT1 axioms are weaker than general injectivity of type formers. (It may somehow imply injectivity of sigT, but that's just one type former.) transport_trivial is logically equivalent to UIP, right? It basically says loops (A = A) are trivial. So that contradicts HoTT, but was already true in ETT. I had taken for granted that untyped reasoning was even less HoTT-like than UIP. In fact, by proving transport_trivial, you seem to have shown that UIP is a consequence of untyped reasoning.

Back to (1):
Untyped reasoning is consistent with type extensionality principles like set extensionality. Injectivity of type formers would contradict this. This kind of extensionality really kicks in with type formers that do not have their own intro/elim forms. In set theory, intro/elim forms are not even primitive, and the "primitive type formers"--like unordered pair, union, and subset (separation axiom)--often give you redundant descriptions of the same set.

Say you have some set Bool := {true,false}. (Never mind what true and false are.) Well you can subset that down to just true, and just false, then union those back together. Injectivity of type formers would say you get a different type, but set extensionality says it's the same as Bool. (Technically, set theory doesn't have type formers at all, but Nuprl does. I started with set theory since it's more familiar.)

In Nuprl, you have the type formers of MLTT, but also things like intersection, union, and subset. So you could actually express the above reconstitution of Bool from singletons, and ask if it's the same type. Nuprl is actually on the fence about this. Injectivity of type formers, and PER extensionality give different answers. This shows that untyped reasoning does not entail injectivity of type formers.

Also, injectivity of type formers does not entail untyped reasoning, since it's modeled by a universe construction (as someone pointed out earlier in the thread), which can be carried out in a fully typed system.

What seems to happen a lot though is that for the type formers of MLTT, because there are corresponding intro forms as the canonical forms of elements, untyped reasoning lets you distinguish types based on the structure (internal structure, as in programming datatypes) of their elements, which is more intensional than univalence, but compatible with set-extensionality-like principles.

[Martin Escardo]

On 06/10/15 15:19, Gabriel Scherer wrote:
> Conversely, injectivity can also be seen as *claiming* that this evil
> set-theoretic notion of equality is the right one: if all base types
> satisfy the fact that only same-elements types are equal, then
> injectivity extends this property to all types.

But notice that injectivity doesn't hold in the set-theoretical
interpretation of types, as I have already illustrated in a previous
message in this thread:

We have that the cartesian products 0*0 and 0*1 of the empty set 0
and the one-element set 1 are equal (empty) sets, but from
injectivity of Sigma we would get that 0=1, which of course is not
the case.

What emerges from this discussion is that people have different views
of types:

(1) Types are certain terms of a certain formal language. Call them
type expressions. This is a meta-theoretic concept.

(2) Types are collections of things. These elements are gathered from
an already-existing super-collection of things. These things can be
concrete (pre-terms) or come from abstract set theory, in which case
the role of type theory is just to impose a type discipline into the
untyped world of sets.

(3) Types are collections of elements, but in a fundamentally
different conception of collection from that of set theory, e.g. much
closer to elementary-topos theory, corresponding to a "structural"
point of view.

For example, in this view, we have the concept of natural numbers
type, in which it doesn't matter how this type is "implemented
concretely". What is important is what we can do with it (recursion,
or more generally induction). So, for instance, in Agda notation, if
you wrote

data N : Set where
z : N
s : N -> N

or

data Nat : set where
zero : Nat
succ : Nat -> Nat

this would just reflect your preference of notation and not your view
of what the natural numbers type is. More subtly, the type

data N' : Set where
zero' : N'
l : N' -> N' -- think of lambda n. 2*n + 1
r : N' -> N' -- think of lambda n. 2*n + 2

cannot be distinguished from the types N or Nat, and moreover, can be
equipped with a function succ' and induction/recursion combinators
such that the structure (N',zero',succ') is indistinguishable, from a
behavioural point of view, from (N,s,z) or (Nat,zero,succ).

(4) Types are certain elements of an inductively defined type(!) of
type codes. This is gives a universe of types a la Tarski. Here type
codes are an object-level concept (losely corresponding to the
meta-level type expressions).

This, of course, requires clarification, as we need to know in advance
what a type is in order to be able to define a type of type codes. You
can take e.g. (2) or (3) as your basis.

(5) As in (2) or (3), but also allow types to live in a
non-inductively defined "universe" of types. A universe a la Russell.

(6) Generalizing (5), and with either (2) or (3) in view (or perhaps
other possibilities), don't try to "exhibit" all types, as opposed to
item (4). Allow for types that you don't know where they come from or
how they have been "constructed". All you need to know is how you
operate with them. We collect these types in an "open-ended"
universe. This view is compatible with (4), which gives a closed
universe living inside the open-ended universe.

Of these views, I personally discard (1) as the primary view of
types. But of course (1) is still important: it gives the notion of
definable type. We may want to know (meta-theoretically speaking) what
special properties definable types do have. Then (4) allows us to
internalize the notion of definable type, so that we can ask similar
questions "internally", rather than meta-theoretically.

I also discard (2), because my objective is not to organize untyped
things into typed things, but rather understand things intrinsically
or structurally, independently of how they are implemented, in the
spirit of (3).

Now, clearly,, what "equal" should mean for types does depend on which
of the above views (1)-(6) one subscribes to.

What is interesting is that the commitment of MLT theories without
equality reflection is minimal, and compatible with each of the above
views, but of course not all of them at the same time.

The structural view (3) leads to understanding Id-equality of types as
type equivalence(~isomorphism), and one can say that the univalence
axiom precisely captures the structural point of view.

The equality reflection rule, on the other hand, only partially
determines type equality, and rules out (3). It tries to capture (2),
but it doesn't. More is needed in addition to equality reflection in
order to capture (2), and it is not clear what it is.

In any case, without further rules or axioms, what MLTT, of any of the
received varieties/stages, says about type equality is not enough to
make interesting positive or negative type identification/distinctions
when working at the object- or mathematical-level inside type theory.

Martin

[Gabriel Scherer]

On Tue, Oct 6, 2015 at 11:50 PM, Matt Oliveri <atm...@gmail.com> wrote:
> (1) I don't agree that injectivity of type constructors properly captures untyped reasoning.

Sorry for not being specific enough. I am not claiming that injectivity captures the full details of relying on an untyped model (for this I think, as you somewhat sketched in a previous message, that we could internalize the forgetful map from typed terms to their erasure into a uni-type of dynamic values, with a counterpart inside this type of each term former). The specific (partial) aspect I was trying to capture, and for which I think injectivity is a nice answer, is the idea that "equal sets have the *exact* same elements". This is weaker (I think?) than fully buying untyped model, and it is precisely the aspect I find interesting.

I also agree that it makes no sense to claim injectivity of union and intersection; those are not "structural" type formers in the sense that they do not determine the head structure of their canonical inhabitants. Injectivity only makes sense for the type connectives that reflect term formers already present in the untyped model.

On UIP: wouldn't be consistent to assume two different identity proofs (say (w1 /= w2 : Unit -> Unit)) whose transport function are (pointwise) equal to the identity?
On another note, it is also known that equality reflection implies UIP (http://ncatlab.org/nlab/show/extensional+type+theory). (That said we could have OTT-inspired type theories where definitional equalities actually computes, and there UIP and identity reflection might be compatible with a model where equalities are not interpreted as the identity).

On Wed, Oct 7, 2015 at 1:21 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

But notice that injectivity doesn't hold in the set-theoretical
interpretation of types, as I have already illustrated in a previous
message in this thread:

    We have that the cartesian products 0*0 and 0*1 of the empty set 0
    and the one-element set 1 are equal (empty) sets, but from
    injectivity of Sigma we would get that 0=1, which of course is not
    the case.

Sorry for being possibly naive on this question, but is this counter-example really correct? My understanding of is that injectivity applied to Sigma(x:0).0 and Sigma(x:0).1 gives you the following (propositional equalities):

  0 = 0

and

  forall (x:0), 0 = 1

As an instance of the general pattern:
  Sigma(x:A1).B1 = Sigma(x:A2).B2
  implies
  Sigma(w:A1=A2). Pi(x:A1), B1 x = B2 (transport w x).

  (or possibly the squashing of that, if you want a canonical principle)

I think it is consistent to have 0 = 1 (propositionally) under the assumption (x:0).

Building non-dependent pairs on top of Sigma requires a strong elimination: A*B defined as Pi(x:2).(if x then A else B). Then a naive set-theoretic model where Pi(x:A).B is the set of functions from A to the union of Bs validates (0*0)=(0*1) and is incompatible with injectivity. But we could also define Pi(x:A).B as an A-indexed family of sets (rather than a set itself), and this other, less standard naive set-theoretic model would invalidate (0*0)=(0*1). (I think this is related to Matt Oliveri's remark that union/intersection are incompatible with injectivity: defining Pi in terms of set-theoretic union gets us in trouble.)

[Andrew Polonsky]

Dear Martin,

I appreciated your comments and the discussion that followed, but I must admit I missed the premise.

  Id U Odds Evens -> 0.  [Not provable, even in extensional MLTT.] 

I don't see this.

Where is the mistake in the following derivation?

Assume Odd/Even : Nat -> U are defined by recursion.

Let context G = (H : Id U Odds Evens).

G |- Odds = Evens : U

G |- (0,p) : T(Evens)

------------------------------

G |- (0,p) : T(Odds)

-----------------------------------------(1)

G |- (0,p) : (n:NN) x T(Odd(n))

------------------------------------------(2)

G |- pi2(0,p) : T(Odd(pi1(0,p)))

G |- pi1(0,p) = 0 : NN

---------------------------------

G |- pi2(0,p) : T(Odd(0))

----------------------------

G |- false.

1) Here NN = T(Nat) are the actual numbers, and (x:A) x B is the actual sigma. (In Type.)

2) Some formulations of MLTT use another elimination rule for sigma types.

If that makes all the difference, then we have a new answer to your question.

Best,

Andrew

On Friday, October 2, 2015 at 12:12:17 AM UTC+2, Martín Escardó wrote:

The Sigma type constructor in MLTT of course has many uses. Under the
CH interpretation, it expresses a (strong) form of existence.

But also, it is said, Sigma types can be used to define subtypes, e.g.

  Odds  = Sigma(n:N). isOdd(n).
  Evens = Sigma(n:N). isEven(n).

These types are isomorphic. Most people, perhaps based on the standard
set-theoretical interpretation of MLTT, would consider these two types
to be different.

However, even if the equality-reflection rule for the universe U in
which the types Odds and Evens live, producing an equality of type

  Id U X Y

from any given judgemental equality

 X=Y,

were added to MLTT, to get so-called extensional MLTT, one still
wouldn't be able to prove/inhabit the negated type

  Id U Odds Evens -> 0.  [Not provable, even in extensional MLTT.]

So, although extensional MLTT somehow refuses to accept that
isomorphic types are equal, it can't prove that they are not. Let's be
more precise.

This "oddity" arises much before we think of univalance, and, indeed,
is present in extensional MLTT, which is incompatible with
univalence, as we have just discussed.

In fact, it is much easier to reconcile intensional MLTT than
extensional MLTT with the above phenomenon: the univalence axiom UA is
consistent with intensional MLTT. So, even if we don't postulate UA,
its consistency explains this phenomenon: nothing prevents the type
Odds from being equal to Evens, in intensional MLTT. Moreover,
anything we can prove about one of these two types can be proved about
the other.

But how does one reconcile this phenomenon with extensional MLTT? On
the one hand, if we were to have an inhabitant of the type

  Id U Odds Even,

in extensional MLTT, it would have to be unique, and so equality can't
amount to isomorphism in this case. On the other hand, it is
consistent that the type

  Id U Odds Even

has an inhabitant. But what would this inhabitant be, if it happens to
exist? It is necessarily contingent: it would have to be a unique
isomorphism, but of course there isn't a canonical choice of an
isomorphism.

I think that this illustrates that it is difficult to deny the
inevitability of the univalence axiom on the grounds of some presumed
"naturality" of the equality reflection rule (as I heard some people
arguing). My contention is that the above argument shows that the
equality reflection rule for the elements of U is rather unnatural,
not because it contradicts univalence, but because it fails to
precisely determine the type Id U X Y in any useful (mathematical,
philosophical or practical) way.

Another type that arises in the above way is the fiber, or inverse
image of a point y:Y, under a function f:X->Y,

 fiber f y = Sigma(x:X). f(x)=y.

One can read this as "the type of x's that are mapped to y by f".

But I think that this reading is problematic if taken too literally in
the set-theoretic sense (although it makes perfect sense in all models
of MLTT we currently have in mind, univalent or not).

For instance, consider the parity function f:N->2 that maps even
numbers to 0 and odd numbers to 1. Then its two fibers are
manifestations of the types Evens and Odds, intuitively, but this
cannot be expressed formally: there is no internal distinction between
these four types, and no particular fiber can be claimed to be a
manifestation of the type Evens, as opposed to the type Odds, for
instance, although an intuition guided by sets leads us to see the
type fiber f 0 as the same thing as the type Evens, but not
necessarily the type Odds.

QUESTION (to try to emphasize my point). Is there any sensible axiom
for MLTT (even if we didn't want to adopt it) that, in the presence of
the equality-reflection rule (or not), allows to prove the negation of

   Id U Even Odds?

For example, certainly the K axiom is not such an axiom, even though
it denies univalence.

Martin

[Matt Oliveri]

On Wednesday, October 7, 2015 at 4:10:58 AM UTC-4, Gabriel Scherer wrote:

On Tue, Oct 6, 2015 at 11:50 PM, Matt Oliveri <atm...@gmail.com> wrote:
> (1) I don't agree that injectivity of type constructors properly captures untyped reasoning.

Sorry for not being specific enough. I am not claiming that injectivity captures the full details of relying on an untyped model (for this I think, as you somewhat sketched in a previous message, that we could internalize the forgetful map from typed terms to their erasure into a uni-type of dynamic values, with a counterpart inside this type of each term former). The specific (partial) aspect I was trying to capture, and for which I think injectivity is a nice answer, is the idea that "equal sets have the *exact* same elements". This is weaker (I think?) than fully buying untyped model, and it is precisely the aspect I find interesting.

I also agree that it makes no sense to claim injectivity of union and intersection; those are not "structural" type formers in the sense that they do not determine the head structure of their canonical inhabitants. Injectivity only makes sense for the type connectives that reflect term formers already present in the untyped model.

OK.

On UIP: wouldn't be consistent to assume two different identity proofs (say (w1 /= w2 : Unit -> Unit)) whose transport function are (pointwise) equal to the identity?
On another note, it is also known that equality reflection implies UIP (http://ncatlab.org/nlab/show/extensional+type+theory). (That said we could have OTT-inspired type theories where definitional equalities actually computes, and there UIP and identity reflection might be compatible with a model where equalities are not interpreted as the identity).

Oh I see what I skipped. transport_trivial only gives that paths are "extensionally" unique, in that their transport behavior is always the identity. Without univalence, this does not imply UIP. But it still contradicts univalence. (And why would you want distinct identity proofs that all act like refl?)

On Wed, Oct 7, 2015 at 1:21 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

But notice that injectivity doesn't hold in the set-theoretical
interpretation of types, as I have already illustrated in a previous
message in this thread:

    We have that the cartesian products 0*0 and 0*1 of the empty set 0
    and the one-element set 1 are equal (empty) sets, but from
    injectivity of Sigma we would get that 0=1, which of course is not
    the case.

Sorry for being possibly naive on this question, but is this counter-example really correct? My understanding of is that injectivity applied to Sigma(x:0).0 and Sigma(x:0).1 gives you the following (propositional equalities):

  0 = 0

and

  forall (x:0), 0 = 1

As an instance of the general pattern:
  Sigma(x:A1).B1 = Sigma(x:A2).B2
  implies
  Sigma(w:A1=A2). Pi(x:A1), B1 x = B2 (transport w x).

  (or possibly the squashing of that, if you want a canonical principle)

I think it is consistent to have 0 = 1 (propositionally) under the assumption (x:0).

I think you lucked out. What if he had said 0*0 = 1*0?

[Matt Oliveri]

The mistake is the line

G |- pi1(0,p) = 0 : NN

.

(0,p) is actually tagged with the predicate Even, but the pi1 is tagged with Odd. The beta rule doesn't apply, in regular ETT. In Nuprl it does, since terms truly have no type annotations. This is the difference we've been discussing between ETT and systems like set theory and Nuprl.

[Gabriel Scherer]

> I think you lucked out. What if he had said 0*0 = 1*0?

Indeed. Thinking more of the matter, I'm convinced that injectivity is incompatible with the fact that two types are equal if and only if they have the same inhabitants.

(I feel that the conversation has been going on a tangent that is not so relevant to the hott mailing-list, so I'll try to resist the various remaining questions/puzzles in the short term. Thanks for the interesting discussion!)

--

[Andrew Polonsky]

On Wednesday, October 7, 2015 at 1:19:25 PM UTC+2, Matt Oliveri wrote:

The mistake is the line
G |- pi1(0,p) = 0 : NN

I am using the following projection rule for disjoint union of types.

Gamma |- A type

Gamma, a:A |- B type

Gamma |- p : (a:A) x B

-------------------------------

Gamma |- pi1(p) : A

Gamma |- pi2(p) : B[a:=pi1(p)]

(0,p) is actually tagged with the predicate Even, but the pi1 is tagged with Odd. The beta rule doesn't apply, in regular ETT. In Nuprl it does, since terms truly have no type annotations. This is the difference we've been discussing between ETT and systems like set theory and Nuprl.

In the previous message (0,p) is "tagged" with Odd in the line that precedes it.

I am not sure what you mean by "pi1 is tagged with..."  Is it something that comes up when the projections are defined using the other (inductive) eliminator?  I actually doubt that that would make such a big difference, but if it does -- that is really, really interesting!

Cheers,

Andrew

[Andrej Bauer]

Dear Andrew,

in type theory with equality reflection you have to explicitly
annotate the types of all applications and projections.
With the annotations your derivation becomes:

G |- Odds = Evens : U

G |- pair_Evens 0 p : T(Evens)
------------------------------
G |- pair_Evens 0 p : T(Odds)
-----------------------------------------(1)
G |- pair_Evens 0 p : (n:NN) x T(Odd(n))
------------------------------------------(2)
G |- pi2_Odds (pair_Evens 0 p) : T(Odd(pi1_Odds (pair_Evens 0 p)))

And we are now stuck because pi2_Odds does not match pair_Evens, so we
cannot reduce.
I cheated a little bit. The correct annotations would be something like

pairs_{n : NN . T(Even(n))}

and

pi2_{n : NN . T(Odd(n))}

Andromeda protects you from such mistakes (and other pitfalls) by
keeping track of the annotations.

There is no proof of Id U Evens Odd → 0 because it is consistent with
type theory that in fact Evens ≡ Odds. (Consider the cardinal model I
described earlier.)

With kind regards,

Andrej

[Michael Shulman]

On Tue, Oct 6, 2015 at 4:21 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> The equality reflection rule, on the other hand, only partially
> determines type equality, and rules out (3). It tries to capture (2),
> but it doesn't. More is needed in addition to equality reflection in
> order to capture (2), and it is not clear what it is.

It's pretty clear to me what it is: the axiom of extensionality of
ZFC. Approach (2) is trying to use the wrong tool for the job. If
you want types to be determined by some collection of pre-existing
things that belong to them, then that "belonging" ought to be a
proposition like ZFC's ∈, not a judgment like type theory's :.
Characterizing equality of types is all about different kinds of
extensionality -- univalence is of course a structural sort of
extensionality -- but extensionality is about the *behavior* of
something, and a typing judgment a:A is not *behavior* since it is
metatheoretic. So to formulate an extensionality axiom for which the
relevant kind of "behavior" is membership of pre-existing elements,
you need membership to be object-theoretic, as it is in set theory.

Mike

[Andrew Polonsky]

Dear Andrej,

in type theory with equality reflection you have to explicitly
annotate the types of all applications and projections.

I am not sure how to read your claim.  Some possibilities:

1) ETT is not just ITT + reflection rule, you also add new notational discipline;

2) term constructors are always annotated, even in ITT, just implicitly;

3) the annotations are indeed not in Martin-Lof [1984], but they really should be;

4) when implementing ETT-like type systems, you really should add annotations to block unwanted reductions.

A priori, I am not opposed to any of the above.  But it matters which one you mean.

There is no proof of Id U Evens Odd → 0 because it is consistent with
type theory that in fact Evens ≡ Odds. (Consider the cardinal model I
described earlier.)

Could you add some details about this model?  I am curious how you make it stable under substitutions.

In particular, I don't think it suffices to simply pick any bijection between [A] and #[A], for the set-theoretic interpretation of each type A.  The choices

{b_A : [A] \iso #[A]}_A in types

must be "coherent" so that, e.g. given

 

f : A->B,

g : B->C,

b_{A->C}[\x.g(fx)] = b_{A->C}([g] o [f])

I guess this can be ensured by some kind of invariance inductively, but it's not completely obvious.

Cheers,

Andrew

[Andrej Bauer]

On Wed, Oct 7, 2015 at 5:53 PM, Andrew Polonsky
<andrew....@gmail.com> wrote:
> I am not sure how to read your claim. Some possibilities:
>
> 1) ETT is not just ITT + reflection rule, you also add new notational
> discipline;

In nice enough type theories you can get away without such
annotations. ITT is one of them.

> 2) term constructors are always annotated, even in ITT, just implicitly;

In ITT as we usually know it the annotations are not needed.

> 3) the annotations are indeed not in Martin-Lof [1984], but they really
> should be;

Yes, they should be annotated, or else very strange things happen. I
spoke about it in Paris at the seminar.

> 4) when implementing ETT-like type systems, you really should add
> annotations to block unwanted reductions.

Yes. I see no way around it.

>> There is no proof of Id U Evens Odd → 0 because it is consistent with
>> type theory that in fact Evens ≡ Odds. (Consider the cardinal model I
>> described earlier.)
>
> Could you add some details about this model? I am curious how you make it
> stable under substitutions.

The category of cardinals and functions is skeletal. There are no
coherence issues as isomorphic objects are equal. Or am I making a
mistake thinking that coherence problems won't arise? (How could
they?)

With kind regards,

Andrej

[Andrew Polonsky]

Yes, they should be annotated, or else very strange things happen. I
spoke about it in Paris at the seminar.

 Sure.

You "restore" subject reduction not by adding missing typings – for which you need injectivity of type constructors – but by forbidding "inconvenient" reductions.

Nothing wrong with that.

But it's a bit funny, isn't it?

If simplifying a term makes its type illegal, intuitively one would think it never should have been given that type in the first place.

The category of cardinals and functions is skeletal. There are no
coherence issues as isomorphic objects are equal. 

You are right, it's not really a "coherence" problem, nor indeed a real problem.

More an observation that the interpretation of  *terms* is not compositional, but factors through the set-theoretic semantics, followed by the globally chosen quotient/isomorphisms.

Cheers,

Andrew

[Andrej Bauer]

> You "restore" subject reduction not by adding missing typings – for which
> you need injectivity of type constructors – but by forbidding "inconvenient"
> reductions.
> Nothing wrong with that.
>
> But it's a bit funny, isn't it?

I rather think that the unannotated type constructs are a bit funny.
They're missing a lot of information which needs to be reconstructed,
and then you have to dance a little dance around them to get the
reconstruction working. From the point of view of
denotational/categorical semantics it makes perfect sense to tag
everything to death.

> If simplifying a term makes its type illegal, intuitively one would think it
> never should have been given that type in the first place.

Well, if in an *untyped* computational model such as Martin-Löf's 1984
version, the untyped terms change type through reductions then
something is wrong with the types, not with the terms. The terms were
there first.

I do not actually know how to make an illegal type in ML1984 (what
does that mean?). What I know is how to prove

Id U (Nat → Bool) (Nat → Nat) → 0

using untagged applications and λ-abstractions, β-reductions, and
equality reflection. This shows that either the type theory is
unreasonable, or that set theory is not a model of it. I prefer to
think that set theory should be a model of type theory.

> More an observation that the interpretation of *terms* is not
> compositional, but factors through the set-theoretic semantics, followed by
> the globally chosen quotient/isomorphisms.

The category of cardinals has all the necessary structure to interpret
type theory directly. Of course, to show that the structure is there,
one would observe that the structure is induced by the set-theoretic
one through an application of the axiom of choice. It's set theory
after all. But you don't have to phrase the semantics in terms of a
set theoretic quotient if you don't want to.

With kind regards,

Andrej

[Matt Oliveri]

On Wednesday, October 7, 2015 at 2:06:28 PM UTC-4, Andrej Bauer wrote:

What I know is how to prove

    Id U (Nat → Bool) (Nat → Nat) → 0

using untagged applications and λ-abstractions, β-reductions, and
equality reflection. This shows that either the type theory is
unreasonable, or that set theory is not a model of it. I prefer to
think that set theory should be a model of type theory.

You mean the category of sets, right? ZF sets would still model types (and terms), I think. After all, the ZF function spaces (Nat->Bool) and (Nat->Nat) are different. For example, only one has an identity function.

The only thing "unreasonable" about untyped reductions is that it makes the system too concrete for types to be universal constructions. But they can still implement universal constructions, albeit in some specific, non-unique way.

[Andrew Polonsky]

On Wed, Oct 7, 2015 at 8:06 PM, Andrej Bauer <andrej...@andrej.com> wrote:

From the point of view of
denotational/categorical semantics it makes perfect sense to tag
everything to death.

I think it makes sense to do that from the syntactic point of view as well.

It is also a powerful feature of the type-theoretic notation, that the *type* arguments given to lambda, application, etc., can be reconstructed mechanically from the subsequent term arguments -- and thus, can be omitted in proof terms.

But that feature depends on uniqueness of typing and decidability of type reconstruction, which are famously absent from ETT.

That's no jaw-dropper: the closer your syntax lies to the semantic world, the less mileage you get out of the language.

 

Cheers,

Andrew

[Martin Escardo]

On 07/10/15 12:07, Matt Oliveri wrote:
> I think it is consistent to have 0 = 1 (propositionally) under the
> assumption (x:0).
>
>
> I think you lucked out. What if he had said 0*0 = 1*0?

Thanks for fixing the example.

Martin

[Andrej Bauer]

On Wed, Oct 7, 2015 at 11:31 PM, Matt Oliveri <atm...@gmail.com> wrote:
> You mean the category of sets, right? ZF sets would still model types (and
> terms), I think. After all, the ZF function spaces (Nat->Bool) and
> (Nat->Nat) are different. For example, only one has an identity function.

I do not quite understand the difference between the "category of
sets" and "ZF sets", but let me just point out, again, hat Nat → Bool
and Nat → Nat are isomorphic sets. In a previous message I described
how you can get them to be equal by tewaking the meaning of →, and
this had nothing much to do with whether we're in a category or not.

Under the isomorphism the identity function of Nat → Nat simply
becomes some other function Nat → Bool. What this tells us is not that
Nat → Bool and Nat → Nat are "really different" as bare objects but
rather that they are different as structures, namely exponentials.

This whole discussion has a distinctly non-mathematical character. In
ordinary mathematics, if there is such a thing, it is mostly
uninteresting to worry about the distinction between isomorphism and
equality. This is why univalence is such a great thing.

With kind regards,

Andrej

[Martin Escardo]

On 07/10/15 23:01, Andrej Bauer wrote:
> This whole discussion has a distinctly non-mathematical character.

The question is whether equality reflection for elements of a universe a
la Russell in MLTT buys us anything that can be considered
mathematically interesting or useful.

The conclusion of this discussion is that it doesn't: (1) with equality
reflection, we rule out the view of the elements of identity types of
types as type equivalences (the univalence axiom)), (2) with equality
reflection, we also don't capture any other competing, mathematically
interesting, previously-existing notion of type equality out there.

> In ordinary mathematics, if there is such a thing, it is mostly
> uninteresting to worry about the distinction between isomorphism and
> equality. This is why univalence is such a great thing.

In addition to your reasons for the greatness of univalence, I would say
that its consistency rigorously establishes the intuitive fact that
intensional MLTT (*without* univalence) cannot distinguish isomorphic
types.

But of course there is a little bit more to univalence than just
reflecting mathematical practice, because mathematical practice doesn't
use univalence, but rather just observes that constructions of interest
are invariant under isomorphism.

If you want to be very cynical, you can say that MLTT (with or without
univalence) is a straight-jacket that prevents you from performing
constructions that are not invariant under isomorphism.

The force of univalence (even without HIT's) is that it adds a lot of
mathematical expressivity to MLTT: with it, we get function
extensionality, quotients, propositional extensionality, propositional
truncation, and much more, which we do need to have in order to do real
mathematics in MLTT. Moreover, as it happens, it allows us to construct
types such as the circle up-to-homotopy (using Grayson's construction).
And so on.

While the fact that MLTT+univalence allows one to capture homotopy
theory is interesting and deep, it is also misleading: there are reasons
to understand and being interested in univalence in MLTT much before we
consider homotopy theory.

Univalence is an extensionality axiom, and the above follows from that.

(And: If one is interested in the meta-theoretical fact that MLTT can
"run proofs in a computer", one can computationally interpret the
univalence axiom very much like one interprets function extensionality:
the cubical model can be seen as a generalization of the setoid model.)

Martin


Martin


Martin

[Martin Escardo]

Thanks for your message, Jon, and sorry for the very late reply.

Hopefully the replies by other people or me have somewhat clarified the
points you made in relation to the discussion I proposed.

There is one thing, though, that I would like to address explicitly,
quoted out of context (but your full message is quoted below):

You say:
> I think that trying to find the "correct /
> real notion" of equality for type theory is perhaps not a super useful
> thing to do, and I would like to avoid statements like "prevent any
> reasonable resolution of the notion of equality in the universe",
> which are highly questionable and perhaps less than constructive.

I am not trying to find the correct notion of equality. I am talking
about intensional MLTT, which comes with its own given notion of
equality, which I don't propose to modify. I only want to understand it.

All I am saying is that (1) this notion of equality is terribly
under-specified when it applies to types living in a universe a la
Russell, and (2) adding equality reflection to the universe doesn't make
it any more precise, and, also, prevents possible useful resolutions
(such as type equality as equivalence/isomorphism).

Best,
Martin


On 03/10/15 04:22, Jon Sterling wrote:
> Martin,
>
> Thanks for the interesting & thoughtful note. A few remarks between the
> lines...
>
> On Fri, Oct 2, 2015, at 02:35 PM, Martin Escardo wrote:
>>
>> What makes any notion of equality, in any mathematical theory, to
>> really be equality? The fact that we can replace equals for equals.
>>
>> In MLTT, this is "transport" (old terminology: "cong"). This is
>> actually the recursion principle for the identity type (the induction
>> principle is J).
>
> I thought that "cong" was the old terminology for what is now often
> called "ap"; "transport" is new terminology for what was frequently
> called "subst".
>
>>
>> In set theory, the situation is similar. We have an axiom scheme
>> (meaning: countably many axioms, one for each syntactical
>> proposition), saying that we can replace equals for equals.
>>
>> Operationally, these axioms are very useful, in both
>> theories. However, they don't tell us how to get any non-trivial
>> (non-tautological) equality to start with.
>>
>> Let's consider set theory first: It is certainly the case that if two
>> sets are equal then they have the same elements:
>>
>> forall(x,y). x=y -> forall(z). z in x iff z in y.
>>
>> The extensionality axiom says that this implication is a (logical)
>> equivalence.
>>
>> We are very used to this: if two sets have the same elements then they
>> are equal. But this doesn't follow from the definition of equality,
>> namely that we can substitute equals for equals (Leibniz
>> principle). It is really a postulate (the extensionality axiom).
>>
>> I wouldn't say that this postulate is asserting some truth. I would
>> instead say that it is determining the nature of sets.
>>
>> Let's abbreviate
>>
>> forall(z). z in x iff z in y
>> by
>> Eq x y
>>
>> so that we have the fact
>>
>> forall(x,y). x=y -> Eq x y,
>>
>> and so that the set-theoretic extensionality axiom says that this
>> implication is an equivalence.
>>
>> You can see two things from this discussion: (1) The set-theoretical
>> axiom of extensionality has the same shape as the univalence axiom.
>> (2) There is nothing intrinsic to the notion of equality that would
>> require that two collections are equal if they have the same elements or
>> instead that they are isormorphic.
>>
>> However, the way collections are set-up in MLTT makes it impossible,
>> by construction, to even formulate the question of whether two
>> collections have the same elements.
>>
>> Intensional MLTT is "incomplete" in the sense that it fails to fully
>> specify the nature of equality, particularly in a universe of types.
>>
>> Extensional MLTT specializes the notion of equality in an odd way so
>> as to prevent any reasonable resolution of the notion of equality in
>> the universe: neither the notion of "equal as having the same
>> elements" or "equal as being isomorphic" make any sense for
>> (so-called) extensional MLTT.
>
> Why doesn't it make sense to consider "equal as having the same
> elements" in ETT? Yes, that exact interpretation is quite impossible,
> but if we amend this to "equal as having the same elements & the same
> equivalence relation", then this is *exactly* the definition of equality
> of types in ETT (or, at least, MLTT 1979-1984). You may choose to have a
> more intensional equality for the universe itself (that is, membership
> in a universe vs typehood, which are two separate concepts in MLTT), but
> this is by no means required (or ruled out). But this is a conversation
> that has already been had on this list, so I won't re-hash it. [I also
> am not trying to say, "This is the right way to do it, listen!", or
> provoke any kind of flamewar; my remarks tonight are meant to emphasize
> a position of pluralism within the design spectrum for type theory, and
> note the usefulness of many different versions of equality.]
>
> In MLTT 1979, you are right that you cannot express the question of
> whether two types have the same elements/equivalence relations
> *internally* in the direct way, but you can do so indirectly using the
> identity type, which reflects exactly the judgmental equality, and
> thence suffices to express that two types have the same equivalence
> relation, if you have arranged the equality in the universe to coincide
> with the equality of types/sets. In Nuprl, which is not ETT (but
> contains it), you can even express this question internally as a
> type/proposition; Nuprl extends ETT with (among other things) a kind of
> "mathematics of the third order", where you can reason about terms &
> computation.
>
> By the way, I also agree with you that there is nothing about equality
> (as a concept) that forces either of those interpretations... In some
> sense, as you and Thorsten have noted, choosing isomorphism as the
> equality of types is perhaps the most extensional option of all, but I
> echo Matt in noting that the design continuum between ETT and Nuprl
> (i.e. varying degrees of ability to talk about raw terms separately from
> their types) can be extremely useful in practice, and is perfectly
> justified intuitively; this doesn't mean that isomorphism as equality
> wouldn't be useful, but let's just remember that nobody as yet has a
> satisfactory meaning explanation for it, so it is certainly not yet
> intuitionistically valid.
>
> [By the way, for the reasons that Thorsten has so convincingly stated in
> his lectures on cubical type theory, and elsewhere, I think it may have
> been a mistake to have used the terminology "extensional" at all in the
> context of type theory, since there are so many fine-grained
> distinctions that can be lost. In particular, there is an inherent
> conflict between "extensional" in the set-theoretic sense and
> "extensional" in the "respects equality" sense; also, the use of the
> term "extensionality" in relation to consequence and hypothetical
> judgment tends to evoke for most people the idea of the classical
> material consequence (a coincidence of truth values), as opposed to the
> intuitionistic material consequence, which involves an effective
> transformation of mathematical acts.]
>
> Coming from a position of mathematical pluralism within the
> intuitionistic framework, I think that trying to find the "correct /
> real notion" of equality for type theory is perhaps not a super useful
> thing to do, and I would like to avoid statements like "prevent any
> reasonable resolution of the notion of equality in the universe", which
> are highly questionable and perhaps less than constructive.
>
> I don't think there is anything definitive at all about type theory such
> that the particular way we have chosen to axiomatize equality should
> require any kind of philosophical commitment on our parts; I won't take
> a particular choice personally, since a given type theory is not a
> definition of mathematical activity, but merely a reflection of some
> portion of it. Type theory is *mathematics of the second order*, in
> Brouwer's terminology, and is not definitive of mathematics of the first
> order, and so we may simply choose any notion of equality which we find
> useful, and that can be justified intuitively (i.e. via a meaning
> explanation); thence many different type theories may flourish and be
> used for different purposes, as we have seen with the three successful
> (but profoundly different) lines of type-theoretic development (Swedish,
> Ithacan and LF).
>
> My message is, then—so long as we have in place a meaning explanation
> for it, the particular choice of equality that we make does not affect
> its worth or validity as defining a theory of types, but rather allows
> us to vary the (idealized) mathematical activity that we have chosen to
> reflect / simulate.
>
> Best wishes,
> Jon
>
>>
>> Martin
>>
>>
>>
>>
>> On 02/10/15 19:25, Martin Escardo wrote:
>>>
>>>
>>> On 02/10/15 09:07, Andrej Bauer wrote:

>>>> On Fri, Oct 2, 2015 at 12:12 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>>>>> QUESTION (to try to emphasize my point). Is there any sensible axiom
>>>>> for MLTT (even if we didn't want to adopt it) that, in the presence of
>>>>> the equality-reflection rule (or not), allows to prove the negation of
>>>>>
>>>>> Id U Even Odds?
>>>>

>>>> Assuming equality reflection, an axiom you can add is that type
>>>> constructors are injective, for instance
>>>>
>>>> Id A x y ≡ Id B u v
>>>> ------------------------------
>>>> A ≡ B x ≡ u y ≡ v
>>>>
>>>> and similarly for Σ (I am omitting some contexts here, we need to pay
>>>> attention to bound variables):
>>>>
>>>> Σ (x:A) B ≡ Σ (y:C) D
>>>> ---------------------------
>>>> A ≡ C B ≡ C[x/y]
>>>>
>>>> If the type Id U Even Odds is inhabited then Even ≡ Odds, which would
>>>> give us isOdd(n) ≡ isEven(n), i.e.,
>>>>
>>>> Σ (m:N) Id N n (2 * m + 1) ≡ Σ (m:N) Id N n (2 * m)
>>>>
>>>> and by injectivity
>>>>
>>>> 2 * m ≡ 2 * m + 1.
>>>>
>>>> I think this is quite similar to what Dan suggested. That is, his
>>>> assumptions imply injectivity of type constructors, right?
>>>
>>> Ok. But what does it *mean*? It all models I know, this seems to fail.
>>>
>>> For example, it fails in the set-theoretical model, in realizability
>>> models (and of course, in univalent models).
>>>
>>> Let's write Id X x y as x=y now.
>>>
>>> Consider the 0-univalence axiom: any two empty types are equal,
>>>
>>> Pi(X:U).(X->0)->(Y->0)->X=Y.
>>>
>>> Equivalently, any empty type is equal to the (canonical) empty type:
>>>
>>> Pi(X:U).(X->0)->X=0.
>>>
>>> This holds in the models mentioned above.
>>>
>>> But now 0-univalence implies
>>>
>>> (0 * 0) = (1 * 0)
>>>
>>> and hence 0=1 by injectivity of constructors.
>>>
>>> This shows that constructor-injectivity negates 0-univalence, and in
>>> particular doesn't hold in the models mentioned above.
>>>
>>> Perhaps I should reformulate the question. I have a sense that the
>>> proponents of the equality-reflection rule have in mind the
>>> set-theoretical model and similar models:
>>>
>>> Question. Is there an axiom for Id-equality in MLTT such that
>>> Id-equality of types (in a universe) turns out to be equality in the
>>> set-theoretical interpretation (and related interpretations)?
>>>
>>> (I don't think so.)
>>>
>>> A related question, given Dan's answer on which Andrej's answer builds
>>> in this.
>>>
>>> Question. Suppose you work in a universe a la Tarski as Dan does. Is
>>> there an axiom that only mentions the extensions [ c ] of the Codes c
>>> and allows to prove that Even /= Odds?
>>>
>>> (I don't think so either.)
>>>
>>> (I think what I am trying to argue is that so-called extensional MLTT
>>> is actually anti-extensional, like Thorsten said, but trying to invoke
>>> mathematics rather than ideology to make this explicit. But I would
>>> like to avoid a flame war in this discussion, and purely concentrate
>>> on the mathematical facts/questions.)
>>>
>>> Martin
>>>
>>
>> --
>> 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 HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>

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

[Matt Oliveri]

On Wednesday, October 7, 2015 at 6:01:43 PM UTC-4, Andrej Bauer wrote:

On Wed, Oct 7, 2015 at 11:31 PM, Matt Oliveri <atm...@gmail.com> wrote:
> You mean the category of sets, right? ZF sets would still model types (and
> terms), I think. After all, the ZF function spaces (Nat->Bool) and
> (Nat->Nat) are different. For example, only one has an identity function.

I do not quite understand the difference between the "category of
sets" and "ZF sets",

It's a difference in perspective. If we're dealing with a category, we avoid thinking about anything that isn't about objects and morphisms. But in raw set theory, it's handy to informally distinguish between sets used roughly as types (objects), and sets used to encode elements. Those element encodings are technically objects too, of course, but my impression is that neither objects nor morphisms are an intuitive way to think about them.

but let me just point out, again, hat Nat → Bool
and Nat → Nat are isomorphic sets. In a previous message I described
how you can get them to be equal by tewaking the meaning of →, and
this had nothing much to do with whether we're in a category or not.

Actually, I thought your tweak to (->) crucially depends on thinking of functions as points of an exponent object. That way, we know the domain and codomain of the function we're applying. If you take a raw function of ZF, you don't know it's "codomain". What is that? You know the set of mappings that the function is. So actually, you know its domain and its image. You can't define application to treat cases specially based on the codomain. Not all functions in (Nat->Nat) map onto the whole of Nat, so you'd get confused. (In fact, Bool is usually a subset of Nat, so you'd get confused right away.)

That's no proof, but I suspect one really could interpret ETT + untyped reduction into ZF, and this would prove that there's a difference between this kind of interpretation and a categorical one, since your tweaked (->) interpretation contradicts untyped reduction.

Under the isomorphism the identity function of Nat → Nat  simply
becomes some other function Nat → Bool. What this tells us is not that
 Nat → Bool and Nat → Nat are "really different" as bare objects but
rather that they are different as structures, namely exponentials.

I don't understand this. I was expecting you to say the opposite, that (Nat->Nat) and (Nat->Bool) can be equated because they're the same as exponentials. They really are different as raw sets, and untyped reductions are sufficient to reveal the difference.

This whole discussion has a distinctly non-mathematical character. In
ordinary mathematics, if there is such a thing, it is mostly
uninteresting to worry about the distinction between isomorphism and
equality. This is why univalence is such a great thing.

Well as the construction of ZFC in the HoTT book shows, all these "non-mathematical" aspects of set theory can be captured and reasoned with in an isomorphism-respecting system of math. It's a matter of perspective whether that construction provides a category of sets or something entirely different. But either way, I'm talking about set theory in the sense of ZF(C). In fact the formal difference between the model of ZFC and the univalent category of sets should make what I'm saying more precise: The ZFC model should also model ETT + untyped reduction. The category of sets probably would not model untyped reduction.

[Jon Sterling]

Martin,

Thanks for the response; I think that the very different perspectives we
are coming from have perhaps led us to speaking across purposes at
times. Though, given your work in synthetic topology and other areas,
which I have always admired greatly, I have a feeling that we may be
more closely aligned on many issues than it has thus far appeared.

On Wed, Oct 7, 2015, at 05:58 PM, Martin Escardo wrote:
> Thanks for your message, Jon, and sorry for the very late reply.
>
> Hopefully the replies by other people or me have somewhat clarified the
> points you made in relation to the discussion I proposed.
>
> There is one thing, though, that I would like to address explicitly,
> quoted out of context (but your full message is quoted below):
>
> You say:
> > I think that trying to find the "correct /
> > real notion" of equality for type theory is perhaps not a super useful
> > thing to do, and I would like to avoid statements like "prevent any
> > reasonable resolution of the notion of equality in the universe",
> > which are highly questionable and perhaps less than constructive.
>
> I am not trying to find the correct notion of equality. I am talking
> about intensional MLTT, which comes with its own given notion of
> equality, which I don't propose to modify. I only want to understand it.
>
> All I am saying is that (1) this notion of equality is terribly
> under-specified when it applies to types living in a universe a la
> Russell, and (2) adding equality reflection to the universe doesn't make
> it any more precise, and, also, prevents possible useful resolutions
> (such as type equality as equivalence/isomorphism).

I agree strongly with both of these statements. I like to see a closed
formal system for type theory as an approximation or a neighborhood
around an ideal type theory (like CTT, or another); as such, it is
natural that the spread which includes all refinements of this
approximation should contain multiple such ideal points, which
corresponds to the possibility of numerous interpretations of (among
other things) the identity type, each of which significantly changes the
character of the theory. With regard to "understanding" equality in ITT,
to understand a judgement is to know its meaning; if you know the
judgment's meaning, then you already have a particular model in mind,
and therefore you are no longer dealing abstractly with ITT, but rather
with an ideal point in the spread I mentioned; so I think that to
"understand the nature of equality in intensional/formal type theory" is
just not possible, since its nature is only clarified by choosing an
"intended semantics".

As for (2), I think you're exactly right that adding equality reflection
to a formal type theory has disastrous consequences; exact equality is
obtainable by other means, and if you arrange your type theory in a
certain way, equality reflection is inevitable (or, alternatively,
impossible); but as a naïve extension it fails to clarify the nature of
the identification type in intensional/formal type theory.

Kindest regards,
Jon

[Thomas Streicher]

In my eyes the underspecification of type equality in traditional
type theory is a feature not a bug. It reflects the catgorical nature
of type constructors whose up to isomorphism nature allows to
interpret them differently in, say, even realizability models.

It's a preGoedelian view of logic that all "true equalities of types"
should be derivable in the type theory.

But this underspecification of type equality doesn't force one to
embrace univalence which generates new equalities one tends to avoid
in everyday reasoning (say NxN equals NxN by twist).

But, of course, it is interesting to investigate such a radical axiom
as one option among others.

Thomas

[Andrej Bauer]

On Thu, Oct 8, 2015 at 4:07 AM, Matt Oliveri <atm...@gmail.com> wrote:
> Actually, I thought your tweak to (->) crucially depends on thinking of
> functions as points of an exponent object. That way, we know the domain and
> codomain of the function we're applying. If you take a raw function of ZF,
> you don't know it's "codomain". What is that? You know the set of mappings
> that the function is. So actually, you know its domain and its image. You
> can't define application to treat cases specially based on the codomain. Not
> all functions in (Nat->Nat) map onto the whole of Nat, so you'd get
> confused. (In fact, Bool is usually a subset of Nat, so you'd get confused
> right away.)

You are confusing levels. The exponential operation → does not act on
functions but rather on sets. There is no mystery about "knowing the
codomain" because → is given both the domain and codomain as
arguments. And by the way, A → B produces *two* things, namely a set,
let us call it Exp(A,B) and a map ev_{A,B} : Exp(A,B) × A → B,
satisfying the usual conditons for an exponential.

All I am saying is that we can "fix" Nat → Bool so that Exp(Nat, Bool)
can be any desired set of continuum cardinality. Of course, we need to
change ev_{Nat, Bool} accordingly. Perhaps I should spell out the
details (again)?

Suppose we wish to replace Exp(Nat, Bool) with a set X which is
isomorphic to it. Let f : X → Exp(Nat, Bool) be such an isomorphism.
Redefine Nat → Bool to be

Nat → Bool := (X, ev')

where ev' : X × Nat → Bool is defined by

ev'(x, n) := ev_{Nat,Bool} (f(x), n).

It is obvious that (X, ev') is an exponential of Nat and Bool.

This construction works also if you do not "think of objects". We can
formulate the → operation in straight set theory and perform exactly
the same modification.

With kind regards,

Andrej

[Neelakantan Krishnaswami]

On 07/10/15 23:01, Andrej Bauer wrote:
>

> This whole discussion has a distinctly non-mathematical character.
> In ordinary mathematics, if there is such a thing, it is mostly
> uninteresting to worry about the distinction between isomorphism and
> equality. This is why univalence is such a great thing.

It would be nice if you were right, but I see many mathematicians
doing things like (for example) building lattices by taking powersets
ordered by inclusion. That's *why* we might wish for Even to
not equal Odd, so that we can distinguish the elements of P(N)!

Now, power sets are impredicative in a fashion which type theory
generally eschews, but many of its uses can be mimicked by subtyping.
For instance, if Even and Odd are subtypes of Nat, then the statement
that they have no elements in common is perfectly expressible in type
theory:

Even-Odd-distinctness : Πn:Even. Πm:Odd. (Id n m Nat) → ⊥

In Nuprl, this kind of subtype relationship is interpreted as inclusion
of PERs (morally, as a subset relation), but that's not the only
choice.

For example, William Lovas and Frank Pfenning show in "Refinement Types
for Logical Frameworks and Their Interpretation as Proof Irrelevance"
how to LF + subtyping in terms of LF + proof-irrelevance.

But the key point is that in standard MLTT, if e : A and e : B, then
we have a metatheorem that A is definitionally equal to B. Subtyping
permits us to loosen that stricture and give the same term multiple
types.

Whether we *should* compare elements of different type is a
philosophical question, but it's unquestionable that we *can* do it
in a coherent way which doesn't break any important syntactic feature
of type theory. (Indeed, universe cumulativity adds a form of subtyping
to type theory already.)

Best,
Neel

PS -- I feel like you know everything I've said, but perhaps I've
arranged it in an interesting way. :)

[Peter LeFanu Lumsdaine]

On Thu, Oct 8, 2015 at 11:18 AM, Neelakantan Krishnaswami <n.krish...@cs.bham.ac.uk> wrote:

On 07/10/15 23:01, Andrej Bauer wrote:

This whole discussion has a distinctly non-mathematical character.
In ordinary mathematics, if there is such a thing, it is mostly
uninteresting to worry about the distinction between isomorphism and
equality. This is why univalence is such a great thing.

It would be nice if you were right, but I see many mathematicians
doing things like (for example) building lattices by taking powersets
ordered by inclusion. That's *why* we might wish for Even to
not equal Odd, so that we can distinguish the elements of P(N)!

Identifying isomorphic types doesn’t mean we lose the distinction between elements of P(N)!  Elements of P(N) are not defined as (just) types: they are defined usually as either predicates on N, or as types equipped with an injective map to N.  (Mathematicians don’t normally state that as extra structure, but that’s because in a material-set-theory setting, they don’t need to; it’s provided canonically on material subsets of N.)

Using either of these definitions, it’s clear that we don’t identify even and odd.  The predicates isEven and isOdd are (provably) not equal.  The pairs (Even, pi_1^isEven) and (Odd, pi_1^isOdd) are (provably) not equal.  So these are still distinct under univalence, or in the cardinality model, when Even and Odd are (propositionally or definitionally) equal as types.

So I wouldn’t see “we want to distinguish elements of P(N)” as an argument against identifying Even and Odd, unless one’s already committed to certain (quite strong) forms of subtyping.  I would read your example as showing that “identifying Even and Odd definitionally is incompatible with a global subtyping that includes Even, Odd ≤ N”, and “identifying Even and Odd propositionally is incompatible with having such a subtyping relation moreover represented by a predicate on the universe”. 

–p.

[Matt Oliveri]

On Thursday, October 8, 2015 at 3:37:21 AM UTC-4, Andrej Bauer wrote:

On Thu, Oct 8, 2015 at 4:07 AM, Matt Oliveri <atm...@gmail.com> wrote:
> Actually, I thought your tweak to (->) crucially depends on thinking of
> functions as points of an exponent object. That way, we know the domain and
> codomain of the function we're applying. If you take a raw function of ZF,
> you don't know it's "codomain". What is that? You know the set of mappings
> that the function is. So actually, you know its domain and its image. You
> can't define application to treat cases specially based on the codomain. Not
> all functions in (Nat->Nat) map onto the whole of Nat, so you'd get
> confused. (In fact, Bool is usually a subset of Nat, so you'd get confused
> right away.)

You are confusing levels. The exponential operation → does not act on
functions but rather on sets. There is no mystery about "knowing the
codomain" because → is given both the domain and codomain as
arguments. And by the way, A → B produces *two* things, namely a set,
let us call it Exp(A,B) and a map ev_{A,B} : Exp(A,B) × A → B,
satisfying the usual conditons for an exponential.

I don't think I'm confused. You are quite right that you know the codomain when defining a function space. I expressed it badly, but what I'm saying is that to validate untyped reduction (for functions), you want to define function application based on a function and an argument *independently of any particular function space*. I haven't said a thing yet about how I would interpret (->). Remember, in ZF, functions exist prior to being collected into function spaces. And any given function belongs to very many different function spaces.

All I am saying is that we can "fix" Nat → Bool so that Exp(Nat, Bool)
can be any desired set of continuum cardinality. Of course, we need to
change ev_{Nat, Bool} accordingly. Perhaps I should spell out the
details (again)?

No, I understand. But the reduction rule you get this way inevitably depends on the type annotations, since it inspects the codomain.

Suppose we wish to replace Exp(Nat, Bool) with a set X which is
isomorphic to it. Let f : X → Exp(Nat, Bool) be such an isomorphism.
Redefine Nat → Bool to be

  Nat → Bool := (X, ev')

where ev' : X × Nat → Bool is defined by

  ev'(x, n) := ev_{Nat,Bool} (f(x), n).

It is obvious that (X, ev') is an exponential of Nat and Bool.

Uh huh.

This construction works also if you do not "think of objects". We can
formulate the → operation in straight set theory and perform exactly
the same modification.

The (->) I want is just an operation on sets. It does not tell us what function application is; we already knew. Your modification does not fit this style. I hope I'm making clear the way in which ZF satisfies untyped reduction. The gist of it is to not think of ZF as a category.

[Neelakantan Krishnaswami]

On 08/10/15 10:54, Peter LeFanu Lumsdaine wrote:
>
> Identifying isomorphic types doesn’t mean we lose the distinction
> between elements of P(N)!
>

> [... many things I agree with elided...]

>
> So I wouldn’t see “we want to distinguish elements of P(N)” as an
> argument against identifying Even and Odd, unless one’s already
> committed to certain (quite strong) forms of subtyping.

I'm not committed to subtyping, but I do want to understand it!

From my point of view, the critical issue is that terms and
derivations are not the same thing. In terms of categorical logic we
should think of having a category of typing derivations and a category
of terms, and a forgetful functor from derivations to terms.
Thanks to the conversion rule, the same term in MLTT can represent many
different derivations, and making the distinction explicit makes it
easier to explain the issues of coherence that arise in the semantics.

Subtyping is primarily useful precisely because it is asymmetric and
we can't interpret it as equality, which forces us to resolve coherence
issues in a principled way.

The fact that it also lets us capture certain features of mathematical
vernacular is a happy bonus -- your parenthetical remark

> (Mathematicians don’t normally state that as extra structure, but
> that’s because in a material-set-theory setting, they don’t need to;
> it’s provided canonically on material subsets of N.)

puts the finger on the issue very precisely. If there is a way
to speak in which this structure becomes canonical, why should
the user have to provide it? Or in positive terms, it seems
quite reasonable to let users take material subsets of structural
types, and let the proof assistant sort out the details.

Best,
Neel

[Michael Shulman]

On Thu, Oct 8, 2015 at 5:22 AM, Neelakantan Krishnaswami
<n.krish...@cs.bham.ac.uk> wrote:
>> (Mathematicians don’t normally state that as extra structure, but
>> that’s because in a material-set-theory setting, they don’t need to;
>> it’s provided canonically on material subsets of N.)
>
> puts the finger on the issue very precisely. If there is a way
> to speak in which this structure becomes canonical, why should
> the user have to provide it?

This structure is canonical already at the level of the predicates
isEven and isOdd, which come before one uses them to define subsets of
N. It's the process of Sigma-ing them which loses the canonical
structure. Material set theory retains it, but there's no virtue in
that because sometimes we *want* to lose it, and if we don't want to
lose it we can just not Sigma.

Mike

[Thorsten Altenkirch]

On 08/10/2015 10:18, "Neelakantan Krishnaswami"

<n.krish...@cs.bham.ac.uk> wrote:

>It would be nice if you were right, but I see many mathematicians
>doing things like (for example) building lattices by taking powersets
>ordered by inclusion. That's *why* we might wish for Even to
>not equal Odd, so that we can distinguish the elements of P(N)!
>

P(N) = N -> Prop and Odd != Even : Nat -> Prop in Hott.

Thorsten

>





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.

[Andrew Polonsky]

One final thought on this thread.

Martin's new criticism of "extensional" type theory, more precisely, the addition to MLTT of the equality reflection rule, is that it still doesn't render equality sharp enough:

  Id U Odds Evens -> 0.  [Not provable, even in extensional MLTT.] 

Others have pointed out that it is provable whenever one has injectivity of type constructors.

But this assumption is not necessary: this fact is already provable in MLTT + reflection.

The derivation uses standard computation rules, which do not check equality between type arguments of the elimination-introduction pair.

Indeed, in standard MLTT this check is overtly superfluous: if the redex is well-typed, the hidden arguments to the intro-elim pair are already matched.  But, as others pointed out, in implementations of MLTT with reflection rule, this check is indispensable.

And this is not just an implementation issue: without the side conditions on the reduction rules, the logic changes as well.  Andrej's favorite example:

What I know is how to prove 

    Id U (Nat → Bool) (Nat → Nat) → 0

using untagged applications and λ-abstractions, β-reductions, and
equality reflection.

Of course, these are exactly the things needed to prove Martin's statement, using untagged beta-reduction for the sigma type.

Since it's a question of logic rather than implementation, we should try to reach a consensus what the so-called ETT should really be.

I do not want to take sides.  I think Andrej's position makes sense from the implementation point of view. (Even if the semantic example I find rather artificial.)

But taking that view renders Martin's original criticism of ETT void.

Best,

Andrew

[Matt Oliveri]

On Thursday, October 8, 2015 at 3:58:05 PM UTC-4, Andrew Polonsky wrote:

One final thought on this thread.

Martin's new criticism of "extensional" type theory, more precisely, the addition to MLTT of the equality reflection rule, is that it still doesn't render equality sharp enough:

  Id U Odds Evens -> 0.  [Not provable, even in extensional MLTT.] 

Others have pointed out that it is provable whenever one has injectivity of type constructors.

But this assumption is not necessary: this fact is already provable in MLTT + reflection.

The derivation uses standard computation rules, which do not check equality between type arguments of the elimination-introduction pair.

This is what I've been calling untyped reduction. But my impression is that for the benefit of categorical semantics, untyped reduction is not taken as standard. (In Nuprl, untyped reduction is inevitable, since there are no type annotations.)

Since it's a question of logic rather than implementation, we should try to reach a consensus what the so-called ETT should really be.

Right, but I think that already happened: no untyped reduction.

I do not want to take sides.  I think Andrej's position makes sense from the implementation point of view. (Even if the semantic example I find rather artificial.)

I am curious if there are any natural examples of models of ETT that don't satisfy untyped reduction. I believe sets are a non-example, and Andrej's example is indeed artificial. I think what's really going on is that most type theorists don't see value in untyped reduction, and don't want to check if models satisfy it.

Of course, starting with a fully typed system, there are tons of natural models of ETT that don't satisfy untyped reductions. But I'd blame that on starting with a fully typed system. See, I'd argue that that system also ought to provide a mode that's partially untyped. The question is if intrinsically-typed models ever arise in an untyped system, other than by syntactic models.

It's kind of a shame, because proof assistants would probably be at least a little more efficient if there weren't so many type annotations under the hood. Maybe they're inferred, but to avoid untyped reduction, annotations still need to be kept around during reduction. At least some of them.

(Using Observational TT instead of ETT actually seems like a good way to minimize the amount of annotation.)

[Michael Shulman]

On Thu, Oct 8, 2015 at 3:27 PM, Matt Oliveri <atm...@gmail.com> wrote:
> I am curious if there are any natural examples of models of ETT that don't
> satisfy untyped reduction.

Maybe I'm misunderstanding, but if we just take an arbitrary locally
cartesian closed category to model ETT, then I don't see any way to
make sense of untyped reduction; is there?

[Matt Oliveri]

Probably not. But I want a specific example. Of course you could've just said "an arbitrary model of ETT without untyped reduction".

I could try to build some other model internally to an arbitrary LCCC, and that one would satisfy untyped reduction, but that would be cheating on my part. I don't know LCCCs well enough to know if that's actually possible, but I mean generally that I shouldn't be doing complex custom constructions to force untyped reduction to work.

[Andrew Polonsky]

It works in set theory.

So I suspect it will also work in any concrete LCCC.

Andrew

--
You received this message because you are subscribed to a topic in the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/HomotopyTypeTheory/qydSwbvj1uE/unsubscribe.
To unsubscribe from this group and all its topics, send an email to HomotopyTypeThe...@googlegroups.com.

[Michael Shulman]

On Thu, Oct 8, 2015 at 3:42 PM, Matt Oliveri <atm...@gmail.com> wrote:
>> Maybe I'm misunderstanding, but if we just take an arbitrary locally
>> cartesian closed category to model ETT, then I don't see any way to
>> make sense of untyped reduction; is there?
>
> Probably not. But I want a specific example.

You mean, you want a specific LCCC? Is "any elementary topos"
specific enough for you? As Andrew points out, it's possible you
could play contrived games in a Grothendieck topos, but it seems less
likely in, say, the effective topos.

However, I would say that's really missing the point anyway. The
point is that we can work with an *arbitrary* LCCC.

[Matt Oliveri]

It's quite possible I'm missing the point. But do we really want to work in an aribitrary LCCC? Maybe all LCCCs we actually care about can be tweaked to satisfy untyped reduction without harming the mathematical content.

Anyway, I can see that I'm going to get myself in trouble with this line of questioning, if only because I don't know categorical semantics very well, and won't be able to defend my hypothesis.

I don't know the details of the effective topos, but I hear it starts with combinators. Well, those combinators' reductions are untyped. It doesn't seem unlikely that an ETT-like type system (or even Nuprl-like, I bet) could be layered on top exposing the untyped equational theory arising from combinator reduction.

[Michael Shulman]

I care about arbitrary LCCCs.

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

[Andrew Polonsky]

It certainly can't work in all LCCCs, because it doesn't work in one of them.

The question is whether untyped reduction is natural.

I think it's natural.

It's certainly what we do on paper.

It's what happens in set theory.

It's also what Coq does.

I also believe that, on the meta-level, type constructors ARE injective wrt strict equality.  Then typed reduction is just unnecessary work.

Andrew

[Michael Shulman]

I can't speak for anyone else, but I only "do untyped reductions on
paper" in the sense that I don't bother to write down the type
annotations, just like I don't generally bother to write the values of
implicit arguments, or check that isomorphisms are natural. I would
certainly regard it as a mistake if I ever happened to write down a
reduction that didn't admit a type annotation. Personally, I think
the fact that it doesn't work in all LCCCs is a watertight argument
that it is unnatural. But there is probably no point in continuing
such an argument. (-:

[Andrew Polonsky]

The i-th projection of (x1,..,xk) is xi, and this is independent of whether we are in R^k, N^k, or A1x...xAk.

In the experience of most mathematicians, it would make no sense to "check that the projection matches the pair".   And that's not a mistake, there is a logical reason for that.

Andrew

[Gabriel Scherer]

For reference (I don't know how familiar the people here are with this
work), the question of whether untyped beta-equivalence and typed
beta-equivalence correspond in the Calculus of Constructions
(traditionally defined without eta-rules), or in all Pure Type
Systems, has remained open for a relatively long time. Type theories
have been described with either the typed or untyped rules, but the
type-checking implementations have traditionally used the untyped
version, and people assumed, but were not quite certain, that the two
notions coincided.

The problem was pointed out in Herman Geuver's PhD thesis, in the
setting of beta-eta equality, in 1993.
Logic and Type Systems, Herman Geuvers, 1993 (pages 187-188)
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.56.7045&rep=rep1&type=pdf
(From what I understand Herman Geuvers assumed that the result would
be easy for the beta-only case by confluence, but it has proved harder
than expected because of difficulties related to non-normalization,
with strong beta-normalization remaining open for many PTSs.)

A first partial solution for the so-called "functional" PTSs was
proposed by Robin Adams in 2006
Pure Type Systems with Judgemental Equality, Robin Adams, 2006
https://www.cs.ru.nl/R.Adams/ptseq8.pdf

The complete solution (for beta-equality) for all PTSs is the PhD work
of Vincent Siles
Investigation on the typing of equality in type systems, Vincent Siles, 2010
http://www.lix.polytechnique.fr/~vsiles/papers/thesis.pdf
with a shorter article version
Equality is typable in Semi-Full Pure Type Systems, Vincent Siles
and Hugo Herbelin, 2010
http://www.lix.polytechnique.fr/~vsiles/papers/herbelin.siles.LICS2010.pdf

In the work of Robin Adams and Vincent Siles, "annotated systems"
(versions of the term language with more explicit type annotations)
play a large role, as they are necessary detours to prove subject
reduction (the key to lift untyped reductions into typed reductions).
Subject reduction, in turn, relies on definitional injectivity-like
properties of pi types (definitional injectivity may not hold in
systems where terms/types do not have a unique type/sort, but weaker
versions do hold and are necessary steps towards subject reduction).

It is thus not so surprising that this non-trivial coincidence between
typed and untyped terms/reductions would fail once the system is
extended. In particular, by collapsing the definitional and
propositional world, the reflection rule changes the status of
definitional injectivity from "an expected meta-theoretical result" to
"a suspicious assumption about the system".

Is it the case that assuming injectivity of pi and sigma-types
suffices to restore the equivalence between typed and untyped
reductions in MLTT+reflection? If this was the case, it would suggest
that there are two reasonable systems for MLTT+reflection, the one
with non-annotated terms plus injectivity rules, and the one with
explicitly-annotated terms without injectivity rules. This is not a
value judgment on whether those are appropriate type theories for your
use-case: it merely follows from the design principle that one should
only use non-annotated terms when their reduction can be trusted
(coincide with the semantic equality which is always typed), to avoid
the confusion underlying this thread.

[Thorsten Altenkirch]

The question is not wether it works in all xyz. The issue is that to base equality on the accidents of term representation is wrong. It makes mathematical development a prisoner of syntax and is antithetical to the ideas of abstraction and extensionality.

Indeed, this is one of the central bugs of set theory which type theory overcomes. It is sad to see that people always stick to the mistakes of the past and NuPRL is indeed a set theory inspired type theory.

The question is whether untyped reduction is natural.

I think it's natural.

It is not – it is a bad habit (like smoking) you should overcome.

It's certainly what we do on paper.

It is not what I do on paper. Get a new sheet!

It's what happens in set theory.

Indeed! 

It's also what Coq does.

In ITT you can prove coherence theorems which allow you to work with terms in an untyped fashion. But what you mean is the typed syntax the rest is only a shorthand. If not, then its a bug.

Thorsten

--

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.

[Gabriel Scherer]

On Fri, Oct 9, 2015 at 11:01 AM, Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> The issue is that to base equality on the accidents of term representation is wrong.

I disagree.

This claim makes perfect sense in the context of *some* uses of type
theory, namely the design of a constructive logic which its
practitioners are convinced represents "truth". It also nicely extend
to all users of type theory that are interesting in mathematical
(typically categorical) models.

However, it is wrong, and it is impoverishing, in that it excludes
users of type theory that focus on the *computation* angle; for
programming language design for example. For programming language
design, untyped term representations have been a key provider of
intuitions and ideas -- and programming problems have, in turn,
benefited the development of type-theory-as-a-logic.

A beautiful aspect of type theory as a field is that these different
communities can cohabit, and exchange ideas and contributions. (In
fact it is not quite so clear-cut a divide as I describe; for example
realizability as a sub-field is strongly interested in untyped terms
as realizers, yet relatively less connected to programming aspects.).
Antagonist claims such as this one make sense inside a sub-community.
They can be good conceptual guides / aesthetic providers to further
discoveries -- when used at a personal level. But we should be careful
not to use them too widely, as they are also harmful by barring some
fertile points of view.

> But what you mean is the typed syntax the rest is only a shorthand. If not, then its a bug.

I agree with this.

[Martin Escardo]

On 09/10/15 10:13, Gabriel Scherer wrote:
> Antagonist claims such as this one make sense inside a sub-community.

Antagonism should be discouraged at all costs, despite the fact that we
*are* in a subcommunity in this list.

Untyped type theory, or Untype Theory, is not what we are looking for in
HoTT/UF (or at least this is my perception of the field).

Martin

[Gabriel Scherer]

Agreed, and of course I meant no snark in my remark. I understand
Thorsten's position (which I of course understand and respect as a
personal opinion) to hold in a rather general setting -- and about
untyped term representations in general rather than just their
equalities; in the specific setting of equalities I think it is even
more reasonable.

[Andrew Polonsky]

First of all, let's be clear on what this debate is NOT about.

In dependent type theories, term constructors – such as abstraction, application, projection, etc. – are *always* annotated with type arguments (which appear in the corresponding inference rule), even if, in most cases, these arguments can be inferred, and therefore kept hidden.

The debate is about whether the computation rules should require checking the equality of these arguments in the intro-elim pair, or whether the language should be designed so as to make such checks unnecessary.

Mathematical practice strongly favors the second view.

In set theory, these checks are unnecessary.

In standard type theories (MLTT, Calculus of Constructions,...) these checks are unnecessary.

In set theory, the "safety" of this notation follows trivially from the definition of a Kuratowski pair.

In type theory, it took some PhD these to see that it was safe.  A deep, difficult mathematical result.

It's certainly what we do on paper.

It is not what I do on paper. Get a new sheet!

Your paper maybe good, but your language sucks! 

Andrew

[Jon Sterling]

Hi Andrew,

One comment only,

On Fri, Oct 9, 2015, at 02:53 AM, Andrew Polonsky wrote:
> First of all, let's be clear on what this debate is NOT about.
>
> In dependent type theories, term constructors – such as abstraction,
> application, projection, etc. – are *always* annotated with type
> arguments
> (which appear in the corresponding inference rule), even if, in most
> cases,
> these arguments can be inferred, and therefore kept hidden.

This is false beyond all doubt. It was never the case in MLTT 1979-1985,
and it is not the case in CTT. Are these not dependent type theories? It
is definitively not the case that the notation on "Constructive
Mathematics and Computer Programming" was a shorthand that was intended
to be elaborated into a fully-annotated calculus. I hope I have simply
misunderstood your remark.

Kind regards,
Jon

>
> The debate is about whether the computation rules should require checking
> the equality of these arguments in the intro-elim pair, or whether the
> language should be designed so as to make such checks unnecessary.
>
> Mathematical practice strongly favors the second view.
>
> In set theory, these checks are unnecessary.
>
> In standard type theories (MLTT, Calculus of Constructions,...) these
> checks are unnecessary.
>
> In set theory, the "safety" of this notation follows trivially from the
> definition of a Kuratowski pair.
>
> In type theory, it took some PhD these to see that it was safe. A deep,
> difficult mathematical result.
>
> It's certainly what we do on paper.
> >
> > It is not what I do on paper. Get a new sheet!
> >
>
> Your paper maybe good, but your language sucks!
>
> Andrew
>

[Andrew Polonsky]

Hi Jon,

> In dependent type theories, term constructors – such as abstraction,
> application, projection, etc. – are *always* annotated with type
> arguments

....

This is false beyond all doubt. It was never the case in MLTT 1979-1985,

From "Intuitionistic Type Theory", 1984, page 21:

Σ-elimination

(x ∈ A, y ∈ B(x)) c ∈ (Σx ∈ A)B(x) d(x,y) ∈ C((x,y))

E(c, (x, y) d(x, y)) ∈ C(c)

where we presuppose the premiss C(z) set (z ∈ (Σx ∈ A)B(x)), although it is not written out explicitly. (To be precise, we should also write out the premisses A set and B(x) set (x ∈ A).)

But actually, you are right.  I was being too categorical.  I just wanted to focus discussion away from annotation of _terms_, which is not the issue.

I stand corrected.

Andrew

[Jon Sterling]

Aha, I see what you were thinking about. It is indeed the case that the
presuppositions of judgments are left implicit in the rules; one
perspective is that they are omitted because they are obvious and
annoying to write (this seems to be what Martin-Löf implies in some of
his writings), but another way to look at it, developed in great detail
by Peter Schroeder-Heister in some work which I can no longer locate, is
that the presupposition to a judgment is implicit because the judgment
does not have a meaning unless the presupposition obtains. So, a rule is
to be read, "assuming this is meaningful, then ...". In any case, the
presuppositions are largely unrelated to the annotations on terms.

Best,
Jon

[Martin Escardo]

On 09/10/15 00:33, Andrew Polonsky wrote:
> It certainly can't work in all LCCCs, because it doesn't work in one of
> them.
>
> The question is whether untyped reduction is natural.
>
> I think it's natural.
> It's certainly what we do on paper.
> It's what happens in set theory.

It really *is* what happens in set theory, on paper or not:

On 02/10/15 04:59, Michael Shulman wrote:
> In set
> theory, an ordered pair is "intrinsically" an ordered pair and you can
> always extract its two components, regardless of what set your ordered
> pair might itself be an element of. But in a fully typed type theory,
> you can't take an element of a Sigma-type, forget that it was an
> element of a particular Sigma-type, and still claim that it's somehow
> "intrinsically" an ordered pair that you can extract the components of
> (perhaps along the way claiming that it's also an element of some
> other Sigma-type).

> It's also what Coq does.

(I can't comment on that.)

> I also believe that, on the meta-level, type constructors ARE injective wrt
> strict equality.

This is a meta-theorem, actually used in order to do type
checking/inference. (Where strict equality = judgemental equality.)

> Then typed reduction is just unnecessary work.

It may be so, and a proof assistant may wish to save labour playing with
what needs to be annotated or not, but this is a completely different story.

From an abstract point of view, the elements of a type in MLT theories
are its own private property. A copy of an element of a type is allowed
as an ingredient to build an element of another type, but the element
itself cannot be in another type.

But you are free to build your own type theories that depart from this
design principle, such as NuPrl.

Also, the elements of a type are not terms (some of them are denoted by
terms), in the same way that in set theory the set of real numbers is
not the set of terms standing for reals.

Of course, part of the confusion comes from the fact that a number of
type theories can be used both as programming languages and as a
foundation of mathematics, and programmers do wish to see elements of
types as terms, but mathematicians certainly do not in general.

Martin

[Dan Licata]

This paper by Giuseppe Primiero is what came to mind for me:
http://logica.ugent.be/giuseppe/Docs/pres.pdf

I think people have different things in mind about the "implicit" type formation premises. For example, sometimes you will see a system with a rule like

Gamma ctx x:A in Gamma
-----------------------------------
Gamma |- x:A

with the intention that it is a theorem that

If Gamma |- M : A then Gamma ctx

because you check that the context is well-formed at the leaves.

Other times, Gamma being a context will be a presupposition of the judgement, so a rule that extends the context

Gamma, x:A |- M : B Gamma |- A type
---------------------------------------------------
Gamma |- \x:A.M : Pi x:A.B

will need to have a premise that ensures that the extended context is well-formed, to keep the induction going.

I think this style corresponds to thinking of the subject of the judgement as not a piece of raw syntax Gamma, but
{Gamma:ctx | ||Gamma ctx||_-1 }

i.e. the subset of the syntax that is (irrelevantly) known to be well-formed.

Whether something is presupposed or checked seems to correlate with whether the the type is an "input" or an "output" to the judgement; e.g. in bidirectional systems it is common to assume that the type is well-formed in the checking judgement, but to ensure that the type is well-formed in the synthesis judgement.

-Dan

[Matt Oliveri]

I think an "untype theory" that manages to model univalence could be worth paying attention to. At least it shouldn't be disqualified just for being untyped in some sense.

[Matt Oliveri]

On Friday, October 9, 2015 at 5:53:47 AM UTC-4, Andrew Polonsky wrote:

First of all, let's be clear on what this debate is NOT about.

In dependent type theories, term constructors – such as abstraction, application, projection, etc. – are *always* annotated with type arguments (which appear in the corresponding inference rule), even if, in most cases, these arguments can be inferred, and therefore kept hidden.

The debate is about whether the computation rules should require checking the equality of these arguments in the intro-elim pair, or whether the language should be designed so as to make such checks unnecessary.

But if the computation rules ignore the type annotations, why should elim forms be annotated? What difference in meaning do those annotations make?

(I know that for bidirectional checking and other proof theoretic tricks, annotations can go wherever it's convenient. That's not what I'm asking about. Which annotations are actually meaningful?)

Annotations on intro forms may also fail to be meaningful, depending on the model. For set theory, the domain annotation on a lambda is meaningful, but a codomain annotation would not be. You could create an alternative encoding of functions where both would be meaningful. In Nuprl, no annotations on intro forms are meaningful.

Of course, in the absence of untyped reduction, you get to abstract away from these particulars. The price you pay is that you must pessimistically assume all annotations are meaningful.

[Andrew Polonsky]

On Sat, Oct 10, 2015 at 4:32 AM, Matt Oliveri <atm...@gmail.com> wrote:

But if the computation rules ignore the type annotations, why should elim forms be annotated? What difference in meaning do those annotations make?

(I know that for bidirectional checking and other proof theoretic tricks, annotations can go wherever it's convenient. That's not what I'm asking about. Which annotations are actually meaningful?)

Those that specify the domain of a binding construct.

The other ones make explicit all other type arguments given to the inference rule, bridging the gap between terms and derivations.  I would say these are only meaningful by the way that they are used during type inference -- which may or may not use untyped conversion.

Annotations on intro forms may also fail to be meaningful, depending on the model. For set theory, the domain annotation on a lambda is meaningful, but a codomain annotation would not be. You could create an alternative encoding of functions where both would be meaningful. In Nuprl, no annotations on intro forms are meaningful.

Of course, in the absence of untyped reduction, you get to abstract away from these particulars. The price you pay is that you must pessimistically assume all annotations are meaningful.

Yes.  A pessimistic state of affairs, indeed.

Andrew

[Thorsten Altenkirch]

On 08/10/2015 13:22, "Neelakantan Krishnaswami"
<n.krish...@cs.bham.ac.uk> wrote:

>On 08/10/15 10:54, Peter LeFanu Lumsdaine wrote:
>>
>> Identifying isomorphic types doesn¹t mean we lose the distinction
>> between elements of P(N)!
>>
>> [... many things I agree with elided...]
>>
>> So I wouldn¹t see ³we want to distinguish elements of P(N)² as an
>> argument against identifying Even and Odd, unless one¹s already
>> committed to certain (quite strong) forms of subtyping.
>
>I'm not committed to subtyping, but I do want to understand it!

It seems to me that subtyping as it usually understood is an intensional
notion and hence should be studied on type-codes (i.e. a universe where
types are defined inductively) and not on types.

>
> From my point of view, the critical issue is that terms and
>derivations are not the same thing. In terms of categorical logic we
>should think of having a category of typing derivations and a category
>of terms, and a forgetful functor from derivations to terms.
>Thanks to the conversion rule, the same term in MLTT can represent many
>different derivations, and making the distinction explicit makes it
>easier to explain the issues of coherence that arise in the semantics.
>
>Subtyping is primarily useful precisely because it is asymmetric and
>we can't interpret it as equality, which forces us to resolve coherence
>issues in a principled way.
>
>The fact that it also lets us capture certain features of mathematical
>vernacular is a happy bonus -- your parenthetical remark
>
>> (Mathematicians don¹t normally state that as extra structure, but
>> that¹s because in a material-set-theory setting, they don¹t need to;
>> it¹s provided canonically on material subsets of N.)
>
>puts the finger on the issue very precisely. If there is a way
>to speak in which this structure becomes canonical, why should
>the user have to provide it? Or in positive terms, it seems
>quite reasonable to let users take material subsets of structural
>types, and let the proof assistant sort out the details.
>
>Best,
>Neel

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

[Thorsten Altenkirch]

On 08/10/2015 08:32, "Thomas Streicher"
<stre...@mathematik.tu-darmstadt.de> wrote:

>But, of course, it is interesting to investigate such a radical axiom
>as one option among others.
>

If we want to *define* type equality in type theory, what alternatives to
equivalence are there?

I mean univalence boils down to saying that

A =_U B := \Sigma f : A -> B. isEquivalence(f)

I think this is the only possible choice.

Thorsten

[Thomas Streicher]

> If we want to *define* type equality in type theory, what alternatives to
> equivalence are there?
>
> I mean univalence boils down to saying that
>
> A =_U B := \Sigma f : A -> B. isEquivalence(f)

> I think this is the only possible choice.

If you want to DEFINE equality of types then yes. But the point is
that it rather should be an open concept.
One may consider it as a problem of ZFC (and alike) that it defines
equality by quantification over the universe. This way one may formulate
silly questions like "is \pi an element of N^N". In mathematics one tends
to rate this as meaningless.
Similarly, I consider it as undesirable to consider the twist map as a
proof that NxN is equal to NxN. Or to take up an example that Odd and
Even are equal since there is a bijection beween them. In Maths there
is a shallow (definitional?) equality of sets and a notion of equipollence
which definitely is different. Similarly, one thing is to consider groups
as definitionally equal and another thing is to say they are isomorphic.

That's the reason why I find Univalence disputable as a principle of
Mathematics.

On might think that judgemental equality is sufficient for the purpose
of equality of types as needed in mathematics. But the problem is that
it can't be combined in a logical way as needed when saying e.g. that for
an N-indexed family A of types A_{n+1} equals [A^n -> A_n]. Therefore,
we do need a propositional equality for types.

That doesn't mean I am perfectly happy with ITT because function
extensionality definitly would be something desirable even if one is
hesitant to embrace Univalence.

Thomas

[Peter LeFanu Lumsdaine]

Note from the moderators: this thread has wandered in several directions from its original topic.  We gently suggest that it has run its course and should be wound up, and that whichever topics people wish to continue would be better served by new threads instead.

Best,

–Peter.

[Thorsten Altenkirch]

On 10/10/2015 19:49, "Thomas Streicher"

<stre...@mathematik.tu-darmstadt.de> wrote:

>> If we want to *define* type equality in type theory, what alternatives
>>to
>> equivalence are there?
>>
>> I mean univalence boils down to saying that
>>
>> A =_U B := \Sigma f : A -> B. isEquivalence(f)
>
>> I think this is the only possible choice.
>
>If you want to DEFINE equality of types then yes. But the point is
>that it rather should be an open concept.

It seems to me that there is something wrong with a language where you
cannot say what it means that 2 things are equal.

Indeed, and this is similar to the issue of functional extensionality:
type theory does not provide any observations to distinguish equivalent
types. Hence, if you fail to identify them you end up with structurally
incomplete language (as opposed to Goedelian incompleteness).

In a language with this sort of incompleteness you end up reproving
theorems you are already know hold by transfering them from an equivalent
structure. You end up wishing for a language where these equivalent and
indistinguishable objects are actually considered equal. The good news is
that such a language already exists: it is HoTT.

>
>One may consider it as a problem of ZFC (and alike) that it defines
>equality by quantification over the universe. This way one may formulate
>silly questions like "is \pi an element of N^N". In mathematics one tends
>to rate this as meaningless.
>Similarly, I consider it as undesirable to consider the twist map as a
>proof that NxN is equal to NxN. Or to take up an example that Odd and
>Even are equal since there is a bijection beween them. In Maths there
>is a shallow (definitional?) equality of sets and a notion of equipollence
>which definitely is different. Similarly, one thing is to consider groups
>as definitionally equal and another thing is to say they are isomorphic.
>
>That's the reason why I find Univalence disputable as a principle of
>Mathematics.
>
>On might think that judgemental equality is sufficient for the purpose
>of equality of types as needed in mathematics. But the problem is that
>it can't be combined in a logical way as needed when saying e.g. that for
>an N-indexed family A of types A_{n+1} equals [A^n -> A_n]. Therefore,
>we do need a propositional equality for types.
>
>That doesn't mean I am perfectly happy with ITT because function
>extensionality definitly would be something desirable even if one is
>hesitant to embrace Univalence.
>
>Thomas
>

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

[Thomas Streicher]

> It seems to me that there is something wrong with a language where you
> cannot say what it means that 2 things are equal.

in mathematics equality is not defined but axiomatized
in particular in set theory equality and elementhood are axiomatize
ina mutually recursive way (see the construction of forcing, Heyting
valued or realizability models)

> Indeed, and this is similar to the issue of functional extensionality:
> type theory does not provide any observations to distinguish equivalent
> types. Hence, if you fail to identify them you end up with structurally
> incomplete language (as opposed to Goedelian incompleteness).

depends on what you mean by observation
if you mean by observation maps to 2 or N then even in the effective
topos subsets of N cannot be separated by observations

> In a language with this sort of incompleteness you end up reproving
> theorems you are already know hold by transfering them from an equivalent
> structure. You end up wishing for a language where these equivalent and
> indistinguishable objects are actually considered equal. The good news is
> that such a language already exists: it is HoTT.

It is not so clear that one gains a lot because the equality `a la HoTT
doesn't allow you to suppress the isos (as is done when working
informally in category theory or topology or algebra or...).
And you get some nonintended new equality proofs like twist on NxN.

Thomas