proposition: Lemma path_ap_carriers_path_algebra `{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: 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]. now destruct (center (ha = hb)). Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet