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/d7ba3f6c-cd33-4d27-9b25-7168d52b2dd9n%40googlegroups.com.
