A Type Theory for Strictly Unital $\infty$-Categories

Eric Finster, David Reutter, Alex Rice +1

We use type-theoretic techniques to present an algebraic theory of $\infty$-categories with strict units. Starting with a known type-theoretic presentation of fully weak $\infty$-c…