Models of predicative type theory are well-studied and have been mechanized, ranging from proofs of consistency for a minimal type theory with a predicative hierarchy in 1000 lines of Rocq to proofs all the way up to decidability of conversion in 10 000 lines of Agda. In contrast, the story for impredicative type theory is not so clear. Incorporating different features alongside an impredicative Prop may require substantially different proof methods. This post catalogues these various models, wh...