Lifschitz Realizability for Homotopy Type Theory
Dimitrios Koutsoulis

Abstract:
This thesis explores a potential development of the constructive tradition of Russian Constructive Mathematics (RUSS) inside Homotopy Type Theory (HoTT). A short introduction to Type Theory is provided. Fragments of RUSS are then formalized inside it, alongside the Lesser Limited Principle of Omniscience (LLPO). A construction that follows closely Van Oosten’s generalization of Lifschitz Realizability is carried out to culminate with a consistency result; that of our selection of RUSS axioms and LLPO under HoTT.