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 2019 paper Definitional Proof-Irrelevance without K by Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau.

This is an experimental extension of Agda guarded by option --prop.


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 _[_]
    ⟦_⟧   : 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₂, …, Propω₀ (= Propω), Propω₁, Propω₂, …, where Prop₀ : Set₁, Prop₁ : Set₂, Prop₂ : Set₃, …, 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

Note that {ℓ} Prop (lsuc ℓ) (and likewise any {ℓ} Prop (t ℓ)) lives in Setω, not Propω.

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 ) : Prop  where
  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.


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

data _≐_ {} {A : Set } (x : A) : A  Prop  where
  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 : 0  1  0≢1 ()