Raw File
Tip revision: dfb2127865dda7ab2db1a29ea1a2d5ac3d60f4b5 authored by AndrasKovacs on 29 October 2021, 18:43:22 UTC
Tip revision: dfb2127

module README where

Agda supplement to the paper "Generalized Universe Hierarchies and First-Class Universe Levels".

This module was checked using Agda 2.6.1, with standard library version 1.3.

For instructions on installing the standard library, see the following:

import Lib          -- library, for equational reasoning and exporting some definitions
import IRUniverse   -- semantic inductive-recursive universes over level structures
import TTGUModel    -- model of type theory with generalized levels
import TTFLModel    -- model of type theory with first-class levels, where levels are strictly the same as internal Nat
import Super        -- some notes on Palmgren's super universes and transfinite hierarchies
back to top