search

statebox / idris-ct

formally verified category theory library
GNU Affero General Public License v3.0
255 stars 23 forks source link

Booleans #67

Closed sjoerdvisscher closed 4 years ago

sjoerdvisscher commented 4 years ago

Fixes #66

marcosh commented 4 years ago

@sjoerdvisscher you could probably use https://github.com/statebox/idris-ct/blob/master/src/Preorder/PreorderAsCategory.lid to implement the category of Booleans

sjoerdvisscher commented 4 years ago

@marcosh Yeah I saw that, but I feared that would complicate things. But looking at the limit and colimit code that might not be the case (I don't ever pattern match on arrows f.e.) so I'll give it a try.

marcosh commented 4 years ago

Good!

Moreover, I don't know if it's a reasonable thing to do, but maybe you could prove the same things for any lattice