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