Define Dagger categories

[anshwad10]

To do:

• Define dagger categories
• Define univalent dagger categories
• Define dagger functors
• Define the binary product of dagger categories
• Define the category of dagger functors between two dagger categories
• Prove that a dagger category is equivalent to its opposite
• Typecheck

[anshwad10]

Somebody please review this, I've been waiting for months. @ecavallo? @mortberg?

[ecavallo]

Contents look good. I have some minor comments mostly about naming.

A question about conventions. Is there any logic to when you use Dagger (e.g. DaggerStr) vs Dag (e.g. DagCat) vs † vs D in names? If not, can we pick one (†?) to use in all names?

[anshwad10]

oops I was trying to see what was the requested change and accidentally clicked on re-request review.

[anshwad10]

@ecavallo I've made the changes you requested (though GitHub is not showing it for some reason) can this be merged now?

[ecavallo]

Hey, sorry for the wait. There are a few more name changes I would suggest for uniformity:

• DagFunctor -> †Functor to match †Category
• IsDagFunctor to either IsDaggerFunctor or Is†Functor
• DagBinProd to †BinProd

Maybe also dagCat≡op and dagCatEquivOp could be renamed to usedagger or † instead of dag.

[anshwad10]

Done!

[ecavallo]

Thanks!