{σ} (A B : Algebra σ) (p : carriers A = carriers B) (q : transport (λ X, ∀ u, Operation X (σ u)) p (operations A) = operations B) : ap carriers (path_algebra A B p q) = p. Proof. destruct A as [A a], B as [B b]. cbn in *. by destruct p,q. Defined.
Require Import Import ne_list.notations.