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