Naïm Camille Favier on Nostr: nprofile1q…4rrqe In your note on algebraic type theory you mention the ...
nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) In your note on algebraic type theory you mention the "Lindenbaum-Tarski model generated by the raw syntax of pure MLTT without connectives". Just to be sure, this model is trivial, right? There are no types, so the only context is the terminal one.