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.