Prop

Prop is Agda’s built-in sort of definitionally proof-irrelevant propositions. It is similar to the sort Set, but all elements of a type in Prop are considered to be (definitionally) equal.

The implementation of Prop is based on the POPL 2018 paper Definitional Proof-Irrelevance without K by Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau.

Usage

Just as for Set, we can define new types in Prop’s as data or record types:

data: Prop where

record: Prop where
  constructor tt

When defining a function from a data type in Prop to a type in Set, pattern matching is restricted to the absurd pattern ():

absurd : (A : Set)  A
absurd A ()

Unlike for Set, all elements of a type in Prop are definitionally equal. This implies all applications of absurd are the same:

only-one-absurdity : {A : Set}  (p q :)  absurd A p ≡ absurd A q
only-one-absurdity p q = refl

Since pattern matching on datatypes in Prop is limited, it is recommended to define types in Prop as recursive functions rather than inductive datatypes. For example, the relation _≤_ on natural numbers can be defined as follows:

_≤_ : Nat  Nat  Prop
zero  ≤ y     = ⊤
suc x ≤ zero  = ⊥
suc x ≤ suc y = x ≤ y

The induction principle for _≤_ can then be defined by matching on the arguments of type Nat:

module _ (P : (m n : Nat)  Set)
  (pzy : (y : Nat)  P zero y)
  (pss : (x y : Nat)  P x y  P (suc x) (suc y)) where

  ≤-ind : (m n : Nat)  m ≤ n  P m n
  ≤-ind zero    y       pf = pzy y
  ≤-ind (suc x) (suc y) pf = pss x y (≤-ind x y pf)
  ≤-ind (suc _) zero    ()

Note that while it is also possible to define _≤_ as a datatype in Prop, it is hard to use that version because of the limitations to matching.

When defining a record type in Set, the types of the fields can be both in Set and Prop. For example:

record Fin (n : Nat) : Set where
  constructor _[_]
  field
    ⟦_⟧   : Nat
    proof : suc ⟦_⟧ ≤ n
open Fin

Fin-≡ :  {n} (x y : Fin n)  ⟦ x ⟧ ≡ ⟦ y ⟧  x ≡ y
Fin-≡ x y refl = refl

The predicative hierarchy of Prop

Just as for Set, Agda has a predicative hierarchy of sorts Prop₀ (= Prop), Prop₁, Prop₂, … where Prop₀ : Set₁, Prop₁ : Set₂, Prop₂ : Set₃, etc. Like Set, Prop also supports universe polymorphism (see universe levels), so for each : Level we have the sort Prop . For example:

True :  {}  Prop (lsuc ℓ)
True {} =  (P : Prop)  P  P

The propositional squash type

When defining a datatype in Prop , it is allowed to have constructors that take arguments in Set ℓ′ for any ℓ′ . For example, this allows us to define the propositional squash type and its eliminator:

data Squash {} (A : Set) : Propwhere
  squash : A  Squash A

squash-elim :  {ℓ₁ ℓ₂} (A : Set ℓ₁) (P : Prop ℓ₂)  (A  P)  Squash A  P
squash-elim A P f (squash x) = f x

This type allows us to simulate Agda’s existing irrelevant arguments (see irrelevance) by replacing .A with Squash A.

irrToSquash :  {} {A : Set}  .A  Squash A
irrToSquash x = squash x

Limitations

It is possible to define an equality type in Prop as follows:

data _≐_ {} {A : Set} (x : A) : A  Propwhere
  refl : x ≐ x

However, the corresponding eliminator cannot be defined because of the limitations on pattern matching. As a consequence, this equality type is only useful for refuting impossible equations:

0≢1 : 01 0≢1 ()