proposition: Lemma path_ap_carriers_path_algebra {σ} (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: Proof. destruct A as [A a], B as [B b]. cbn in *. by destruct p,q. Defined.
imports: HoTT.Utf8Minimal HoTT.Basics HoTT.Classes.implementations.ne_list HoTT.Classes.implementations.family_prod HoTT.Types HoTT.HSet HoTT.Classes.implementations.list