Skip to content

Instantly share code, notes, and snippets.

@AndyShiue

AndyShiue/SetOmega.agda

Created November 9, 2023 15:34
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save AndyShiue/2580d3a70fdbd536d1259f3aa7f95ea6 to your computer and use it in GitHub Desktop.
Save AndyShiue/2580d3a70fdbd536d1259f3aa7f95ea6 to your computer and use it in GitHub Desktop.
Download ZIP
Demonstrate Setω+n
Raw
SetOmega.agda
open import Agda.Primitive using (Setω)
test : Setω₂
test = Setω₁
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment