From 04fe6c66dbf5fe6f6dfda85e546466feb3622db9 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Fri, 7 Jul 2023 06:15:17 -0600
Subject: [PATCH] Enderton. Heterogeneous relations and additional exercises.

---
 Bookshelf/Enderton/Set.tex            |  68 +++-
 Bookshelf/Enderton/Set/Chapter_3.lean | 439 +++++++++++++++++++-------
 Bookshelf/Enderton/Set/Relation.lean  | 126 ++++----
 3 files changed, 438 insertions(+), 195 deletions(-)

diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index 262281e..2cfd8a8 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -4491,7 +4491,7 @@ Show that for any sets $B$ and $C$,
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.24}}%
+\subsection{\verified{Exercise 3.24}}%
 \label{sub:exercise-3.24}
 
 Show that for a function $F$,
@@ -4499,6 +4499,9 @@ Show that for a function $F$,
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Relation}
+    {Enderton.Set.Chapter\_3.exercise\_3\_24}
+
   Let $F$ be a function.
   By definition of the \nameref{ref:inverse} of a set,
     \begin{align*}
@@ -4506,13 +4509,13 @@ Show that for a function $F$,
         & = \{x \mid (\exists y \in A) yF^{-1}x\} \\
         & = \{x \mid (\exists y \in A) xFy\} \\
         & = \{x \mid (\exists y \in A) \left< x, y \right> \in F\} \\
-        & = \{x \mid \exists x \in F, F(x) \in A\} \\
+        & = \{x \mid x \in \dom{F} \land F(x) \in A\} \\
         & = \{x \in \dom{F} \mid F(x) \in A\}.
     \end{align*}
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.25}}%
+\subsection{\verified{Exercise 3.25}}%
 \label{sub:exercise-3.25}
 
 \begin{enumerate}[(a)]
@@ -4525,18 +4528,45 @@ Show that for a function $F$,
 
 \begin{proof}
 
+  \statementpadding
+
+  \lean*{Bookshelf/Enderton/Set/Relation}
+    {Enderton.Set.Chapter\_3.exercise\_3\_25\_b}
+
+  \lean{Bookshelf/Enderton/Set/Relation}
+    {Enderton.Set.Chapter\_3.exercise\_3\_25\_a}
+
   \paragraph{(b)}%
   \label{par:exercise-3.25-b}
 
-    Let $G$ be a function.
-    Let $\left< x, y \right> \in G \circ G^{-1}$.
-    By definition of the \nameref{ref:composition} of sets, there exists some
-      set $t$ such that $x(G^{-1})t$ and $tGy$.
-    By definition of the \nameref{ref:inverse} of a set,
-      $$x(G^{-1})t \iff tGx.$$
-    By hypothesis, $G$ is single-valued.
-    Thus $x = y$.
-    That is, $G \circ G^{-1}$ is the identity function on $\ran{G}$.
+    Let $G$ be an arbitrary function.
+    We show that $G \circ G^{-1} \subseteq I_{\ran{G}}$ and that
+      $I_{\ran{G}} \subseteq G \circ G^{-1}$.
+
+    \subparagraph{($\subseteq$)}%
+
+      Let $\left< x, y \right> \in G \circ G^{-1}$.
+      By definition of the \nameref{ref:composition} of sets, there exists some
+        set $t$ such that $x(G^{-1})t$ and $tGy$.
+      By definition of the \nameref{ref:inverse} of a set,
+        $$x(G^{-1})t \iff tGx.$$
+      The right hand side of the above biconditional indicates $x \in \ran{G}$.
+      Since $G$ is single-valued, $tGy \land tGx$ implies $x = y$.
+      Thus $\left< x, y \right> \in I_{\ran{G}}$.
+
+    \subparagraph{($\supseteq$)}%
+
+      Let $\left< x, x \right> \in I_{\ran{G}}$ where $x \in \ran{G}$.
+      By definition of the \nameref{ref:range} of a function, there exists some
+        $t$ such that $\left< t, x \right> \in G$.
+      By definition of the \nameref{ref:inverse} of a set, it follows
+        $\left< x, t \right> \in G^{-1}$.
+      Thus $\left< x, x \right> \in G \circ G^{-1}$.
+
+    \subparagraph{Conclusion}%
+
+      Since $G \circ G^{-1}$ is a subset of $I_{\ran{G}}$ and vice versa, it
+        follows that these two sets are equal.
 
   \paragraph{(a)}%
 
@@ -4544,7 +4574,7 @@ Show that for a function $F$,
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.26}}%
+\subsection{\verified{Exercise 3.26}}%
 \label{sub:exercise-3.26}
 
 Prove the second halves of parts (a) and (b) of Theorem 3K.
@@ -4556,7 +4586,7 @@ Prove the second halves of parts (a) and (b) of Theorem 3K.
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.27}}%
+\subsection{\verified{Exercise 3.27}}%
 \label{sub:exercise-3.27}
 
 Show that $\dom{(F \circ G)} = \img{G^{-1}}{\dom{F}}$ for any sets $F$ and $G$.
@@ -4564,6 +4594,9 @@ Show that $\dom{(F \circ G)} = \img{G^{-1}}{\dom{F}}$ for any sets $F$ and $G$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Relation}
+    {Enderton.Set.Chapter\_3.exercise\_3\_27}
+
   Let $F$ and $G$ be arbitrary sets.
   We show that each side of our desired equality is a subset of the other.
 
@@ -4597,7 +4630,7 @@ Show that $\dom{(F \circ G)} = \img{G^{-1}}{\dom{F}}$ for any sets $F$ and $G$.
 
 \end{proof}
 
-\subsection{\pending{Exercise 3.28}}%
+\subsection{\verified{Exercise 3.28}}%
 \label{sub:exercise-3.28}
 
 Assume that $f$ is a one-to-one function from $A$ into $B$, and that $G$ is the
@@ -4607,9 +4640,14 @@ Show that $G$ maps $\powerset{A}$ one-to-one into $\powerset{B}$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Relation}
+    {Enderton.Set.Chapter\_3.exercise\_3\_28}
+
   By construction, $\dom{G} = \powerset{A}$.
   Likewise, $\ran{G} \subseteq \powerset{B}$ by definition of the
     \nameref{ref:image} of sets.
+  Thus $G$ maps $\powerset{A}$ into $\powerset{B}$.
+
   Let $y \in \ran{G}$.
   Then there exists an $X_1 \in \powerset{A}$ such that $\img{f}{X_1} = y$.
   To prove $G$ is one-to-one into $\powerset{B}$, assume there exists an
diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean
index 150c60a..bfdc161 100644
--- a/Bookshelf/Enderton/Set/Chapter_3.lean
+++ b/Bookshelf/Enderton/Set/Chapter_3.lean
@@ -229,12 +229,16 @@ theorem theorem_3d {A : Set (Set (Set α))} (h : OrderedPair x y ∈ A)
   have : {x, y} ⊆ ⋃₀ ⋃₀ A := Chapter_2.exercise_2_3 {x, y} hq
   exact ⟨this (by simp), this (by simp)⟩
 
+section Relation
+
+open Set.Relation
+
 /-- #### Exercise 3.6
 
 Show that a set `A` is a relation **iff** `A ⊆ dom A × ran A`.
 -/
-theorem exercise_3_6 {A : Set.Relation α}
-  : A ⊆ Set.prod (A.dom) (A.ran) := by
+theorem exercise_3_6 {A : Set.HRelation α β}
+  : A ⊆ Set.prod (dom A) (ran A) := by
   show ∀ t, t ∈ A → t ∈ Set.prod (Prod.fst '' A) (Prod.snd '' A)
   intro (a, b) ht
   unfold Set.prod
@@ -301,8 +305,8 @@ theorem exercise_3_7 {R : Set.Relation α}
     -- `t = y` then `t ∈ ran R`.
     have hxy_mem : t = x ∨ t = y → t ∈ Set.Relation.fld R := by
       intro ht
-      have hz : R ⊆ Set.prod (R.dom) (R.ran) := exercise_3_6
-      have : (x, y) ∈ Set.prod (R.dom) (R.ran) := hz p
+      have hz : R ⊆ Set.prod (dom R) (ran R) := exercise_3_6
+      have : (x, y) ∈ Set.prod (dom R) (ran R) := hz p
       unfold Set.prod at this
       simp at this
       apply Or.elim ht
@@ -326,10 +330,6 @@ theorem exercise_3_7 {R : Set.Relation α}
       simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at this
       exact hxy_mem this
 
-section Relation
-
-open Set.Relation
-
 /-- #### Exercise 3.8 (i)
 
 Show that for any set `𝓐`:
