Convert to Agda https://github.com/UniMath/TypeTheory/tree/master/TypeTheory
Some Agda implementations here https://github.com/UniMath/agda-unimath/tree/master/src/type-theories
Categories with Families: Unityped, Simply Typed, and Dependently Typed https://arxiv.org/pdf/1904.00827.pdf