On Friday, March 1, 2019 at 3:19:21 PM UTC-6, Philip Thrift wrote: > > > > On Friday, March 1, 2019 at 3:09:23 PM UTC-6, Lawrence Crowell wrote: >> >> The question is whether HoTT is also the language of entanglement. >> >> LC >> > > > > All "entanglement" is is a path integral [ > https://ncatlab.org/nlab/show/path+integral ] so it should. > > > - pt >
Also entanglement can be defined by the σCP (Stochastic Concurrent Prolog) language. - pt > > >> >> On Thursday, February 21, 2019 at 3:15:34 AM UTC-6, Philip Thrift wrote: >>> >>> >>> HoTT (Homotopy Type Theory) is re-expressed here as a programming >>> language to encode mathematics. >>> >>> >>> [ >>> https://www.researchgate.net/publication/326645835_HoTT_The_Language_of_Space >>> >>> ] >>> >>> [ https://github.com/groupoid/cafe) github.com/groupoid/cafe ] >>> >>> >>> Abstract >>> Homotopy Type Theory (HoTT) is the most advanced programming language in >>> the domain of intersection of several theories: algebraic topology, >>> homological algebra, higher category theory, mathematical logic, and >>> theoretical computer science. That is why it can be considered as a >>> language of space, as it can encode any existent mathematics. >>> >>> Speaker: Maxim Sokhatsky is an author of Privat24 deposits, 20 years of >>> working experience as a programmer, one of the 30 top-commiters in Ukraine >>> in Open Source, author of N2O, the best Erlang Web Framework, CEO of Synrc >>> Research Center, author of several embedded operating system runtimes and >>> production programming languages. Maxim is familiar with any programming >>> language on the planet and had seen sources of all operating systems. >>> >>> Now Maxim is doing his Ph.D. research (the second year of education) in >>> HoTT, trying to encode as much mathematics in the programming language as >>> possible along the way. >>> >>> During this lecture, Maxim will try to smoothly guide you from the >>> programming perspective to the pure space of mathematics and will show the >>> evolution of mathematical provers from AUTOMATH to the family of Cubical >>> Type Checkers. Also, this lecture is considered as a general introduction >>> to HoTT course Maxim is preparing for his friends. >>> >>> cf. [ http://groupoid.space) groupoid.space ] >>> >>> - pt >>> >>> -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.

