search

mikeizbicki / subhask

Type safe interface for working in subcategories of Hask
BSD 3-Clause "New" or "Revised" License
418 stars 43 forks source link

Is every Heyting algebra a cancellative Abelian semigroup? #34

Closed sacsar closed 8 years ago

sacsar commented 8 years ago

If I've understood the definitions properly, I think the answer is no. The standard topology on R forms a Heyting algebra and the semigroup operation is set intersection (right?). Take a = (0, 2), b = (1, 3) and c = (1, 4). Certainly, a \cap b = a \cap c, but b != c.

If this looks right, I'll make a little pull request deleting the FIX ME and adding the example.

mikeizbicki commented 8 years ago

Yes, I think you're right. I'm not sure what I was thinking of when I wrote that comment :)