[Agda] [Coq-Club] Concepts within Type Theory – Re: Type Theory vs. Set Theory – Re: Why dependent type theory?

[Thorsten Altenkirch]

This means that types are the result of simple operations such as lambda abstraction and lambda application (cf. wff constructions (b) and (c) at [Andrews 2002 (ISBN 1-4020-0763-9), p. 211]).

This means you have a very intensional view of Mathematics centred around encodings. I think this is misleading because Mathematics is about abstraction and abstract concepts, encodings are only coincidental.

Moreover, using Andrews' concept of "expressiveness" (also intuitively used by Church before), all mathematical concepts can be reduced – naturally (not like in machine language) – to a few basic notions:
Q0 basically has a single variable binder (lambda), two primitive symbols and two primitive types, and a single rule of inference.
R0 has only little more (some features required for type variables, type abstraction, and dependent types).
Both are Hilbert-style systems (operating at the object language level only).

This seems to be a view of mathematical foundations stuck in the middle of the last century.

The notion of type theory you refer to seems to intend more than just preventing (negative) self-reference.
The univalence axiom, and the desire to „structure mathematical constructions in a reasonable way“ are motivated by philosophical or metamathematical considerations.
These motivations have their legitimation, but shouldn’t be part of the formal language.

For this reason I already object to the Pi type (as implemented in Lean), or dependent function type, which I consider a metamathematical notion: https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ
I believe that type abstraction is fully sufficient to express what the Pi type is supposed to express.

So you are only interested in some mathematical machine code but not in the high level notions. Such a view of mathematical foundation is akin to the view some programmers had (and maybe still have) that all what matters is machine code. To the contrary you can build the same foundations on different notions of machine code. The machine code is irrelevant, all what matters are the abstractions.

How is type abstraction implemented in Lean, and where can I find the group definition?

I have no idea about Lean, not do I know what you mean by “type abstraction”. Polymorphism, that is constructions which are parametric in types are simply depdnent functions which have a universe as input.

Concerning constructivism (intuitionism) and intensionality, these are philosophical debates with little relevance for mathematics nowadays.
I fully agree to Kevin Buzzard’s argument that "within mathematics departments, the prevailing view is that Hilbert won the argument 100 years ago and we have not looked back since, despite what constructivists want us to believe." – https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/

I think you miss a trick or two here. Constructivism is highly relevant, especially in computer science when we want to marry computer science with mathematical constructions. Hilbert is already dead since a while and before the first computer has been build. The world is changing, maybe philosophers and mathematicians should take notice of this.

Cheers,
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 contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200313/dbbbdaee/attachment.html>