proposition: Lemma F_preserves_power_pr {n : nat} (i : stn n) : #F (ProductPr _ _ (power n) i) = F_power_iso n · ProductPr _ _ (power' n) i · inv_from_z_iso F_preserves_X.
proof: Proof. induction n as [ | n IHn]. - induction (negnatlthn0 _ (stnlt i)). - rewrite <- (homotweqinvweq stnweq i). induction (invmap stnweq i) as [i' | i']; refine (maponpaths (λ x, # F(_ x)) (homotinvweqweq stnweq _) @ !_); refine (maponpaths (λ x, _ · _ x · _) (homotinvweqweq stnweq _) @ !_). + refine (_ @ maponpaths (λ x, x · _) (assoc' _ _ _)). refine (_ @ maponpaths (λ x, x · _ · _) (assoc _ _ _)). refine (_ @ !maponpaths (λ x, _ · x · _ · _) (BinProductOfArrowsPr2 _ _ _ _ _)). refine (_ @ maponpaths (λ x, x · _ · _) (assoc' _ _ _)). refine (_ @ !maponpaths (λ x, x · _ · _ · _) (BinProductPr2Commutes _ _ _ _ _ _ _)). refine (functor_comp _ _ _ @ _). refine (maponpaths _ (IHn _) @ _). refine (assoc _ _ _ @ _). exact (maponpaths (λ x, x · _) (assoc _ _ _)). + cbn. refine (_ @ maponpaths (λ x, x · _) (assoc _ _ _)). refine (_ @ !maponpaths (λ x, _ x · _) (BinProductOfArrowsPr1 _ _ _ _ _)). refine (_ @ maponpaths (λ x, x · _) (assoc' _ _ _)). refine (_ @ assoc _ _ _). refine (_ @ !maponpaths _ (z_iso_inv_after_z_iso _)). refine (_ @ !id_right _). exact (!BinProductPr1Commutes _ _ _ _ _ _ _). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.LambdaTheories UniMath.AlgebraicTheories.LambdaTheoryCategoryCore UniMath.AlgebraicTheories.LambdaTheoryMorphisms UniMath.Combinatorics.Tuples