Definition funtranspos0 {T: UU} (t1 t2 : T) (is2 : isisolated T t2) (x : compl T t1) : compl T t2 := match (is2 (pr1 x)) with | ii1 e => match (is2 t1) with | ii1 e' => fromempty (pr2 x (pathscomp0 (pathsinv0 e') e)) | ii2 ne' => make_compl T t2 t1 ne' end | ii2 ne => make_compl T t2 (pr1 x) ne end.