Agda code by Andrew Pitts

• Pritam Choudhury's Constructive Representation of Nominal Sets in Agda (project for the Cambridge MPhil in Advanced Computer Science 2015) [disseration (pdf)] [agda sources (zip)]
• Agda code accompanying the paper Axioms for Modelling Cubical Type Theory in a Topos (joint work with Ian Orton).
• Agda code accompanying the BigProof talk Using Agda to Explore Path-Oriented Models of Type Theory (27 June 2017).
• Agda code accompanying the paper Internal Universes in Models of Homotopy Type Theory (joint work with Dan Licata, Ian Orton and Bas Spitters).
• Agda code accompanying the paper Typal Heterogeneous Equality Types.
• Agda code accompanying the paper Quotients, Inductive Types and Quotient Inductive Types. (joint work with Marcelo Fiore and S. C. Steenkamp).
• Agda code accompanying the paper Constructing Initial Algebras Using Inflationary Iteration (joint work with S. C. Steenkamp).
• Agda code accompanying the paper Locally Nameless Sets.