Isomorphisms are equal if the underlying morphisms are equal

statebox / idris-ct

formally verified category theory library

GNU Affero General Public License v3.0

255 stars 23 forks source link

Isomorphisms are equal if the underlying morphisms are equal #75

Closed jcranch closed 4 years ago

jcranch commented 4 years ago

Previously this was just a postulate (with an extra assumption, too)

marcosh commented 4 years ago

very nice @jcranch! removing a postulate is always nice. It was there for historical reasons, I guess, before we splitted InverseMorphisms, Isomorphism and Isomorphic

marcosh commented 4 years ago

I made that hom argument implicit and merged this. Thanks again @jcranch