Definition invezmap1 {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (ez : complxstr f g z) (y : Y) : hfiber f y -> (g y) = z := λ xe: hfiber f y, match xe with tpair _ x e => pathscomp0 (maponpaths g (pathsinv0 e)) (ez x) end.