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:

  1. data ⊥ : Prop where
  3. record ⊤ : Prop where
  4.   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 ():

  1. absurd : (A : Set) → ⊥ → A
  2. absurd A ()

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

  1. only-one-absurdity : {A : Set} → (p q : ⊥) → absurd A p ≡ absurd A q
  2. 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:

  1. _≤_ : Nat → Nat → Prop
  2. zero  ≤ y     = ⊤
  3. suc x ≤ zero  = ⊥
  4. suc x ≤ suc y = x ≤ y

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

  1. module _ (P : (m n : Nat) → Set)
  2.   (pzy : (y : Nat) → P zero y)
  3.   (pss : (x y : Nat) → P x y → P (suc x) (suc y)) where
  5.   ≤-ind : (m n : Nat) → m ≤ n → P m n
  6.   ≤-ind zero    y       pf = pzy y
  7.   ≤-ind (suc x) (suc y) pf = pss x y (≤-ind x y pf)
  8.   ≤-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:

  1. record Fin (n : Nat) : Set where
  2.   constructor _[_]
  3.   field
  4.     ⟦_⟧   : Nat
  5.     proof : suc ⟦_⟧ ≤ n
  6. open Fin
  8. Fin-≡ : ∀ {n} (x y : Fin n) → ⟦ x ⟧ ≡ ⟦ y ⟧ → x ≡ y
  9. 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:

  1. True : ∀ {ℓ} → Prop (lsuc ℓ)
  2. 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:

  1. data Squash {ℓ} (A : Set ℓ) : Prop ℓ where
  2.   squash : A → Squash A
  4. squash-elim : ∀ {ℓ₁ ℓ₂} (A : Set ℓ₁) (P : Prop ℓ₂) → (A → P) → Squash A → P
  5. 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:

  1. data _≐_ {ℓ} {A : Set ℓ} (x : A) : A → Prop ℓ where
  2.   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:

  1. 0≢1 : 0 ≐ 1 → ⊥
  2. 0≢1 ()