proposition: Theorem isinclfromhfiber {X Y : UU} (f: X -> Y) (is : isaset Y) (y : Y) : @isincl (hfiber f y) X (@pr1 _ _).
proof: Proof. intros. refine (isofhlevelfhfiberpr1 _ _ _ _). assumption. Defined.
imports: UniMath.Foundations.PartA