Emily Riehl & Michael Shulman. A type theory for synthetic \(\infty \)-categories. Higher Structures, 1(1):147--224, 2017. https://higher-structures.math.cas.cz/api/files/issues/Vol1Iss1/RiehlShulman