UIP 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

UIP 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.