AlgebraicJulia / GATlab.jl

GATlab: a computer algebra system based on generalized algebraic theories (GATs)
https://algebraicjulia.github.io/GATlab.jl/
MIT License
23 stars 2 forks source link

Support for Opposite Categories #101

Closed jpfairbanks closed 11 months ago

jpfairbanks commented 11 months ago

@olynch and @kris-brown, I know that you have been motivated by Slice Categories as a driving example for categories as contexts approach. I was trying to implement contravariant functors on FinSet in Catlab and got stuck on how the OppositeCategory type works in Catlab.

If we had Categories as Contexts implemented, then when you do op(FinSet) you could get a new context that knows that morphisms should have the same type as in FinSet, but that composition of morphisms is just in the opposite order. With the current wrapper type implementation, if you want to implement FinSetOp, you would have to make wrapper types for OpFinFunction.

olynch commented 11 months ago

Yeah, this shouldn't be hard at all, and is a good motivating example!