Convenience for declaring isomorphisms

[olynch]

It takes 4 declarations to declare an isomorphism in a category; you have to declare the forwards and backwards directions, and then you have to have two equalities for the composites.

There should be a macro or something that declares an isomorphism, and then gives programmatic Names to the forwards and backwards directions and equalities.

Are there other scenarios like this that we might want shorthand for? What's the general solution to things like this?

[jpfairbanks]

Have you tried diagrams?

Maybe it's a "this diagram commutes" sugar. You write out the edge list of the diagram and say all the parallel path commute in one shot? So for isos it would be

@commutative begin f:x->y g:y->x end

[olynch]

Wait, this is genius. I love it.

[olynch]

And then it would all be in a certain context, i.e. for assoc, it would be

@commutative begin
  assocr(A,B,C) : A x (B x C) -> (A x B) x C
  assocr(A,B,C) : (A x B) x C -> A x (B x C)
end \dashv [(A,B,C) :: Ob]

This does only work in theories that extend ThCategory, but that's fine; the whole point of Gatlab is to have convenient features for special cases.

It is a bit of a question how to extract the actual equalities here. Also, there are cases where we want to declare commutative diagrams without declaring term constructors. So maybe the thing to do is to declare the term constructors before, and then have

@commutative begin
   assocr(A,B,C), assocl(A,B,C)
end \dashv [(A,B,C)::Ob]

I'm not exactly sure what the general semantics of this would be though.