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.