search

statebox / idris-ct

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

Universal Objects are Isomorphic #80

Closed Jake-Gillberg closed 4 years ago

Jake-Gillberg commented 4 years ago

Wondering if the proof should be done this way, or start with InitialObjectsAreIsomorphic and use properties of Dual Categories to complete

marcosh commented 4 years ago

hi @Jake-Gillberg thanks for your contribution.

I guess it would be nice to use initialObjectsAreIsomorphic to prove Isomorphic (dualCategory cat) (carrier a) (carrier b) and then, adding some code in DualCategory.lidr, prove that two objects are isomorphic in a category only if they are isomorphic in the dual category.

What do you say?

Jake-Gillberg commented 4 years ago

I'll give it a go!

Jake-Gillberg commented 4 years ago

Closing while work in progress

Jake-Gillberg commented 4 years ago

@marcosh this should be good to go!

marcosh commented 4 years ago

thanks @Jake-Gillberg, this looks awesome! I merged it manually