Definition embeddingRepresentability {C D:category} {X:[C^op,HSET]} {Y:[D^op,HSET]} (s:Representation Y) (i:categoryEmbedding C D) : z_iso (Y □ functorOp (opp_ob (pr1 i))) X -> (∑ c, i c = universalObject s) -> Representation X. Proof. intros j ce. apply (z_iso_Representation_weq j). exists (pr1 ce). exists (transportf (λ d, Y ◾ d : hSet) (!pr2 ce) s). intro c'. apply (twooutof3c (# i) (λ g, _ ⟲ g)). - apply (pr2 i). - induction (! pr2 ce). exact (weqproperty (universalProperty _ _)). Defined.
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.