{σ : Signature} {C : Carriers σ} (R : forall s, Relation (C s)) {s : Sort σ} : CarriersTermAlgebra C s -> CarriersTermAlgebra C s -> Type := ExtendDRelTermAlgebra R. Section extend_rel_term_algebra. Context `{Funext} {σ : Signature} {C : Carriers σ} (R : forall s, Relation (C s)) `{!forall s, is_mere_relation (C s) (R s)}. Global Instance hprop_extend_drel_term_algebra {s1 s2 : Sort σ} (S : CarriersTermAlgebra C s1) (T : CarriersTermAlgebra C s2) : IsHProp (ExtendDRelTermAlgebra R S T). Proof. generalize dependent s2. induction S; intros s2 T; destruct T; exact _. Qed.
Require Import