Bundled First-Order Structures #

This file bundles types together with their first-order structure.

Main Definitions #



A type bundled with the structure induced by an equivalence.

Instances For

    An equivalence of types as a first-order equivalence to the bundled structure on the codomain.

    Instances For

      The equivalence relation on bundled L.Structures indicating that they are isomorphic.

      The type of nonempty models of a first-order theory.

      Instances For

        The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses.

        Instances For