This talk will discuss some problems encountered when scaling libraries in the dependently typed language Agda. In particular it will explore how the size of the Agda standard library (100kloc and growing rapidly) and its resulting memory requirements when type-checked have influenced the design of the library in areas that, at first glance, appear unrelated. These design decisions include the semi-artificial chunking of concepts into many small files and limiting the use of dependent types. The former has the knock-on effect of preventing the enforcement of abstraction barriers. While the talk will have no concrete proposal for solving the underlying issue, it will briefly discuss what enhancements to Agda might be needed to regain the ability to erect effective abstraction barriers.