fact: Definition image_hsubtype_comp {X Y Z : UU} (U : hsubtype X) (f : X → Y) (g : Y → Z) : image_hsubtype U (funcomp f g) = image_hsubtype (image_hsubtype U f) g.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions