Theorem isdecinclcomp {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (isf : isdecincl f) (isg : isdecincl g) : isdecincl (λ x : X, g (f x)). Proof. intros. intro z. set (gf := λ x : X, g (f x)). assert (wy : ∏ ye : hfiber g z, weq (hfiber f (pr1 ye)) (hfiber (hfibersgftog f g z) ye)) by apply ezweqhf. assert (ww : ∏ y : Y, weq (hfiber f y) (hfiber gf (g y))). { intro. apply (samehfibers f g). apply (isdecincltoisincl _ isg). } induction (pr1 (isg z)) as [ ye | nye ]. - induction ye as [ y e ]. induction e. apply (isdecpropweqf (ww y) (isf y)). - assert (wz : (hfiber gf z) ≃ (hfiber g z)). { split with (hfibersgftog f g z). intro ye. induction (nye ye). } apply (isdecpropweqb wz (isg z)). Defined.