`{Funext} {σ : Signature} (A B : Algebra σ) (p : carriers A = carriers B) (q : transport (fun i => forall u, Operation i (σ u)) p (operations A) = operations B) : A = B. Proof. apply (ap (issig_algebra σ)^-1)^-1; cbn. apply (path_sigma' _ p). refine (transport_sigma p _ @ _). apply path_sigma_hprop. exact q. Defined.
Require Import