[Agda] Univalent foundations in Agda lecture notes

[Martin Escardo]

Dear Sergei,

Yes, I also don't like "foundations" too much, and often speak of 
"univalent mathematics".

But "univalent foundations" is a brand name, and the notes are about 
what goes under this name.

Moreover, and these notes are about both "univalent foundations" 
(including the type theory under consideration, and the foundational 
mathematical development of the fundamental notions (hlevels, 
equivalences, univalence)) *and* "univalent mathematics" (once we have 
the foundations in place).

Martin

On 21/03/2019 12:22, mechvel at botik.ru wrote:
> 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
> 
> 
> 
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe