Post #2728851

Does anybody know of a good introductory reference or lecture notes for the use of categorical gluing in proofs of normalization and other metatheoretic properties of type theory? It's topic I'm finding more and more interesting, but I'm also finding it very hard to get into. I've tried going back to the source, the Altenkirch, Hofmann, Streicher articles from the 90s, and although I feel like I have the necessary categorical background, I'm finding them pretty hard to follow. In more modern articles, there's even more that goes way over my head. Does there exist a gentler introduction to this stuff?