proposition: Lemma path_algebra {σ : Signature} (A B : Algebra σ) (p : carriers A = carriers B) (q : transport (λ X, ∀ u, Operation X (σ u)) p (operations A) = operations B) : A = B.
proof: Proof. destruct A,B. cbn in *. by path_induction. Defined.
imports: HoTT.Utf8Minimal HoTT.Basics HoTT.Classes.implementations.ne_list HoTT.Classes.implementations.family_prod HoTT.Types HoTT.HSet HoTT.Classes.implementations.list