diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean
index 1cecbcf..b37dd43 100644
--- a/Bookshelf/Enderton/Set/Chapter_2.lean
+++ b/Bookshelf/Enderton/Set/Chapter_2.lean
@@ -91,7 +91,7 @@ theorem exercise_3_3 {A : Set (Set α)}
 
 Show that if `A ⊆ B`, then `⋃ A ⊆ ⋃ B`.
 -/
-theorem exercise_3_4 (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B := by
+theorem exercise_3_4 {A B : Set (Set α)} (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B := by
   show ∀ x ∈ { a | ∃ t, t ∈ A ∧ a ∈ t }, x ∈ { a | ∃ t, t ∈ B ∧ a ∈ t }
   intro x hx
   rw [Set.mem_setOf_eq] at hx
@@ -103,7 +103,8 @@ theorem exercise_3_4 (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B := by
 
 Assume that every member of `𝓐` is a subset of `B`. Show that `⋃ 𝓐 ⊆ B`.
 -/
-theorem exercise_3_5 (h : ∀ x ∈ 𝓐, x ⊆ B) : ⋃₀ 𝓐 ⊆ B := by
+theorem exercise_3_5 {𝓐 : Set (Set α)} (h : ∀ x ∈ 𝓐, x ⊆ B)
+  : ⋃₀ 𝓐 ⊆ B := by
   show ∀ y ∈ { a | ∃ t, t ∈ 𝓐 ∧ a ∈ t }, y ∈ B
   intro y hy
   rw [Set.mem_setOf_eq] at hy
@@ -267,7 +268,7 @@ theorem exercise_3_9 (ha : a = {1}) (hB : B = {{1}})
 
 Show that if `a ∈ B`, then `𝓟 a ∈ 𝓟 𝓟 ⋃ B`.
 -/
-theorem exercise_3_10 (ha : a ∈ B)
+theorem exercise_3_10 {B : Set (Set α)} (ha : a ∈ B)
   : 𝒫 a ∈ 𝒫 (𝒫 (⋃₀ B)) := by
   have h₁ := exercise_3_3 a ha
   have h₂ := Chapter_1.exercise_1_3 h₁
diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean
index e7d4e74..06adea4 100644
--- a/Bookshelf/Enderton/Set/Chapter_3.lean
+++ b/Bookshelf/Enderton/Set/Chapter_3.lean
@@ -115,14 +115,4 @@ theorem exercise_5_3 {A : Set (Set α)} {𝓑 : Set (Set β)}
       · intro ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩
         exact ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩
 
-/-- ### Exercise 5.5b
-
-With `A`, `B`, and `C` as above, show that `A × B = ⋃ C`.
--/
-theorem exercise_5_5b {A : Set α} {B : Set β}
-  : Set.prod A B = ⋃₀ {Set.prod {x} B | x ∈ A} := by
-  -- TODO: `Set.OrderedPair` should allow two different types.
-  -- TODO: We can cast `(α × β)` up into type `Set (Set (α ⊕ β))`.
-  sorry
-
 end Enderton.Set.Chapter_3
\ No newline at end of file
diff --git a/Common/Set/OrderedPair.lean b/Common/Set/OrderedPair.lean
index 2978cb7..497b184 100644
--- a/Common/Set/OrderedPair.lean
+++ b/Common/Set/OrderedPair.lean
@@ -7,11 +7,16 @@ namespace Set
 
 /--
 Kazimierz Kuratowski's definition of an ordered pair.
+
+Like `Set`, this is a homogeneous structure.
 -/
 def OrderedPair (x y : α) : Set (Set α) := {{x}, {x, y}}
 
 namespace OrderedPair
 
+/--
+For any sets `x`, `y`, `u`, and `v`, `⟨u, v⟩ = ⟨x, y⟩` **iff** `u = x ∧ v = y`.
+-/
 theorem ext_iff
   : (OrderedPair x y = OrderedPair u v) ↔ (x = u ∧ y = v) := by
   unfold OrderedPair