Auxiliary Agda files

This folder contains some auxiliary files for the Agda track of the HoTTEST Summer School 2022. Everything here is optional material.

1. Paradoxes derived from “type in type”:
   1. Hurkens’ paradox
   2. Russell’s paradox