proposition: Lemma path_algebra `{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: Proof. apply (ap (issig_algebra σ)^-1)^-1; cbn. apply (path_sigma' _ p). refine (transport_sigma p _ @ _). apply path_sigma_hprop. exact q. Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet