Theorem isofhlevelfpmap (n : nat) {X Y : UU} (f : X -> Y) (Q : Y -> UU) : isofhlevelf n f -> isofhlevelf n (fpmap f Q). Proof. intros X0. unfold isofhlevelf. unfold isofhlevelf in X0. intro y. set (yy := pr1 y). set (g := hfiberfpmap f Q y). set (is := isweqhfiberfp f Q y). set (isy := X0 yy). apply (isofhlevelweqb n (make_weq g is) isy). Defined.