{s : Sort σ} (S T : CarriersTermAlgebra C s) (e : ExtendPathTermAlgebra S T) : S = T. Proof. destruct (dependent_path_extend_path_term_algebra S T e) as [p q]. by induction (hset_path2 idpath p). Defined.
Require Import