search

statebox / idris-ct

formally verified category theory library
GNU Affero General Public License v3.0
259 stars 23 forks source link

Reimplemented NaturalIsomorphism as an Isomorphism in the functorCategory #47

Closed bgavran closed 5 years ago

bgavran commented 5 years ago

As per issue #46 , I have removed the NaturalIsomorphism record and refactored the Isomorphism record to not include the invertible morphism in its type, but rather in its constructor.

I have also replaced every use of NaturalIsomorphism cat1 cat2 fun1 fun2 by Isomorphism (functorCategory cat1 cat2) fun1 fun2 in the project.

bgavran commented 5 years ago

The build seems to be failing because of long compilation times, as everything checks out on my machine. Error in CI is as follows:

No output has been received in the last 10m0s, this potentially indicates a stalled build or something wrong with the build itself.
clayrat commented 5 years ago

Might be worth keeping NaturalIsomorphism as a synonym to keep the latter definitions a bit less verbose? Otherwise looks reasonable.

marcosh commented 5 years ago

hi Bruno, sorry for the late reply, I was taking some days off.

your approach is very elegant but, as I mentioned in the issue, I think our approach is more simpler and I would prefer to keep a more basic definition of NaturalIsomorphism. This is mainly for didactic purposes (it's easier to explain what a natural isomorphism is without needing to introduce the functor category).

Moreover (I don't really know why) I have some issues compiling your code, because Idris takes too much times and the process gets killed

It would still be very nice to have a proof that natural isomorphisms (defined as we do) are exactly the isomorphisms in the functor category. Would you be up to prove that?

bgavran commented 5 years ago

I would prefer to keep a more basic definition of NaturalIsomorphism.

No worries!

your approach is very elegant but, as I mentioned in the issue, I think our approach is more simpler

I'm not sure I understand. How is it simpler?

It would still be very nice to have a proof that natural isomorphisms (defined as we do) are exactly the isomorphisms in the functor category. Would you be up to prove that?

I'll see what I can do!

marcosh commented 5 years ago

I think it is simpler because you just need to know what a natural transformation and what an isomorphism is. With your definition you also need to know what a functor category is, so there are more prerequisites for stating the definition

bgavran commented 5 years ago

I would argue that this natural isomorphism has to live somewhere, but I see your point.

marcosh commented 5 years ago

as per the above discussion, I'm closing this for the moment. @bgavran if you want, you're very welcome to open another PR addressing what we discussed above