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