Skip to content

Instantly share code, notes, and snippets.

@SkySkimmer

SkySkimmer/Universe.v

Created June 11, 2016 21:29
Show Gist options
  • Save SkySkimmer/f0593798d699e1aa13d71ea5d0c6f10e to your computer and use it in GitHub Desktop.
Save SkySkimmer/f0593798d699e1aa13d71ea5d0c6f10e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Universe.v
Section Univ.
Universe i.
Definition identity (A : Type@{i}) (x : A) := x.
End Univ.
Definition id2 := identity _ identity.
Print Universes.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment