Extensionality for structures of relational languages

A structure for a relational language has no function symbols to interpret, so two structures on the same type are equal when they interpret every relation symbol alike.

Main results

• FirstOrder.Language.Structure.ext_of_isRelational: structures for a relational language are determined by their relations.

theorem FirstOrder.Language.Structure.ext_of_isRelational {L : Language} [L.IsRelational] {M : Type u_1} {S T : L.Structure M} (h : ∀ {l : ℕ} (R : L.Relations l) (x : Fin l → M), RelMap R x ↔ RelMap R x) : S = T

Two structures for a relational language on the same type are equal when they interpret every relation symbol alike.