Expand description
Data structures for managing toplevel declarations in the type theory.
The three kinds mirror the comprehension category of D-models: a Type
is a model (a context, i.e. an object of the base), a Def is a tight
transformation (a substitution, i.e. a morphism of the base), and an
Instance is an object of a fiber (a type in context).
Structs§
- Def
- A toplevel declaration of a term judgment.
- Instance
- A toplevel declaration of an instance of a model.
- Toplevel
- Storage for toplevel declarations.
- Type
- A toplevel declaration of a type.
Enums§
- TopDecl
- A toplevel declaration.