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.
• WSLN: Well Scoped Locally Nameless Agda library. Accompanying paper Well Scoped Locally Nameless Representation of Syntax.
• IntensionalSetoids: A model of Extensional Type Theory (ETT) in safe Agda, the latter being used as a formalization of basic Intensional Type Theory with a universe closed under inductive-recursive definitions. The model makes use of a new (?) notion of displayed, type-valued setoid. Universes in the model are constructed inductive-recursively, á la Altenkirch, Boulier, Kaposi, Sattler and Sestini (FoSSaCS 2021).