Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory Chapter