Theorem isdeceqinclb {X Y : UU} (f : X -> Y) (is : isdeceq Y) (is' : isincl f) : isdeceq X. Proof. intros. intros x x'. set (w := weqonpathsincl f is' x x'). set (int := is (f x) (f x')). induction int as [ i | ni ]. - apply (ii1 ((invweq w) i)). - apply (ii2 ((negf w) ni)). Defined.