Definition isomorphismRepresentability {C D:category} {X:[C^op,HSET]} {Y:[D^op,HSET]} (s:Representation Y) (i:categoryIsomorphism C D) : z_iso (Y □ functorOp (opp_ob (pr1 (pr1 i)))) X -> Representation X := λ j, embeddingRepresentability s i j (iscontrpr1 (pr2 i (universalObject s))).
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.