Sample literate Rzk markdown

#lang rzk-1
#define id (A : U)
  : A → A
  := \ x → x

A is contractible if there exists a : A such that for any x : A we have a = x.

#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)

#def isagroupoid (A : U)
  : U
  := (x : A) → (y : A) → isaset (x =_{A} y)

#def app (A B : U) (f : A → B) (a a' : A)
  : ( a = a') → (f a = f a')
  := \lambda -> ?