proposition: Lemma algebra_eq {T : algebraic_theory} (A B : algebra T) (H1 : (A : hSet) = (B : hSet)) (H2 : ∏ n f, transportf (λ (X : hSet), (stn n → X) → X) H1 (action f) = action f) : A = B.
proof: Proof. use total2_paths_f. - exact H1. - use subtypePath. { intro. apply isaprop_full_is_algebra. } refine (pr1_transportf H1 _ @ _). refine (transportf_sec_constant _ _ @ _). apply funextsec. intro. refine (transportf_sec_constant _ _ @ _). apply funextsec. intro. apply H2. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraCategoryCore