Entity Modelling

www.entitymodelling.org - entity modelling introduced from first principles - relational database design theory and practice - dependent type theory

Dependent Type Structure

Figure 14
A model of a system of dependent types.
Figure 15
Dependent type reference to scope triangle.
Figure 16
Scope diagram for substituting into a variable type - an example of a scope square which is also a pullback.
Figure 17
Scope diagram for substituting actuals for formals in a function - also a pullback diagram.
Figure 18
An extended model including construction of types using existential and universal quantifiers.