FredericPaugam

If schemes are not implemented yet, i wanted to recommend you the reading of Demazure-Gabriel ``groupes algébriques'', because their presentation of schemes should be adapted to a cubical agda implementation...