Univalent Foundations of Mathematics with Agda

[Philip Thrift]

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

[Lawrence Crowell]

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

[Philip Thrift]

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

Topological spaces in the presence of propositional resizing

"And, after the reader has gained enough experience ..."

    Agda HoTT library

    Cubical Agda 

cf. https://homotopytypetheory.org/2018/12/06/cubical-agda/

@philipthrift

[Philip Thrift]

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