idris-ct icon indicating copy to clipboard operation
idris-ct copied to clipboard

formally verified category theory library

Results 30 idris-ct issues
Sort by recently updated
recently updated
newest added

one of the big complaints of the current state of the library is that many arguments which could be implicit are not. Try to refactor to actually make them implicit

This adds some generic code for dealing with (extensional) quotients

As discussed in dev call, after implementing #34 we want to call out to JS FFI and compile the Idris code to JS so that can run a morphism it...