dan's lab notebook

• Internal ∞-Categorical Models of Depedent Type Theory