The type theory fire triangle: how to mix substitution, dependent elimination, a