Prop

Prop is Agda’s built-in sort of definitionally proof-irrelevant propositions. It is similar to the sort Type, 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 Type, 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 Type, pattern matching is restricted to the absurd pattern ():

absurd : (A : Type) → ⊥ → A
absurd A ()

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

only-one-absurdity : {A : Type} → (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) → Type)
  (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 Type, the types of the fields can be both in Type and Prop. For example:

record Fin (n : Nat) : Type 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 Type, Agda has a predicative hierarchy of sorts Prop₀ (= Prop), Prop₁, Prop₂, …, Propω₀ (= Propω), Propω₁, Propω₂, …, where Prop₀ : Type₁, Prop₁ : Type₂, Prop₂ : Type₃, …, Propω₀ : Typeω₁, Propω₁ : Typeω₂, Propω₂ : Typeω₃, etc. Like Type, 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 Typeω, not Propω.

The propositional squash type

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

data Squash {ℓ} (A : Type ℓ) : Prop ℓ where
  squash : A → Squash A

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

This type allows us to simulate Agda’s irrelevant arguments by replacing .A with Squash A.

Limitations

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

data _≐_ {ℓ} {A : Type ℓ} (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 ()