not all types are propositions

[Vladimir Voevodsky]

This is from the first published Martin-Lof’s paper where he introduces his type theory (Logic Colloquium 1973):

Note the “When B(s) represents a proposition” clause. There is also a discussion in the intro to this paper.

Obviously at that time there was no concept of h-level and so it was difficult to see how to distinguish propositions from the rest of the types and Per says that both every proposition defines a type and a type defines a proposition - the proposition saying that this type is non-empty. This is of course when we call the squash type or propositional truncation. 

Vladimir.

[Daniel R. Grayson]

Was the paper by Awodey and Bauer in 2001 ( see http://repository.cmu.edu/philosophy/67/ ) the first
to distinguish propositions from general types and to give semantics for the squash operation?

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

[Vladimir Voevodsky]

I do not know. There are claims that the squash types have been used in NuPRL much earlier than that paper but

I do not understand NuPRL’s theory well enough to compare what was there to what A&B suggested. 

Vladimir.

On Feb 8, 2015, at 8:12 PM, Daniel R. Grayson <d...@math.uiuc.edu> wrote:

Was the paper by Awodey and Bauer in 2001 ( see http://repository.cmu.edu/philosophy/67/ ) the first
to distinguish propositions from general types and to give semantics for the squash operation?

On Sun Feb 08 2015 at 5:10:38 PM Vladimir Voevodsky <vlad...@ias.edu> wrote:

This is from the first published Martin-Lof’s paper where he introduces his type theory (Logic Colloquium 1973):

<Screen Shot 2015-02-08 at 6.05.13 PM.png>

Note the “When B(s) represents a proposition” clause. There is also a discussion in the intro to this paper.

Obviously at that time there was no concept of h-level and so it was difficult to see how to distinguish propositions from the rest of the types and Per says that both every proposition defines a type and a type defines a proposition - the proposition saying that this type is non-empty. This is of course when we call the squash type or propositional truncation. 

Vladimir.

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

<Screen Shot 2015-02-08 at 6.05.13 PM.png>

[Steve Awodey]

There is nothing new about distinguishing propositions from general types: it is the standard way of doing things in topos theory, and in similar type theories going all the way back to Frege and Russell.  It was the idea that all types can be regarded as (“proof relevant”) propositions that was new in M-L type theory, as motivated by proof-theoretic considerations and predicativity.  

The point of A&B was to show how to relate the two approaches while staying within a M-L style system (LCCC rather than topos) by distingishing the proof-irrelevant types among the others.  The rules for [bracket types] are not the same as those for Nuprl’s squash types, but the basic idea is very similar.  I don’t think there were any semantics before A&B — at least none that I am aware of.

Steve

[Michael Shulman]

I've been thinking about the question "which types are propositions"
some more recently, and come to the conclusion that it is actually
several related but distinct questions (or, rather, classes of
questions), which may have different answers. To wit:


1. The only truly *mathematical* class of questions is: in any
particular definition, do we insert a truncation or not? In general
the answer depends on the definition. For instance, in the definition
of contractibility, we want Sigma, but in the definition of the image
of a function between sets, we want truncated-Sigma. However, when
translating set-based mathematics into type theory, very often we want
to translate "there exists" to a truncated sigma --- chapter 11 of the
book is full of examples of this, but also some counterexamples, e.g.
the definition of Cauchy sequence in (11.2.9).

One guiding principle is that we want the result of our definitions to
have the "correct" homotopy type; another is that (as in (11.2.9)) we
may want to avoid a classical use of LEM or AC. Relatedly,
surprisingly often it turns out that the truncation is unnecessary:
the Sigma or + automatically ends up being (-1)-truncated.
Contractibility is one example; others are decidability of an hprop
and finite sets (with a sigma over cardinality). In this case, we
generally *don't* want to include a truncation in the definition,
since the untruncated version is just as easy to prove and more
powerful to use.


2. The next question is whether we allow untruncated types to be "used
as propositions". Specifically, do we allow ourselves to label them
as "theorems" and talk about "proving" them? I still believe that we
definitely do. For example, consider the "theorem" that pi_1(S^1) is
equivalent to Z. The "proof" of this constructs a *particular*
equivalence, i.e. an element of the untruncated type
Equiv(pi_1(S^1),Z). The truncated statement is significantly weaker,
and not sufficient for the uses we would like to make of it.

To be sure, set-based mathematics is afflicted by this same problem,
but in that case it is generally "solved" by ignoring it.
Mathematicians state "theorems" such as this one, but if they were to
be formalized, these "theorems" would have to be made into
"definitions" instead. Type theory gives us a better way to formalize
what mathematicians actually do, so we should take advantage of it.

A couple of years ago I wrote at
https://golem.ph.utexas.edu/category/2012/11/freedom_from_logic.html
about this point:

> This... reminds me of Bishop's comment that the axiom of choice is most often used to extract elements from equivalence classes into which they should never have been put in the first place. If what we have actually constructed is a particular term belonging to some informative type (one that isn't (-1)-truncated), why force ourselves to say *less* by asserting only that the (-1)-truncation of that type is inhabited, simply because we want to "prove a theorem" and we dogmatically require that "theorems" must be (-1)-types?

> Just as intuitionistic logic is *more expressive* than classical logic because it doesn't *force* us to assume the law of excluded middle (but allows us to assume it as an additional hypothesis like any other hypothesis), type theory is allowing us to see a further distinction which was invisible to the classical mind: we aren't *forced* to (-1)-truncate all theorems (but we are allowed to, if we so desire, by simply applying the truncation operator).

That second paragraph could perhaps be stated even better by saying
that intuitionistic logic doesn't force us to use a double-negated
existential, but allows us to distinguish it from a constructive one;
so similarly type theory doesn't force us to use a truncated
existential, but allows us to distinguish it from an untruncated one.


3. The last question is whether when speaking informal type theory, we
should use natural language phrases such as "there exists" and "or" to
refer to truncated or untruncated types. Here questions (1) and (2)
seem to pull in different directions. On one hand, if "there exists"
usually ends up truncated when translating set-based mathematics into
type theory, then we ought to allow ourselves to say "there exists"
when speaking about type theory; but on the other hand, how then are
we to state informally the untruncated theorems that we want to prove?

In section 3.10, the book actually suggests a general solution that
allows for the fact that different people may have different
preferences: set your default meaning for "there exists" and then use
an adverb like "merely" or "purely" for the other one.

The book does then choose an untruncated default itself, giving
various reasons listed in that section. However, it seems to me now
that most of those reasons actually pertain to question (2) and not
question (3); whereas there is no reason we can't allow untruncated
*theorems* but also (if we want) use "there exists" and "or" in a
truncated way by default. The book even comes close to doing this
already, because the symbols ∨ and ∃ are defined to be truncated (Def.
3.7.1).

I have said before that I would love to see a fork of the book written
with truncated logic, so that we could compare them and see which is
more convenient and comfortable. That way we'd actually have some
data, rather than just arguing back and forth about abstractions. Has
anyone written *any* informal type theory yet using truncated logic?

(One thing that worries me a bit is how to speak about
truncation-elimination; e.g. "... there exists x:A such that P(x).
Since our goal is a proposition, by truncation-induction we may assume
that ..." what? "there purely exists such an x"? "we have such an
x"?)

Mike

[Andrew Polonsky]

On Monday, February 9, 2015 at 4:33:19 AM UTC+1, Steve Awodey wrote:

There is nothing new about distinguishing propositions from general types: it is the standard way of doing things in topos theory, and in similar type theories going all the way back to Frege and Russell.  It was the idea that all types can be regarded as (“proof relevant”) propositions that was new in M-L type theory, as motivated by proof-theoretic considerations and predicativity.  

Shouldn't that be the other way?

The new idea is that all propositions (formulae) can be regarded as types (after Howard), and one can identify every proposition with the type of its proofs.

There are still types which are not propositions, like natural numbers and universes.

Andrew

On Monday, February 9, 2015 at 4:33:19 AM UTC+1, Steve Awodey wrote:

There is nothing new about distinguishing propositions from general types: it is the standard way of doing things in topos theory, and in similar type theories going all the way back to Frege and Russell.  It was the idea that all types can be regarded as (“proof relevant”) propositions that was new in M-L type theory, as motivated by proof-theoretic considerations and predicativity.  

The point of A&B was to show how to relate the two approaches while staying within a M-L style system (LCCC rather than topos) by distingishing the proof-irrelevant types among the others.  The rules for [bracket types] are not the same as those for Nuprl’s squash types, but the basic idea is very similar.  I don’t think there were any semantics before A&B — at least none that I am aware of.

Steve

On Feb 8, 2015, at 8:21 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

I do not know. There are claims that the squash types have been used in NuPRL much earlier than that paper but

I do not understand NuPRL’s theory well enough to compare what was there to what A&B suggested. 

Vladimir.

On Feb 8, 2015, at 8:12 PM, Daniel R. Grayson <d...@math.uiuc.edu> wrote:

Was the paper by Awodey and Bauer in 2001 ( see http://repository.cmu.edu/philosophy/67/ ) the first
to distinguish propositions from general types and to give semantics for the squash operation?

On Sun Feb 08 2015 at 5:10:38 PM Vladimir Voevodsky <vlad...@ias.edu> wrote:

This is from the first published Martin-Lof’s paper where he introduces his type theory (Logic Colloquium 1973):

<Screen Shot 2015-02-08 at 6.05.13 PM.png>

Note the “When B(s) represents a proposition” clause. There is also a discussion in the intro to this paper.

Obviously at that time there was no concept of h-level and so it was difficult to see how to distinguish propositions from the rest of the types and Per says that both every proposition defines a type and a type defines a proposition - the proposition saying that this type is non-empty. This is of course when we call the squash type or propositional truncation. 

Vladimir.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

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

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

<Screen Shot 2015-02-08 at 6.05.13 PM.png>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

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

[Andrew Polonsky]

In Howard's 1969 "On Formulae-as-Types notion of construction" (which PAT gets its name from), the type structure had natural numbers and equality between them as the ground types, and on top of that there was propositional logic and pi-types over naturals (to represent universal quantification).

So already in the first formal exposition of the propositions-as-types idea, there was a distinction between types that represent the "domain", and other types representing propositions about that domain.  The equality on the domain formed a proposition (a type).  The propositions did not have equality type.

Andrew

On Monday, February 9, 2015 at 12:10:34 AM UTC+1, v v wrote:

This is from the first published Martin-Lof’s paper where he introduces his type theory (Logic Colloquium 1973):

[Martin Escardo]

On 08/02/15 23:10, Vladimir Voevodsky wrote:
> This is from the first published Martin-Lof’s paper where he
> introduces his type theory (Logic Colloquium 1973):
>
>

> Note the “When B(s) represents a proposition” clause. There is also
> a discussion in the intro to this paper.
>
> Obviously at that time there was no concept of h-level and so it
> was difficult to see how to distinguish propositions from the rest
> of the types and Per says that both every proposition defines a
> type and a type defines a proposition - the proposition saying that
> this type is non-empty. This is of course when we call the squash
> type or propositional truncation.
>
> Vladimir.

Have you asked Per Martin-Loef himself to see what he meant then and
what he may mean today based on both his own revision of his thoughts
and what we are saying here?

It seems to me that there is a wide variety of degrees of existence. A
nice example is the following:

http://www.lmcs-online.org/ojs/viewarticle.php?id=971&layout=abstract

The nice thing about constructive mathematics is not (only) its
computational content, but (also) its ability to express subtle
notions of existence that are not available in the usual (official)
language of classical mathematics.

(But my contention is that classical mathematicians are perfectly
capable of appreciating the differences. It is just that by a
historical accident of the formalization of classical mathematics (by
logicians), it was decided that there is only one notion of existence
in classical mathematics. But practice demonstrates that this is
dubious. Classical mathematicians can see (and do), in practice,
various degrees of existence.)

M.

[Vladimir Voevodsky]

I suggest that we separate the question “what is existence” from the question “what is a proposition in the univalent foundations”.

Vladimir.

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

[Thomas Streicher]

> I suggest that we separate the question ???what is existence??? from the question ???what is a proposition in the univalent foundations???.

In my understanding in Martin-Loef type theory it was never intended
to accept as propositions only types all whose elements are
propositionally equal.
For example one certainly wants to distinguish different proofs that
there are infinitely many prime numbers since they give rise to
different functions from N to N.

Since Martin-Loef has in mind predicative foundations a type of
propositions doesn't make sense for him. (In Calulus of Constructions
this is different).
But even there propositions are not required to be proof irrelevant as
e.g. in realizability models where props are often identified with
modets sets (pers on a pca).

Thomas

[Jon Sterling]

Indeed. I think the idea of "propositions" being proof irrelevant seems
to be a very new notion, popularized by the UF/HoTT vocabulary. In
Nuprl, for instance, propositions-as-types was taken quite literally, in
the sense of the BHK interpretation; when speaking about type theory
from the 1970s and 1980s, one has got to be careful not to conveniently
back-date new definitions that were not in common use at the time.

On the other hand, in Brouwer's intuitionism it is sometimes difficult
to determine whether statements were meant to be proof relevant or not;
for instance, Escardó/Xu's new paper, “The inconsistency of a Brouwerian
continuity principle with the CH interpretation”
(http://www.cs.bham.ac.uk/~mhe/papers/escardo-xu-inconsistency-continuity.pdf)
seems to illustrate that the continuity principle for the Baire space
cannot be taken seriously as a proof-relevant proposition.

Kind regards,
Jon

[Michael Shulman]

On Mon, Feb 23, 2015 at 11:19 AM, Jon Sterling <j...@jonmsterling.com> wrote:
> Indeed. I think the idea of "propositions" being proof irrelevant seems
> to be a very new notion, popularized by the UF/HoTT vocabulary.

Let's not get too carried away -- propositions in ordinary mathematics
(based on first-order logic) have been proof irrelevant since ever.
(-: Only with type theory are proof-relevant propositions even
possible.

Mike

[Thierry Coquand]

The terminology "proof irrelevance" comes from de Bruijn 1974 (see e.g. his paper A survey of the project
Automath, section 24 and his reference there).
However, compared with the new notion of proposition, it was
for expressing the fact that any two given proofs are equal for judgemental equality (and not propositional
equality, or "book equality" in the terminology of Automath).

Best regards,
Thierry

________________________________________
From: HomotopyT...@googlegroups.com [HomotopyT...@googlegroups.com] on behalf of Jon Sterling [j...@jonmsterling.com]
Sent: Monday, February 23, 2015 8:19 PM
To: HomotopyT...@googlegroups.com
Subject: Re: [HoTT] not all types are propositions

[Steve Awodey]

and, of course, old-fashioned type theory a la Frege-Russell always had proof-irrelevant propositions.
Church’s formulation from 1940 even had a type of propositions which was a *poset*, in virtue of the extensionality axiom for propositions.
this is essentially the same in modern systems of higher-order logic / type theory.

Steve

[Jon Sterling]

:) You're quite right of course; to clarify, I mean propositions in
Martin-Löf's Type Theory.

Kind regards,
Jon

[Martin Escardo]

On 22/02/15 23:54, Vladimir Voevodsky wrote:
> I suggest that we separate the question “what is existence” from
> the question “what is a proposition in the univalent foundations”.

But the point is that some forms of existence, as in the so-called BHK
interpretation, deliberately are not "propositions" in the sense of
being types with at most one element.

Martin

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

[Thomas Streicher]

> But the point is that some forms of existence, as in the so-called BHK
> interpretation, deliberately are not "propositions" in the sense of
> being types with at most one element.

absolutely! and as long as propositions are proof irrelevant (in the
wider sense that all their proofs are propositionally equal) there
would not be much point in doing type theory `a la Martin-Loef, one could
work with HA_\omega or HAH

thomas

[Martin Escardo]

Coming back to the original issue of this thread, concerning what *is*
a proposition.

In classical mathematics, a *syntactical proposition* denotes a truth
value (not a type).

And so it does in many varieties of (formal) constructive mathematics,
including higher-type Heyting arithmetic and CZF (among many others).

And also in some models of (classical and constructive) mathematics,
such as toposes, where truth values are understood as subterminal
objects.

Type theory provides a point of departure from this idea, motivated by
the Brouwer-Heyting-Kolmogorov--Curry--Howard interpretation of
*syntactical propositions*. Now, under this interpretation, the
denotations of syntactical propositions are arbitrary types, not
necessarily truth values.

As we know, it turns out that that some types can be regarded as truth
values. The UF terminology for such a type is "proposition". Again,
internally, this is the same thing as a subterminal object.

For some special syntactical propositions, it turns our that their
BHK-CH interpretation is a truth-value.

A pertinent example is univalence. Vladimir proved in pure MLTT that
the type expressing univalence is a truth value. This is good, because
if we postulate it, as we do in UF, we don't want to worry about which
inhabitant we pick: all of them are equal. All that matters is that
univalence is true. (Proof irrelevance.)

It is good to talk about the types that are "truth values", or
"propositions" in UF terminology. We need to talk about them and hence
they deserve a name. What I am not sure about is whether they deserve
the terminology "proposition" as an appropriate designation.

Having said that, I do use this designation for them in publications,
although with regrets.

Martin

On 08/02/15 23:10, Vladimir Voevodsky wrote:

> This is from the first published Martin-Lof’s paper where he
> introduces his type theory (Logic Colloquium 1973):
>
>

> Note the “When B(s) represents a proposition” clause. There is also
> a discussion in the intro to this paper.
>
> Obviously at that time there was no concept of h-level and so it
> was difficult to see how to distinguish propositions from the rest
> of the types and Per says that both every proposition defines a
> type and a type defines a proposition - the proposition saying that
> this type is non-empty. This is of course when we call the squash
> type or propositional truncation.
>
> Vladimir.
>
>

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

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

[Vladimir Voevodsky]

Hi Martin,

what do you find disagreeable in the word “proposition”? Here is a definition from Boole (1847) p.19:

"A Proposition is a sentence which either affirms or denies"

When we think about representing propositions by sets we think of the false ones as represented by the empty set and the true ones as represented by the one point set.

The fact that this pair of sets (empty, one point) can be characterized by the property that the set of equalities between any two elements of these sets is a one point set is, I think, a very beautiful fact.

Logic was designed as a simplification of the real language. A subset that can be made understandable (and usable) for humans on a higher level of understanding than the wider language.

There is nothing surprising that as we move towards higher level of understanding of a wider part of the world of concepts logic becomes comprehended as a relatively small subset of what we can see and study today.

Vladimir.

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

[Martin Escardo]

Hi Vladimir,

On 25/02/15 01:03, Vladimir Voevodsky wrote:
> Hi Martin,
>
> what do you find disagreeable in the word “proposition”?

First of all, I agree with everything written by you below.

What I don't agree with is the following: the BHK-CH interpretation
maps *syntactical propositions* to types, and comes under the slogan

"propositions as types".

(Or sometimes "Formulas as types", which I think is more accurate.)

If one is allowed to read between the lines, my reading of this slogan
is

"[syntactical] propositions [interpreted as] as types [in such a
way that one doesn't necessarily get truth-value types]".

This was my reading in the previous message.

This is not at all incompatible with what you say below, except
terminologically.

It is a fact that the BHK-CH interpretation *does map* syntactical
propositions to types which are not in general propositions in your
sense (or truth-values in my proposed terminology).

This is not a matter of terminological decisions: it is the definition
of the BHK-CH interpretation: It takes a syntactical proposition, and
it maps it to a type, which is not necessarily a proposition in your
sense.

You may well disagree with considering the BHK-CH interpretation as
something useful. But it is there, and people work with it, and,
moreover, it is at the heart of the conception of MLTT.

So: usual practice, as you discuss below, by quoting Boole (1847),
takes syntactical propositions (interpreted) as truth values. But,
more recently, in the last century other people proposed another
interpretation of syntactical propositions. As types.

In the end, the discussion is purely terminological.

The problem here is that types are in the "semantic domain". And given
any syntactical proposition, there are two ways of mapping it into to
a type (Aristotle-Boole and BHKCH). You prefer one of the two, which
gives a truth-value in my terminology and a proposition in your
terminology (which I actually adopt in practice).

I'd rather have both, even combined.

Best wishes,
Martin

[Vladimir Voevodsky]

> It is a fact that the BHK-CH interpretation *does map* syntactical
> propositions to types which are not in general propositions in your
> sense (or truth-values in my proposed terminology).

Could you give an example?

[Martin Escardo]

On 25/02/15 02:33, Vladimir Voevodsky wrote:
>> It is a fact that the BHK-CH interpretation *does map*
>> syntactical propositions to types which are not in general
>> propositions in your sense (or truth-values in my proposed
>> terminology).
>
> Could you give an example?

If you want a truth value as an answer, the answer is simply yes.

More seriously, consider "for every n:N there is p:N such that p>n and
p is prime". The type that BHKCH-interprets this has infinitely many
inhabitants.

The propositional truncation, or truth-value reflection, of this is
given by the BHKCH-interpretation of "for every n:N there is a minimal
p>n such that p is prime".

But, in general, the truth-value reflection of the BHKCH
interpretation of a formula is not necessarily expressible in MLTT.

As another example, consider "every function N^N->N is
continuous". The BHK interpretation of this is false (despite the fact
that this principle holds in Brouwerian mathematics). But the standard
interpretation of this is independent (in MLTT - what happens in UF
regarding this is open).

M.

[Thomas Streicher]

Thanks, Martin, for expressing things so clearly.

As to terminology type theorists before HoTT would have called HoTT's
propositions "proof irrelevant" propositions.

In MLTT there was no proper notion of proposition but rather all types
were considered as propositions. Of course, one could stratify them
via universes.

This changed with CoC when there was introduced a type Prop of all
propositions which, however, were no aimed to be proof irrelevant.
Proof irrelevant models of Coq were easy and it was considered as a
major breakthrough that there were proof relevant models of CoC where
propositions are modest sets (PERs on a pca).

Squashing (not under this name) was known to exist in these models
those days. But the computational meaning was not clear and still it
is not (equalities for eliminator holding only propositionally).

BTW there is an alternative to "squashing" namely posetal reflection
of fibrations and that's the categorical formulation of what is done
in Martin-Loef type theory when going from t:A to A true. (One can
reflect categories to posets and so one an do in the fibres).

Thomas

[Vladimir Voevodsky]

On Feb 24, 2015, at 10:01 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

More seriously, consider "for every n:N there is p:N such that p>n and
p is prime". The type that BHKCH-interprets this has infinitely many
inhabitants.

What is this type?

Vladimir.

[David Roberts]

Wouldn't the inhabitants are sequences of pairs {(n,p_n) | n:N} such
that p_n > n is a prime?

David

[Martin Escardo]

Let's assume we know what the type "isPrime x" is, and that we have
defined as a "proposition" or "truth value". Assume likewise we have a
(propositional) type "x > y"

The type is then

Pi(n:N). Sigma(p:N). isPrime n \times p > n.

This is not a proposition in your sense, but is the BHK-CH
interpretation of the quoted statement.

Martin


>
> Vladimir.

[Vladimir Voevodsky]

We can keep the BHKCH interpretation in the UF. It is a valid and interesting construction and I see nothing wrong with it. However, having an interpretation of formulas into type theory, an interpretation that itself *depends on having the types already defined* does not make types into propositions.

The syntactic proposition ‘there exists a natural number n” is mapped by this construction to the type nat of natural numbers. This does not make nat into a proposition. Moreover, in order to even state the syntactic proposition in question one has to already have the type nat defined!

Vladimir.

[Vladimir Voevodsky]

On Feb 25, 2015, at 5:23 AM, Thomas Streicher <stre...@mathematik.tu-darmstadt.de> wrote:

This changed with CoC when there was introduced a type Prop of all
propositions which, however, were no aimed to be proof irrelevant. 
Proof irrelevant models of Coq were easy and it was considered as a
major breakthrough that there were proof relevant models of CoC where 
propositions are modest sets (PERs on a pca).

Is the type of propositions in these models impredicative? I would think that the negation of proof irrelevance combined with impredicativity would lead to an inconsistency.

Vladimir.

[Michael Shulman]

On Wed, Feb 25, 2015 at 2:23 AM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> As to terminology type theorists before HoTT would have called HoTT's
> propositions "proof irrelevant" propositions.

But it is true, isn't it, that Vladimir was the first to realize that
the notion "P is proof irrelevant" could be defined *inside* type
theory? In CoC the type Prop is introduced by fiat, whereas in
UF/HoTT the corresponding type is *defined*.

Mike

[Michael Shulman]

On Wed, Feb 25, 2015 at 8:08 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> We can keep the BHKCH interpretation in the UF. It is a valid and interesting construction and I see nothing wrong with it. However, having an interpretation of formulas into type theory, an interpretation that itself *depends on having the types already defined* does not make types into propositions.
>
> The syntactic proposition "there exists a natural number n" is mapped by this construction to the type nat of natural numbers. This does not make nat into a proposition. Moreover, in order to even state the syntactic proposition in question one has to already have the type nat defined!

I think exactly the same thing could be said about the interpretation
you favor. The same syntactic proposition "there exists a natural
number n" is mapped by that interpretation to the propositional
truncation ||nat|| of the type nat. But that doesn't make ||nat||
into a proposition either! Unless we *declare* that we will use the
word "proposition" also for certain types, and then we have a choice
about which types to use.

I don't see much point in arguing about the "correct" way to use the
word "proposition". I am more interested in the three concrete
questions I raised in my email 2 weeks ago. But since no one has
responded to it, maybe no one else is interested in them...

Mike

[Jon Sterling]

Mike,

Can you clarify what you mean by this? First "P is proof irrelevant" is
a predicate on types P, and has been *definable* in standard type theory
for ages prior to UF (via squash types, or even just by means of the
identity type); on the other hand, Prop in CoC is a sort which
guarantees this property syntactically, and as such seems not to have an
analogue in UF/HoTT or "proper" MLTT.

Kind regards,
Jon


>
> Mike

[Michael Shulman]

On Wed, Feb 25, 2015 at 9:49 AM, Jon Sterling <j...@jonmsterling.com> wrote:
> First "P is proof irrelevant" is
> a predicate on types P, and has been *definable* in standard type theory
> for ages prior to UF (via squash types, or even just by means of the
> identity type)

I don't mean via squash types: the propositional truncation in UF/HoTT
is defined in terms of the notion of "being proof irrelevant", not the
other way around. But yes, via identity types, as with Vladimir's
definition. Are you saying that people knew for a long time how to
define "being proof irrelevant" in terms of the identity type? It's
not hard, of course, but I guess I assumed that if people knew it,
they would have used it, and I've never seen it used anywhere. E.g.
why would you postulate a type of possibly-proof-irrelevant
propositions by fiat, as with CoC's Prop, if you know how to *define*
proof-irrelevance?

Mike

[Jon Sterling]

Hi Mike,

1. Can you clarify what you mean by propositional truncation being
defined in terms of "being proof irrelevant"? In my view, the
propositional truncation is precisely a replay of one of the several
flavors of squash types that were invented in the past 20-30 years (i.e.
squashing by taking a quotient, which is precisely the propositional
truncation in UF/HoTT). In short, here are the methods of truncation
which pre-dated UF/HoTT: ||P|| can be defined using quotient types
x,y:P//Unit, subset types {x:Unit | P}, image types Img(A; x. <>).

2. I do not know if people had previously used the identity type for the
purpose of defining the concept of being "proof irrelevant". Squash
stability, which seems equivalent (at least in ETT), is a bit easier to
deal with anyway, so this is what was used (i.e. ||P|| -> P).

3. I think CoC's Prop has to do with two things. CoC doesn't have a
squash type, so you need the Prop sort in order to take advantage of the
kind of "proof irrelevant modality" that often becomes necessary. Not to
mention that there is impredicative quantification over Prop, so it is
necessary to consider it separately from sets in general.

Best,
Jon

[Vladimir Voevodsky]

As far as I know, the first ones to define propositions by the condition of p[roof irrelevance inside type theory (MLTT) were Awodey and Bauer.

I was the first one to realize that the notion of being proof irrelevant is one of the infinitely many notions of the hierarchy of h-levels.

This connection between being "proof irrelevant" and being “an n-type” is, as far as I know, something that I have discovered.

Vladimir.

[Michael Shulman]

On Wed, Feb 25, 2015 at 10:07 AM, Jon Sterling <j...@jonmsterling.com> wrote:
> 1. Can you clarify what you mean by propositional truncation being
> defined in terms of "being proof irrelevant"?

The HIT propositional truncation is, essentially by definition, a type
||A|| such that any map from A into a proof irrelevant type B factors
through ||A|| uniquely. Vladimir's earlier impredicative construction
of ||A|| is even more explicit about this: ||A|| is the assertion that
A implies all proof irrelevant types. So you have to have an internal
definition of proof irrelevance (in terms of the identity type) before
you can state either of these definitions.

Also, thanks Vladimir for pointing out Awodey-Bauer. I think I was
thinking that their definition isn't quite as internal as yours, i.e.
they only hypothesize proof-irrelevance judgmentally in the rules for
[A], rather than defining a *type* isProofIrrelevant(P). But of
course they couldn't have done that anyway, given that their desired
semantics was regular categories (hence no Pi-types); and quite likely
they did have it in mind (Steve, Andrej?).

Mike

[Martin Escardo]

Our disagreement is only terminological. Martin

[Bas Spitters]

IIUC Awodey and Bauer where trying to capture NuPrl's squash types
categorically.
They only did the extensional version, as this had a more natural fit
with categorical semantics.
When we were discussing this apparent mismatch in 2004 Steve mentioned
that he had started thinking about higher groupoid models to "fix"
this, i.e. to extend it too intentional models.

There was quite a bit of work around UIP, K-axiom, etc. I have the
impression that people realized that there were much more complex
types, but this was seen as a bug rather than a feature. Thomas will
certainly know more about the history. I imagine that the step from
the then conjectured n-groupoid models to the n-levels would not have
been so big. However, it was unclear to most type theorists why anyone
would care. I think it is more clear now :-)

[Thomas Streicher]

> But it is true, isn't it, that Vladimir was the first to realize that
> the notion "P is proof irrelevant" could be defined *inside* type
> theory? In CoC the type Prop is introduced by fiat, whereas in
> UF/HoTT the corresponding type is *defined*.

well, the problem was to find models where Prop was proof relevevant

those days one used extensional type theory (outside Sweden) and it
was obvious how to formulate proof irrelevance inside type theory
I even don't see why this were a great insight, it's really obvious

Martin I formulated UIP in our paper but that was not original at all
the problem only was to find a model where UIP fails

thomas

[Michael Shulman]

Ok, I stand corrected.

[Nicola Gambino]

Dear all,

Another reference that may be useful in this discussion is

Maria Emilia Maietti, “The type theory of categorical universeses”, PhD thesis, University of Padova, 1998

and her paper "Modular correspondence between dependent type theories and categorical universes including pretopoi and topoi”, which appeared in Mathematical Structures in Computer Science.

Best wishes,
Nicola


===
Dr Nicola Gambino
School of Mathematics
University of Leeds
n.ga...@leeds.ac.uk

[Andrei Rodin]

Concerning Michael’s Question #2 from this thread. When one reserves the term “proposition” only to “mere” proposition in the sense of the Book, one does not need to understand the word “theorem” also so restrictively. Each theorem *contains* a proposition but is not itself a (mere) proposition. In a different context this point has been made clear already by Proclus in his Commentary to Euclid.  So I cannot see that the Question #2 indeed pulls us to a more liberal understanding of the term.
The type-theoretic analysis of the concept of proposition sheds a new light on the received notion of axiomatic theory; I developed this argument here:  http://arxiv.org/abs/1408.3591v3 

On Monday, 9 February 2015 03:10:34 UTC+4, v v wrote:

This is from the first published Martin-Lof’s paper where he introduces his type theory (Logic Colloquium 1973):