proposition: Lemma issig_morphism (xa yb : object) : { f : Category.Core.morphism X xa.1 yb.1 | is_structure_homomorphism _ _ _ f xa.2 yb.2 } <~> morphism xa yb.
proof: Proof. issig. Defined.
imports: Category.Core HoTT.Basics HoTT.Types HSet