Definition holds {σ: signature} {V: varspec σ} (a: algebra σ) (e: equation σ V) : UU := ∏ α, fromterm (ops a) α (eqsort e) (lhs e) = fromterm (ops a) α (eqsort e) (rhs e).
Require Import UniMath.MoreFoundations.Notations.