[howling]

System F just isn't flexible enough to encode most of mathematics. You need at the minimum dependent type and preferably a more flexible identity type to avoid setoid hell. The closest attempts I know of are HOTT in Coq and Cubical Agda. These systems still have a lot of kinks to be sorted out though, e.g. https://www.youtube.com/watch?v=TpUOweB2kHU