@@ -337,7 +337,7 @@ Show that for any set `𝓐`:
 dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
 ```
 -/
-theorem exercise_3_8_i {A : Set (Set.Relation α)}
+theorem exercise_3_8_i {A : Set (Set.HRelation α β)}
   : dom (⋃₀ A) = ⋃₀ { dom R | R ∈ A } := by
   ext x
   unfold dom Prod.fst
@@ -363,7 +363,7 @@ Show that for any set `𝓐`:
 ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
 ```
 -/
-theorem exercise_3_8_ii {A : Set (Set.Relation α)}
+theorem exercise_3_8_ii {A : Set (Set.HRelation α β)}
   : ran (⋃₀ A) = ⋃₀ { ran R | R ∈ A } := by
   ext x
   unfold ran Prod.snd
@@ -389,7 +389,7 @@ operation in the preceding problem.
 dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
 ```
 -/
-theorem exercise_3_9_i {A : Set (Set.Relation α)}
+theorem exercise_3_9_i {A : Set (Set.HRelation α β)}
   : dom (⋂₀ A) ⊆ ⋂₀ { dom R | R ∈ A } := by
   show ∀ x, x ∈ dom (⋂₀ A) → x ∈ ⋂₀ { dom R | R ∈ A }
   unfold dom Prod.fst
@@ -415,7 +415,7 @@ operation in the preceding problem.
 ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
 ```
 -/
-theorem exercise_3_9_ii {A : Set (Set.Relation α)}
+theorem exercise_3_9_ii {A : Set (Set.HRelation α β)}
   : ran (⋂₀ A) ⊆ ⋂₀ { ran R | R ∈ A } := by
   show ∀ x, x ∈ ran (⋂₀ A) → x ∈ ⋂₀ { ran R | R ∈ A }
   unfold ran Prod.snd
@@ -437,9 +437,9 @@ theorem exercise_3_9_ii {A : Set (Set.Relation α)}
 
 Assume that `F` is a one-to-one function. If `x ∈ dom F`, then `F⁻¹(F(x)) = x`.
 -/
-theorem theorem_3g_i {F : Set.Relation α}
-  (hF : F.isOneToOne) (hx : x ∈ dom F)
-  : ∃! y, (x, y) ∈ F ∧ (y, x) ∈ F.inv := by
+theorem theorem_3g_i {F : Set.HRelation α β}
+  (hF : isOneToOne F) (hx : x ∈ dom F)
+  : ∃! y, (x, y) ∈ F ∧ (y, x) ∈ inv F := by
   simp only [mem_self_comm_mem_inv, and_self]
   have ⟨y, hy⟩ := dom_exists hx
   refine ⟨y, hy, ?_⟩
@@ -451,9 +451,9 @@ theorem theorem_3g_i {F : Set.Relation α}
 
 Assume that `F` is a one-to-one function. If `y ∈ ran F`, then `F(F⁻¹(y)) = y`.
 -/
-theorem theorem_3g_ii {F : Set.Relation α}
-  (hF : F.isOneToOne) (hy : y ∈ F.ran)
-  : ∃! x, (x, y) ∈ F ∧ (y, x) ∈ F.inv := by
+theorem theorem_3g_ii {F : Set.HRelation α β}
+  (hF : isOneToOne F) (hy : y ∈ ran F)
+  : ∃! x, (x, y) ∈ F ∧ (y, x) ∈ inv F := by
   simp only [mem_self_comm_mem_inv, and_self]
   have ⟨x, hx⟩ := ran_exists hy
   refine ⟨x, hx, ?_⟩
@@ -468,13 +468,13 @@ Assume that `F` and `G` are functions. Then
 dom (F ∘ G) = {x ∈ dom G | G(x) ∈ dom F}.
 ```
 -/
-theorem theorem_3h_dom {F G : Set.Relation α}
-  (_ : F.isSingleValued) (hG : G.isSingleValued)
-  : dom (F.comp G) = {x ∈ dom G | ∃! y, (x, y) ∈ G ∧ y ∈ dom F} := by
+theorem theorem_3h_dom {F : Set.HRelation β γ} {G : Set.HRelation α β}
+  (_ : isSingleValued F) (hG : isSingleValued G)
+  : dom (comp F G) = {x ∈ dom G | ∃! y, (x, y) ∈ G ∧ y ∈ dom F} := by
   let rhs := {x ∈ dom G | ∃! y, (x, y) ∈ G ∧ y ∈ dom F }
   rw [Set.Subset.antisymm_iff]
   apply And.intro
-  · show ∀ t, t ∈ dom (F.comp G) → t ∈ rhs
+  · show ∀ t, t ∈ dom (comp F G) → t ∈ rhs
     intro t ht
     simp only [Set.mem_setOf_eq]
     have ⟨z, hz⟩ := dom_exists ht
@@ -488,7 +488,7 @@ theorem theorem_3h_dom {F G : Set.Relation α}
     refine ⟨a, ⟨ha.left, z, ha.right⟩, ?_⟩
     intro y₁ hy₁
     exact fun _ _ => single_valued_eq_unique hG hy₁ ha.left
-  · show ∀ t, t ∈ rhs → t ∈ dom (F.comp G)
+  · show ∀ t, t ∈ rhs → t ∈ dom (comp F G)
     intro t ht
     simp only [Set.mem_setOf_eq] at ht
     unfold dom
@@ -507,15 +507,15 @@ Assume that `F : A → B`, and that `A` is nonempty. There exists a function
 `G : B → A` (a "left inverse") such that `G ∘ F` is the identity function on `A`
 **iff** `F` is one-to-one.
 -/
-theorem theorem_3j_a {F : Set.Relation α} {A B : Set α}
-  (hF : F.isSingleValued ∧ F.mapsInto A B) (hA : Set.Nonempty A)
-  : (∃ G : Set.Relation α,
-      G.isSingleValued ∧ G.mapsInto B A ∧
-        (∀ p ∈ G.comp F, p.1 = p.2)) ↔ F.isOneToOne := by
+theorem theorem_3j_a {F : Set.HRelation α β} {A : Set α} {B : Set β}
+  (hF : isSingleValued F ∧ mapsInto F A B) (hA : Set.Nonempty A)
+  : (∃ G : Set.HRelation β α,
+      isSingleValued G ∧ mapsInto G B A ∧
+        (∀ p ∈ comp G F, p.1 = p.2)) ↔ isOneToOne F := by
   apply Iff.intro
   · intro ⟨G, ⟨hG₁, hG₂, hI⟩⟩
     refine ⟨hF.left, ?_⟩
-    show F.isSingleRooted
+    show isSingleRooted F
     intro y hy
     have ⟨x, hx⟩ := ran_exists hy
     sorry
@@ -528,11 +528,11 @@ Assume that `F : A → B`, and that `A` is nonempty. There exists a function
 `H : B → A` (a "right inverse") such that `F ∘ H` is the identity function on
 `B` **iff** `F` maps `A` onto `B`.
 -/
-theorem theorem_3j_b {F : Set.Relation α} {A B : Set α}
-  (hF : F.isSingleValued ∧ F.mapsInto A B) (hA : Set.Nonempty A)
-  : (∃ H : Set.Relation α,
-      H.isSingleValued ∧ H.mapsInto B A ∧
-        (∀ p ∈ F.comp H, p.1 = p.2)) ↔ F.mapsOnto A B := by
+theorem theorem_3j_b {F : Set.HRelation α β} {A : Set α} {B : Set β}
+  (hF : isSingleValued F ∧ mapsInto F A B) (hA : Set.Nonempty A)
+  : (∃ H : Set.HRelation β α,
+      isSingleValued H ∧ mapsInto H B A ∧
+        (∀ p ∈ comp F H, p.1 = p.2)) ↔ mapsOnto F A B := by
   sorry
 
 /-- #### Theorem 3K (a)
@@ -543,11 +543,11 @@ The image of a union is the union of the images:
 F⟦⋃ 𝓐⟧ = ⋃ {F⟦A⟧ | A ∈ 𝓐}
 ```
 -/
-theorem theorem_3k_a {F : Set.Relation α} {𝓐 : Set (Set α)}
-  : F.image (⋃₀ 𝓐) = ⋃₀ { F.image A | A ∈ 𝓐 } := by
+theorem theorem_3k_a {F : Set.HRelation α β} {𝓐 : Set (Set α)}
+  : image F (⋃₀ 𝓐) = ⋃₀ { image F A | A ∈ 𝓐 } := by
   rw [Set.Subset.antisymm_iff]
   apply And.intro
-  · show ∀ v, v ∈ F.image (⋃₀ 𝓐) → v ∈ ⋃₀ { F.image A | A ∈ 𝓐 }
+  · show ∀ v, v ∈ image F (⋃₀ 𝓐) → v ∈ ⋃₀ { image F A | A ∈ 𝓐 }
     intro v hv
     unfold image at hv
     simp only [Set.mem_sUnion, Set.mem_setOf_eq] at hv
