This repository contains a small Agda implementation of idempotent equivalences, as suggested in my paper

Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT

The file Identities.agda contains information on the Agda version and dependencies.