Lemma homotd3g {Y Z : UU} (g : Y -> Z) {z : Z} (y : Y) (ye' : hfiber g z) (e : (g y) = z) (ee : (make_hfiber g y e) = ye') : (d3g g y ye' e ee) = (maponpaths (@pr1 _ _) (pathsinv0 ee)). Proof. intros. unfold d3g. unfold d2. simpl. apply pathscomp0rid. Defined.