I don't follow your technical aside. Isn't the point of an isomorphism that all the isomorphisms are the same in the sense in which you are isomorphic?
I can prove that True|False and Yes|No are isomorphic, but I can do so in multiple ways: I can map True to Yes and False to No, or I can map True to No and False to Yes (and then show that there are respective inverses which preserve identity, obviously)
I don't understand this example, because if you have A|B, A+A = A, B+B=B, but if A+B=A then A maps to true and if A+B=B then B maps to true.
The classical-style logic in the preceding paragraph does not apply to constructivist logic used for software formalisation!
But how? Like, what is the failure mode that you might get if you try to prove the correctness of a program for which this disquisition about isomorphisms is relevant?
p
I don't follow your technical aside. Isn't the point of an isomorphism that all the isomorphisms are the same in the sense in which you are isomorphic?
I don't understand this example, because if you have A|B, A+A = A, B+B=B, but if A+B=A then A maps to true and if A+B=B then B maps to true.
But how? Like, what is the failure mode that you might get if you try to prove the correctness of a program for which this disquisition about isomorphisms is relevant?
More options
Context Copy link