GitHub repository: takahashi-yt/large-universes
Primary language: Agda
Created: 2024-03-10T05:13:21Z
Description: An Agda formalisation of large universe types of Martin-Löf type theory