Univalent Foudations – Homotopy Type Theory

@Book{hottbook, author = {The {Univalent Foundations Program}}, title = {Homotopy Type Theory: Univalent Foundations of Mathematics}, publisher = {\url{https://homotopytypetheory.org/book}}, address = {Institute for Advanced Study}, year = 2013}

The expression Curry–Howard–Lambek correspondence is now used by some people to refer to the three way isomorphism between intuitionistic logic, typed lambda calculus and cartesian closed categories, with objects being interpreted as types or propositions and morphisms as terms or proofs. The correspondence works at the equational level and is not the expression of a syntactic identity of structures as it is the case for each of Curry’s and Howard’s correspondences: i.e. the structure of a well-defined morphism in a cartesian-closed category is not comparable to the structure of a proof of the corresponding judgment in either Hilbert-style logic or natural deduction.

Recently, the isomorphism has been proposed as a way to define search space partition in genetic programming.[9] The method indexes sets of genotypes (the program trees evolved by the GP system) by their Curry–Howard isomorphic proof (referred to as a species).

Generalizations

The correspondences listed here go much farther and deeper. For example, cartesian closed categories are generalized by closed monoidal categories. The internal language of these categories is the linear type system (corresponding to linear logic), which generalizes simply-typed lambda calculus as the internal language of cartesian closed categories. Moreover, these can be shown to correspond to cobordisms,[10] which play a vital role in string theory.

An extended set of equivalences is also explored in homotopy type theory, which became a very active area of research around 2013 and as of 2018 still is.[11] Here, type theory is extended by the univalence axiom (“equivalence is equivalent to equality”) which permits homotopy type theory to be used as a foundation for all of mathematics (including set theory and classical logic, providing new ways to discuss the axiom of choice and many other things). That is, the Curry–Howard correspondence that proofs are elements of inhabited types is generalized to the notion homotopic equivalence of proofs (as paths in space, the identity type or equality type of type theory being interpreted as a path).[12]

https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence

Genetic programming possibly relevant to model technology evolving.

Inverse semigroups look a lot like univalence.

Could be useful to learn Haskell while learning lambda calculus.

Coq and Agda both used with HoTT.

https://en.m.wikipedia.org/wiki/Coq

https://en.m.wikipedia.org/wiki/Agda_(programming_language)

Agda less well established than Coq. Uses Haskell like syntax and implemented in Haskell.

@book
{
book:1541134,
resid = {1541134},
status = {OK},
title = {Verified Functional Programming in Agda},
author = {Aaron Stump},
size = {1201323},
type = {pdf},
isbn = {},
edition = {},
volume = {},
md5 = {6c9637553d5ccbe1a9d232b5f7aeda2f},
url = {}
}

item 5a1f05883a044650f5121979

Uses emacs Agda mode. Can compile to Haskell. Potentially good book to also learn Haskell.

Microsoft also has a open source prover that might be relevant:

https://leanprover.github.io/documentation/

Has a maths library that might include the basics needed:

https://github.com/leanprover/mathlib

 

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s