@@ -555,11 +555,11 @@ theorem theorem_3k_a {F : Set.Relation α} {𝓐 : Set (Set α)}
     have ⟨A, hA⟩ := hu.left
     simp only [Set.mem_sUnion, Set.mem_setOf_eq, exists_exists_and_eq_and]
     refine ⟨A, hA.left, ?_⟩
-    show v ∈ F.image A
+    show v ∈ image F A
     unfold image
     simp only [Set.mem_setOf_eq]
     exact ⟨u, hA.right, hu.right⟩
-  · show ∀ v, v ∈ ⋃₀ {x | ∃ A, A ∈ 𝓐 ∧ F.image A = x} → v ∈ F.image (⋃₀ 𝓐)
+  · show ∀ v, v ∈ ⋃₀ {x | ∃ A, A ∈ 𝓐 ∧ image F A = x} → v ∈ image F (⋃₀ 𝓐)
     intro v hv
     simp only [Set.mem_sUnion, Set.mem_setOf_eq, exists_exists_and_eq_and] at hv
     have ⟨A, hA⟩ := hv
@@ -580,9 +580,9 @@ F⟦⋂ 𝓐⟧ ⊆ ⋂ {F⟦A⟧ | A ∈ 𝓐}
 Equality holds if `F` is single-rooted.
 -/
 
-theorem theorem_3k_b_i {F : Set.Relation α} {𝓐 : Set (Set α)}
-  : F.image (⋂₀ 𝓐) ⊆ ⋂₀ { F.image A | A ∈ 𝓐} := by
-  show ∀ v, v ∈ F.image (⋂₀ 𝓐) → v ∈ ⋂₀ { F.image A | A ∈ 𝓐}
+theorem theorem_3k_b_i {F : Set.HRelation α β} {𝓐 : Set (Set α)}
+  : image F (⋂₀ 𝓐) ⊆ ⋂₀ { image F A | A ∈ 𝓐} := by
+  show ∀ v, v ∈ image F (⋂₀ 𝓐) → v ∈ ⋂₀ { image F A | A ∈ 𝓐}
   intro v hv
   unfold image at hv
   simp only [Set.mem_sInter, Set.mem_setOf_eq] at hv
@@ -599,9 +599,9 @@ theorem theorem_3k_b_i {F : Set.Relation α} {𝓐 : Set (Set α)}
   simp only [Set.mem_setOf_eq]
   exact ⟨u, hu.left A hA, hu.right⟩
 
-theorem theorem_3k_b_ii {F : Set.Relation α} {𝓐 : Set (Set α)}
-  (hF : F.isSingleRooted) (h𝓐 : Set.Nonempty 𝓐)
-  : F.image (⋂₀ 𝓐) = ⋂₀ { F.image A | A ∈ 𝓐} := by
+theorem theorem_3k_b_ii {F : Set.HRelation α β} {𝓐 : Set (Set α)}
+  (hF : isSingleRooted F) (h𝓐 : Set.Nonempty 𝓐)
+  : image F (⋂₀ 𝓐) = ⋂₀ { image F A | A ∈ 𝓐} := by
   rw [Set.Subset.antisymm_iff]
   refine ⟨theorem_3k_b_i, ?_⟩
   show ∀ v, v ∈ ⋂₀ {x | ∃ A, A ∈ 𝓐 ∧ image F A = x} → v ∈ image F (⋂₀ 𝓐)
@@ -640,9 +640,9 @@ F⟦A⟧ - F⟦B⟧ ⊆ F⟦A - B⟧.
 Equality holds if `F` is single-rooted.
 -/
 
-theorem theorem_3k_c_i {F : Set.Relation α} {A B : Set α}
-  : F.image A \ F.image B ⊆ F.image (A \ B) := by
-  show ∀ v, v ∈ F.image A \ F.image B → v ∈ F.image (A \ B)
+theorem theorem_3k_c_i {F : Set.HRelation α β} {A B : Set α}
+  : image F A \ image F B ⊆ image F (A \ B) := by
+  show ∀ v, v ∈ image F A \ image F B → v ∈ image F (A \ B)
   intro v hv
   have hv' : v ∈ image F A ∧ v ∉ image F B := hv
   conv at hv' => arg 1; unfold image; simp only [Set.mem_setOf_eq, eq_iff_iff]
@@ -660,9 +660,9 @@ theorem theorem_3k_c_i {F : Set.Relation α} {A B : Set α}
   simp only [Set.mem_diff, Set.mem_setOf_eq]
   exact ⟨u, ⟨hu.left, hu'⟩, hu.right⟩
 
-theorem theorem_3k_c_ii {F : Set.Relation α} {A B : Set α}
-  (hF : F.isSingleRooted)
-  : F.image A \ F.image B = F.image (A \ B) := by
+theorem theorem_3k_c_ii {F : Set.HRelation α β} {A B : Set α}
+  (hF : isSingleRooted F)
+  : image F A \ image F B = image F (A \ B) := by
   rw [Set.Subset.antisymm_iff]
   refine ⟨theorem_3k_c_i, ?_⟩
   show ∀ v, v ∈ image F (A \ B) → v ∈ image F A \ image F B
@@ -670,11 +670,11 @@ theorem theorem_3k_c_ii {F : Set.Relation α} {A B : Set α}
   unfold image at hv
   simp only [Set.mem_diff, Set.mem_setOf_eq] at hv
   have ⟨u, hu⟩ := hv
-  have hv₁ : v ∈ F.image A := by
+  have hv₁ : v ∈ image F A := by
     unfold image
     simp only [Set.mem_setOf_eq]
     exact ⟨u, hu.left.left, hu.right⟩
-  have hv₂ : v ∉ F.image B := by
+  have hv₂ : v ∉ image F B := by
     intro nv
     unfold image at nv
     simp only [Set.mem_setOf_eq] at nv
@@ -695,20 +695,20 @@ G⁻¹⟦A - B⟧ = G⁻¹⟦A⟧ - G⁻¹⟦B⟧.
 ```
 -/
 
-theorem corollary_3l_i {G : Set.Relation α} {𝓐 : Set (Set α)}
-  : G.inv.image (⋃₀ 𝓐) = ⋃₀ {G.inv.image A | A ∈ 𝓐} := theorem_3k_a
+theorem corollary_3l_i {G : Set.HRelation β α} {𝓐 : Set (Set α)}
+  : image (inv G) (⋃₀ 𝓐) = ⋃₀ {image (inv G) A | A ∈ 𝓐} := theorem_3k_a
 
-theorem corollary_3l_ii {G : Set.Relation α} {𝓐 : Set (Set α)}
-  (hG : G.isSingleValued) (h𝓐 : Set.Nonempty 𝓐)
-  : G.inv.image (⋂₀ 𝓐) = ⋂₀ {G.inv.image A | A ∈ 𝓐} := by
-  have hG' : G.inv.isSingleRooted :=
+theorem corollary_3l_ii {G : Set.HRelation β α} {𝓐 : Set (Set α)}
+  (hG : isSingleValued G) (h𝓐 : Set.Nonempty 𝓐)
+  : image (inv G) (⋂₀ 𝓐) = ⋂₀ {image (inv G) A | A ∈ 𝓐} := by
+  have hG' : isSingleRooted (inv G) :=
     single_valued_self_iff_single_rooted_inv.mp hG
   exact theorem_3k_b_ii hG' h𝓐
 
-theorem corollary_3l_iii {G : Set.Relation α} {A B : Set α}
-  (hG : G.isSingleValued)
-  : G.inv.image (A \ B) = G.inv.image A \ G.inv.image B := by
-  have hG' : G.inv.isSingleRooted :=
+theorem corollary_3l_iii {G : Set.HRelation β α} {A B : Set α}
+  (hG : isSingleValued G)
+  : image (inv G) (A \ B) = image (inv G) A \ image (inv G) B := by
+  have hG' : isSingleRooted (inv G) :=
     single_valued_self_iff_single_rooted_inv.mp hG
   exact (theorem_3k_c_ii hG').symm
 
@@ -719,10 +719,10 @@ Assume that `f` and `g` are functions and show that
 f ⊆ g ↔ dom f ⊆ dom g ∧ (∀ x ∈ dom f) f(x) = g(x).
 ```
 -/
-theorem exercise_3_12 {f g : Set.Relation α}
-  (hf : f.isSingleValued) (_ : g.isSingleValued)
+theorem exercise_3_12 {f g : Set.HRelation α β}
+  (hf : isSingleValued f) (_ : isSingleValued g)
   : f ⊆ g ↔ dom f ⊆ dom g ∧
