Andrew Pitts
Agda code
Department of Computer Science & Technology
>
Andrew Pitts
>
Agda code
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
.