Hey you might be interested in this work-in-progress type theory for Poly: https://github.com/toposInstitute/polytt