Andrew Pitts
Agda code
Department of Computer Science & Technology
>
Andrew Pitts
>
Agda code
Agda
code by Andrew Pitts
Quotient types using private and primTrustMe declarations
[
quotient.agda
].
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).
Code
accompanying the paper
Typal Heterogeneous Equality Types
.
Initial algebra for a strictly positive endofunctor constructed using sized types and quotient types
[
code
].