Mere propositions

This is a literate Rzk file:

#lang rzk-1

This module assumes function extensionality:

#assume funext : FunExt

Definition 3.3.1

A type \(P\) is a mere proposition if for all \(x, y : P\) we have \(x = y\).

#define isProp
  ( A : U)
  : U
  := (x : A) → (y : A) → x = y

Examples

#define isProp-Unit
  : isProp Unit
  := \ unit unit → refl

#define isProp-function uses (funext)
  ( A : U)
  ( B : A → U)
  ( isProp-B : (a : A) → isProp (B a))
  : isProp ((a : A) → B a)
  := \ f g → map-funext funext A B f g (\ a → isProp-B a (f a) (g a))