trying to have an informal discussion
How many people do you think are familiar with it?
HOTT states nothing about optimization.
None of the foundations of mathematics
really tackle optimization.
There is such a thing as linear types
Linear types let you to trully distinguish
between values and references.
that our current understanding of math is really
"all there is".
 Yiannis Moschovakis, Notes on Set Theory (https://www.amazon.com/Notes-Theory-Undergraduate-Texts-Math...)
> Notions of minimun/maximum as well as related concepts can be expressed, too.
Exactly. There are two types of minimum and maximum, something that isn't expressible in any of the current foundations of mathematics. There is your minimum and maximum, and my minimum maximum. This is exactly what linear logic is about.
Can you post your papers
on linear logic?
Show me a peer reviews paper showing this. Extraordinary claims bla bla bla. Do you feel like we have progressed anywhere?