Module model_instance 

Instances of models of a double theory.

An instance of a model (see Carlson-Patterson 2025) is here presented via a set of generators living over each object of the model, together with equations between terms built from morphisms of the model applied to those generators. Crucially, the lift targets and lift morphisms forced by the discrete-opfibration condition may be used in equations but are not materialized as explicit generators.

The term language is left to each doctrine to define, via the InstanceTerm trait and the HasInstanceTerm extension on DblModel. Discrete doctrines need only bare generators and morphism applications; modal doctrines additionally allow list terms to feed list-shaped morphism domains.

For the related but distinct notion of a diagram in a model — a morphism into the model from a free model — see model_diagram.

Structs

DblModelInstance

An instance of a model: a fibered set of generators plus equations between terms in the model’s instance-term language.

Traits

HasInstanceTerm

A DblModel that has an associated term language for instances.

InstanceTerm

A term in the language of an instance of some model.