I am wondering where I can find literature describing the rules for a simple type theory with just products, sums, function types, unit and the empty type. Robert Harper describes such a theory 3 minutes in to this YouTube video:
Robert Harper's Type Theory Video
He says such a type theory corresponds to intuitionistic propositional logic, as well as to the theory of a free bicartesian closed category. Harper does not go over all the details , and I would appreciate some literature covering all the inference rules etc. Ideally using the notation with $\vdash$ and horizontal lines. This is the same notation used in
Any literature exhaustively covering the rules behind a type theory with products and function objects would be appreciated.