(xa yb : object) : { f : Category.Core.morphism X xa.1 yb.1 | is_structure_homomorphism _ _ _ f xa.2 yb.2 } <~> morphism xa yb. Proof. issig. Defined.
Require Import Category.Core. Require Import HoTT.Basics HoTT.Types HSet. Import PreCategoryOfStructures.