-      (∀ x ∈ dom f, ∃! y : α, (x, y) ∈ f ∧ (x, y) ∈ g) := by
+      (∀ x ∈ dom f, ∃! y : β, (x, y) ∈ f ∧ (x, y) ∈ g) := by
   apply Iff.intro
   · intro h
     apply And.intro
@@ -747,8 +747,8 @@ theorem exercise_3_12 {f g : Set.Relation α}
 Assume that `f` and `g` are functions with `f ⊆ g` and `dom g ⊆ dom f`. Show
 that `f = g`.
 -/
-theorem exercise_3_13 {f g : Set.Relation α}
-  (hf : f.isSingleValued) (hg : g.isSingleValued)
+theorem exercise_3_13 {f g : Set.HRelation α β}
+  (hf : isSingleValued f) (hg : isSingleValued g)
   (h : f ⊆ g) (h₁ : dom g ⊆ dom f)
   : f = g := by
   have h₂ := (exercise_3_12 hf hg).mp h
@@ -770,9 +770,9 @@ theorem exercise_3_13 {f g : Set.Relation α}
 
 Assume that `f` and `g` are functions. Show that `f ∩ g` is a function.
 -/
-theorem exercise_3_14_a {f g : Set.Relation α}
-  (hf : f.isSingleValued) (_ : g.isSingleValued)
-  : (f ∩ g).isSingleValued :=
+theorem exercise_3_14_a {f g : Set.HRelation α β}
+  (hf : isSingleValued f) (_ : isSingleValued g)
+  : isSingleValued (f ∩ g) :=
   single_valued_subset hf (Set.inter_subset_left f g)
 
 /-- #### Exercise 3.14 (b)
@@ -780,9 +780,9 @@ theorem exercise_3_14_a {f g : Set.Relation α}
 Assume that `f` and `g` are functions. Show that `f ∪ g` is a function **iff**
 `f(x) = g(x)` for every `x` in `(dom f) ∩ (dom g)`.
 -/
-theorem exercise_3_14_b {f g : Set.Relation α}
-  (hf : f.isSingleValued) (hg : g.isSingleValued)
-  : (f ∪ g).isSingleValued ↔
+theorem exercise_3_14_b {f g : Set.HRelation α β}
+  (hf : isSingleValued f) (hg : isSingleValued g)
+  : isSingleValued (f ∪ g) ↔
       (∀ x ∈ dom f ∩ dom g, ∃! y, (x, y) ∈ f ∧ (x, y) ∈ g) := by
   apply Iff.intro
   · intro h x hx
@@ -860,16 +860,16 @@ theorem exercise_3_14_b {f g : Set.Relation α}
 Let `𝓐` be a set of functions such that for any `f` and `g` in `𝓐`, either
 `f ⊆ g` or `g ⊆ f`. Show that `⋃ 𝓐` is a function.
 -/
-theorem exercise_3_15 {𝓐 : Set (Set.Relation α)}
-  (h𝓐 : ∀ F ∈ 𝓐, F.isSingleValued)
+theorem exercise_3_15 {𝓐 : Set (Set.HRelation α β)}
+  (h𝓐 : ∀ F ∈ 𝓐, isSingleValued F)
   (h : ∀ F, ∀ G, F ∈ 𝓐 → G ∈ 𝓐 → F ⊆ G ∨ G ⊆ F)
   : isSingleValued (⋃₀ 𝓐) := by
   intro x hx
   have ⟨y₁, hy₁⟩ := dom_exists hx
   refine ⟨y₁, ⟨mem_pair_imp_snd_mem_ran hy₁, hy₁⟩, ?_⟩
   intro y₂ hy₂
-  have ⟨f, hf⟩ : ∃ f : Set.Relation α, f ∈ 𝓐 ∧ (x, y₁) ∈ f := hy₁
-  have ⟨g, hg⟩ : ∃ g : Set.Relation α, g ∈ 𝓐 ∧ (x, y₂) ∈ g := hy₂.right
+  have ⟨f, hf⟩ : ∃ f : Set.HRelation α β, f ∈ 𝓐 ∧ (x, y₁) ∈ f := hy₁
+  have ⟨g, hg⟩ : ∃ g : Set.HRelation α β, g ∈ 𝓐 ∧ (x, y₂) ∈ g := hy₂.right
   apply Or.elim (h f g hf.left hg.left)
   · intro hf'
     have := hf' hf.right
@@ -884,9 +884,9 @@ Show that the composition of two single-rooted sets is again single-rooted.
 Conclude that the composition of two one-to-one functions is again one-to-one.
 -/
 
-theorem exercise_3_17_i {F G : Set.Relation α}
-  (hF : F.isSingleRooted) (hG : G.isSingleRooted)
-  : (F.comp G).isSingleRooted := by
+theorem exercise_3_17_i {F : Set.HRelation β γ} {G : Set.HRelation α β}
+  (hF : isSingleRooted F) (hG : isSingleRooted G)
+  : isSingleRooted (comp F G):= by
   intro v hv
   
   have ⟨u₁, hu₁⟩ := ran_exists hv
@@ -907,11 +907,11 @@ theorem exercise_3_17_i {F G : Set.Relation α}
   rw [ht] at ht₁
   exact single_rooted_eq_unique hG ht₂.left ht₁.left
 
-theorem exercise_3_17_ii {F G : Set.Relation α}
-  (hF : F.isOneToOne) (hG : G.isOneToOne)
-  : (F.comp G).isOneToOne := And.intro
-    (single_valued_comp_is_single_valued hF.left hG.left)
-    (exercise_3_17_i hF.right hG.right)
+theorem exercise_3_17_ii {F : Set.HRelation β γ} {G : Set.HRelation α β}
+  (hF : isOneToOne F) (hG : isOneToOne G)
+  : isOneToOne (comp F G) := And.intro
+      (single_valued_comp_is_single_valued hF.left hG.left)
+      (exercise_3_17_i hF.right hG.right)
 
 /-! #### Exercise 3.18
 
@@ -929,7 +929,7 @@ variable {R : Set.Relation ℕ}
 variable (hR : R = {(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)})
 
 theorem exercise_3_18_i
-  : R.comp R = {(0, 2), (0, 3), (1, 3)} := by
+  : comp R R = {(0, 2), (0, 3), (1, 3)} := by
   rw [hR]
   unfold comp
   simp only [Set.mem_singleton_iff, Set.mem_insert_iff, or_self, Prod.mk.injEq]
@@ -970,7 +970,7 @@ theorem exercise_3_18_i
           exact ⟨rfl, h.right⟩
 
 theorem exercise_3_18_ii
-  : R.restriction {1} = {(1, 2), (1, 3)} := by
+  : restriction R {1} = {(1, 2), (1, 3)} := by
   rw [hR]
   unfold restriction
   ext p
@@ -1006,7 +1006,7 @@ theorem exercise_3_18_ii
       rw [hab.left, hab.right]
 
 theorem exercise_3_18_iii
-  : R.inv.restriction {1} = {(1, 0)} := by
+  : restriction (inv R) {1} = {(1, 0)} := by
   rw [hR]
   unfold inv restriction
   ext p
@@ -1031,14 +1031,14 @@ theorem exercise_3_18_iii
     simp
 
 theorem exercise_3_18_iv
-  : R.image {1} = {2, 3} := by
+  : image R {1} = {2, 3} := by
   rw [hR]
   unfold image
   ext y
   simp
 
 theorem exercise_3_18_v
-  : R.inv.image {1} = {0} := by
+  : image (inv R) {1} = {0} := by
   rw [hR]
   unfold inv image
   ext y
@@ -1067,12 +1067,12 @@ theorem exercise_3_19_i
   simp
 
 theorem exercise_3_19_ii
-  : A.image ∅ = ∅ := by
+  : image A ∅ = ∅ := by
   unfold image
   simp
 
 theorem exercise_3_19_iii
-  : A.image {∅} = {{∅, {∅}}} := by
+  : image A {∅} = {{∅, {∅}}} := by
   unfold image
   rw [hA]
   ext x
@@ -1098,7 +1098,7 @@ theorem exercise_3_19_iii
     simp
 
 theorem exercise_3_19_iv
-  : A.image {∅, {∅}} = {{∅, {∅}}, ∅} := by
+  : image A {∅, {∅}} = {{∅, {∅}}, ∅} := by
   unfold image
   rw [hA]
   ext x
@@ -1131,7 +1131,7 @@ theorem exercise_3_19_iv
     · intro hx₁; right; exact hx₁
 
 theorem exercise_3_19_v
-  : A.inv = {({∅, {∅}}, ∅), (∅, {∅})} := by
+  : inv A = {({∅, {∅}}, ∅), (∅, {∅})} := by
   unfold inv
   rw [hA]
   ext x
@@ -1154,7 +1154,7 @@ theorem exercise_3_19_v
     · intro hx₁; right; rw [← hx₁]
 
 theorem exercise_3_19_vi
