The λ-calculus is a versatile tool both in mathematical logic and computer science. This thesis studies and expands upon Martin Hyland’s paper ‘Classical lambda calculus in modern dress’. It gives examples for the definitions and provides more detailed proofs, as well as one new proof for Hyland’s fundamental theorem of the λ-calculus. It complements these definitions and proofs with material of previous authors by which Hyland has been inspired. The thesis translates Hyland’s paper from set theory with classical logic to univalent foundations, and showcases where subtleties arise in such a translation. In particular, it discusses the different implementations of the Karoubi envelope in univalent foundations. Lastly, it discusses the accompanying formalization of parts of Hyland’s paper, with in particular a tactic that was developed for applying β-reduction and substitution to λ-terms.

In deze scriptie volgen we de lijn die in W. van Est in “A group theoretic interpretation of area in the elementary geometries” heeft uitgezet, maar we gaan grondiger in op de stof en bewijzen de meeste claims die door Van Est worden gedaan. We kijken naar wat triviale en nontriviale centrale groepsuitbreidingen zijn, wat die te maken hebben met cocykels en coranden en cohomologieklassen. We zien dat iedere cocykel een corresponderende homogene cocykel heeft. Aan de hand van het oppervlaktebegrip in een tweedimensionale ruimte kunnen we een homogene cocykel definiëren en daarmee kunnen we dan een centrale groepsuitbreiding construeren van de symmetriegroepen op het tweedimensionale hyperbolische, euclidische en elliptische vlak. We zien dat die uitbreidingen niet triviaal zijn, maar dat wanneer we ieder van deze uitbreidingen verheffen naar hun universele overdekking, de uitbreiding op de symmetriegroep van het hyperbolische vlak triviaal wordt, in tegenstelling tot die van het euclidische vlak.