Why is NaturalIsomorphism implemented as a separate type rather than as Isomorphism in the functor category?

[bgavran]

Is there a particular reason why

NaturalIsomorphism 
  (cat1 : Category)  
  (cat2 : Category) 
  (fun1 : CFunctor cat1 cat2)  
  (fun2 : CFunctor cat1 cat2)

isn't simply implemented as

Isomorphism (functorCategory cat1 cat2) fun1 fun2

where Isomorphism record is defined as:

record Isomorphism (cat : Cat) (a : obj cat) (b : obj cat) where
  constructor MkIso
  forward : hom cat a b
  inverse : hom cat b a
  rightInverse : o cat {a=a} {b=b} {c=a}              inverse forward === idd cat {a=a}
  leftInverse  :  o cat {a=b} {b=a} {c=b} forward inverse              === idd cat {a=b}

It seems to be a simplification and allows us to talk about all sorts of Isomorphisms in different categories. For example, monoidal categories look slightly different. The reason for slightly different function names is because I'm implementing a ct libary as well here.

[marcosh]

Hi Bruno, thanks for your suggestion!

The main reason is that we had not defined functorCategory when we implemented NaturalIsomorphism.

One reason to keep NaturalIsomorphism as it is is the will to keep things as simple as possible. This repo has also some didactic purposes, so I think using the most basic definitions could be useful.

Anyway, I quite like your definition of Isomorphism, which is more symmetric than ours. I'll have a look at how it fits in the rest of the repo

[FabrizioRomanoGenovese]

Yo Bruno!

As @marcosh said, this was a mere question of priorities, we defined functorCategory after defining NaturalIsomorphism.

Anyway, if you feel like it, why don't you prove that the two definitions are equivalent and open a PR? I don't know if/how you plan to use our library, but that would probably be a nice way to get acquainted with it (and we'd appreciate the contribution, obviously :) ).

[bgavran]

Sure, I could try to cook something up! Is there anything I need to know before implementing? I assume I should work on a new branch, change things as proposed in the original comment and keep fixing type errors until I can get idris --checkpkg idris-ct.ipkg to build?

[FabrizioRomanoGenovese]

Yes, I think you assumption is correct. Please notice that once you open a pull request, an automatic CLA script should ask you to sign and intellectual property thing. In case you are not used to this, this is standard practice to keep all the intellectual property of the library in the same place, in case license modifications should be required!

[bgavran]

Hi Fabrizio,

I've opened a pull request with more information inside. I've refactored the code, but haven't proved the two definitions are equivalent, as you say. I'm not sure exactly what would that require, in terms of implementation

[marcosh]

as per the discussion in #47, I'm closing this for the moment