Bundled First-Order Structures #
This file bundles types together with their first-order structure.
Main Definitions #
FirstOrder.Language.Theory.ModelTypeis the type of nonempty models of a particular theory.
FirstOrder.Language.equivSetoidis the isomorphism equivalence relation on bundled structures.
- Define category structures on bundled structures and models.
The type of nonempty models of a first-order theory.
The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses.
The reduct of any model of
φ.onTheory T is a model of
φ is injective,
defaultExpansion expands a model of
T to a model of
A model of a theory is also a model of any subtheory.
A structure that is elementarily equivalent to a model, bundled as a model.
An elementary substructure of a bundled model as a bundled model.