https://arxiv.org/abs/2001.10490
Lean's approach to hygiene macros

While we're still at it, I'd like to announce my project to formalize the Stacks project in Arend

Categorical Logic by Andrew M. Pitts https://www.cl.cam.ac.uk/~amp12/papers/catl/catl.pdf

Categories with Families: Unityped, Simply Typed, and Dependently Typed https://arxiv.org/abs/1904.00827

Cubical Agda paper v2 with transpX discussed
https://staff.math.su.se/anders.mortberg/papers/cubicalagda2.pdf

RefinedC

Automating the Foundational Verification of C Code with Refined Ownership Types

https://plv.mpi-sws.org/refinedc/

Choosing is Losing:
How to combine the benefits of shallow and deep embeddings through reflection in dependently-typed host languages

https://arxiv.org/abs/2105.10819

Categorical Logic and Type Theory by Bart Jacobs. Jacobs invented comprehension categories after CwA (by Cartmell) being well-established, which is closer to a purely categorical construction instead of a mechanically-derived category from TT. It is defined in terms of Grothendieck fibrations, which is well-established in the study of advanced mathematics such as AT. IMO, these studies had induced the grand work on homotopy type theory, an application of categorical logic and homotopy theory, based on the bridge built on top of category theory. This is very beautiful.

https://people.mpi-sws.org/~dreyer/courses/catlogic/jacobs.pdf

My lecture notes on categorical logic. It is still a draft, and proofreads and corrections are appreciated. It serves as a referential material rather than a book — because it is written to be read from the middle instead of the beginning. It discusses CwA, comprehension categories and explains the pi type, universe of propositions, and simple constructions like propositional truncation in the framework of CwA. I hope you like it :)

https://personal.psu.edu/yqz5714/cwa.pdf

Note that this document is updated frequently, so make sure you update to the latest version. The old version has serious technical issues and I strongly discourage reading them.