Proof-relevance

This section is empty…

A proof-irrelevant type

  data ⊤ : Type where
    tt : ⊤

Interpretation as a proof: tt is a proof of proposition ⊤.

A proof-relevant type

  data â„• : Type where
    zero : â„•
    suc : ℕ → ℕ

The type â„• has no interpretation as a classical proposition. In classical mathematics, one cannot distinguish between proofs of a given proposition [cite:@hottgame]. Constructions like â„• are known as proof-relevant types.