A model of Extensional Type Theory (ETT) in safe Agda, the latter being used as a formalization of basic Intensional Type Theory with a universe closed under inductive-recursive definitions. The model makes use of a new (?) notion of displayed, type-valued setoid. Universes in the model are constructed inductive-recursively, á la Altenkirch, Boulier, Kaposi, Sattler and Sestini (FoSSaCS 2021).
ETT is constructed in safe Agda using the WSLN library for the well-scoped locally nameless representation of syntax.
Checked with Agda version 2.8.0 using flags
--safe
--without-K
--no-postfix-projections