Hi, There are numerous implementations of untyped lambda calculus and simply typed lambda calculus in Agda online. However, I can't find any mention of encoding of other "higher" lambda calculus in the lambda cube like λ2 or λP in Agda. Is it because they are inherently impredicative and can't be represented in Agda? Thanks, Si Yu