fact: Fixpoint ExtendDRelTermAlgebra {σ : Signature} {C : Carriers σ} (R : forall s, Relation (C s)) {s1 s2 : Sort σ} (S : CarriersTermAlgebra C s1) (T : CarriersTermAlgebra C s2) : Type := match S, T with | var_term_algebra s1 x, var_term_algebra s2 y => {p : s1 = s2 | R s2 (p # x) y} | ops_term_algebra u1 a, ops_term_algebra u2 b => { p : u1 = u2 | forall i : Arity (σ u1), ExtendDRelTermAlgebra R (a i) (b (transport (fun v => Arity (σ v)) p i))} | _, _ => Empty end.
imports: HoTT.Algebra.Universal.Algebra HoTT.HSet HoTT.Classes.interfaces.canonical_names HoTT.Algebra.Universal.Homomorphism HoTT.Algebra.Universal.Congruence