Structured lessons on type systems, lambda calculi, and their connections to logic and semiotic structure. Entries dependent-types typed-lambda-calculus