From 848cdb72dcbe4d23214b86237b3d5ba207f98a56 Mon Sep 17 00:00:00 2001
From: Sergei Winitzki <winitzki@gmail.com>
Date: Sat, 2 Nov 2024 16:15:28 +0100
Subject: [PATCH] singleton types

---
 tutorial/programming_dhall.md | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/tutorial/programming_dhall.md b/tutorial/programming_dhall.md
index d7fa9a8a..f09d476d 100644
--- a/tutorial/programming_dhall.md
+++ b/tutorial/programming_dhall.md
@@ -5254,7 +5254,7 @@ This code defines a type `Text_abc` and a value `x` of that type:
 ```dhall
 let Text_equals_abc = λ(text : Text) → (text === "abc")
 let Text_abc : Type = DependentPair Text Text_equals_abc
-let x : Text_abc = makeDependentPair Text "abc" Text_equals_abc (assert : "abc === "abc")
+let x : Text_abc = makeDependentPair Text "abc" Text_equals_abc (assert : "abc" === "abc")
 ```
 We can then extract the `Text`-valued part of `x` and verify that it is equal to the string `"abc"`:
 
@@ -5264,15 +5264,15 @@ let _ = assert : dependentPairFirstValue Text Text_equals_abc x === "abc"
 
 We can generalize this code to define a (dependent) type constructor for singleton types that are limited to a given `Text` value:
 ```dhall
-let TextSigletonPredicate = λ(fixed : Text) → λ(text : Text) → (text === fixed)
+let TextSingletonPredicate = λ(fixed : Text) → λ(text : Text) → (text === fixed)
 let TextSingleton : Text → Type
-  = λ(fixed : Text) → DependentPair Text (TextSigletonPredicate fixed)
+  = λ(fixed : Text) → DependentPair Text (TextSingletonPredicate fixed)
 let makeTextSingleton : ∀(fixed : Text) → TextSingleton fixed
-  = λ(fixed : Text) → makeDependentPair Text fixed (TestSingletonPredicate fixed) (assert : fixed === fixed)
+  = λ(fixed : Text) → makeDependentPair Text fixed (TextSingletonPredicate fixed) (assert : fixed === fixed)
 let x : TextSingleton "abc" = makeTextSingleton "abc"
 -- let x : TextSingleton "abc" = makeTextSingleton "def"  -- This will fail!
-let x : TextSingleton "abc" = makeDependentPair Text "abc" (TextSigletonPredicate "abc") (assert : "abc" === "abc")
-let _ = assert : dependentPairFirstValue Text (TextSigletonPredicate "abc") x === "abc"
+let x : TextSingleton "abc" = makeDependentPair Text "abc" (TextSingletonPredicate "abc") (assert : "abc" === "abc")
+let _ = assert : dependentPairFirstValue Text (TextSingletonPredicate "abc") x === "abc"
 ```
 
 The repetition in this code can be reduced by using Dhall's built-in function `Text/replace`. -- Is this necessary?