search

ohnosequences / stuff

Useful stuff.
GNU Affero General Public License v3.0
1 stars 0 forks source link

Dagger categories #16

Closed laughedelic closed 7 years ago

laughedelic commented 8 years ago

I want to try to do this to dive into the stuff and understand better how things work here.

eparejatobes commented 8 years ago

I don't get much what you're trying to do with spans. See my next commit for how you could define dagger categories

laughedelic commented 8 years ago

I didn't get what have you changed with respect to dagger-stuff besides renaming things.. And what's with spans? I just wanted to build Span for a given category and use it as an example for the dagger structure. But I could do the dagger functor for spans, that just switches source/target, because of the #C[X,Y] type member (you can't do is(..) trick on it)

eparejatobes commented 8 years ago

I didn't get what have you changed with respect to dagger-stuff besides renaming things..

About what you had in cdbb0e0b0469aa95350d1ff654089c0d2c27b4a9

  1. Dagger categories are not the same as categories with an involution
  2. a dagger functor is a functor between dagger categories which commutes with the dagger
  3. C[X,Y] for a dagger category is not (C[X,Y], C[Y,X]); and the composition you're writing there is that of the cofree dagger category on a category

And what's with spans?

  1. What's this type here? how is it related with spans?
  2. It could be possible to define something like spans for types together with a equality typeclass (so that one can simulate equalizers)