Relation Between Type Theory, Category Theory and Logic

   reconciliation in my mind between dependent types and higher kinded types. 

They are orthogonal concepts. This is made very clear in Barendregt's λ-cube [1]. Orthogonal here means that a typing system might be higher-kinded without allowing type-dependency, or it might allow type-dependency without having higher-kinds. An example of the latter is LF, the Logical Framework of Harper et al. Haskell, or at least some forms of Haskell are an example of the former.

Higher-kinded types simply allow functions and function application at the type level which can take functions as arguments and can return functions. For example (lambda x.x => bool) and (lambda xy. x => y) are functions at the type level.

An example of a dependent type is List(2+4)[bool], of lists of length 6 carrying booleans. Here (2+4) is a program. This parameterisation happens without having type-functions.

[1] https://en.wikipedia.org/wiki/Lambda_cube

I'll try to keep it short and skip the details of the mathematical framework itself.

Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not constructive (which I think is silly).

Their ideas faded out of popularity among mainstream mathematicians, but their goal was to rewrite the foundations of all mathematics using only constructive proofs, and to their credit they got pretty damn far in certain subjects like real analysis (calculus).

Today, their ideas are seeing a resurgence in the homotopy type theorists (HTTs). Their goal is also to rewrite all of mathematics in a constructive way, but now they have the hindsight of these great tools like category theory and homology and computers and all these great things developed in the mid to late 20th century. So they are working on building this framework and seeing what it can prove.

The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) and one of their main selling points is that their work will eventually lead to "computer assisted mathematics," not in the sense of Stephen Wolfram but rather in the sense that a computer will check your proofs as you prove them and find stupid mistakes.

I personally am not all that excited about HTT, due to what I see as misguided hype around it. My preferred way to view it is as logicians studying a really fascinating new logical system and seeing how far they can push it. Saying things like "I deny all mathematics that's not constructive" and "computers will start doing our proofs for us," makes me cringe. But it is what it is :)

Typing systems (at least some of them) are also logics. This is called the Curry-Howard correspondence (CHC).

At first the CHC was made to work for propositional logic only, i.e. logic without for-all and existential quantification. Later typing systems were developed which correspond to logic with quantification. This requires dependent types. However, early typing systems with dependent types had an inelegant handling of equality. Logic needs equality to express things like forall x. x = 3 => x > 2. To overcome this problem, Per Martin-Loef introduced a dependent type-theory (MLTT) with "identity-types" which enables an elegant handling of equality. MLTT and all other extant formalisations of mathematics still suffered from another problem, in that many mathematical constructs are 'morally' the same, but formally distinct. For example you can define a group to be a triple ( G, 1, * ) where G is a set, 1 the neutral element and * the binary operation, or you can define it as ( G, *, 1 ). The former and the latter are not the same thing, but we don't really want to say that they formalise different concepts. This is similar to how in many programming languages certain types are formally distinct but somehow capture the same content.

Homotopy type theory (HoTT) overcomes this problem (or parts of this problem) by adding a single axiom to MLTT, called the "univalence axiom" which can informally be rendered as:

   Things that are 'morally' the same, really are identical.

The key idea behind the univalence axiom is that MLTT (and hence HoTT) restricts the mathematical objects that can be constructed such that whenever you have objects O1 and O2 that are morally the same, then there is a function that transforms any construction involving O1 automatically into a construction involving O2 or vice versa, but in a truth preserving way.

It turns out that proofs in HoTT are formally similar to certain aspects of geometry/topology.

Much of current research on HoTT is about the consequences of the univalence axiom and the similarity between logic and geometry/topology.

The key hope in all this is that HoTT will streamline formalised mathematics.

If you limit yourself to only constructive proofs, do you even get the real numbers? I'm not very clear on the definition of "constructive," but given that almost all real numbers are non-computable (i.e. most likely, the set of all real numbers you have ever encountered outside of computability theory has the same cardinality as the integers), it doesn't feel very constructive to me. I've always found it odd that we learn early on in discrete mathematics about how the cardinality of the reals is larger than that of the integers and rationals, and yet it seems like you'll never deal with anything from this larger set of reals unless you're studying computability.

While Goedel's first incompleteness theorem indeed shows that there will always be true statements that don't follow from a given set of (computable) axioms, this is almost never a problem in practise. It is hard to find natural examples of such statements. Almost every mathematical statement (or its negation) you or I can come up with is a consequence of the axioms of ZFC set theory, or whatever other foundation you prefer.