nLab
notions of type

type, type theory

• propositions as types, inductive type, W-type

dependent type, dependent type theory, Martin-Löf dependent type theory

homotopy type, homotopy type theory

• identity type, higher inductive type