Description: The inverse relation is a bijection from isomorphisms to isomorphisms. This means that every isomorphism F e. ( X I Y ) has a unique inverse, denoted by ( ( InvC )F ) . Remark 3.12 of Adamek p. 28. (Contributed by Mario Carneiro, 2-Jan-2017)