Theorem nat_plus_associativity {n} {m:stn n->nat} (k:∏ (ij : ∑ i, stn (m i)), nat) : stnsum (λ i, stnsum (curry k i)) = stnsum (k ∘ lexicalEnumeration m). Proof. intros. apply weqtoeqstn. intermediate_weq (∑ i, stn (stnsum (curry k i))). { apply invweq. apply weqstnsum1. } intermediate_weq (∑ i j, stn (curry k i j)). { apply weqfibtototal; intro i. apply invweq. apply weqstnsum1. } intermediate_weq (∑ ij, stn (k ij)). { exact (weqtotal2asstol (stn ∘ m) (stn ∘ k)). } intermediate_weq (∑ ij, stn (k (lexicalEnumeration m ij))). { apply (weqbandf (inverse_lexicalEnumeration m)). intro ij. apply eqweqmap. apply (maponpaths stn), (maponpaths k). apply pathsinv0, homotinvweqweq. } apply inverse_lexicalEnumeration. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.