The Telescopic Library This is work in progress for an Agda library for dealing with telescopes, equivalences, and datatypes. Currently you can find a general implementation of level-polymorphic telescopes and telescopic equality.