-  : A.comp A = {({∅}, {∅, {∅}})} := by
+  : comp A A = {({∅}, {∅, {∅}})} := by
   unfold comp
   rw [hA]
   ext x
@@ -1179,13 +1179,13 @@ theorem exercise_3_19_vi
     · left ; rw [hb]; simp
 
 theorem exercise_3_19_vii
-  : A.restriction ∅ = ∅ := by
+  : restriction A ∅ = ∅ := by
   unfold restriction
   rw [hA]
   simp
 
 theorem exercise_3_19_viii
-  : A.restriction {∅} = {(∅, {∅, {∅}})} := by
+  : restriction A {∅} = {(∅, {∅, {∅}})} := by
   unfold restriction
   rw [hA]
   ext x
@@ -1206,7 +1206,7 @@ theorem exercise_3_19_viii
     simp
 
 theorem exercise_3_19_ix
-  : A.restriction {∅, {∅}} = A := by
+  : restriction A {∅, {∅}} = A := by
   unfold restriction
   rw [hA]
   ext x
@@ -1300,9 +1300,9 @@ end Exercise_3_19
 
 Show that `F ↾ A = F ∩ (A × ran F)`.
 -/
-theorem exercise_3_20 {F : Set.Relation α} {A : Set α}
-  : F.restriction A = F ∩ (Set.prod A (ran F)) := by
-  calc F.restriction A
+theorem exercise_3_20 {F : Set.HRelation α β} {A : Set α}
+  : restriction F A = F ∩ (Set.prod A (ran F)) := by
+  calc restriction F A
     _ = {p | p ∈ F ∧ p.fst ∈ A} := rfl
     _ = {p | p ∈ F ∧ p.fst ∈ A ∧ p.snd ∈ ran F} := by
       ext x
@@ -1323,9 +1323,9 @@ Show that the following is correct for any sets.
 A ⊆ B → F⟦A⟧ ⊆ F⟦B⟧
 ```
 -/
-theorem exercise_3_22_a {A B : Set α} {F : Set.Relation α} (h : A ⊆ B)
-  : F.image A ⊆ F.image B := by
-  show ∀ x, x ∈ F.image A → x ∈ F.image B
+theorem exercise_3_22_a {A B : Set α} {F : Set.HRelation α β} (h : A ⊆ B)
+  : image F A ⊆ image F B := by
+  show ∀ x, x ∈ image F A → x ∈ image F B
   unfold image
   simp only [Set.mem_setOf_eq]
   intro x hx
@@ -1340,10 +1340,10 @@ Show that the following is correct for any sets.
 (F ∘ G)⟦A⟧ = F⟦G⟦A⟧⟧
 ```
 -/
-theorem exercise_3_22_b {A B : Set α} {F : Set.Relation α}
-  : (F.comp G).image A = F.image (G.image A) := by
-  calc (F.comp G).image A
-    _ = { v | ∃ u ∈ A, (u, v) ∈ F.comp G } := rfl
+theorem exercise_3_22_b {A B : Set α} {F : Set.HRelation α β}
+  : image (comp F G) A = image F (image G A) := by
+  calc image (comp F G) A
+    _ = { v | ∃ u ∈ A, (u, v) ∈ comp F G } := rfl
     _ = { v | ∃ u ∈ A, ∃ a, (u, a) ∈ G ∧ (a, v) ∈ F } := rfl
     _ = { v | ∃ a, ∃ u ∈ A, (u, a) ∈ G ∧ (a, v) ∈ F } := by
       ext p
@@ -1362,8 +1362,8 @@ theorem exercise_3_22_b {A B : Set α} {F : Set.Relation α}
       · intro ⟨a, ⟨u, hu⟩, ha⟩
         exact ⟨a, u, hu.left, hu.right, ha⟩
     _ = { v | ∃ a ∈ { w | ∃ u ∈ A, (u, w) ∈ G }, (a, v) ∈ F } := rfl
-    _ = { v | ∃ a ∈ G.image A, (a, v) ∈ F } := rfl
-    _ = F.image (G.image A) := rfl
+    _ = { v | ∃ a ∈ image G A, (a, v) ∈ F } := rfl
+    _ = image F (image G A) := rfl
 
 /-- #### Exercise 3.22 (c)
 
