Lemma isdeceqweqf {X Y : UU} (w : X ≃ Y) (is : isdeceq X) : isdeceq Y. Proof. intros. intros y y'. set (w' := weqonpaths (invweq w) y y'). set (int := is ((invweq w) y) ((invweq w) y')). induction int as [ i | ni ]. - apply (ii1 ((invweq w') i)). - apply (ii2 ((negf w') ni)). Defined.