[FOM] Alternative foundations?

[Hendrik Boom]

On Thu, Feb 20, 2014 at 09:08:08AM +1030, David Roberts wrote:
> The
> key part is that equality is not what it usually is in set theory, and
> in fact, as I understand it, the substrate of logic is subsumed into
> the type theory, rather than sitting behind/under the usual axiomatic
> material.

Subsuming logic into the type theory has been around since 
Martin-Lof's intuitionistic type theory.  What's interesting about 
homotopy type theory appears to be the treatment of equality types.  
The original theory isn't concerned much about their structure at 
all; the newer one has discovered that equality proofs have the 
structure of homotopy, which is how it turns the traditional stack of 
concepts (with sets at the bottom and homotopy one of the specialized 
branches at the top) upside down.  

-- hendrik