`{Funext} {σ} (A B : Algebra σ) (p : carriers A = carriers B) (q : transport (fun i => forall u, Operation i (σ u)) p (operations A) = operations B) : ap carriers (path_algebra A B p q) = p. Proof. destruct A as [A a ha], B as [B b hb]; cbn in p, q. destruct p, q. unfold path_algebra, path_sigma_hprop, path_sigma_uncurried. cbn -[center]. by destruct (center (ha = hb)). Defined.
Require Import