diff --git a/src/Data/Maybe/Properties.agda b/src/Data/Maybe/Properties.agda
index 2df06d3f88..00fa5beceb 100644
--- a/src/Data/Maybe/Properties.agda
+++ b/src/Data/Maybe/Properties.agda
@@ -31,6 +31,9 @@ private
 ------------------------------------------------------------------------
 -- Equality
 
+just≢nothing : ∀ {x} → (Maybe A ∋ just x) ≢ nothing
+just≢nothing ()
+
 just-injective : ∀ {x y} → (Maybe A ∋ just x) ≡ just y → x ≡ y
 just-injective refl = refl
 
diff --git a/src/Data/PriorityQueue.agda b/src/Data/PriorityQueue.agda
new file mode 100644
index 0000000000..3c28ea813f
--- /dev/null
+++ b/src/Data/PriorityQueue.agda
@@ -0,0 +1,11 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Priority queue
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.PriorityQueue where
+
+open import Data.PriorityQueue.Base public
diff --git a/src/Data/PriorityQueue/Base.agda b/src/Data/PriorityQueue/Base.agda
new file mode 100644
index 0000000000..a8e1e8a211
--- /dev/null
+++ b/src/Data/PriorityQueue/Base.agda
@@ -0,0 +1,144 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Interface definition of priority queue
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (TotalOrder)
+
+module Data.PriorityQueue.Base
+  {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where
+
+open import Data.Empty
+open import Data.Maybe as Maybe
+open import Data.Maybe.Properties
+open import Data.Nat using (ℕ; zero; suc; _+_)
+open import Data.Nat.Properties
+open import Data.Product
+open import Data.List
+open import Data.List.Relation.Binary.Permutation.Propositional
+open import Data.List.Relation.Unary.All using (All)
+open import Function.Base
+open import Level renaming (suc to ℓ-suc)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as P
+open import Relation.Unary hiding (Empty)
+open import Relation.Nullary
+open import Induction.WellFounded
+
+open TotalOrder totalOrder renaming (Carrier to A)
+
+record RawPriorityQueue b ℓ : Set (a ⊔ ℓ-suc (b ⊔ ℓ)) where
+  field
+    Queue  : Set b
+    size   : Queue → ℕ
+    empty  : Queue
+    insert : A → Queue → Queue
+    meld   : Queue → Queue → Queue
+    popMin : Queue → Maybe (A × Queue)
+
+  singleton : A → Queue
+  singleton x = insert x empty
+
+  findMin : Queue → Maybe A
+  findMin = Maybe.map proj₁ ∘ popMin
+
+  deleteMin : Queue → Maybe Queue
+  deleteMin = Maybe.map proj₂ ∘ popMin
+
+  Empty : Pred Queue (a ⊔ b)
+  Empty q = popMin q ≡ nothing
+
+  ¬Empty : Pred Queue (a ⊔ b)
+  ¬Empty q = ¬ Empty q
+
+  PopMin : Queue → A → Queue → Set (a ⊔ b)
+  PopMin q x q' = popMin q ≡ just (x , q')
+
+  FindMin : REL Queue A a
+  FindMin q x = findMin q ≡ just x
+
+  DeleteMin : Rel Queue b
+  DeleteMin q q' = deleteMin q ≡ just q'
+
+  _≺_ : Rel Queue b
+  q' ≺ q = DeleteMin q q'
+
+  _⊀_ : Rel Queue b
+  q' ⊀ q = ¬ (q' ≺ q)
+
+  Empty⇒⊀ : ∀ {q} → Empty q → (∀ q' → q' ⊀ q)
+  Empty⇒⊀ {q} ≡nothing q' ≡just = just≢nothing $ begin
+    just q'     ≡˘⟨ ≡just ⟩
+    deleteMin q ≡⟨ P.cong (Maybe.map proj₂) ≡nothing ⟩
+    nothing     ∎
+    where open P.≡-Reasoning
+
+
+record SizeLaws {b ℓ} (rawPriorityQueue : RawPriorityQueue b ℓ) : Set (a ⊔ b) where
+  open RawPriorityQueue rawPriorityQueue
+
+  field
+    Empty⇒size≡0 : ∀ q → Empty q → size q ≡ 0
+    ≺-size        : ∀ q q' → q' ≺ q → size q ≡ 1 + size q'
+    size-empty    : size empty ≡ 0
+    size-insert   : ∀ x q → size (insert x q) ≡ 1 + size q
+    size-meld     : ∀ q₁ q₂ → size (meld q₁ q₂) ≡ size q₁ + size q₂
+
+  size≡0⇒Empty : ∀ q → size q ≡ 0 → Empty q
+  size≡0⇒Empty q #q≡0 with popMin q in eq
+  ... | nothing = P.refl
+  ... | just (x , q') = ⊥-elim ∘ 0≢1+n $ begin
+    0           ≡˘⟨ #q≡0 ⟩
+    size q      ≡⟨ ≺-size q q' (P.cong (Maybe.map proj₂) eq) ⟩
+    1 + size q' ∎
+    where open P.≡-Reasoning
+
+  ≺-wellFounded : WellFounded _≺_
+  ≺-wellFounded = λ q → Size⇒Acc _ q P.refl
+    where
+    Size⇒Acc : ∀ n q → size q ≡ n → Acc _≺_ q
+    Size⇒Acc zero    q #q≡0 = acc λ q' q'≺q →
+      ⊥-elim (Empty⇒⊀ (size≡0⇒Empty q #q≡0) q' q'≺q)
+    Size⇒Acc (suc m) q #q≡n = acc λ q' q'≺q →
+      Size⇒Acc m q' ∘ suc-injective $ begin
+        1 + size q' ≡˘⟨ ≺-size q q' q'≺q ⟩
+        size q      ≡⟨ #q≡n ⟩
+        1 + m       ∎
+      where open P.≡-Reasoning
+
+  toListAux : ∀ q → @0 Acc _≺_ q → List A
+  toListAux q (acc rs) with popMin q
+  ... | nothing       = []
+  ... | just (x , q') = x ∷ toListAux q' (rs q' P.refl)
+
+  toList : Queue → List A
+  toList q = toListAux q (≺-wellFounded q)
+
+
+record ElementLaws
+  {b ℓ}
+  (rawPriorityQueue : RawPriorityQueue b ℓ)
+  (sizeLaws : SizeLaws rawPriorityQueue)
+  : Set (a ⊔ b ⊔ ℓ₂) where
+
+  open RawPriorityQueue rawPriorityQueue
+  open SizeLaws sizeLaws
+
+  field
+    toList-insert  : ∀ q x → toList (insert x q) ↭ x ∷ toList q
+    toList-meld    : ∀ q₁ q₂ → toList (meld q₁ q₂) ↭ toList q₁ ++ toList q₂
+    toList-FindMin : ∀ q x → FindMin q x → All (x ≤_) (toList q)
+
+
+record PriorityQueue b ℓ : Set (a ⊔ ℓ-suc (b ⊔ ℓ) ⊔ ℓ₂) where
+  field
+    rawPriorityQueue : RawPriorityQueue b ℓ
+    sizeLaws         : SizeLaws rawPriorityQueue
+    elementLaws      : ElementLaws rawPriorityQueue sizeLaws
+
+  open RawPriorityQueue rawPriorityQueue public
+  open SizeLaws sizeLaws public
+  open ElementLaws elementLaws public
diff --git a/src/Data/PriorityQueue/Properties.agda b/src/Data/PriorityQueue/Properties.agda
new file mode 100644
index 0000000000..a74db0a87e
--- /dev/null
+++ b/src/Data/PriorityQueue/Properties.agda
@@ -0,0 +1,81 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of priority queue
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (TotalOrder)
+open import Data.PriorityQueue.Base
+
+module Data.PriorityQueue.Properties
+  {a ℓ₁ ℓ₂} {b ℓ}
+  (totalOrder : TotalOrder a ℓ₁ ℓ₂)
+  (priorityQueue : PriorityQueue totalOrder b ℓ)
+  where
+
+open import Data.Empty
+import Data.Empty.Irrelevant as Irrelevant
+open import Data.List
+open import Data.Maybe as Maybe
+open import Data.Nat
+open import Data.Product
+open import Relation.Binary.PropositionalEquality as P
+open import Induction.WellFounded
+
+open TotalOrder totalOrder renaming (Carrier to A)
+open PriorityQueue priorityQueue
+
+popMin⇒deleteMin : ∀ {q t} → popMin q ≡ t → deleteMin q ≡ Maybe.map proj₂ t
+popMin⇒deleteMin = P.cong (Maybe.map proj₂)
+
+popMin′ : ∀ q → .(¬Empty q) → A × Queue
+popMin′ q q≢∅ with popMin q
+... | nothing = Irrelevant.⊥-elim (q≢∅ P.refl)
+... | just p = p
+
+findMin′ : ∀ q → .(¬Empty q) → A
+findMin′ q q≢∅ = proj₁ (popMin′ q q≢∅)
+
+deleteMin′ : ∀ q → .(¬Empty q) → Queue
+deleteMin′ q q≢∅ = proj₂ (popMin′ q q≢∅)
+
+Empty-empty : Empty empty
+Empty-empty = size≡0⇒Empty empty size-empty
+
+toListAux-irrelevant : ∀ q (rec₁ rec₂ : Acc _≺_ q) → toListAux q rec₁ ≡ toListAux q rec₂
+toListAux-irrelevant q (acc rs₁) (acc rs₂) with popMin q
+... | nothing = P.refl
+... | just (x , q') = P.cong (x ∷_) (toListAux-irrelevant q' (rs₁ q' P.refl) (rs₂ q' P.refl))
+
+toListAux-length : ∀ q (@0 rec : Acc _≺_ q) → length (toListAux q rec) ≡ size q
+toListAux-length q (acc rs) with popMin q in eq
+... | nothing = P.sym (Empty⇒size≡0 q eq)
+... | just (x , q') = begin
+  1 + length (toListAux q' (rs q' P.refl)) ≡⟨ P.cong suc (toListAux-length q' (rs q' P.refl)) ⟩
+  1 + size q'                              ≡˘⟨ ≺-size q q' (popMin⇒deleteMin eq) ⟩
+  size q                                   ∎
+  where open P.≡-Reasoning
+
+toList-length : ∀ q → length (toList q) ≡ size q
+toList-length q = toListAux-length q (≺-wellFounded q)
+
+toListAux-Empty : ∀ q (@0 rec : Acc _≺_ q) → Empty q → toListAux q rec ≡ []
+toListAux-Empty q (acc rs) q≡∅ with popMin q
+toListAux-Empty q (acc rs) refl   | nothing = P.refl
+
+toList-Empty : ∀ q → Empty q → toList q ≡ []
+toList-Empty q = toListAux-Empty q (≺-wellFounded q)
+
+toList-empty : toList empty ≡ []
+toList-empty = toList-Empty empty (Empty-empty)
+
+toList-unfold : ∀ q x q' → PopMin q x q' → toList q ≡ x ∷ toList q'
+toList-unfold q x q' p    with ≺-wellFounded q
+toList-unfold q x q' p    | acc rs with popMin q in eq
+toList-unfold q x q' refl | acc rs | just (x , q') =
+  P.cong (x ∷_) (toListAux-irrelevant q' rec₁ rec₂)
+  where
+    rec₁ = rs q' P.refl
+    rec₂ = ≺-wellFounded q'