Months ago, I formalized the definitions of syntax, {deductive, computational, concretized} semantics and more at LATIN2@tetrapod: https://gl.mathhub.info/MMT/LATIN2/-/tree/tetrapod/source/type_theory/tetrapod
Be cautious when merging into devel. Dennis already did that and those files at devel. So I don't know what happens if we remerge.
Months ago, I formalized the definitions of syntax, {deductive, computational, concretized} semantics and more at LATIN2@tetrapod: https://gl.mathhub.info/MMT/LATIN2/-/tree/tetrapod/source/type_theory/tetrapod
Be cautious when merging into devel. Dennis already did that and those files at devel. So I don't know what happens if we remerge.