Skip to content

Instantly share code, notes, and snippets.

@deemp

deemp/example.rzk

Created October 2, 2023 13:42
Show Gist options
  • Save deemp/9c2d845997bb519c282b536e84994e1c to your computer and use it in GitHub Desktop.
Save deemp/9c2d845997bb519c282b536e84994e1c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
example.rzk
#lang rzk-1
-- A is contractible there exists x : A such that for any y : A we have x = y.
#def iscontr (A : U) : U
:= ∑ (a : A), (x : A) -> a =_{A} x
-- A is a proposition if for any x, y : A we have x = y
#def isaprop (A : U) : U
:= (x : A) -> (y : A) -> x =_{A} y
-- A is a set if for any x, y : A the type x =_{A} y is a proposition
#def isaset (A : U) : U
:= (x : A) -> (y : A) -> isaprop (x =_{A} y)
-- Non-dependent product of A and B
#def prod (A : U) (B : U) : U
:= ∑ (x : A), B
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment