Entity Modelling

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

Dependent Type Structure

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