proposition: Lemma path_extend_path_term_algebra {s : Sort σ} (S T : CarriersTermAlgebra C s) (e : ExtendPathTermAlgebra S T) : S = T.
proof: Proof. destruct (dependent_path_extend_path_term_algebra S T e) as [p q]. by induction (hset_path2 idpath p). Defined.
imports: HoTT.Algebra.Universal.Algebra HoTT.HSet HoTT.Classes.interfaces.canonical_names HoTT.Algebra.Universal.Homomorphism HoTT.Algebra.Universal.Congruence