initiality theorem

Got to the nlab page to find the very salty demotion of this from theorem to conjecture

For any reasonable type theory the proof technique of building Henkin models lets you also prove canonicity etc