Morphoid Type Theory

[David McAllester]

I have just posted an arXiv paper Morphoid Type Theory presenting an independently developed typed foundation.  This foundation is classical and extensional and has a denotational semantics taking values from a model of ZFC.

I have intentionally not studied HoTT --- I wanted the development to be independent. Now however, my system is now well enough formulated that it seems imperative for me to try to relate it to HoTT.  I have applied to be added to this list.  I look forward to exploring HoTT.

David McAllester

Abstract:

Morphoid type theory is a typed foundation for mathematics in which each type is associated with an equality relation in correspondence with the standard notions of isomorphism in mathematics.  The main result is an abstraction theorem stating
that isomorphic objects are substitutable in well typed contexts.  A corollary is ``Voldemort's theorem'' stating that a non-canonical object, like a point on a circle, or an isomorphism between a finite dimensional vector space and its dual, cannot be named by a well typed expression.

Morphoid type theory seems different from the recently developed homotopy type theory (HoTT). Morphoid type theory is classical and extensional while HoTT is constructive and intensional. Morphoid type theory does not involve homotopy theory.  Morphoids are technically quite different from the infinity groupoids of HoTT.

[Thorsten Altenkirch]

From: David McAllester <mcall...@ttic.edu>
Date: Thu, 29 Jan 2015 12:48:05 +0000
To: "HomotopyT...@googlegroups.com" <homotopyt...@googlegroups.com>
Subject: [HoTT] Morphoid Type Theory

I have just posted an arXiv paper Morphoid Type Theory presenting an independently developed typed foundation.  This foundation is classical and extensional and has a denotational semantics taking values from a model of ZFC.

What is the point of non-constructive foundations, especially in Computer Science?

I have intentionally not studied HoTT --- I wanted the development to be independent. Now however, my system is now well enough formulated that it seems imperative for me to try to relate it to HoTT.  I have applied to be added to this list.  I look forward to exploring HoTT.

David McAllester

Abstract:

Morphoid type theory is a typed foundation for mathematics in which each type is associated with an equality relation in correspondence with the standard notions of isomorphism in mathematics.  The main result is an abstraction theorem stating
that isomorphic objects are substitutable in well typed contexts.  A corollary is ``Voldemort's theorem'' stating that a non-canonical object, like a point on a circle, or an isomorphism between a finite dimensional vector space and its dual, cannot be named by a well typed expression.

Morphoid type theory seems different from the recently developed homotopy type theory (HoTT). Morphoid type theory is classical and extensional while HoTT is constructive and intensional. Morphoid type theory does not involve homotopy theory.  Morphoids are technically quite different from the infinity groupoids of HoTT.

In what sense is HoTT not extensional?

Cheers,

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.

[Frédéric Blanqui]

Le 29/01/2015 14:48, Thorsten Altenkirch a écrit :

From: David McAllester <mcall...@ttic.edu>
Date: Thu, 29 Jan 2015 12:48:05 +0000
To: "HomotopyT...@googlegroups.com" <homotopyt...@googlegroups.com>
Subject: [HoTT] Morphoid Type Theory

I have just posted an arXiv paper Morphoid Type Theory presenting an independently developed typed foundation.  This foundation is classical and extensional and has a denotational semantics taking values from a model of ZFC.

What is the point of non-constructive foundations, especially in Computer Science?

The formalization of non-constructive maths?

[David McAllester]

What is the point of non-constructive foundations, especially in Computer Science?

Perhaps mathematics is more than computer science.

In what sense is HoTT not extensional?

I admit to being naive regarding HoTT.  But from the HoTT home page we have:

Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.

From the Wikipedia page we have:

In mathematical logic and computer science, homotopy type theory (HoTT) refers to various lines of development of intensional type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies.

I'm not sure how one precisely defines "intensional" and "extensional" but the property that I value is that expressions have compositional semantics (denotations) and that the meaning (the extension) is intuitively correct.  For example, an expression denoting the real numbers should denote the actual real numbers up to isomorphism in sense of mainstream mathematics.  There should be uncountably many reals --- the same cardinality as the power set of the integers.

