{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. 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.
Require Import