@joey What I actually mean by it is the (0, infinity) fragment of QTT. I have no idea yet how that relates to the thing that is called polymorphic dependent type theory, which for example is the title of one of the later chapters in Jacobs' categorical logic book
=> More informations about this toot | View the thread | More toots from julesh@mathstodon.xyz
=> View joey@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).