initiality theorem

ID: ec8a3148-670b-4994-b224-90df8d4ab28c
ROAM_REFS: https://ncatlab.org/nlab/show/initiality+conjecture
REVIEW_SCORE: 0.0
MTIME: [2024-12-25 Wed 15:54]

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

This node is a singleton!