@@ -1373,27 +1373,27 @@ Q ↾ (A ∪ B) = (Q ↾ A) ∪ (Q ↾ B)
 ```
 -/
 theorem exercise_3_22_c {A B : Set α} {Q : Set.Relation α}
-  : Q.restriction (A ∪ B) = (Q.restriction A) ∪ (Q.restriction B) := by
-  calc Q.restriction (A ∪ B)
+  : restriction Q (A ∪ B) = (restriction Q A) ∪ (restriction Q B) := by
+  calc restriction Q (A ∪ B)
     _ = { p | p ∈ Q ∧ p.1 ∈ A ∪ B } := rfl
     _ = { p | p ∈ Q ∧ (p.1 ∈ A ∨ p.1 ∈ B) } := rfl
     _ = { p | (p ∈ Q ∧ p.1 ∈ A) ∨ (p ∈ Q ∧ p.1 ∈ B) } := by
       ext p
       simp only [Set.sep_or, Set.mem_union, Set.mem_setOf_eq]
     _ = { p | p ∈ Q ∧ p.1 ∈ A} ∪ { p | p ∈ Q ∧ p.1 ∈ B } := rfl
-    _ = (Q.restriction A) ∪ (Q.restriction B) := rfl
+    _ = (restriction Q A) ∪ (restriction Q B) := rfl
 
 /-- #### Exercise 3.23 (i)
 
 Let `I` be the identity function on the set `A`. Show that for any sets `B` and
 `C`, `B ∘ I = B ↾ A`.
 -/
-theorem exercise_3_23_i {A : Set α} {B : Set.Relation α} {I : Set.Relation α}
+theorem exercise_3_23_i {A : Set α} {B : Set.HRelation α β} {I : Set.Relation α}
   (hI : I = { p | p.1 ∈ A ∧ p.1 = p.2 })
-  : B.comp I = B.restriction A := by
+  : comp B I = restriction B A := by
   rw [Set.Subset.antisymm_iff]
   apply And.intro
-  · show ∀ p, p ∈ B.comp I → p ∈ B.restriction A
+  · show ∀ p, p ∈ comp B I → p ∈ restriction B A
     intro (x, y) hp
     have ⟨t, ht⟩ := hp
     rw [hI] at ht
@@ -1401,7 +1401,7 @@ theorem exercise_3_23_i {A : Set α} {B : Set.Relation α} {I : Set.Relation α}
     show (x, y) ∈ B ∧ x ∈ A
     rw [← ht.left.right] at ht
     exact ⟨ht.right, ht.left.left⟩
-  · show ∀ p, p ∈ B.restriction A → p ∈ B.comp I
+  · show ∀ p, p ∈ restriction B A → p ∈ comp B I
     unfold restriction comp
     rw [hI]
     simp only [Set.mem_setOf_eq, and_true]
@@ -1415,8 +1415,8 @@ Let `I` be the identity function on the set `A`. Show that for any sets `B` and
 -/
 theorem exercise_3_23_ii {A C : Set α} {I : Set.Relation α}
   (hI : I = { p | p.1 ∈ A ∧ p.1 = p.2 })
-  : I.image C = A ∩ C := by
-  calc I.image C
+  : image I C = A ∩ C := by
+  calc image I C
     _ = { v | ∃ u ∈ C, (u, v) ∈ I } := rfl
     _ = { v | ∃ u ∈ C, u ∈ A ∧ u = v } := by
       ext v
@@ -1443,6 +1443,205 @@ theorem exercise_3_23_ii {A C : Set α} {I : Set.Relation α}
     _ = C ∩ A := rfl
     _ = A ∩ C := Set.inter_comm C A
 
+/-- #### Exercise 3.24
+
+Show that for a function `F`, `F⁻¹⟦A⟧ = { x ∈ dom F | F(x) ∈ A }`.
+-/
+theorem exercise_3_24 {F : Set.HRelation α β} {A : Set β}
+  (hF : isSingleValued F)
+  : image (inv F) A = { x ∈ dom F | ∃! y : β, (x, y) ∈ F ∧ y ∈ A } := by
+  calc image (inv F) A
+    _ = { x | ∃ y ∈ A, (y, x) ∈ inv F } := rfl
+    _ = { x | ∃ y ∈ A, (x, y) ∈ F } := by simp only [mem_self_comm_mem_inv]
+    _ = { x | x ∈ dom F ∧ (∃ y : β, (x, y) ∈ F ∧ y ∈ A) } := by
+      ext x
+      simp only [Set.mem_setOf_eq]
+      apply Iff.intro
+      · intro ⟨y, hy, hyx⟩
+        exact ⟨mem_pair_imp_fst_mem_dom hyx, y, hyx, hy⟩
+      · intro ⟨_, y, hxy, hy⟩
+        exact ⟨y, hy, hxy⟩
+    _ = { x ∈ dom F | ∃ y : β, (x, y) ∈ F ∧ y ∈ A } := rfl
+    _ = { x ∈ dom F | ∃! y : β, (x, y) ∈ F ∧ y ∈ A } := by
+      ext x
+      simp only [Set.mem_setOf_eq, and_congr_right_iff]
+      intro _
+      apply Iff.intro
+      · intro ⟨y, hy⟩
+        refine ⟨y, hy, ?_⟩
+        intro y₁ hy₁
+        exact single_valued_eq_unique hF hy₁.left hy.left
+      · intro ⟨y, hy⟩
+        exact ⟨y, hy.left⟩
+
+/-- #### Exercise 3.25 (b)
+
+Show that the result of part (a) holds for any function `G`, not necessarily
+one-to-one.
+-/
+theorem exercise_3_25_b {G : Set.HRelation α β} (hG : isSingleValued G)
+  : comp G (inv G) = { p | p.1 ∈ ran G ∧ p.1 = p.2 } := by
+  ext p
+  have (x, y) := p
+  apply Iff.intro
+  · unfold comp inv
+    intro h
+    simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq] at h
+    have ⟨t, ⟨a, b, ⟨hab, hb, ha⟩⟩, ht⟩ := h
+    simp only [Set.mem_setOf_eq]
+    rw [hb, ha] at hab
+    exact ⟨mem_pair_imp_snd_mem_ran hab, single_valued_eq_unique hG hab ht⟩
+  · intro h
+    simp only [Set.mem_setOf_eq] at h
+    unfold comp inv
+    simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq]
+    have ⟨t, ht⟩ := ran_exists h.left
+    exact ⟨t, ⟨t, x, ht, rfl, rfl⟩, by rwa [← h.right]⟩
+
+/-- #### Exercise 3.25 (a)
+
+Assume that `G` is a one-to-one function. Show that `G ∘ G⁻¹` is the identity
+function on `ran G`.
+-/
+theorem exercise_3_25_a {G : Set.HRelation α β} (hG : isOneToOne G)
+  : comp G (inv G) = { p | p.1 ∈ ran G ∧ p.1 = p.2 } :=
+  exercise_3_25_b hG.left
+
+/-- #### Exercise 3.27
+
+Show that `dom (F ∘ G) = G⁻¹⟦dom F⟧` for any sets `F` and `G`. (`F` and `G` need
+not be functions.)
+-/
+theorem exercise_3_27 {F : Set.HRelation β γ} {G : Set.HRelation α β}
+  : dom (comp F G) = image (inv G) (dom F) := by
+  rw [Set.Subset.antisymm_iff]
+  apply And.intro
+  · show ∀ x, x ∈ dom (comp F G) → x ∈ image (inv G) (dom F)
+    intro x hx
+    have ⟨y, hy⟩ := dom_exists hx
+    unfold comp at hy
+    simp only [Set.mem_setOf_eq] at hy
+    have ⟨t, ht⟩ := hy
+    have htF : t ∈ dom F := mem_pair_imp_fst_mem_dom ht.right
+    
+    unfold image inv
+    simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq]
+    exact ⟨t, htF, x, t, ht.left, rfl, rfl⟩
+
+  · show ∀ x, x ∈ image (inv G) (dom F) → x ∈ dom (comp F G)
+    intro x hx
+    unfold image at hx
+    simp only [mem_self_comm_mem_inv, Set.mem_setOf_eq] at hx
+    have ⟨u, hu⟩ := hx
+    have ⟨t, ht⟩ := dom_exists hu.left
+
+    unfold dom comp
+    simp only [
+      Set.mem_image,
+      Set.mem_setOf_eq,
+      Prod.exists,
+      exists_and_right,
+      exists_eq_right
+    ]
+    exact ⟨t, u, hu.right, ht⟩
+
+/-- #### Exercise 3.28
+
+Assume that `f` is a one-to-one function from `A` into `B`, and that `G` is the
+function with `dom G = 𝒫 A` defined by the equation `G(X) = f⟦X⟧`. Show that `G`
+maps `𝒫 A` one-to-one into `𝒫 B`.
+-/
+theorem exercise_3_28 {A : Set α} {B : Set β}
+  {f : Set.HRelation α β} {G : Set.HRelation (Set α) (Set β)}
+  (hf : isOneToOne f ∧ mapsInto f A B)
+  (hG : G = { p | p.1 ∈ 𝒫 A ∧ p.2 = image f p.1 })
+  : isOneToOne G ∧ mapsInto G (𝒫 A) (𝒫 B) := by
+  have dG : dom G = 𝒫 A := by
+    rw [hG]
+    ext p
+    unfold dom Prod.fst
+    simp
+
+  have hG₁ : isSingleValued G := by
+    intro x hx
+    have ⟨y, hy⟩ := dom_exists hx
+    refine ⟨y, ⟨mem_pair_imp_snd_mem_ran hy, hy⟩, ?_⟩
+    intro y₁ hy₁
+    rw [hG, Set.mem_setOf_eq] at hy
+    conv at hy₁ => rhs; rw [hG, Set.mem_setOf_eq]
+    simp only at *
+    rw [hy.right, hy₁.right.right]
+
+  apply And.intro
+  · show isOneToOne G
+    refine ⟨hG₁, ?_⟩
+    intro y hy
+    have ⟨X₁, hX₁⟩ := ran_exists hy
+    refine ⟨X₁, ⟨mem_pair_imp_fst_mem_dom hX₁, hX₁⟩, ?_⟩
+    intro X₂ hX₂
+    have hX₁' : y = image f X₁ := by
+      rw [hG] at hX₁
+      simp only [Set.mem_powerset_iff, Set.mem_setOf_eq] at hX₁
+      exact hX₁.right
+    have hX₂' : y = image f X₂ := by
+      have := hX₂.right
+      rw [hG] at this
+      simp only [Set.mem_powerset_iff, Set.mem_setOf_eq] at this
+      exact this.right
+
+    ext t
+    apply Iff.intro
+    · intro ht
+      rw [dG] at hX₂
+      simp only [Set.mem_powerset_iff] at hX₂
+
+      have ht' := hX₂.left ht
+      rw [← hf.right.right.left] at ht'
+      have ⟨ft, hft⟩ := dom_exists ht'
+      have hft' : ft ∈ image f X₂ := ⟨t, ht, hft⟩
+
+      rw [← hX₂', hX₁'] at hft'
+      have ⟨t₁, ht₁⟩ := hft'
+      rw [single_rooted_eq_unique hf.left.right hft ht₁.right]
+      exact ht₁.left
+
+    · intro ht
+      have hX₁sub := mem_pair_imp_fst_mem_dom hX₁
+      rw [dG] at hX₁sub
+      simp only [Set.mem_powerset_iff] at hX₁sub
+      
+      have ht' := hX₁sub ht
+      rw [← hf.right.right.left] at ht'
+      have ⟨ft, hft⟩ := dom_exists ht'
+      have hft' : ft ∈ image f X₁ := ⟨t, ht, hft⟩
+
+      rw [← hX₁', hX₂'] at hft'
+      have ⟨t₁, ht₁⟩ := hft'
+      rw [single_rooted_eq_unique hf.left.right hft ht₁.right]
+      exact ht₁.left
+
+  · show mapsInto G (𝒫 A) (𝒫 B)
+    refine ⟨hG₁, dG, ?_⟩
+    show ∀ x, x ∈ ran G → x ∈ 𝒫 B
+    intro x hx
+    rw [hG] at hx
+    unfold ran Prod.snd at hx
+    simp only [
+      Set.mem_powerset_iff,
+      Set.mem_image,
+      Set.mem_setOf_eq,
+      Prod.exists,
+      exists_eq_right
+    ] at hx
+    have ⟨a, ha⟩ := hx
+    rw [ha.right]
+    show ∀ y, y ∈ image f a → y ∈ B
+    intro y hy
+    simp only [Set.mem_setOf_eq] at hy
+    have ⟨b, hb⟩ := hy
+    have hz := mem_pair_imp_snd_mem_ran hb.right
+    exact hf.right.right.right hz
+
 end Relation
 
 end Enderton.Set.Chapter_3
\ No newline at end of file
diff --git a/Bookshelf/Enderton/Set/Relation.lean b/Bookshelf/Enderton/Set/Relation.lean
index a91dfdd..a14e999 100644
--- a/Bookshelf/Enderton/Set/Relation.lean
+++ b/Bookshelf/Enderton/Set/Relation.lean
@@ -16,7 +16,12 @@ Kuratowski's definition of a set.
 
 Not to be confused with the Lean-provided `Rel`.
 -/
-abbrev Relation (α : Type _) := Set (α × α)
+abbrev HRelation (α β : Type ) := Set (α × β)
+
+/--
+A homogeneous variant of the `HRelation` type.
+-/
+abbrev Relation (α : Type _) := HRelation α α
 
 namespace Relation
 
@@ -25,13 +30,13 @@ namespace Relation
 /--
 The domain of a `Relation`.
 -/
-def dom (R : Relation α) : Set α := Prod.fst '' R
+def dom (R : HRelation α β) : Set α := Prod.fst '' R
 
 /--
 The first component of any pair in a `Relation` must be a member of the
 `Relation`'s domain.
 -/
-theorem mem_pair_imp_fst_mem_dom {R : Relation α} (h : (x, y) ∈ R)
+theorem mem_pair_imp_fst_mem_dom {R : HRelation α β} (h : (x, y) ∈ R)
   : x ∈ dom R := by
   unfold dom Prod.fst
   simp only [mem_image, Prod.exists, exists_and_right, exists_eq_right]
@@ -40,8 +45,8 @@ theorem mem_pair_imp_fst_mem_dom {R : Relation α} (h : (x, y) ∈ R)
 /--
 If `x ∈ dom R`, there exists some `y` such that `⟨x, y⟩ ∈ R`.
 -/
-theorem dom_exists {R : Relation α} (hx : x ∈ R.dom)
-  : ∃ y : α, (x, y) ∈ R := by
+theorem dom_exists {R : HRelation α β} (hx : x ∈ dom R)
+  : ∃ y : β, (x, y) ∈ R := by
   unfold dom at hx
   simp only [mem_image, Prod.exists, exists_and_right, exists_eq_right] at hx
   exact hx
@@ -49,9 +54,9 @@ theorem dom_exists {R : Relation α} (hx : x ∈ R.dom)
 /--
 The range of a `Relation`.
 -/
-def ran (R : Relation α) : Set α := Prod.snd '' R
+def ran (R : HRelation α β) : Set β := Prod.snd '' R
 
-theorem mem_pair_imp_snd_mem_ran {R : Relation α} (h : (x, y) ∈ R)
+theorem mem_pair_imp_snd_mem_ran {R : HRelation α β} (h : (x, y) ∈ R)
   : y ∈ ran R := by
   unfold ran Prod.snd
   simp only [mem_image, Prod.exists, exists_eq_right]
@@ -60,7 +65,7 @@ theorem mem_pair_imp_snd_mem_ran {R : Relation α} (h : (x, y) ∈ R)
 /--
 If `x ∈ ran R`, there exists some `t` such that `⟨t, x⟩ ∈ R`.
 -/
-theorem ran_exists {R : Relation α} (hx : x ∈ R.ran)
+theorem ran_exists {R : HRelation α β} (hx : x ∈ ran R)
   : ∃ t : α, (t, x) ∈ R := by
   unfold ran at hx
   simp only [mem_image, Prod.exists, exists_eq_right] at hx
@@ -74,14 +79,14 @@ def fld (R : Relation α) : Set α := dom R ∪ ran R
 /--
 The inverse of a `Relation`.
 -/
-def inv (R : Relation α) : Relation α := { (p.2, p.1) | p ∈ R }
+def inv (R : HRelation α β) : HRelation β α := { (p.2, p.1) | p ∈ R }
 
 /--
 `(x, y)` is a member of relation `R` **iff** `(y, x)` is a member of `R⁻¹`.
 -/
 @[simp]
-theorem mem_self_comm_mem_inv {R : Relation α}
-  : (y, x) ∈ R.inv ↔ (x, y) ∈ R := by
+theorem mem_self_comm_mem_inv {R : HRelation α β}
+  : (y, x) ∈ inv R ↔ (x, y) ∈ R := by
   unfold inv
   simp only [Prod.exists, mem_setOf_eq, Prod.mk.injEq]
   apply Iff.intro
@@ -95,8 +100,8 @@ theorem mem_self_comm_mem_inv {R : Relation α}
 The inverse of the inverse of a `Relation` is the `Relation`.
 -/
 @[simp]
-theorem inv_inv_eq_self (R : Relation α)
-  : R.inv.inv = R := by
+theorem inv_inv_eq_self (R : HRelation α β)
+  : inv (inv R) = R := by
   unfold inv
   simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq]
   ext x
@@ -115,8 +120,8 @@ theorem inv_inv_eq_self (R : Relation α)
 For a set `F`, `dom F⁻¹ = ran F`.
 -/
 @[simp]
-theorem dom_inv_eq_ran_self {F : Relation α}
-  : dom (F.inv) = ran F := by
+theorem dom_inv_eq_ran_self {F : HRelation α β}
+  : dom (inv F) = ran F := by
   ext x
   unfold dom ran inv
   simp only [
@@ -138,8 +143,8 @@ theorem dom_inv_eq_ran_self {F : Relation α}
 For a set `F`, `ran F⁻¹ = dom F`.
 -/
 @[simp]
-theorem ran_inv_eq_dom_self {F : Relation α}
-  : ran (F.inv) = dom F := by
+theorem ran_inv_eq_dom_self {F : HRelation α β}
+  : ran (inv F) = dom F := by
   ext x
   unfold dom ran inv
   simp only [
@@ -162,7 +167,7 @@ theorem ran_inv_eq_dom_self {F : Relation α}
 /--
 The restriction of a `Relation` to a `Set`.
 -/
-def restriction (R : Relation α) (A : Set α) : Relation α :=
+def restriction (R : HRelation α β) (A : Set α) : HRelation α β :=
   { p ∈ R | p.1 ∈ A } 
 
 /-! ## Image -/
@@ -170,7 +175,7 @@ def restriction (R : Relation α) (A : Set α) : Relation α :=
 /--
 The image of a `Relation` under a `Set`.
 -/
-def image (R : Relation α) (A : Set α) : Set α :=
+def image (R : HRelation α β) (A : Set α) : Set β :=
   { y | ∃ u ∈ A, (u, y) ∈ R }
 
 /-! ## Single-Rooted and Single-Valued -/
@@ -179,14 +184,14 @@ def image (R : Relation α) (A : Set α) : Set α :=
 A `Relation` `R` is said to be single-rooted **iff** for all `y ∈ ran R`, there
 exists exactly one `x` such that `⟨x, y⟩ ∈ R`.
 -/
-def isSingleRooted (R : Relation α) : Prop :=
+def isSingleRooted (R : HRelation α β) : Prop :=
   ∀ y ∈ ran R, ∃! x, x ∈ dom R ∧ (x, y) ∈ R
 
 /--
 A single-rooted `Relation` should map the same output to the same input.
 -/
-theorem single_rooted_eq_unique {R : Relation α} {x₁ x₂ y : α}
-  (hR : R.isSingleRooted)
+theorem single_rooted_eq_unique {R : HRelation α β} {x₁ x₂ : α} {y : β}
+  (hR : isSingleRooted R)
   : (x₁, y) ∈ R → (x₂, y) ∈ R → x₁ = x₂ := by
   intro hx₁ hx₂
   unfold isSingleRooted at hR
@@ -203,14 +208,14 @@ exists exactly one `y` such that `⟨x, y⟩ ∈ R`.
 
 Notice, a `Relation` that is single-valued is a function.
 -/
-def isSingleValued (R : Relation α) : Prop :=
+def isSingleValued (R : HRelation α β) : Prop :=
   ∀ x ∈ dom R, ∃! y, y ∈ ran R ∧ (x, y) ∈ R
 
 /--
 A single-valued `Relation` should map the same input to the same output.
 -/
-theorem single_valued_eq_unique {R : Relation α} {x y₁ y₂ : α}
-  (hR : R.isSingleValued)
+theorem single_valued_eq_unique {R : HRelation α β} {x : α} {y₁ y₂ : β}
+  (hR : isSingleValued R)
   : (x, y₁) ∈ R → (x, y₂) ∈ R → y₁ = y₂ := by
   intro hy₁ hy₂
   unfold isSingleValued at hR
@@ -224,8 +229,8 @@ theorem single_valued_eq_unique {R : Relation α} {x y₁ y₂ : α}
 /--
 For a set `F`, `F⁻¹` is a function **iff** `F` is single-rooted.
 -/
-theorem single_valued_inv_iff_single_rooted_self {F : Set.Relation α}
-  : F.inv.isSingleValued ↔ F.isSingleRooted := by
+theorem single_valued_inv_iff_single_rooted_self {F : HRelation α β}
+  : isSingleValued (inv F) ↔ isSingleRooted F := by
   apply Iff.intro
   · intro hF
     unfold isSingleValued at hF
@@ -234,7 +239,7 @@ theorem single_valued_inv_iff_single_rooted_self {F : Set.Relation α}
       ran_inv_eq_dom_self,
       mem_self_comm_mem_inv
     ] at hF
-    suffices ∀ x ∈ F.ran, ∃! y, (y, x) ∈ F from hF
+    suffices ∀ x ∈ ran F, ∃! y, (y, x) ∈ F from hF
     intro x hx
     have ⟨y, hy⟩ := hF x hx
     simp only [
@@ -258,17 +263,17 @@ theorem single_valued_inv_iff_single_rooted_self {F : Set.Relation α}
 /--
 For a relation `F`, `F` is a function **iff** `F⁻¹` is single-rooted.
 -/
-theorem single_valued_self_iff_single_rooted_inv {F : Set.Relation α}
-  : F.isSingleValued ↔ F.inv.isSingleRooted := by
+theorem single_valued_self_iff_single_rooted_inv {F : HRelation α β}
+  : isSingleValued F ↔ isSingleRooted (inv F) := by
   conv => lhs; rw [← inv_inv_eq_self F]
   rw [single_valued_inv_iff_single_rooted_self]
 
 /--
 The subset of a function must also be a function.
 -/
-theorem single_valued_subset {F G : Set.Relation α}
-  (hG : G.isSingleValued) (h : F ⊆ G)
-  : F.isSingleValued := by
+theorem single_valued_subset {F G : HRelation α β}
+  (hG : isSingleValued G) (h : F ⊆ G)
+  : isSingleValued F := by
   unfold isSingleValued
   intro x hx
   have ⟨y, hy⟩ := dom_exists hx
@@ -283,14 +288,14 @@ theorem single_valued_subset {F G : Set.Relation α}
 /--
 A `Relation` `R` is one-to-one if it is a single-rooted function.
 -/
-def isOneToOne (R : Relation α) : Prop :=
-  R.isSingleValued ∧ R.isSingleRooted
+def isOneToOne (R : HRelation α β) : Prop :=
+  isSingleValued R ∧ isSingleRooted R
 
 /--
 A `Relation` is one-to-one **iff** it's inverse is.
 -/
-theorem one_to_one_self_iff_one_to_one_inv {R : Relation α}
-  : R.isOneToOne ↔ R.inv.isOneToOne := by
+theorem one_to_one_self_iff_one_to_one_inv {R : HRelation α β}
+  : isOneToOne R ↔ isOneToOne (inv R) := by
   unfold isOneToOne isSingleValued isSingleRooted
   conv => rhs; simp only [
     dom_inv_eq_ran_self,
@@ -309,28 +314,28 @@ Indicates `Relation` `F` is a function from `A` to `B`.
 
 This is usually denoted as `F : A → B`.
 -/
-def mapsInto (F : Relation α) (A B : Set α) :=
-  F.isSingleValued ∧ dom F = A ∧ ran F ⊆ B
+def mapsInto (F : HRelation α β) (A : Set α) (B : Set β) :=
+  isSingleValued F ∧ dom F = A ∧ ran F ⊆ B
 
 /--
 Indicates `Relation` `F` is a function from `A` to `ran F = B`.
 -/
-def mapsOnto (F : Relation α) (A B : Set α) :=
-  F.isSingleValued ∧ dom F = A ∧ ran F = B
+def mapsOnto (F : HRelation α β) (A : Set α) (B : Set β) :=
+  isSingleValued F ∧ dom F = A ∧ ran F = B
 
 /-! ## Composition -/
 
 /--
 The composition of two `Relation`s.
 -/
-def comp (F G : Relation α) : Relation α :=
-  { p | ∃ t : α, (p.1, t) ∈ G ∧ (t, p.2) ∈ F}
+def comp (F : HRelation β γ) (G : HRelation α β) : HRelation α γ :=
+  { p | ∃ t : β, (p.1, t) ∈ G ∧ (t, p.2) ∈ F}
 
 /--
 If `x ∈ dom (F ∘ G)`, then `x ∈ dom G`.
 -/
-theorem dom_comp_imp_dom_self {F G : Relation α}
-  : x ∈ dom (F.comp G) → x ∈ dom G := by
+theorem dom_comp_imp_dom_self {F : HRelation β γ} {G : HRelation α β}
+  : x ∈ dom (comp F G) → x ∈ dom G := by
   unfold dom comp
   simp only [
     mem_image,
@@ -346,8 +351,8 @@ theorem dom_comp_imp_dom_self {F G : Relation α}
 /--
 If `y ∈ ran (F ∘ G)`, then `y ∈ ran F`.
 -/
-theorem ran_comp_imp_ran_self {F G : Relation α}
-  : y ∈ ran (F.comp G) → y ∈ ran F := by
+theorem ran_comp_imp_ran_self {F : HRelation β γ} {G : HRelation α β}
+  : y ∈ ran (comp F G) → y ∈ ran F := by
   unfold ran comp
   simp only [
     mem_image,
@@ -362,10 +367,10 @@ theorem ran_comp_imp_ran_self {F G : Relation α}
 /--
 Composition of functions is associative.
 -/
-theorem comp_assoc {R S T : Relation α}
-  : (R.comp S).comp T = R.comp (S.comp T) := by
-  calc (R.comp S).comp T
-    _ = { p | ∃ t, (p.1, t) ∈ T ∧ (t, p.2) ∈ R.comp S} := rfl
+theorem comp_assoc {R : HRelation γ δ} {S : HRelation β γ} {T : HRelation α β}
+  : comp (comp R S) T = comp R (comp S T) := by
+  calc comp (comp R S) T
+    _ = { p | ∃ t, (p.1, t) ∈ T ∧ (t, p.2) ∈ comp R S} := rfl
     _ = { p | ∃ t, (p.1, t) ∈ T ∧ (∃ a, (t, a) ∈ S ∧ (a, p.2) ∈ R) } := rfl
     _ = { p | ∃ t, ∃ a, ((p.1, t) ∈ T ∧ (t, a) ∈ S) ∧ (a, p.2) ∈ R } := by
       ext p
@@ -391,15 +396,16 @@ theorem comp_assoc {R S T : Relation α}
         exact ⟨a, ⟨t, h.left⟩, h.right⟩
       · intro ⟨a, ⟨t, ht⟩, ha⟩
         exact ⟨a, t, ht, ha⟩
-    _ = { p | ∃ a, (p.1, a) ∈ S.comp T ∧ (a, p.2) ∈ R } := rfl
-    _ = R.comp (S.comp T) := rfl
+    _ = { p | ∃ a, (p.1, a) ∈ comp S T ∧ (a, p.2) ∈ R } := rfl
+    _ = comp R (comp S T) := rfl
 
 /--
 The composition of two functions is itself a function.
 -/
-theorem single_valued_comp_is_single_valued {F G : Relation α}
-  (hF : F.isSingleValued) (hG : G.isSingleValued)
-  : (F.comp G).isSingleValued := by
+theorem single_valued_comp_is_single_valued
+  {F : HRelation β γ} {G : HRelation α β}
+  (hF : isSingleValued F) (hG : isSingleValued G)
+  : isSingleValued (comp F G) := by
   unfold isSingleValued
   intro x hx
   have ⟨y, hxy⟩ := dom_exists hx
@@ -433,9 +439,9 @@ theorem single_valued_comp_is_single_valued {F G : Relation α}
 /--
 For `Relation`s `F` and `G`, `(F ∘ G)⁻¹ = G⁻¹ ∘ F⁻¹`.
 -/
-theorem comp_inv_eq_inv_comp_inv {F G : Relation α}
-  : (F.comp G).inv = G.inv.comp F.inv := by
-  calc (F.comp G).inv
+theorem comp_inv_eq_inv_comp_inv {F : HRelation β γ} {G : HRelation α β}
+  : inv (comp F G) = comp (inv G) (inv F) := by
+  calc inv (comp F G)
   _ = {p | ∃ t, (p.2, t) ∈ G ∧ (t, p.1) ∈ F} := by
     rw [Set.Subset.antisymm_iff]
     apply And.intro
@@ -460,7 +466,7 @@ theorem comp_inv_eq_inv_comp_inv {F G : Relation α}
       simp only [mem_setOf_eq] at *
       have ⟨t, p, q⟩ := ht
       exact ⟨t, q, p⟩
-  _ = {p | ∃ t, (p.1, t) ∈ F.inv ∧ (t, p.2) ∈ G.inv } := by
+  _ = {p | ∃ t, (p.1, t) ∈ inv F ∧ (t, p.2) ∈ inv G } := by
     rw [Set.Subset.antisymm_iff]
     apply And.intro
     · intro (a, b) ht