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

## 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 ℓ) : 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 ()
```