I am going to try to get more familiar with the details of HoTT.

David

[Thorsten Altenkirch]

From: David McAllester <mcall...@ttic.edu>
Date: Thu, 29 Jan 2015 15:24:14 +0000
To: "HomotopyT...@googlegroups.com" <homotopyt...@googlegroups.com>

Subject: Fwd: [HoTT] Morphoid Type Theory

What is the point of non-constructive foundations, especially in Computer Science?

Perhaps mathematics is more than computer science.

Indeed, if you work for a company with a large Cobol library you may not be interested in modern programming languages. That doesn’t mean that we should all program in Cobol.

The evolution of Mathematics is held back by its long history – a modern discipline like Computer Science could have a positive impact here. I find it disappointing when Computer Scientists to whom constructive thinking should come natural are stuck in the past just because the mainstream Maths is.

In what sense is HoTT not extensional?

I admit to being naive regarding HoTT.  But from the HoTT home page we have:

Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.

In a sense HoTT is more extensional as set theory or extensional type theory can be because it interprets equality of structures as equivalence. E.g. For ordinary “sets” this is isomorphism since type theory prevents you to observe any property of a set which is not stable under isomorphism.

From the Wikipedia page we have:

In mathematical logic and computer science, homotopy type theory (HoTT) refers to various lines of development of intensional type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies.

I'm not sure how one precisely defines "intensional" and "extensional" but the property that I value is that expressions have compositional semantics (denotations) and that the meaning (the extension) is intuitively correct.  For example, an expression denoting the real numbers should denote the actual real numbers up to isomorphism in sense of mainstream mathematics.  There should be uncountably many reals --- the same cardinality as the power set of the integers.

To me extensionality means that we identify objects up to their observable behaviour. E.g. The only thing you can do with a function is to apply it to an argument hence extensionally two functions which have the same input/output behaviour should be identified. If you start talking about how the function is actually defined (e.g. It uses primitive recursion) you refer to intensional properties.

Btw, constructively the reals are not isomorphic to the powerset of the integers. 

Thorsten

I am going to try to get more familiar with the details of HoTT.

David

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

> In what sense is HoTT not extensional?

in the sense that propositional equality doesn't entail judgemental
equality

thomas

[Andrej Bauer]

It would be good to know how your theory relates to that of HOL, or
Church's simple type theory, as it looks somewhat similar.

It would also be good to have a quick overview of what is going on.
Let me start, and you correct me when I go wrong.

It's a type theory with (simple) function spaces, dependent sums,
subtypes, and a hierarchy of type universes. There is Bool, which
embodies classical logic and there is choice.

There is an equality relation on each type which maps into Bool.

Correct me if I am wrong, but you do not have in your syntax any
constructs for defining functions, nor do you have an introduction
rule for the function types. Consequently, you do not give any axioms
for equality on a function type, such as beta-reduction. One would
presumably have to give all of these, or I completely missed them.

