clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;

tuned signature;

explicit operations to instantiate frees: typ, term, thm, morphism;

tuned signature;

more explicit instantiate_morphism (without checks for typ / term component);

tuned;

careful export of type-dependent functions, without losing their special status;

clarified modules;
tuned signature;

clarified modules;
tuned signature;

tuned signature;

maintain morphism names for diagnostic purposes;

tuned signature;

slightly more explicit/syntactic modelling of morphisms;

modernized some structure names, keeping a few legacy aliases;

eliminated obsolete var morphism;

binding is alias for Binding.T

cleaned up binding module and related code

name/var morphism operates on Name.binding;

type Morphism.declaration;

added Morphism.transform/form (generic non-sense);

renamed comp to compose (avoid clash with Alice keywords);

added cterm interface;

simultaneous fact morphism;

added name/var/typ/term/thm_morphism;
removed transfer;

Abstract morphisms on formal entities.