proposition: Lemma F_preserves_product_arrow {n : nat} (Y : C) (f : stn n → C⟦Y, X⟧) : #F (ProductArrow _ _ (power n) f) = ProductArrow _ _ (power' n) (λ i, #F (f i) · F_preserves_X) · inv_from_z_iso (F_power_iso n).
proof: Proof. apply z_iso_inv_on_left. apply ProductArrow_eq. intro i. refine (!_ @ assoc _ _ _). refine (!maponpaths _ ((z_iso_inv_to_right _ _ _ _ _ _ (F_preserves_power_pr _))) @ _). refine (assoc _ _ _ @ _). refine (!maponpaths (λ x, x · _) (functor_comp _ _ _) @ _). refine (maponpaths (λ x, #F x · _) (ProductPrCommutes _ _ _ _ _ _ _) @ !_). exact (ProductPrCommutes _ _ _ _ _ _ _). 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