(Research notes are also available below.)
pdf , Agda version, slides for the IHP 2014 talk, slides for the Mittag-Leffler 2015 talk. slides for the TLCA'2015 talk.
pdf, Agda formalization (also as a zip file).
pdf.
pdf.
pdf.
pdf, Agda (with combinatory version of system T), Agda without comments, Agda using Church encoding of dialogues, Agda internalizing the modulus of continuity, Agda (with lambda-calculus version of system T), more.
pdf, Agda, A family of types that fail to be provably collapsible (also in Agda), Constant choice.
See also the companion programs/proofs in Agda.
pdf.
paper, slides presented at MAP'2011 in Leiden, draft full version (a more polished full version will be eventually available, for the moment the paper is more readable).
Electronically available as Technical Report 97:05, School of Cognitive and Computing Sciences, University of Sussex.
ECS-LFCS-97-374 (follow this link and then find file at the bottom).
html.
pdf.
pdf abstract, talk at HoTT/UF in Warsaw 2015, cubicaltt code with full formal proofs.
zip file with Haskell programs and scripts.
There is also a literate program derived from this used for a talk in Fun in the Afternoon (March 2011).
pdf.
pdf.
pdf.