Relation Between Type Theory, Category Theory and Logic

Wonderfully accessible synopsis. One ever so _minor_ point. Did you really mean to say "The former and the latter are not the same thing" or "The former and the latter are not _formally_ the same thing" ???

Here's a fun fact for you, you might enjoy this. I picked up a copy of a 1943, second edition, hardback copy of Bertrand Russell's An Inquiry into Meaning and Truth. (In an antiquarian bookstore for €25, as one does... the colophon even states BOOK PRODUCTION WAR ECONOMY STANDARD)

Anyway, chapter XX is titled "The Law of The Excluded Middle" and in it Russell states, "[…] As everyone knows, Brouwer has challenged the law, and has done so on epistemological grounds. He, in common with many others, holds that “truth” can only be defined in terms of “verifiability”, which is obviously a concept belonging to the theory of knowledge. If he is right, it follows that the law of the excluded middle, and the law of contradiction also, belong to epistemology, and must be reconsidered in the light of whatever definition of truth and falsehood epistemology permits."

What strikes me about this (apart from the fact that I did not know previously that Russell tackled the question of constructivism/intuitionism so directly) is that he claims that everyone! knows this. If we are being charitable by everyone he means mathematicians, and perhaps logicians, maybe even philosophers, I still think it's quite a broad statement. It shows that the school of the logical positivists springs from Brouwer -- which firstly I was never taught, and which secondly does not appear in, for instance, Language, Truth, and Logic[1] by A.J. Ayer. Finally I can see how the law of double negation becomes an epistemological matter, but not the law of what he calls here contradiction (noncontradiction?).

He goes on to disprove the verifiability claim over many pages, and thus constructivism. There's a swipe at Wittgenstein further on still. It's a fascinating text. Russell grapples with mathematical and logical issues in a clear fashion using everyday language. Kind of like what you might get if you took the intro to HoTT and lengthened it and made it more philosophical.

[1] https://archive.org/stream/AlfredAyer/LanguageTruthAndLogic_...

ps: is there markup for blockquote on HN?

EDIT: clarity, markup, prose style

Another addendum to the discussion, from an angle more relevant to computer programmers: if we find a computational meaning for the univalence axiom, then it'll be a crazy nuclear weapon of generic programming and code generation.

The univalence axiom says that two types are equal if we can convert their values back and forth (without loss of information). For example, one Boolean type may be defined as an enum containing True and False. But we could rename the values to Foo and Bar and it would be still a fine implementation, because it's easy to convert between the two representations. We can imagine more far-fetched representations too, with more complicated conversion functions.

But in type theory, if two types are equal, then we can freely substitute one for another in any context! For example, if we have a function "Bool -> Bool", and we know that Bool is equal to Bool2, then we can coerce the function to type "Bool2 -> Bool2".

Imagine a complex program that uses a complex piece of data type. If we can provide a correct conversion function to another type (i. e. prove that the type is equivalent to another one), then the univalence axiom can take the conversion function and our program as input, and spits out a new program that uses the new data type, and also preserves all properties of the program. By our current standards of generic programming, this is just insane!

Now, the issue is that currently we don't actually have a computational interpretation for the univalence axiom, so the above magic doesn't yet work. But there is meaningful progress towards that, and there are already some experimental implementations that can do some magic, for example this one:

https://github.com/mortberg/cubicaltt

First the type theory part of homotopy type theory. Mathematicians have been doing logic for a long time, but mathematical statements and proofs were not themselves mathematical objects. They were just human language text with some math notation thrown in. Around 1900 Brouwer, Heyting and Komolgorov came up with a cool idea: treat proofs as first class mathematical objects. Then giving a proof is equivalent to constructing a mathematical object.

* A proof of `P and Q` is a pair of proofs (a,b) where a is a proof of P and b is a proof of Q

* A proof of `P implies Q` is a function that takes a proof of P and returns a proof of Q

* A proof of `P or Q` is a pair (x,c) where either x=0 and c is a proof of P or x=1 and c is a proof of Q

In modern terms; to give a proof of `P and Q` is to give a value of the pair type `(P, Q)`. To give a proof of `P or Q` is to give a value of the disjoint sum type `P + Q`. To give a proof of `P implies Q` is to give a value of the function type `P -> Q`.

Take the theorem `(A and B) implies (B and A)`. A proof of this is, in Haskell notation:

    proof :: (A,B) -> (B,A)
    proof (a,b) = (b,a)

So a proof of `(A and B) implies (B and A)` is a function that swaps the order of a pair.

An interesting property of this way of doing things is that statements are not merely true or false, but statements can in general be true in more than one way. For example the statement `(A and A) implies A` has two different proofs:

    proof1 :: (A,A) -> A
    proof1 (a1,a2) = a1
 
    proof2 :: (A,A) -> A
    proof2 (a1,a2) = a2

The proof1 of `(A and A) implies A` is a function that returns the first component of a pair, and proof2 a function that returns the second component.

I'll skip over dependent types.

That's the type theory part. Now the homotopy part. For a long time there was a problem with type theory. There was no really good way to do equality in it. To do math you want to use equality all the time. Since we've defined what the proofs of `P and Q`, `P or Q`, `P implies Q` are, what are the proofs of `x = y`? There has existed some notion of equality in type theory for a long time, but it wasn't satisfactory for various reasons. You couldn't prove two functions equal even though they gave the same outputs for the same inputs. Homotopy type theory fixes equality in type theory. The idea is that a proof of `x = y` depends on the type of x and y.

* Two pairs c,d are equal if their first components are equal and their second components are equal.

* Two functions f,g are equal if for all x, f x is equal to g x.

* etc.

More precisely, the proofs of equality on the type (A,B) is a pair of a proof of equality on A and a proof of equality on B. Just like previously a statement can be true in more than one way (have more than one proof), things can now also be equal in more than one way (have more than one proof of equality).

Another extension that homotopy theory theory does is with user defined types. When you define a type you are allowed to define its type of equality proofs at the same time. This allows you to define things like integers modulo k ((i mod k) is equal to (i+k mod k)), unordered sets (a set S is equal to any permutation of S), and more.

I've brushed over a lot of details and presented only a very narrow way of looking at type theory:

1. A type itself is a value.

2. Full dependent types.

3. When are two types equal?

4. When are two proofs of equality equal?

5. What exactly is a function, what is a pair, etc.? This leads us into category theory, which gives an abstract description of functions and pairs.

Hopefully this still made some amount of sense.

Two line summary:

1. Type theory: using conventional mathematical objects like pairs and functions as proof objects.

2. Homotopy type theory: extends type theory with proofs of equality in a proper way.

Eh? Your very own link says that there is debate within the mathematical community about whether Cantor's uncountability proof is constructive or not.

I just realised that in my mind uncountable (not in a one-to-one correspondence with the natural numbers) means non-constructive. For me countability just says that we have a (constructive) method for generating a sequence of what would be all the terms in the sequence (if it were ever to terminate which it doesn't) and no term outside the sequence in a non-repeating fashion that is unbounded.

Clearly if some sequence is uncountable it means that one of these criteria fails to hold. Which one? Not the non-repeating stipulation. Not the no term outside the sequence stipulation. It must be the stipulation that every term will be encountered during the generation. So there isn't a (constructive) method for generating uncountable sequences. The reals are uncountable, ergo there is no constructive method for generating the reals.

Where am I going wrong?

NB: I am not saying that you can't have a method for constructing individual reals like e and pi and so on.