proposition: 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: 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.
imports: UniMath.Combinatorics.Lists UniMath.Combinatorics.FiniteSequences UniMath.Algebra.RigsAndRings UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.Algebra.Groups UniMath.MoreFoundations.NegativePropositions UniMath.Combinatorics.FiniteSets UniMath.Foundations.NaturalNumbers