diff --git a/book/String.cmp.kind2 b/book/String.cmp.kind2
new file mode 100644
index 00000000..1f33e9d3
--- /dev/null
+++ b/book/String.cmp.kind2
@@ -0,0 +1,22 @@
+String.cmp
+: ∀(a: String)
+  ∀(b: String)
+  Cmp
+= λa λb
+  let P    = λx ∀(b: String) (Cmp)
+  let cons = λa.head λa.tail λb
+    let P    = λx ∀(a.head: Char) ∀(a.tail: String) (Cmp)
+    let cons = λb.head λb.tail λa.head λa.tail
+      let P = λx Cmp
+      let ltn = Cmp.ltn
+      let eql = (String.cmp a.tail b.tail)
+      let gtn = Cmp.gtn
+      (~(U60.cmp a.head b.head) P ltn eql gtn)
+    let nil  = λa.head λa.tail Cmp.gtn
+    ((~b P cons nil) a.head a.tail)
+  let nil  = λb
+    let P    = λx Cmp
+    let cons = λb.head λb.tail Cmp.ltn
+    let nil  = Cmp.eql
+    (~b P cons nil)
+  (~a P cons nil b)
\ No newline at end of file
diff --git a/book/U60.cmp.kind2 b/book/U60.cmp.kind2
new file mode 100644
index 00000000..530f233f
--- /dev/null
+++ b/book/U60.cmp.kind2
@@ -0,0 +1,7 @@
+U60.cmp
+: ∀(a: #U60)
+  ∀(b: #U60)
+  (Cmp)
+= λa λb
+  (U60.if #(== a b) Cmp (U60.if #(< a b) Cmp Cmp.gtn Cmp.ltn) Cmp.eql)
+ 
\ No newline at end of file