diff --git a/CHANGES.md b/CHANGES.md
index 0ddb7de..3e7bc1e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -5,18 +5,23 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ## Unreleased
 
-- Declare istrue as injective
+- Add files for higher-order logic:
+  HOL: Set constructor ⤳ for quantifying over function types
+  Impred: Set constructor o for quantifying over propositions
+  Epsilon: Hilbert's ε operator
+- Set: add ι:Set
+- Bool: declare istrue as injective
 
 ## 1.1.0 (2024-06-21)
 
-- Add classical logic
-- Rename top into ⊤ᵢ
-- Declare more arguments of ∃ᵢ and ∃ₑ implicit
+- Classic: classical logic
+- Prop: rename top into ⊤ᵢ
+- FOL: declare more arguments of ∃ᵢ and ∃ₑ implicit
 
 ## 1.0.0 (2023-10-19)
 
-- Add integers (Quentin Garchery)
+- Z: integers (Quentin Garchery)
 
 ## 0.0.0 (2022-01-27)
 
-- Add natural numbers and lists (Quentin Buzet)
+- Nat, List: natural numbers and lists (Quentin Buzet)
diff --git a/Epsilon.lp b/Epsilon.lp
new file mode 100644
index 0000000..07bfd2d
--- /dev/null
+++ b/Epsilon.lp
@@ -0,0 +1,4 @@
+require open Stdlib.Set Stdlib.Prop Stdlib.FOL;
+
+symbol ε [a:Set] : (τ a → Prop) → τ a;
+symbol εᵢ [a:Set] (p:τ a → Prop) : π (∃ p) → π (p (ε p));
diff --git a/HOL.lp b/HOL.lp
new file mode 100644
index 0000000..8bb76f7
--- /dev/null
+++ b/HOL.lp
@@ -0,0 +1,7 @@
+require open Stdlib.Set;
+
+symbol ⤳ : Set → Set → Set; // \leadsto
+
+notation ⤳ infix right 20;
+
+rule τ ($x ⤳ $y) ↪ τ $x → τ $y;
diff --git a/Impred.lp b/Impred.lp
new file mode 100644
index 0000000..38b5eb3
--- /dev/null
+++ b/Impred.lp
@@ -0,0 +1,5 @@
+require open Stdlib.Set Stdlib.Prop;
+
+symbol o : Set;
+
+rule τ o ↪ Prop;
diff --git a/Set.lp b/Set.lp
index 16d3539..086e526 100644
--- a/Set.lp
+++ b/Set.lp
@@ -2,6 +2,8 @@
 
 constant symbol Set : TYPE;
 
+constant symbol ι : Set;
+
 // Interpretation of set codes in TYPE
 
 injective symbol τ : Set → TYPE; // `t or \tau