[Agda] Univalent foundations in Agda lecture notes

[Sergei Meshveliani]

On Thu, 2019-03-21 at 00:18 +0000, Martin Escardo wrote:
> I would like to advertise these lecture notes on univalent foundations 
> of mathematics with Agda:
> 
>   https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html
> 
> Issues and pull requests via github are welcome.
> 
> (This relies on the pre-released version 2.6.0 of Agda, mainly for 
> `variables` and for the new options for generating html from Agda 
> literate code. I thank the dedicated development team.)
> 

During many years the appear books which titles include the words
"foundations of mathematics", while they are actually about various 
_set theory formalisms_ and logic tools.

This leads students to misunderstanding of certain basic things. 

I suggest to correct these words in their titles to something like  
"basic formalisms for mathematics". 

Any set theory formalism cannot be a foundation of mathematics.
For example, Archimedes and Newton were great mathematicians, and they
knew foundations of mathematics, but they knew nothing about the set
theory formalisms, nor of univalent foundations.

Mathematics is about _solving problems_. For example, "find a formula
for the square of a sphere". 
Foundation of mathematics consists of certain basic approaches and
methods for solving such problems.
And any set theory formalism is only way to write a proof for solution
after such is found, so that there will be a hope that it can be more or
less automatically checked.
It is not about methods to search a solution. 

Regards,

------
Sergei