diff --git a/src/Data/Queue.agda b/src/Data/Queue.agda
new file mode 100644
index 0000000000..cd50200bbc
--- /dev/null
+++ b/src/Data/Queue.agda
@@ -0,0 +1,11 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Queues
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Queue where
+
+open import Data.Queue.TwoList.Base public
diff --git a/src/Data/Queue/QueueSpec.agda b/src/Data/Queue/QueueSpec.agda
new file mode 100644
index 0000000000..507c1ce28b
--- /dev/null
+++ b/src/Data/Queue/QueueSpec.agda
@@ -0,0 +1,84 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Queue specification
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Queue.QueueSpec where
+
+open import Data.Bool.Base using (Bool)
+open import Data.List.Base as List using (List; []; length; _∷_)
+open import Data.List.Relation.Unary.All using (Null)
+open import Data.Maybe.Base using (Maybe; nothing; just)
+open import Data.Nat.Base using (ℕ)
+open import Data.Product.Base using (_×_; proj₁; proj₂)
+open import Function.Base using (_∘_)
+open import Level
+open import Relation.Binary.Core using (Rel; _=[_]⇒_)
+open import Relation.Binary.Definitions using (_Respects_)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Nullary.Decidable.Core using (yes; no; isYes; False; does)
+open import Relation.Unary using (Pred; Decidable)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+-- RawQueue defines the 'computations' available on Queues
+-- without any of the associated proofs that determine its
+-- correctness.
+record RawQueue (Q : Set a → Set a) : Set (suc a) where
+
+  field
+    _≈_      : ∀ {A : Set a} → Rel (Q A) a
+    Empty    : ∀ {A : Set a} → Pred (Q A) a
+    empty?   : Decidable (Empty {A = A})
+    fromList : List A → Q A
+    toList   : Q A → List A
+    enqueue  : A → Q A → Q A
+    dequeue  : (q : Q A) → .{{False (empty? q)}} → A × Q A
+
+  empty : Q A
+  empty = fromList []
+
+  pure    : A → Q A
+  pure = fromList ∘ List.[_]
+
+  size : Q A → ℕ
+  size = length ∘ toList
+
+  to𝔹 : Q A → Bool
+  to𝔹 = isYes ∘ empty?
+
+  dequeue′ : Q A → Maybe (A × Q A)
+  dequeue′ q with empty? q in eq
+  ... | yes _ = nothing
+  ... | no _  = just (dequeue q)
+    where instance
+    _ : False (empty? q)
+    _ rewrite eq = _
+
+-- IsQueue bundles RawQueue with proofs of a Queues correctness,
+-- such as enqueue adding 1 to the Queue's size
+-- NOTE: not finished adding everything!
+record IsQueue {Q : Set a → Set a} (rawQ : RawQueue Q) : Set (suc a) where
+
+  open RawQueue rawQ
+
+  field
+    isEquivalence   : IsEquivalence (_≈_ {A = A})
+    ≈-resp-Empty    : Empty Respects (_≈_ {A = A})
+    ≈-=[toList]⇒-≡  : (_≈_ {A = A}) =[ toList ]⇒ _≡_
+    empty-toList    : ∀ {q : Q A} → Empty q → Null (toList q)
+    empty-fromList  : ∀ {xs : List A} → Null {A = A} xs → Empty (fromList xs)
+    toList-fromList : ∀ {q : Q A} {xs : List A} → q ≈ fromList xs → toList q ≡ xs
+    fromList-toList : ∀ {q : Q A} {xs : List A} → xs ≡ toList q → fromList xs ≈ q
+    toList-enqueue  : ∀ {q : Q A} {x : A} → toList (enqueue x q) ≡ toList q List.∷ʳ x
+    -- for some reason, let x , r = ... doesn't bind x and r??
+    toList-dequeue  : ∀ {q : Q A} → .{{i : False (empty? q)}} →
+                      let xr = dequeue q {{i}} in toList q ≡ proj₁ xr ∷ toList (proj₂ xr)
diff --git a/src/Data/Queue/TwoList/Base.agda b/src/Data/Queue/TwoList/Base.agda
new file mode 100644
index 0000000000..e17df82b21
--- /dev/null
+++ b/src/Data/Queue/TwoList/Base.agda
@@ -0,0 +1,155 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Queues, basic types and operations
+------------------------------------------------------------------------
+{-# OPTIONS --without-K --safe #-}
+
+-- Queues implemented with the two-list method described in
+-- "Purely Functional Data Structures", Chris Okasaki, 1996
+--
+-- Note that the weaker invariant is used here that only guarantees
+-- amortized O(1) when the structure is used non-persistently.
+
+module Data.Queue.TwoList.Base where
+
+open import Level using (Level)
+open import Data.Bool.Base using (Bool; true; false)
+open import Data.Empty using (⊥-elim)
+open import Data.List.Base as List using (List; []; _∷_; reverse; _++_; length; null)
+open import Data.List.Relation.Unary.All using (Null; []; _∷_)
+open import Data.List.Relation.Unary.All.Properties using (null⇒Null; Null⇒null)
+open import Data.Maybe.Base using (Maybe; nothing; just)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Product using (_×_; _,_; proj₂)
+open import Data.Queue.QueueSpec using (RawQueue; IsQueue)
+open import Data.SnocList.Base as SnocList using (List<; toList>; fromList>; []; _<:_)
+open import Data.SnocList.Relation.Unary.All
+open import Data.Unit.Base using (⊤)
+open import Function.Base using (id; const; _∘_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Decidable.Core using (yes; no; isYes; False)
+open import Relation.Nullary.Reflects using (ofʸ; ofⁿ)
+open import Relation.Unary using (Pred; Decidable)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+  ¬null : {a : A} {as : List A} → ¬ (Null (a ∷ as))
+  ¬null (() Data.List.Relation.Unary.All.∷ n)
+
+  ¬null< : {a : A} {as : List< A} → ¬ (Null< (as <: a))
+  ¬null< (() Data.SnocList.Relation.Unary.All.<: n)
+
+  null-[] : ∀ {xs : List A} → Null xs → Null {A = A} []
+  null-[] = const []
+
+  null<-[] : ∀ {xs : List< A} → Null< xs → Null {A = A} []
+  null<-[] = const []
+
+  null-∷ : ∀ {x} {xs ys : List A} → Null (x ∷ xs) → Null ys
+  null-∷ (()∷ _)
+
+  null-<: : ∀ {x} {xs : List< A} {ys : List A} → Null< (xs <: x) → Null ys
+  null-<: (()<: _)
+
+-- A Queue consists of a front (dequeue) and back (enqueue) list
+-- When enqueing (unless it is the first element), elements are cons'd
+-- to the enqueue list.
+--
+-- When dequeuing, elements are taken from the head of the dequeue
+-- list. If this is empty, the enqueue list is reversed and swapped
+-- with the dequeue list.
+--
+-- The dequeue-list should be empty iff the whole queue is empty.
+
+record Queue (A : Set a) : Set a where
+  constructor mkQ
+  field
+    front : List< A
+    back  : List A
+    inv : Null< front → Null back
+
+------------------------------------------------------------------------
+--- Basic Functions/Relations/Operators
+
+Empty    : ∀ {A : Set a} → Pred (Queue A) a
+Empty {a} {A} q = Null< (Queue.front q)
+
+empty? : Decidable (Empty {A = A})
+empty? (mkQ front back inv) .Relation.Nullary.does = SnocList.null front
+empty? (mkQ [] back inv) .Relation.Nullary.proof = ofʸ []
+empty? (mkQ (xs <: x) back inv) .Relation.Nullary.proof = ofⁿ (λ e → ⊥-elim (¬null< e))
+
+isEmpty : Queue A → Bool
+isEmpty q = SnocList.null (Queue.front q)
+
+------------------------------------------------------------------------
+--- Smart Constructor
+
+queue : List< A → List A → Queue A
+queue []          ys = mkQ (fromList> (reverse ys)) [] null<-[]
+queue xs@(_ <: _) ys = mkQ xs ys null-<:
+
+------------------------------------------------------------------------
+--- Conversion to/from List
+
+-- Create a List from a Queue, such that the last that would be dequeued
+-- becomes the head of the list
+toList : Queue A → List A
+toList q = (Queue.back q) ++ (toList> (Queue.front q))
+
+-- Create a Queue from a List, such that the elements
+-- of the list would be dequeued starting from its last element
+fromList : List A → Queue A
+fromList xs = queue (fromList> xs) []
+
+------------------------------------------------------------------------
+-- Construction & Destruction
+
+empty : Queue A
+empty = fromList []
+
+enqueue : A → Queue A → Queue A
+enqueue x q with bs ← Queue.back q | Queue.front q
+... | []            = queue ([] <: x) []
+... | front@(_ <: _) = queue front (x ∷ bs)
+
+dequeue : ∀ (q : Queue A) .{{_ : False (empty? q)}} → A × Queue A
+dequeue (mkQ (xs <: x) back _) = x , queue xs back
+
+-- Create a queue with a single element
+singleton : A → Queue A
+singleton = fromList ∘ List.[_]
+
+-- map : (A → B) → Queue A → Queue B
+-- map f empty = empty
+-- map f (queue x xs ys) = queue (f x) (List.map f xs) (List.map f ys)
+
+------------------------------------------------------------------------
+-- Relations
+
+-- Under the property that toList returns a list in
+-- the order of dequeue
+_≈_ : ∀ {A : Set a} → Rel (Queue A) a
+q ≈ q' = (toList q) ≡ (toList q')
+
+------------------------------------------------------------------------
+--- TwoList Queue is a Queue
+
+instance
+  TwoList-RawQueue : RawQueue {a} Queue
+  TwoList-RawQueue = record
+    { _≈_      = _≈_
+    ; Empty    = Empty
+    ; empty?   = empty?
+    ; fromList = fromList
+    ; toList   = toList
+    ; enqueue  = enqueue
+    ; dequeue  = dequeue
+    }
diff --git a/src/Data/Queue/TwoList/Properties.agda b/src/Data/Queue/TwoList/Properties.agda
new file mode 100644
index 0000000000..78a2ba6074
--- /dev/null
+++ b/src/Data/Queue/TwoList/Properties.agda
@@ -0,0 +1,190 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Queue-related properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Queue.TwoList.Properties where
+
+open import Level using (Level)
+open import Data.Empty using (⊥-elim)
+open import Data.List.Base
+open import Data.List.Properties using (++-identityʳ; length-++; length-reverse)
+open import Data.List.Relation.Unary.All using (Null; [])
+open import Data.Nat.Base using (suc; _+_)
+open import Data.Nat.Properties using (+-comm; +-suc; +-assoc)
+open import Data.Queue.QueueSpec using (RawQueue; IsQueue)
+open import Data.Queue.TwoList.Base
+open import Data.SnocList.Base as SnocList using (List<; []; _<:_; toList>; fromList>)
+open import Data.SnocList.Properties using (toList>-fromList>)
+open import Data.SnocList.Relation.Unary.All using (All<; Null<; []; _<:_)
+open import Function.Base using (_∘_)
+open import Relation.Binary.PropositionalEquality.Core as ≡
+open import Relation.Binary.PropositionalEquality.Properties as ≡
+open import Relation.Binary.Definitions using (Reflexive; _Respects_)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Nullary using (¬_)
+
+open ≡-Reasoning
+open RawQueue {{...}} using (size)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+  ¬Null : {x : A} {xs : List A} → ¬ Null (x ∷ xs)
+  ¬Null (() Data.List.Relation.Unary.All.∷ n)
+
+  null-<: : ∀ {x} {xs : List< A} {ys : List A} → Null< (xs <: x) → Null ys
+  null-<: (()<: _)
+
+  queue-back[] : ∀ {xs : List< A} → (Queue.back (queue xs [])) ≡ []
+  queue-back[] {xs = []} = refl
+  queue-back[] {xs = xs <: x} = refl
+
+  queue-front : ∀ {xs : List< A} → (Queue.front (queue xs [])) ≡ xs
+  queue-front {xs = []} = refl
+  queue-front {xs = xs <: x} = refl
+
+toList-fromList : ∀ {q : Queue A} {xs : List A} → q ≈ fromList xs → toList q ≡ xs
+toList-fromList {q = q} {xs = xs} q≈xs = begin
+  toList q             ≡⟨ q≈xs ⟩
+  toList (fromList xs) ≡⟨ toList-fromList' xs ⟩
+  xs                   ∎
+  where
+    -- TODO: can probably cleanup a little
+    toList-fromList' : ∀ (xs : List A) → toList (fromList xs) ≡ xs
+    toList-fromList' xs = begin
+      toList (fromList xs)                                     ≡⟨⟩
+      toList (queue (fromList> xs) [])                         ≡⟨ cong₂ _++_ (queue-back[] {xs = fromList> xs}) refl ⟩
+      [] ++ (toList> (Queue.front (queue (fromList> xs) [])))  ≡⟨⟩
+      toList> (Queue.front (queue (fromList> xs) []))          ≡⟨ cong toList> (queue-front {xs = fromList> xs}) ⟩
+      toList> (fromList> xs)                                   ≡⟨ toList>-fromList> xs ⟩
+      xs                                                       ∎
+
+-- enqueue increases size by 1
+-- rewrite could make it cleaner, but are we trying to use that less?
+size-enqueue : (x : A) (q : Queue A) → size (enqueue {a} x q) ≡ suc (size q)
+size-enqueue {a = a} {A = A} x q@(mkQ [] back inv) = begin
+  size (queue ([] <: x) []) ≡⟨⟩
+  length (x ∷ [])           ≡⟨⟩
+  suc 0                     ≡⟨ cong suc (sym sizeq) ⟩
+  suc (size q)              ∎
+  where
+    null[] : Null back → back ≡ []
+    null[] [] = refl
+
+    back[] : back ≡ []
+    back[] = null[] (inv [])
+
+    -- why does length need {a} and {A} after back ↦ []?
+    sizeq : size q ≡ 0
+    sizeq = begin
+      size q              ≡⟨⟩
+      length (toList q)   ≡⟨⟩
+      length (back ++ []) ≡⟨ cong length (++-identityʳ back) ⟩
+      length back         ≡⟨ cong length back[] ⟩
+      length {a} {A} []   ≡⟨⟩
+      0 ∎
+
+size-enqueue {A = A} x q@(mkQ front@(_ <: _) back inv) = begin
+  size (queue front (x ∷ back))              ≡⟨⟩
+  length (x ∷ back ++ toList> front)         ≡⟨ length-++ (x ∷ back) ⟩
+  length (x ∷ back) + length (toList> front) ≡⟨⟩
+  suc (length back) + length (toList> front) ≡⟨ +-comm (suc (length back)) (length (toList> front)) ⟩
+  length (toList> front) + suc (length back) ≡⟨ +-suc (length (toList> front)) (length back)⟩
+  suc (length (toList> front) + length back) ≡⟨ cong suc (+-comm (length (toList> front)) (length back)) ⟩
+  suc (length back + length (toList> front)) ≡⟨ cong suc (sym (length-++ back {toList> front})) ⟩
+  suc (length (back ++ (toList> front)))     ≡⟨⟩
+  suc (length (toList q))                    ≡⟨⟩
+  suc (size q)                               ∎
+
+-- trivial, but ensures empty works correctly
+size-empty : size (empty {a} {A}) ≡ 0
+size-empty = refl
+
+------------------------------------------------------------------------
+-- Properties of _≈_
+
+-- it becomes propositional equality on lists, so easy!
+≈-isEquivalence : IsEquivalence (_≈_ {A = A})
+≈-isEquivalence = record
+  { refl = refl
+  ; sym = sym
+  ; trans = trans
+  }
+
+-- NOTE: *most* of these:
+--        A) Can be moved elsewhere (e.g. the null proofs that are repeated in TwoList.Base, etc...)
+--        B) Should be renamed
+private
+  toList-Empty : ∀ {x : Queue A} → Empty x → toList x ≡ []
+  toList-Empty {x = x@(mkQ [] back inv)} [] = begin
+    toList (mkQ [] back inv)  ≡⟨⟩
+    back ++ [] ≡⟨ ++-identityʳ back ⟩
+    back ≡⟨ back[] ⟩
+    [] ∎
+    where
+      null[] : Null back → back ≡ []
+      null[] [] = refl
+
+      back[] : back ≡ []
+      back[] = null[] (inv [])
+
+  ++-[] : ∀ {xs ys : List A} → (xs ++ ys) ≡ [] → ys ≡ []
+  ++-[] {xs = []} {ys = []} xs++ys≡[] = xs++ys≡[]
+
+  ¬null< : {a : A} {as : List< A} → ¬ (Null< (as <: a))
+  ¬null< (() Data.SnocList.Relation.Unary.All.<: n)
+
+  null[] : ∀ {xs : List< A} → xs ≡ [] → Null< xs
+  null[] xs≡[] rewrite xs≡[] = []
+
+  ¬<>>[] : ∀ {x} {xs : List< A} {ys : List A} → xs SnocList.<>> (x ∷ ys) ≢ []
+  ¬<>>[] {xs = []} ()
+  ¬<>>[] {xs = xs <: x} wrong = ¬<>>[] {xs = xs} wrong
+
+  <>>[] : ∀ {xs : List< A} → xs SnocList.<>> [] ≡ [] → xs ≡ []
+  <>>[] {xs = []} xs<>>[]≡[] = refl
+  <>>[] {xs = (xs <: x)} xs<>>[]≡[] = ⊥-elim (¬<>>[] {x = x} {xs = xs} {ys = []} xs<>>[]≡[])
+
+  toList-front : ∀ {xs : Queue A} → toList xs ≡ [] → Queue.front xs ≡ []
+  toList-front {xs = xs@(mkQ front [] inv)} xs≡[] = <>>[] xs≡[]
+
+  empty[] : ∀ {xs : Queue A} → toList xs ≡ [] → Empty xs
+  empty[] {xs = xs} xs≡[] = null[] (toList-front {xs = xs} xs≡[])
+
+≈-resp-Empty : Empty Respects (_≈_ {A = A})
+≈-resp-Empty {x = x} {y = y} x≈y empty-x = empty[] {xs = y} (begin
+  toList y ≡⟨ sym x≈y ⟩
+  toList x ≡⟨ toList-Empty {x = x} empty-x ⟩
+  []       ∎
+  )
+
+-- For some reason, gives unresolved implicits of
+--  _x.inv_750 : Null< (Queue.front x) → Null (Queue.back x)
+--  _y.inv_753 : Null< (Queue.front y) → Null (Queue.back y)
+-- But I'm too tired to trace it through and figure out why for today!
+-- ≈-resp-Empty' : Empty Respects (_≈_ {A = A})
+-- ≈-resp-Empty' = ≈-resp-Empty
+
+------------------------------------------------------------------------
+-- TwoList Queue is a Queue!
+
+-- instance
+--   TwoList-IsQueue : IsQueue {a} TwoList-RawQueue
+--   TwoList-IsQueue = record
+--     { isEquivalence = ≈-isEquivalence
+--     ; ≈-resp-Empty = ≈-resp-Empty
+--     ; ≈-=[toList]⇒-≡ = {!!}
+--     ; empty-toList = {!!}
+--     ; empty-fromList = {!!}
+--     ; toList-fromList = {!!}
+--     ; fromList-toList = {!!}
+--     ; toList-enqueue = {!!}
+--     ; toList-dequeue = {!!}
+--     }
diff --git a/src/Data/SnocList/Properties.agda b/src/Data/SnocList/Properties.agda
new file mode 100644
index 0000000000..e89db2bb65
--- /dev/null
+++ b/src/Data/SnocList/Properties.agda
@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- SnocList properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.SnocList.Properties where
+
+open import Data.SnocList.Base
+open import Relation.Binary.PropositionalEquality.Core as ≡
+open import Relation.Binary.PropositionalEquality.Properties as ≡
+open import Level using (Level)
+
+open ≡-Reasoning
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+-- Yummy! Best gotten from Penarth Pier :-)
+fish-and-chips : ∀ (xs : List> A) (sx : List< A) (ys : List> A) →
+                   (sx <>< xs) <>> ys ≡ sx <>> ( ([] <>< xs) <>> ys )
+fish-and-chips []        sx ys = refl
+fish-and-chips xs'@(x :> xs) sx ys = begin
+  (sx <>< (x :> xs)) <>> ys                   ≡⟨⟩
+  ((sx <: x) <>< xs) <>> ys                   ≡⟨ fish-and-chips xs (sx <: x) ys ⟩
+  (sx <: x) <>> (([] <>< xs) <>> ys)          ≡⟨⟩
+  sx <>> (x :> (([] <>< xs) <>> ys))          ≡⟨⟩
+  sx <>> (([] <: x) <>> (([] <>< xs) <>> ys)) ≡⟨ sym (cong (λ hole → sx <>> hole) (fish-and-chips xs ([] <: x) ys)) ⟩
+  sx <>> ((([] <: x) <>< xs) <>> ys)          ≡⟨⟩
+  sx <>> (([] <>< (x :> xs)) <>> ys)          ∎
+
+toList>-fromList> : ∀ (xs : List> A) → toList> (fromList> xs) ≡ xs
+toList>-fromList> [] = refl
+toList>-fromList> (x :> xs) = begin
+  toList> (fromList> (x :> xs))        ≡⟨⟩
+  (([] <: x) <>< xs) <>> []            ≡⟨ fish-and-chips xs ([] <: x) [] ⟩
+  ([] <: x) <>> (([] <>< xs) <>> [])   ≡⟨⟩
+  [] <>> (x :> (([] <>< xs) <>> []))   ≡⟨⟩
+  [] <>> (x :> toList> (fromList> xs)) ≡⟨ cong (λ e → [] <>> (x :> e)) (toList>-fromList> xs) ⟩
+  [] <>> (x :> xs)                     ≡⟨⟩
+  x :> xs                              ∎
diff --git a/src/Data/SnocList/Relation/Unary/All.agda b/src/Data/SnocList/Relation/Unary/All.agda
new file mode 100644
index 0000000000..7f36e3a3cd
--- /dev/null
+++ b/src/Data/SnocList/Relation/Unary/All.agda
@@ -0,0 +1,39 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- SnocLists where all elements satisfy a given property
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.SnocList.Relation.Unary.All where
+
+open import Data.SnocList.Base
+open import Relation.Unary using (Pred; ∅)
+open import Level using (Level; suc; _⊔_)
+
+private
+  variable
+    a b p q r ℓ : Level
+    A : Set a
+    B : Set b
+    P Q R : Pred A p
+    x : A
+    xs : List< A
+
+------------------------------------------------------------------------
+-- Definitions
+
+-- Given a predicate P, then All P xs means that every element in xs
+-- satisfies P. See `Relation.Unary` for an explanation of predicates.
+--
+-- Equivalent to the definition on List>, but now for List<
+
+infixr 5 _<:_
+
+data All< {A : Set a} (P : Pred A p) : Pred (List< A) (a ⊔ p) where
+  []  : All< P []
+  _<:_ : ∀ {x xs} (px : P x) (pxs : All< P xs) → All< P (xs <: x)
+
+Null< : Pred (List< A) _
+Null< = All< ∅