proposition: Lemma sn_power_arrow_commutes (i : stn (S n)) : sn_power_arrow · sn_power_projection i = cone' i.
proof: Proof. rewrite <- (homotweqinvweq stnweq i). induction (invmap stnweq i) as [i' | i']. - refine (maponpaths (λ x, _ · (_ x)) (homotinvweqweq stnweq (inl i')) @ _). refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (BinProductPr2Commutes _ _ _ _ _ _ _) @ _). apply (ProductPrCommutes _ _ _ P). - refine (maponpaths (λ x, _ · (_ x)) (homotinvweqweq stnweq (inr i')) @ _). refine (BinProductPr1Commutes _ _ _ (BP c P) _ _ _ @ _). apply maponpaths. now apply stn_eq. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorCategory UniMath.Combinatorics.StandardFiniteSets