See the license file for copyright information.
A Lean 4 formalization of triposes for the course Formalized mathematics and proof assistants, taught in the Fall of 2024 by Andrej Bauer at the Faculty of mathematics and physics, University of Ljubljana.
Further information is available at the project web pages: