proposition: Lemma dependent_path_extend_path_term_algebra {s1 s2 : Sort σ} (S : CarriersTermAlgebra C s1) (T : CarriersTermAlgebra C s2) (e : ExtendDRelTermAlgebra (fun s => paths) S T) : {p : s1 = s2 | p # S = T}.
proof: Proof. generalize dependent s2. induction S as [| u c h]; intros s2 [? d | ? d] e; solve [elim e] || destruct e as [p e]. - exists p. by induction p, e. - induction p. exists idpath. cbn. f_ap. funext a. destruct (h a _ (d a) (e a)) 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