You do not give any notion of equality between types. Thus, for
instance, it is not clear whether and in what sense SubType(x:t, phi)
and SubType(x:t, phi') are interchangable when phi = phi'.

In the semantics, a type is interpreted by a "morphoid", which is a
substructure of groupoids (I would appreciate some motivation after
Definition 3.3.) There is the groupoid of "points" (Definition 3.6),
which for the rest of us is just the indiscrete groupoid on a universe
of sets U (i.e., the objects are sets and there is one morphism
between any two sets). A type is interpreted as a morphpoid in the
groupoid of points. This is going to take care of all coherence issues
regarding subtypes, presumably.

Figure 5 on page 25 seems to indicate that you're doing some sort of
parametric and/or polymorphic semantics with respect to the indiscrete
groupoid of a universe of sets. The abstraction theorem reminds one of
parametricity results in polymoprhic lambda calculus.

The semantics is given recursively on the structure of the expression
and a type. In particular, you need not know what type a given
expression has in order to give its meaning (in John Reynold's
terminology you're doing extrinsic semantics). This way you avoid
coherence questions. Non-sensical expressions still have a meaning in
virtue of set-theoretic hackery.

I could not find a clear explanation on how you handle type dependency
in subtypes, and how you handle type variables. My guess is that since
you have a groupoid which acts as the universe, you may simply think
of an expression with a type parameter as a map from the universe (and
of course there will be limitations on what such maps may be).

I apologize if I missed large chunks of the axioms, but you should
consider introduction forms for functions (lambda abstraction),
equations governing functions (beta and eta rules), and you should
explain when one type is interchangable with another (because you have
dependent types in the form of SubType).

If these things are there, it's going to look like a groupid model
based on the indiscrete groupoid of a universe of sets. There might be
something much nicer in there, but for that I would have to undertand
the idea of morphoids first.

With kind regards,

Andrej

[David McAllester]

Constructivity goes back to Brouwer.  In the 1950s and 60s constructivity had more currency in mainstream mathematics than it does today.  Time will tell which camp is stuck in the past.

This is a very old debate and we are not going to settle it here.  My paper shows that a classical non-constructive typed foundation supporting the substitution of isomorphics is possible.

Btw, constructively the reals are not isomorphic to the powerset of the integers. 

My point exactly .

David 

[Andrej Bauer]

On Thu, Jan 29, 2015 at 5:41 PM, Andrej Bauer <andrej...@andrej.com> wrote:
> There is Bool, which embodies classical logic and there is choice.

As soon as I pressed "Send" I realized that choice gives you plenty of
elements of function types. However, it's still not clear to me how
his works in the end. Your axiom of choice concludes existence of a
choice function in terms of the existential quantifier, which through
classical logic is encoded with negation and universal quantifier.
There is no definite description operator a la Russell, not Hilbert's
indefinite description operator, so how do you ever generate a term of
a function type.

Concretely, is there a term which denotes the identity function t -> t
where t is a type? Of course, you can show one exists, but is there a
term denoting it?

With kind regards,

Andrej

[Andrej Bauer]

On Thu, Jan 29, 2015 at 5:46 PM, David McAllester <mcall...@ttic.edu> wrote:

My paper shows that a classical non-constructive typed foundation supporting the substitution of isomorphics is possible.

I understand that such a theorem is possible in the semantics, but it would be far more useful if the type theory internalized it -- as then it actually becomes something that can be used in formalization. That is,  your theory should/could have a notion of equality between types and a principle which stated that isomorphic types are interchangable everywhere. Is this in your paper?

With kind regards,

Andrej

[David McAllester]

It's a type theory with (simple) function spaces, dependent sums,
subtypes, and a hierarchy of type universes. There is Bool, which
embodies classical logic and there is choice. 

There is an equality relation on each type which maps into Bool.

Correct me if I am wrong, but you do not have in your syntax any
constructs for defining functions, nor do you have an introduction
rule for the function types.

There is an introduction rule for function types at the beginning of the third line of figure 1. There are indeed no lambda terms or beta reduction rule.  There are technical difficulties in the semantics of lambda expressions and I was essentially forced to omit them. Functions are introduced with the axiom of choice which simply says that functions with desired properties exist.  There is an argument in section 2 that the axiom of choice subsumes the introduction rule for lambda expressions.  This is very classical.

Equality is entirely in the semantics and not in the rules.  More on this later.

For any two types sigma and tau we have sigma =_{type} tau if sigma and tau have the same cardinality.  If we have

Sigma;  alpha:type  |=  e[alpha]:tau

and

Sigma |=  sigma =_{type} gamma

then we have

Sigma |=     e[sigma] =_{tau} e[gamma]

This is a special case of the general substitution rule.  Here =_{type} semantically means "same cardinality" where this is defined classically as the existence of a (classical)  bijection.

In the semantics, a type is interpreted by a "morphoid", which is a
substructure of groupoids (I would appreciate some motivation after
Definition 3.3.)

There is motivation in the informal overview (section 1).  We want x:sigma to mean in general that x is a sigma-isomorphism.  Here the type elements are also the isomorphisms.  We than have the conundrum of the context alpha:type; x: alpha. Here alpha acts as both a type isomorphism (a bijection) and a type (a thing that has isomorphisms as elements).  A morphoid is the structure that satisfies these two constraints together as explained informally in section 1 and formally in lemmas 3.10, 3.11 and 3.12.

There is the groupoid of "points" (Definition 3.6),
which for the rest of us is just the indiscrete groupoid on a universe
of sets U (i.e., the objects are sets and there is one morphism
between any two sets). A type is interpreted as a morphpoid in the
groupoid of points.

In later sections there are also types whose element are not points.  For example the type "Group" has groups as elements.

The abstraction theorem reminds one of
parametricity results in polymoprhic lambda calculus.

Yes, this is a good analogy.  Logical relations are in some sense analogous to isomorphism relations but much simpler.  Reynold's abstraction theorem implies that objects which are related at a type are substitutable into Boolean contexts accepting that type.  But this only holds it a language without equality at function types and without quantification at infinite types.  Isomorphism allows substitution into much richer contexts and the technical issues are (for me) much more difficult.

The semantics is given recursively on the structure of the expression
and a type. In particular, you need not know what type a given
expression has in order to give its meaning (in John Reynold's
terminology you're doing extrinsic semantics).

Hmm...  I'm not sure that I can concisely do justice to section 13 here.  Perhaps I can say simply that the semantics fully specifies a meaning for Sigma |= e:tau and that if this holds then for every model rho of the context Sigma we have

V_{Sigma}[e]rho     \in    V_{Sigma}[tau]rho

I should also add that the set of models of any well formed context Sigma itself forms a groupoid and we can think of the context as a type whose semantics is also well defined.

I could not find a clear explanation on how you handle type dependency

in subtypes.

We have that x:sigma |= x:tau states naive set theoretic containment as in

G: AbelianGroup |= G:Group

and how you handle type variables.

Type variables are introduced with variable declarations alpha:type which is a special case of general declarations of the form x:sigma.

I am being called to lunch, more later.

David

P.S. Thank you for your interest!!

[David McAllester]

The idea is that no term denoting the identity function is needed.  If I can prove that something exists then I can declare a variable at the base of the context and then I have a term (the variable).

Set theory has no terms at all.  Some books on set theory discuss "virtual terms". This is a systems engineering issue.  I am confident that one could construct a proof assistant with appropriate virtual terms.

David

[Thorsten Altenkirch]

This is the definition of "extensional type theory" which is a misnomer. While like set theory ETT has functional extensionality it cannot (like set theory) support the univalence principle which identifies equivalent structures.

Thorsten

Sent from my iPad

[David McAllester]

Yes, equality is handled in the semantics.  There are partial rules for equality given in section 18 and I agree that extending these two an adequate set is important.  I am confident that this can be done, but there are some technicalities.

David

[Peter LeFanu Lumsdaine]

It is perhaps worth restating here that HoTT is *not* anti-classical, it’s just *agnostic* about classicality principles.

Excluded middle for propositions, and AC stated using sets and the hprop logic, can be added alongside Univalence and HITs. These hold in the simplicial sets model over a classical foundation, for instance.  This is then a rather classical setup: one will be able to prove that the reals *are* isomorphic to the powerset of the integers, and so on.

I haven’t read the morphoids work, so I don’t know how this compares to the picture there.  But I just want to beat back, again, the apparent misconception that Univalence in HoTT is in some way anti-classical.

–p.

[David McAllester]

Peter,

Thanks for the reminder that HoTT and Coq are agnostic on constructivity.

I have a strong belief that the standard practice of mathematics incorporates a well defined notion of isomorphism.  If both HoTT and morphoid type theory capture this intuitive notion then they should agree. 

I need to study HoTT.  One thing that I find mysterious is the role of homotopy theory.  I did not use any homotopy theory.  Another thing that I find mysterious is univalence as an axiom.  The central statement in morphoid type theory is a theorem --- the abstraction theorem stating the validity of substitution of isomorphics.  But, as I said, I need to study HoTT.

David

[Jason Gross]

On Thu, Jan 29, 2015 at 1:10 PM, David McAllester <mcall...@ttic.edu> wrote:

Another thing that I find mysterious is univalence as an axiom.  The central statement in morphoid type theory is a theorem --- the abstraction theorem stating the validity of substitution of isomorphics.

I suspect the corresponding theorem in HoTT is that the univalence axiom is true of some models.  The slightly stronger(?) theorem, which justifies assuming univalence as an axiom within the theory, is that the univalence axiom holds internally in some models.

As I understand it, the difference is similar to the difference between Reynold's abstraction theorem, and internalizing parametricity.

[Vladimir Voevodsky]

Hi Thorsten,

please stop being difficult. I have a more math question - how morphoids are different from setoids?

Vladimir.

[Martin Escardo]

On 29/01/15 20:21, Peter LeFanu Lumsdaine wrote:
> It is perhaps worth restating here that HoTT is *not* anti-classical,
> it’s just *agnostic* about classicality principles.

(1) Like Bishop mathematics.
(2) Like Martin-Loef type theory.
(3) Like HA^omega.
(4) Like the internal language of an unspecified elementary topos.

All of them are referred to as constructive or intuitionistic
mathematics, but really they are agnostic mathematics.

But I don't like "agnostic", as terminology, because it implies a
philosophical, and even religious, take, which really is not necessary
for the purposes of understanding, justifying, and practising this
kind of mathematics.

Privately, I have advocated "neutral" or "absolute", in analogy with
the terminology applied to Eucliean geometry, rather than
"constructive".

* You get neutral or absolute geometry by omitting the parallel
postulate from the axioms of geometry.

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

* You get Euclidean geometry by having the parallel postulate.

* You get non-Eucliean geometries (of many kinds) by having any
postulate that implies the negation of the parallel postulate.

I would advocate adopting "absolute mathematics" as an alternative to
"constructive mathematics".

But perhaps this sounds pretentious.

More humbly, I would advocate adopting "neutral mathematics".

But perhaps this sounds defensive.

Whether we call it constructive, intuitionistic, agnostic, absolute,
neutral or whatever, the point is that it is *more general* than
classical mathematics.

However, constructive mathematics is perceived as less general.

The examples (1)-(4) are definitely *more* general. And so is HoTT.

I would refer to the two typical anti-classical examples of
"constructive" mathematics (Brouwer, Markov) as non-classical
mathematics (in analogy with non-Euclidean geometry).

In any case, "agnostic", "neutral", "absolute" convey in a much better
way what is going on, compared to "constructive" (which may include
anti-classical varieties of mathematics).

The theorems of absolute/neutral mathematics, in your chosen (formal
or informal) foundation for mathematics, hold for the classical,
non-classical, constructive, and non-constructive special cases of
your foundation.

| Classical mathematics
|
|
| Non-classical mathematics \
| (Brouwer, Markov) \
| \
| -> include all varieties of
| / "constructive" mathematics
| /
| Neutral/absolute mathematics /
| (Bishop, Martin-Loef)

Peter Aczel has a similar position, using (non-)Abelian groups as an
analogy to explain this understanding.

However, the geometric analogy given above has the advantage that
once-upon-a-time non-Euclidean geometry was considered as a
philosophical problem.

Likewise, constructive mathematics should *not* be regarded as a
philosophical problem any longer. But it seems to be.

The terminologies "absolute" or "neutral" better characterize what is
intended. (But, as discussed above, they are not without their PR
problems.)

Martin

[Fran Mota]

Voevodsky wrote:
> I have a more math question - how morphoids are different from setoids?

From what I understand, morphoids can have multiple "isomorphisms" between two objects, rather than just defining a binary relation.

My understanding from reading a little bit of the paper is that morphoids are like groupoids in which not all arrows are invertible. My question then is: how are morphoids different from categories?

[Bas Spitters]

EB Davis uses "pluralism" in this nice article from 2004:
http://www.mth.kcl.ac.uk/staff/eb_davies/EBDRS1.pdf
PLURALISM IN MATHEMATICS
"We defend pluralism in mathematics, and in particular Errett Bishop’s
constructive approach to mathematics, on pragmatic grounds, avoiding the
philosophical issues which have dissuaded many mathematicians from taking
it seriously. We also explain the computational value of interval arithmetic.
keywords: pluralism, constructive mathematics, interval arithmetic"

[Andrej Bauer]

Generalized mathematics.

[Erik Palmgren]

I think a relevant reference is

Fred Richman. Intuitionism as generalization, Philosophia Mathematica, 5
(1990), 124-128.

http://math.fau.edu/richman/Docs/philmath.pdf

________________________________________
Från: HomotopyT...@googlegroups.com
[HomotopyT...@googlegroups.com] f&#246;r Andrej Bauer
[andrej...@andrej.com]
Skickat: den 30 januari 2015 08:25
Till: Martin Escardo
Kopia: HomotopyT...@googlegroups.com
Ämne: Re: [HoTT] Agnostic mathematics

Generalized mathematics.

[David McAllester]

A morphoid is defined to be a subset (not a subcategory) of (the arrows of) a groupoid such that for x,y,z in M with x circ y^{-1} circ z defined (domains matching codomains), we have x circ y^{-1} circ z in M (the morphoid closure condition).  I identify objects with their identity morphisms. Two arrows x and y in Morphoid M are equivalent if there exists an arrow z in M with x circ z^{-1} circ y defined.    The morphoid closure condition implies that this is indeed an equivalence relation on the elements (arrows) of the morphoid.  It also implies that the arrows of the form x circ y^{inv} for x,y in M forms a "left groupoid" and the arrows of the form x^{inv} \circ y form a "right groupoid" and the morphoid itself defines a bijection between the equivalence classes (connected components) of the left and right groupoids.  Every arrow in the morphoid is directed from the left groupoid to the right groupoid. A morphoid is simultaneously a type (a set of arrows) and a type isomorphism (a bijection between types).

David

[Andrej Bauer]

Definition 3.3 of moprhoid seems to have a typo (it shoudl say "for
all x, y, z in O" instead of "for all x, y, x in O"). Let suppose I
correctly interpreted the typo, then it says:

"A morphoid is a subset of the arrows of a groupoid such that,
whenver x * y^-1 * z is defined then x * y^-1 * z is in O."

From this it follows that the only morphoid is the whole groupoid
itself: given any arrow w in the ambient groupoid, take x = w, y = w
and z = w. Then x * y^-1 * z = w * w^-1 * w = w is well defined and
equal to w, hence w is in the morphoid.

Unless I am mistaken, there are no nontrivial morphoids.

With kind regards,

Andrej

[Andrej Bauer]

On Fri, Jan 30, 2015 at 11:22 AM, Andrej Bauer <andrej...@andrej.com> wrote:
> Definition 3.3 of moprhoid seems to have a typo (it shoudl say "for
> all x, y, z in O" instead of "for all x, y, x in O"). Let suppose I
> correctly interpreted the typo, then it says:

I misread the definition, sorry for the noise. It says:

"A morphoid within a given groupoid C is a subset O of C
such that for x, y, x ∈ O with x ◦ y−1 ◦ z defined
we have x ◦ y−1 ◦ z ∈ O."

The problem is with "for x, y, x ∈ O" which shuld be "x, y, z ∈ O",
whereas I read it as "x, y, x ∈ C". So my argument doesn't go through.

With kind regards,

Andrej

[Peter LeFanu Lumsdaine]

On Fri, Jan 30, 2015 at 1:24 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

Privately, I have advocated "neutral" or "absolute", in analogy with
the terminology applied to Eucliean geometry, rather than
"constructive".

I find “absolute” rather problematic: it suggests something very final, and, well, absolute, which is surely inaccurate and a bit hubristic.  We’ve stopped taking AC and LEM for granted — but there are plenty of ways our systems could be weakened/generalised still further.  If we call our maths “absolute”, what do we say when someone else comes along with a cool new foundational system based on, say, linear or relevant logic?

–p.

[Michael Shulman]

These sorts of discussions are important for clarifying the meaning of
the word "constructive" and conveying that meaning to the wider
mathematical audience, but frankly I think that at this point any
attempt to actually *replace* the word "constructive" isn't going to
get very far off the ground.

[Martin Escardo]

I agree that we are stuck with the terminology "constructive".

But I feel compelled to make explicit that it is misleading.

(1) Take Brouwerian mathematics.

It is non-classical: its continuity axioms imply the negation
of excluded middle (our analogue of the parallel postulate).

But it is constructive in the sense that algorithms can
be attached to it.

Brouwerian mathematics is like non-Euclidean geometry.

(2) Take synthetic differential geometry. It postulates the
existence of d > 0 with d^2=0 and the axiom of local linearity
for functions R->R, using this d to formulate this.

It is non-classical again. It negates excluded middle.

So again it is like non-Euclidean geometry.

But it is not constructive (a priori): I don't think anybody
ever claimed that SDT has (or should have) computational
content.

(3) Take HoTT (in its HoTT-book incarnation).

It doesn't assume or reject excluded middle, and qualifies as a
form of intuitionistic mathematics, and hence, terminologically
speaking, constructive mathematics.

HoTT is excluded-middle agnostics (or politically correct).

But it is not constructive a priori, in the sense of having
algorithms attached to it by design.

In fact, the constructivity problem for HoTT has attracted
considerable attention (with positive outcomes in this
direction, but with hard work to get them).

There is a long way from agnosticism to constructivity.

Martin

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

[David McAllester]

I have just posted a new version of my paper on morphoid type theory on arXiv.  Unlike the version of a year ago, this version includes an internalization of isomorphism and a meaningful discussion of the relationship to HoTT.

​  I also believe that this version is vastly more accessible.

Abstract: Morphoid type theory (MorTT) is a typed foundation for mathematics extending classical predicate calculus under Platonic compositional semantics and supporting the concept of isomorphism. MorTT provides a formal account of the substitution of isomorphics, the distinction between general functions and natural maps, and "Voldemort's theorem" stating that certain objects exist but cannot be named. For example, there is no natural point on a geometric circle --- no point on a geometric circle can be named by a well-typed expression. Similarly

​,​

it is not possible to name any particular basis for a vector space or any particular isomorphism of a finite dimensional vector space with its dual. Homotopy type theory (HoTT) also provides a formal account of isomorphism but extends constructive logic rather than classical predicate calculus. MorTT's classical approach avoids HoTT's propositions-as-types, path induction, squashing and higher order isomorphisms. Unlike HoTT, MorTT is designed to be compatible with Platonic mathematical thought.

​David McAllester​

[Andrej Bauer]

Dear David,

I had a look at your new version of MoTT
(http://arxiv.org/pdf/1407.7274v5.pdf). I have not had the time to
study is seriously, but here are a couple of technical remarks. As it
stands, the formulation of MoTT does not seem to hold water.


It would be very helpful if at the beginning you listed not only all
syntax of terms and propositions, but also the syntax of types (it
looks like the only types are Bool, type_i, and function types?), as
well as all forms of judgements. Several constructs are missing
formation rules (:: and iso for instance), you never announce the fact
that there will be judgmenal equality (which you call absolute
equality), etc. Such omissions create a confusion that is hard to
penetrate. Also, I find "Γ ⊢ True" to be a strange way of saying that
Γ is well-formed context. How about something like "Γ context"?


At the bottom of page 7 you make it sound like in HoTT people are only
concerned with consistency of HoTT and not at all the meaning. You
base this opinion on the HoTT book. I would just like to point out
that the HoTT book does pay attention to the *intuitive* explanation
of what types are, but was purposely written *avoiding* any
discussions of models of HoTT (as a foundation, HoTT/UF has to stand
on its own feet, without reference to a "model"). There are other
bibliographical sources discussing the meaning of HoTT.


Your axioms for the definite description operator The(x:A, φ) require
that the only free variable appearing in φ is x. You then define
λ-abstraction λx:A.e:B as an abbreviation for The(f : A → B. ∀x:A.
f(x) = e). This is going to be severely limiting because we cannot
nest λ-abstractions, for instance the K combinator

λx:A. ((λy:B x:A) : B → A) : A → (B → A)

is not a valid expression because the inner abstraction is invalid, as
it becomes

The (f : B → A, ∀y:B . f(y) = x)

and this is not closed. The readers should be warned about this. How
do you express the K combinator of type A → (B → A)? And how would
you write down the isomorphisms from A × B → C to A → (B → C)? The
usual ones is

λf : A × B → C . λy:A . λx:B . f (x, y)

and this is not valid in your calculus, again because of nested
λ-abstractions. It looks like you can use the axiom of choice (page
10, Figure 2, bottom row) for this purpose. Can you say a bit more
about this? Why don't you allow a definite description operator with
parameters?


I cannot make sense of the iso(σ, a, b) things (figure 6). Something
is wrong there. First of all, the third line of Figure 6 reads:

a ↔_􏰇σ b ≡ ∃x:iso(σ,a,b)

This does not make sense as the thing on the right-hand side of ≡ is
not a well-formed formula. I think you meant

∃x:iso(σ,a,b) . true.

Next, how does one form an iso(σ, a, b) type? I expected a rule such
as "if σ is a type, a : σ and σ : A then iso(σ, a, b) is a type". If
σ : type_i where does iso(σ, a, b) live, also in type_i? In the second
row of Figure 6 has things like

x ↔_􏰇iso(σ, τ, f) y

which unfolds to

∃_:iso(􏰇iso(σ, τ, f), x, y) . true

This is very strange, as it seems to suggest that whenever x : σ then
also x : iso(σ, τ, f). Can you please give the standard formation,
introduction, and elimination rules for iso-types? The reader should
be able to answer these questions by looking only at the rules:

1) Does iso(σ, a, a) always have an element for a : σ ?
2) What does iso(Bool, true, false) look like, and what does iso(Bool,
true, true) look like?


When you introduce the double colon :: you say

"A sequent of the form Σ ⊢ e :: τ is valid if in every semantic
interpretation of Σ
we have that the semantic value of e is a member of the value of τ."

What does this mean? In that entire part of the text you are referring
to semantic validity before having given any semantics to your formal
system. If the paragraph is meant to just give helpful intuition then
you should say so. It cannot serve as an official definition for parts
of your formal system.



What is the status of dependent products, Figure 11. You tell us that
they are not "first-class types", but what never tell us what they
*are*? Are they types? If so, do you have "first-class" and
"second-class" types in your type theory? You write (Λx:σ e[x]) ::
Πx:σ τ[x], so it looks like Πx:σ τ[x] ought to be a type. Or is it
that r :: s can be well-formed even when s is not a type? It would be
really helpful if you properly stated formation rules for all
constructs: what does it take for r :: s to be well-formed? Is there a
judgement expressing the fact that "Πx:σ τ[x] is well-formed"? You
should give all forms of judgements up front.



In Theorem 2.1 please state clearly what the status of the symbols a
and b is. I am guessing that a : σ and b : τ[b]. If this is indeed so,
then doesn't Theorem 2.1 just say that from (a, b) = (a, e) we can
derive b = e? I am pretty sure Voldemort is a bit more evil than
that.

On page 21, the last displayed formula states that

Pair(S2,b) = Pair(S2,e[S2])

where equality is at type PairOf(X:Sphere, z:π1(X)) and all we know
about b and e[S2] is that they are of type S2. Why does this hold?



Morphoid Type Theory is quite similar in several respects to Church's
Type Theory (http://plato.stanford.edu/entries/type-theory-church/),
which is a theory of simple types. You should explain in what sense
Morphoid Type Theory differs from Church's Type Theory. Church's types
are *simple*, while yours are kind-of-dependent (you allow dependent
sums, dependent SubType's and iso-types, but not dependent products).

Another relevant piece of work is Aczel & Gambino's Logic-Enriched
Type Theory, see http://dx.doi.org/10.2178/jsl/1140641163. Their are
agnostic about excluded middle, but their setup is similar in the
sense that there is "logic over types", which by the way has appeared
in various forms elsewhere, for instance in categorical logic. I am
pointing out this particular work because it might be useful to look
at how they set things up.

With kind regards,

Andrej