proposition: Lemma reflexive_extend_path_term_algebra_path {s : Sort σ} {S T : CarriersTermAlgebra C s} (p : S = T) : ExtendPathTermAlgebra S T.
proof: Proof. induction p. apply reflexive_extend_path_term_algebra. Defined.
imports: HoTT.Algebra.Universal.Algebra HoTT.HSet HoTT.Classes.interfaces.canonical_names HoTT.Algebra.Universal.Homomorphism HoTT.Algebra.Universal.Congruence