Document some connections to type theory

yeslogic / fathom

🚧 (Alpha stage software) A declarative data definition language for formally specifying binary data formats. 🚧

Apache License 2.0

259 stars 14 forks source link

Document some connections to type theory #365

Closed brendanzab closed 2 years ago

brendanzab commented 2 years ago

This mentions some connections between our approach to format descriptions and universes in type theory. Considering it took me a bit to get my head around I think it could be worth documenting it.