Lemma weqstnsum1_prelim_eq' { n : nat } (f : ⟦n⟧ -> nat) : invweq (weqstnsum1_prelim f) ~ weqstnsum_invmap f. Proof. revert f. induction n as [|n I]. - intros f k. apply fromempty, negstn0. exact k. - intros f. rewrite weqstnsum1_step. intros k. rewrite 2 invweqcomp. rewrite 2 weqcomp_to_funcomp_app. rewrite 3 pr1_invweq. unfold weqcoprodf1. change (invmap (weqcoprodf (weqstnsum1_prelim (λ i, f (dni lastelement i))) (idweq (⟦ f lastelement ⟧)))) with (coprodf (invweq (weqstnsum1_prelim (λ i, f (dni lastelement i)))) (idweq (⟦ f lastelement ⟧))). intermediate_path (invmap (weqoverdnicoprod (λ i : ⟦ S n ⟧, ⟦ f i ⟧)) (coprodf (weqstnsum_invmap (λ i : ⟦ n ⟧, f (dni lastelement i))) (idweq (⟦ f lastelement ⟧)) (invmap (weqfromcoprodofstn (stnsum (f ∘ dni lastelement)) (f lastelement)) k))). + apply maponpaths. change (invmap _ k) with (invmap (weqfromcoprodofstn (stnsum (f ∘ dni lastelement)) (f lastelement)) k). generalize (invmap (weqfromcoprodofstn (stnsum (f ∘ dni lastelement)) (f lastelement)) k). intro c. apply homotcoprodfhomot. * apply I. * apply homotrefl. + clear I. generalize k; clear k. use (homotweqinv (λ c, invmap (weqoverdnicoprod (λ i, ⟦ f i ⟧)) (coprodf (weqstnsum_invmap (λ i, f (dni lastelement i))) (idweq (⟦ f lastelement ⟧)) c)) (weqfromcoprodofstn (stnsum (f ∘ dni lastelement)) (f lastelement)) ). unfold funcomp. intro c. induction c as [r|s]. * unfold coprodf. change (pr1weq (weqfromcoprodofstn (stnsum (λ x, f (dni lastelement x))) (f lastelement))) with (weqfromcoprodofstn_map (stnsum (λ x, f (dni lastelement x))) (f lastelement)). set (P := (λ i : ⟦ S n ⟧, ⟦ f i ⟧)). rewrite weqstnsum_invmap_step1. change (λ i : ⟦ n ⟧, f (dni lastelement i)) with (f ∘ dni lastelement). generalize (weqstnsum_invmap (f ∘ dni lastelement) r); intro ij. induction ij as [i j]. apply idpath. * unfold coprodf. change (pr1weq (idweq _) s) with s. set (P := (λ i : ⟦ S n ⟧, ⟦ f i ⟧)). change (pr1weq _) with (weqfromcoprodofstn_map (stnsum (λ x : ⟦ n ⟧, f (dni lastelement x))) (f lastelement)). rewrite weqstnsum_invmap_step2. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.