http://dorais.org/archives/1425
Alguns excertos: What is so hot abou HoTT? "The most interesting aspect from my point of view is that HoTT fully supports proof-relevant mathematics, a way of doing mathematics where proofs are real objects that are manipulated on the same level as numbers, sets, functions and all the usual objects of classical mathematics. This is not a brand new idea, logicians have been playing with proofs in this way for a long while, but HoTT brings this idea into the realm of everyday mathematics and that is a major step forward in mathematics." What is the big deal with univalence? "It is natural to identify things that are not significantly different. For example, the axiom of extensionality in set theory identifies sets that have the same elements since the elements of a set are all that matter in this context. Extensionality for functions identifies functions that agree on all inputs. Univalence is an indiscernibility axiom in the same spirit: it identifies types that are not significantly different." * * * uma digressão sobre o Axioma da Univalência e o princípio de Abstração de Leibniz http://m-phi.blogspot.com.br/2013/06/leibniz-abstraction-structure-identity.html * * * jm On Fri, Jun 21, 2013 at 2:45 PM, Joao Marcos <[email protected]> wrote: > "The long-awaited book on Homotopy Type Theory, a creation of a group > of mathematicians working under the collective name of Univalent > Foundations Program, is now out!" > http://m-phi.blogspot.com.br/2013/06/homotopy-type-theory-book-is-out.html > > "We are a group of two dozen mathematicians who wrote a 600 page book > in less than half a year." > http://audrey.fmf.uni-lj.si/hott.html > (para controle de revisões eles usaram o github) > http://vimeo.com/68761218 > > O livro está inteiramente disponível sob a licença Creative Commons. > http://homotopytypetheory.org/book/ > > > JM -- http://sequiturquodlibet.googlepages.com/ _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
