@NunoSempere's banner p

NunoSempere


				

				

				
0 followers   follows 3 users  
joined 2022 September 10 10:19:29 UTC

				

User ID: 1101

NunoSempere


				
				
				

				
0 followers   follows 3 users   joined 2022 September 10 10:19:29 UTC

					

No bio...


					

User ID: 1101

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?

the previous ones would come back?

Here I'm just speculating, but there are frictions. You can't just boot up a relatively capital intensive business just like so?