Also,, "Agda is named after the Swedish song 'Hönan Agda' [written by Cornelis Vreeswijk], which is about a hen named Agda. This alludes to the naming of Coq." https://en.wikipedia.org/wiki/Agda_(programming_language)
Song: https://www.youtube.com/watch?v=npfTwJgZAKY @philipthrift On Friday, August 14, 2020 at 6:47:25 AM UTC-5 Philip Thrift wrote: > Here, *Agda* is the base language. This is a programming manual. All > definitions are in Agda. > > Agda is a "dependently-typed functional programming language" ... "for > defining mathematical notions (e.g. group or topological space)." > > Topological spaces > <https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#topological-sip> > > Topological spaces in the presence of propositional resizing > <https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#topol-resizing> > > > "And, after the reader has gained enough experience ..." > > Agda HoTT library <https://github.com/HoTT/HoTT-Agda> > > Cubical Agda > <https://agda.readthedocs.io/en/latest/language/cubical.html#cubical> > > > cf. https://homotopytypetheory.org/2018/12/06/cubical-agda/ > > @philipthrift > > On Friday, August 14, 2020 at 6:13:46 AM UTC-5 Lawrence Crowell wrote: > >> This is a long document. I don’t see at the start something which >> encapsulates the topic. Homotopy Type Theory (HoTT). HoTT is based on >> homotopy, which is a system of diffeomorphisms on sub-space regions of a >> manifold that describe invariants based on obstructions. These denoted as >> π_p(M^n) = 0, ℤ or ℤ_i. for i an integer. The first fundamental form is >> π_1(M^n), or a set of curves that are equivalent under diffeomorphisms. >> These are related to homology groups H_p(M^n), but with additional >> commutator information. >> >> Physics with partition functions or path integrals >> >> Z[φ] = ∫δ[φ]e^{-iS[φ]} >> >> For the integration measure δ[φ] = d^nx/diffeo[φ]. The continuous maps or >> diffeomorphisms are in a sense lifted away from what is fundamental, being >> a form of coordinate or gauge condition. What is left is then analogous to >> what is computed by a topological charge. >> >> I am not sure if these document or others lead to this prospect, but if >> it did it would be of considerable interest. If the binary on or off >> definition of HoTT were connected to physics this way it would be of >> interests. In particular if this connected with entanglements it would also >> be of interest. >> >> LC >> >> On Friday, August 14, 2020 at 1:34:55 AM UTC-5 [email protected] wrote: >> >>> Inroduction to Univalent Foundations of Mathematics with Agda >>> 4th March 2019, version of 13 August 2020 >>> >>> >>> https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html >>> >>> @philipthrift >>> >> -- 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 view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/87c5693f-19d9-440a-9b16-c7247ffcb5e5n%40googlegroups.com.
