Theorem isdecpropfibseq0 {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (fs : fibseqstr f g z) : isdecprop Y -> isdeceq Z -> isdecprop X. Proof. intros isy isz. assert (isg : isofhlevelf 1 g) by apply (isofhlevelffromXY 1 g (isdecproptoisaprop _ isy) (isasetifdeceq _ isz)). assert (isp : isaprop X) by apply (isofhlevelXfromg 1 f g z fs isg). induction (pr1 isy) as [ y | ny ]. - apply (isdecpropfibseq1 _ _ y (fibseq1 f g z fs y) (isdecproppaths isz (g y) z) (isdecproptoisaprop _ isy)). - apply (isdecpropif _ isp (ii2 (negf f ny))). Defined.