[FOM] Alternative foundations?
hendrik at topoi.pooq.com
Fri Feb 21 10:01:57 EST 2014
On Thu, Feb 20, 2014 at 09:08:08AM +1030, David Roberts wrote:
> 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
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.
More information about the FOM