Comment by Luna Tuna (luna-tuna) on Basic building blocks of dependent type theory · 2025-03-27T04:58:26.218Z · LW · GW

I see the notation you used in your post.  Can you point me to a standard notation that a futuristic proof assistant should be using?  Or have you covered it here?  Thanks 😀