4 ms·
I'm a beginner in proof assistents, can you give some examples of many kinds of math ruled out? And what is UIP?
by JoeCamel 6y ago
I'm a beginner in proof assistents, can you give some examples of many kinds of math ruled out? And what is UIP?
- bollu 6y agoUIP is "unicity of identity proofs". I think this will rule proofs where we wish to talk about proofs of equality of two objects. I don't know off the top of my head any math that wants to do such a thing, but I'm far from an expert.
- TheAsprngHacker 6y agoUIP is uniqueness of identity proofs. It's an axiom that says that all proofs of x = y (that two terms are propositionally equal) are the same. Now, UIP is valid if the only way of proving an equality is to show that the two terms are definitionally equal. However, there are various type theories, such as Homotopy Type Theory, in which this axiom does not hold because propositional equality can have other proofs.