Definition weqcutonweq (T : UU) (t : T) (is : isisolated T t) : (T ≃ T) ≃ isolated T × (compl T t ≃ compl T t). Proof. intros. set (f := cutonweq t is). set (g := invcutonweq t is). apply (weq_iso f g). - intro w. Set Printing Coercions. idtac. apply (invmaponpathsincl _ (isinclpr1weq _ _)). apply funextfun; intro t'. simpl. unfold invmap; simpl. unfold coprodf, invrecompl. induction (is t') as [ ett' | nett' ]. + simpl. rewrite (pathsinv0 ett'). apply pathsfuntransposoft1. + unfold funtranspos0; simpl. induction (is (w t)) as [ etwt | netwt ]. * induction (is (w t')) as [ etwt' | netwt' ]. -- induction (negf (invmaponpathsincl w (isofhlevelfweq 1 w) t t') nett' (pathscomp0 (pathsinv0 etwt) etwt')). -- simpl. assert (newtt'' := netwt'). rewrite etwt in netwt'. apply (pathsfuntransposofnet1t2 t (w t) is _ (w t') newtt'' netwt'). * simpl. induction (is (w t')) as [ etwt' | netwt' ]. -- simpl. rewrite (pathsinv0 etwt'). apply (pathsfuntransposoft2 t (w t) is _). -- simpl. assert (ne : neg (w t = w t')) by apply (negf (invmaponpathsweq w _ _) nett'). apply (pathsfuntransposofnet1t2 t (w t) is _ (w t') netwt' ne). - intro xw. induction xw as [ x w ]. induction x as [ t' is' ]. simpl in w. apply pathsdirprod. + apply (invmaponpathsincl _ (isinclpr1isolated _)). simpl. unfold recompl, coprodf, invmap; simpl. unfold invrecompl. induction (is t) as [ ett | nett ]. * apply pathsfuntransposoft1. * induction (nett (idpath _)). + simpl. apply (invmaponpathsincl _ (isinclpr1weq _ _) _ _). apply funextfun. intro x. induction x as [ x netx ]. unfold g, invcutonweq; simpl. set (int := funtranspos (t,, is) (t',, is') (recompl T t (coprodf w (λ x0 :unit, x0) (invmap (weqrecompl T t is) t)))). assert (eee : int = t'). { unfold int. unfold recompl, coprodf, invmap; simpl. unfold invrecompl. induction (is t) as [ ett | nett ]. - apply pathsfuntransposoft1. - induction (nett (idpath _)). } assert (isint : isisolated _ int). { rewrite eee. apply is'. } apply (ishomotinclrecomplf _ _ isint (funtranspos0 _ _ _) _ _). simpl. change (recomplf int t isint (funtranspos0 int t is)) with (funtranspos (int,, isint) (t,, is)). assert (ee : (int,, isint) = (t',, is')). { apply (invmaponpathsincl _ (isinclpr1isolated _) _ _). simpl. apply eee. } rewrite ee. set (e := homottranspost2t1t1t2 t t' is is' (recompl T t (coprodf w (λ x0 : unit, x0) (invmap (weqrecompl T t is) x)))). simpl in e. rewrite e. unfold recompl, coprodf, invmap; simpl. unfold invrecompl. induction (is x) as [ etx | netx' ]. * induction (netx etx). * apply (maponpaths (@pr1 _ _)). apply (maponpaths w). apply (invmaponpathsincl _ (isinclpr1compl _ _) _ _). simpl. apply idpath. Unset Printing Coercions. Defined.