Re: Homotopy Type Theory ( HoTT )

There is a conference on the subject of the foundations of mathematics
with a talk on HoTT in London 12/13 January.

http://events.sas.ac.uk/ip/events/view/16403/IP+Conference%3A+Second+Symposium+on+the+Foundations+on+Mathematics3A+Second+Symposium+on+the+Foundations+on+Mathematics

Won't be able to make it sadly.

Henry

> On 29 Dec 2014, at 12:55, henry.story@bblfish.net wrote:
> 
> Hi,
> 
> At the Scala eXchange conference I talked to Odersky ( that 'father' of the Scala 
> programming language ) about Category Theory, and he pointed me to Homotopy Type 
> Theory as the mathematics that is claiming to overtake Category Theory as the foundational 
> mathematical language. The book for HoTT is online, under an CC licence, and available
> for LateX compilation and patches on github
> 
> http://homotopytypetheory.org
> 
> So as a foundational mathematical language this should be of interest to 
> Philosophers. In HoTT you never have an object without a type, which if I remember
> correctly was one of the key intuitions of Evans in his book The Variety of 
> Reference. So in terms of a simple distinction that is à la mode one can think of
> 
> 1. in set theory you start with objects, and then you group them into sets.
> It's emprical in that way
> 2. In category theory you also have objects but they are equivalent to the sets in set thory.
> The objects of set theory can only be reached via functions from the final object ( the object
> which has maps from all other objects ( ie. the singleton set  Because if you take the singleton
> you can create as many functions to a set as there are objects in it, and you can then name the
> objects via those functions. )
> So this is top/down or rationalist. You start with categories and maps between them, and the 
> objects of set theory fall out it.
> 3. HoTT you start with both. It makes sense. If you have an object
> with no type, there is no way you would know what to do with it. ( is it a number, an electron, a person ? )
> 
> 
> From a programmatic point of view: Having read the first 60 pages, I am starting to see 
> why Scala contains a very simple ( but powerful ) inferencing engine in the type system, and why
> very advanced scala users tend to make types that read like proofs
> 
> You will find that recent conference on Scala [1][2] have talks on logic programming
> related issues
> 
> • lambda calculus ( the first part of the HoTT book uses typed lambda calculus )
> https://skillsmatter.com/skillscasts/5863-introduction-to-lambda-calculus
> • dependent types ( the shapeless library uses that fully )
> "Scala is a language with a very sophisticated type system. It is even said to be the "poor-man's prolog"
> https://skillsmatter.com/skillscasts/5946-42-rise-of-the-dependent-types
> • demysifying type inference  
> https://skillsmatter.com/skillscasts/5841-demystifying-type-inference
> • Let Curry Howard Code for me
> http://scala.io/talks.html#/#NGJ-113 ( not online )
> • There's a prolog in your Scala
> http://scala.io/talks.html#/#WKU-122 ( not online )
> 
> But all of what is happening there is becoming much clearer after studying HoTT.
> What is interesting is that it encapsulates Category Theory, but I have
> not yet reached that chapter.
> 
> My talk "Building a Secure Distributed Social Web with Scala and Scala-JS"
> also points a lot to logic - modal logic and semantic web logic and short snippets
> from the history of logic/philosophy - but I have not yet worked through the connections 
> with HoTT, ( the HoTT book has a section on modal logic - early ones pre David Lewis' 
> Counterfactuals)
> 
>  https://skillsmatter.com/skillscasts/5960-building-a-secure-distributed-social-web-using-scala-scala-js
> 
> What is good is that I know there is a paper on Category Theory and RDF, which should help
> 
> "Formal Modelling and Application of Graph Transformations in the Resource Description Framework"
> 
> https://www.researchgate.net/publication/40635984_Formal_Modelling_and_Application_of_Graph_Transformations_in_the_Resource_Description_Framework
> 
> 
> Henry
> 
> 
> [1] London Scala eXchange 2014
> https://skillsmatter.com/conferences/1948-scala-exchange-2014#program
>  ( those talks can be viewed after loggin in to the skillsmatter site
>   which requires an account )
> [2] Paris Scala.io ( they don't have their videos online yet )
>  http://scala.io/talks.html#/
> 
> 
> Social Web Architect
> http://bblfish.net/
> 

Social Web Architect
http://bblfish.net/

Received on Monday, 29 December 2014 21:23:44 UTC