*** package:partial-isomorphisms

the product type constructor (,) is a bifunctor from Iso $times$ Iso to Iso, so that we have the bifunctorial map *** which allows two separate isomorphisms to work on the two components of a tuple.