Lambdapi formalization of the Theory U introduced in Axioms for Mathematics, by Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, FSCD'21.
The theory U is modular: you can build your own sub-logic by only requiring the files you need. For instance, by requiring Set, Prop, Quant and Arrow, you get predicate intuitionist higher-order logic. If you add Impredicativity, you get impredicative intuitionist higher-order logic. If you add again ProofObj, DepArrow and DepImpl, you get the calculus of constructions. Etc.