Categorical semantics for Unary Type Theory in agda.
Categorical semantics in agda for Unary Type Theory