I had a limited interest in exploring type theories for their own sake some time ago but it receded when I was unable to resolve, or find a resolution to, a conceptual problem that seems extremely foundational.
Each type theory has a hierarchy of types: 1-types, 2-types, 3.1*10^62-types, etc. but some niche type theories allow for types indexed by transfinite ordinals: ω-types, ω+5-types, I even found a construction of a theory that supports φ_α-types. There is apparently at least one very counterintuitive type theory where the hierarchy of indexable types provably continues past the proof-theoretic ordinal of the theory, somehow, but I haven't seen it myself.
These have real implications of what kinds of proofs you can do with a given type theory.
.
The problem is deciding which of these theories to permit, or possibly even deciding how to decide which theories to permit, if you'll pardon the pun. I decided to give it up and get back to PDEs.
I think this is on some level very much like deciding which programming language to use. It really depends on what problems you're trying to solve and there isn't a single one that is the best.
The difference is that type theories are much less of a "solved" problem and a lot of the variations are subject to ongoing research. As a consequence we're still at the stage where we're trying to figure out the "deciding how to decide", as opposed to programming languages, where decision criteria are relatively well understood.
I have been trying for some time to understand what Homotopy Type Theory or Univalent Foundations is actually about.
The HOTT book announces a new branch of mathematics, what is it?
Martín Escardó addresses this directly at the beginning with his 8 points.
HOTT is a Martin-Löf Type Theory variant.
MLTT has been developing since at least 1970, so it's not exactly brand new.
In contrast to First Order Logic and Zermelo Fränkel Set Theory, MLTT works with types that are constructed and applied according to certain rules.
Some of the rules are more logical (Cartesian product = conjunction, function = implication) some are more mathematical (induction rules, e.g. for natural numbers).
Martin-Löf's innovations are the Dependent Types (corresponding to logical quantifiers) and the Identity Types.
Identity types have always been somewhat mysterious; equality actually seems to be the simplest thing in the world.
On the one hand, two expressions are equal if they have the same simplification (assuming confluence).
This is called definitional (extensional) equality. But there is also equality that has to be proven (differently), that is intensional equality.
Definitional equality implies intensional equality (the expressions are equal => their equality is proven).
HOTT now sees a non-trivial structure in the proofs of equality. Various equality proofs are possible. One level higher, however, there is the possibility of proving the equality of equality proof and on and on.
This is an infinity groupoid or homotopy type.
This results in a hierarchy of mathematical objects. At the bottom are objects whose equality is trivial (old school sets and propositions).
The new ones are the Higher Types, whose elements (e.g. cell complexes) are complicated set constructions in traditional mathematics.
For Univalence I better refer to Point 3, otherwise I would write that Univalence enables treating equal Objects as equal.
Although I had absolute no idea what I was doing when we played around with Agda in university, it was kind of fun constructing a few very basic proofs. It kind of felt like smashing some buttons until it worked. The Emacs integration with all the Unicode goodness was really something.
Each type theory has a hierarchy of types: 1-types, 2-types, 3.1*10^62-types, etc. but some niche type theories allow for types indexed by transfinite ordinals: ω-types, ω+5-types, I even found a construction of a theory that supports φ_α-types. There is apparently at least one very counterintuitive type theory where the hierarchy of indexable types provably continues past the proof-theoretic ordinal of the theory, somehow, but I haven't seen it myself.
These have real implications of what kinds of proofs you can do with a given type theory.
.
The problem is deciding which of these theories to permit, or possibly even deciding how to decide which theories to permit, if you'll pardon the pun. I decided to give it up and get back to PDEs.