ContinuityType This is the Agda implementation of Chuangjie Xu's PhD thesis, namely A Continuous Computational Interpretation of Type Theories