Lemma weqstnsum1_prelim_eq { n : nat } (f : ⟦n⟧ -> nat) : weqstnsum1_prelim f ~ weqstnsum_map f. Proof. revert f. induction n as [|n I]. - intros f ij. apply fromempty, negstn0. exact (pr1 ij). - intros f. rewrite weqstnsum1_step. intros ij. rewrite 2 weqcomp_to_funcomp_app. unfold weqcoprodf1. change (pr1weq (weqcoprodf (weqstnsum1_prelim (λ i, f (dni lastelement i))) (idweq (⟦ f lastelement ⟧)))) with (coprodf (weqstnsum1_prelim (λ i, f (dni lastelement i))) (idfun (⟦ f lastelement ⟧))). intermediate_path ((weqfromcoprodofstn (stnsum (f ∘ dni lastelement)) (f lastelement)) (coprodf (weqstnsum_map (λ i, f (dni lastelement i))) (idfun (⟦ f lastelement ⟧)) ((weqoverdnicoprod (λ i, ⟦ f i ⟧)) ij))). + apply maponpaths. apply homotcoprodfhomot. * apply I. * intro x. apply idpath. + clear I. apply pathsinv0. generalize ij ; clear ij. apply (homotweqinv' (weqstnsum_map f) (weqoverdnicoprod (λ i : ⟦ S n ⟧, ⟦ f i ⟧)) (λ c, pr1weq (weqfromcoprodofstn (stnsum (f ∘ dni lastelement)) (f lastelement)) (coprodf (weqstnsum_map (λ i, f (dni lastelement i))) (idfun _) c)) ). intros c. simpl. set (P := λ i, ⟦ f i ⟧). change (pr1weq (weqfromcoprodofstn (stnsum (λ x : ⟦ n ⟧, f (dni lastelement x))) (f lastelement))) with (weqfromcoprodofstn_map (stnsum (λ x : ⟦ n ⟧, f (dni lastelement x))) (f lastelement)). induction c as [jk|k]. * unfold coprodf. induction jk as [j k]. change (invmap (weqoverdnicoprod P) (ii1 (j,,k))) with (tpair P (dni lastelement j) k). unfold weqfromcoprodofstn_map. unfold coprod_rect. unfold weqstnsum_map. apply subtypePath_prop. induction k as [k K]. simpl. apply (maponpaths (λ x, x+k)). unfold funcomp, stntonat, di. clear K k. induction (natlthorgeh _ n) as [G|G']. -- simpl. apply stnsum_eq; intro k. apply maponpaths. apply subtypePath_prop. simpl. apply pathsinv0, di_eq1. exact (istransnatlth _ _ _ (stnlt k) G). -- apply fromempty. exact (natlthtonegnatgeh _ _ (stnlt j) G'). * change (invmap (weqoverdnicoprod P) (ii2 k)) with (tpair P lastelement k). simpl. unfold weqstnsum_map. apply subtypePath_prop. induction k as [k K]. simpl. apply (maponpaths (λ x, x+k)). apply maponpaths. apply funextfun; intro i. induction i as [i I]. simpl. apply maponpaths. apply subtypePath_prop. simpl. apply pathsinv0, di_eq1. assumption. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.