Type family and dependent function type.excalidraw

⚠ Switch to EXCALIDRAW VIEW in the MORE OPTIONS menu of this document. ⚠ You can decompress Drawing data with the command palette: ‘Decompress current Excalidraw file’. For more info check in plugin settings under ‘Saving’

Excalidraw Data

Text Elements

x

A

f

B

Type

Term

Input

Output

Input

Output

dependent function type

type family

dependent function

type of type family

Embedded Files

2ac32adecf2abd035aa737b4ec51d1c26392dca9: ${\Pi }_{(x:A)}B(x)$

a9cda798425d6d416ecaad0c4c7a8490e5c2f038: $A\to \mathcal{U}$

44a822b01e15432d8b149bd8ac88743e96e3aafd: $B(x)$

72c67de3b382f9c9894dc502dc2ae3a6a373f82e: $f(x)$

6e48c148490b97fa98607c2c4420eb8ba2e0f8f3: $\mathcal{U}$