proposition: Lemma path_path_algebra `{Funext} {σ} {A B : Algebra σ} (p q : A = B) (r : ap carriers p = ap carriers q) : p = q.
proof: Proof. apply path_path_algebra_issig. 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.
imports: HoTT.Basics HoTT.Types HoTT.HSet