search

statebox / idris-ct

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

pedagogically adding some non trivial structure #76

Open nrolland opened 4 years ago

nrolland commented 4 years ago

Not sure if it fits here, but I was looking at this library and wanted to see how to, say, add the definition of 2-categories as a test case.

Now it can be done with all the elementary pieces (whiskering, interchange, etc..) but trying to do it abstractly (with a composition functor etc) leads to interesting (easy but not trivial) parts which are currently missing.

Say, the iso in Cat between a category A and 1 * A, proving equalities of functors (?). Those kind of things are great opportunities for pedagogical material. Not trivial stuff. But not too hard.

I would very much like to see some experienced user adding those in a twitch / youtube / in person. That would be ideal to further develop this nice library.

Or maybe there are similar content in the same vein someone could recommend ?

Thanks in advance

marcosh commented 4 years ago

Thanks @nrolland for your suggestion.

What you propose is definitely interesting, but at the moment does not align 100% with the developments we are working on.

We'll definitely keep it in mind for the future.

On the other hand, if you or someone else is willing to work on this, we'll be glad to review and integrate the material