`{Funext} {σ : Signature} {A B : Algebra σ} `{IsHSetAlgebra B} (p q : A = B) (r : ap carriers p = ap carriers q) : p = q. Proof. apply path_path_algebra. unshelve eapply path_path_sigma. - transitivity (ap carriers p); [by destruct p |]. transitivity (ap carriers q); [exact r | by destruct q]. - apply path_ishprop. Defined.
Require Import Import ne_list.notations.