proposition: Lemma hfibershomotftog {X Y : UU} (f g : X -> Y) (h : f ~ g) (y : Y) : hfiber f y -> hfiber g y.
proof: Proof. intros xe. induction xe as [x e]. split with x. apply (!(h x) @ e). Defined.
imports: UniMath.Foundations.Preamble