[Agda] An article by Jean-Yves Girard

[mechvel at scico.botik.ru]

On 2020-04-20 22:04, mechvel at scico.botik.ru wrote:
> May be, this is related to the following theorem in geometry:
> each smooth orientable surface in a three-dimensional space
> is topologically equal to a sphere with several handles.
> [..]

Soory, it is needed to add the condition of a compact surface without 
edge
(sphere, torus, and many others, but not a paraboloid, for example).

--
SM