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

.

## 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₂`

, …,
`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`

.

## Limitations¶

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 ()
```