fact: Definition CarriersTermAlgebra_rect {σ} := @CarriersTermAlgebra_ind σ.
imports: HoTT.Algebra.Universal.Algebra HoTT.HSet HoTT.Classes.interfaces.canonical_names HoTT.Algebra.Universal.Homomorphism HoTT.Algebra.Universal.Congruence