From e7af7527ce7da67f3aa18b7ab966247d0481783f Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Sun, 6 Aug 2023 07:32:58 +0100
Subject: [PATCH] Restriction categories (#247)

This PR defines restriction categories, and proves that every allegory
has a restriction structure on its category of partial maps.
---
 src/Cat/Allegory/Maps.lagda.md                |  39 +-
 src/Cat/Allegory/Morphism.lagda.md            | 283 +++++++++-
 src/Cat/Allegory/Reasoning.lagda.md           |  46 +-
 src/Cat/Restriction/Base.lagda.md             | 100 ++++
 src/Cat/Restriction/Functor.lagda.md          | 148 +++++
 .../Restriction/Instances/Allegory.lagda.md   |  70 +++
 src/Cat/Restriction/Reasoning.lagda.md        | 525 ++++++++++++++++++
 src/Cat/Restriction/Total.lagda.md            |  64 +++
 src/index.lagda.md                            |  24 +
 src/preamble.tex                              |   2 +
 10 files changed, 1260 insertions(+), 41 deletions(-)
 create mode 100644 src/Cat/Restriction/Base.lagda.md
 create mode 100644 src/Cat/Restriction/Functor.lagda.md
 create mode 100644 src/Cat/Restriction/Instances/Allegory.lagda.md
 create mode 100644 src/Cat/Restriction/Reasoning.lagda.md
 create mode 100644 src/Cat/Restriction/Total.lagda.md

diff --git a/src/Cat/Allegory/Maps.lagda.md b/src/Cat/Allegory/Maps.lagda.md
index fa115c72c..8517a158f 100644
--- a/src/Cat/Allegory/Maps.lagda.md
+++ b/src/Cat/Allegory/Maps.lagda.md
@@ -3,7 +3,7 @@
 open import Cat.Allegory.Base
 open import Cat.Prelude
 
-import Cat.Allegory.Reasoning as Ar
+import Cat.Allegory.Morphism
 ```
 -->
 
@@ -20,28 +20,32 @@ some category of "sets and relations", to recover the associated
 category of "sets and functions". So, let's start by thinking about $\Rel$!
 
 If you have a relation $R \mono A \times B$, when does it correspond to
-a function $A \to B$? Well, it must definitely be _functional_: if we
+a function $A \to B$? Well, it must definitely be [functional]: if we
 want $R(x, y)$ to represent "$f(x) = y$", then surely if $R(x, y) \land
 R(x, z)$, we must have $y = z$. In allegorical language, we would say
 $RR^o \le \id$, which we can calculate to mean (in $\Rel$) that, for
 all $x, y$,
 
+[functional]: Cat.Allegory.Morphism.html#functional-morphisms
+
 $$
 (\exists z, R(z, x) \land R(z, y)) \to (x = y)\text{.}
 $$
 
-It must also be an _entire_ relation: Every $x$ must at least one $y$ it
+It must also be an [entire] relation: Every $x$ must at least one $y$ it
 is related to, and by functionality, _exactly_ one $y$ it is related to.
 This is the "value of" the function at $y$.
 
+[entire]: Cat.Allegory.Morphism.html#entire-morphisms
+
 ```agda
 module _ {o ℓ h} (A : Allegory o ℓ h) where
-  open Allegory A
+  open Cat.Allegory.Morphism A
   record is-map x y (f : Hom x y) : Type h where
     constructor mapping
     field
-      functional : f ∘ f † ≤ id
-      entire     : id ≤ f † ∘ f
+      functional : is-functional f
+      entire     : is-entire f
 
 module _ {o ℓ h} {A : Allegory o ℓ h} where
   open Allegory A
@@ -87,7 +91,7 @@ arbitrary relations).
 
 ```agda
 module _ {o ℓ h} (A : Allegory o ℓ h) where
-  private module A = Ar A
+  private module A = Cat.Allegory.Morphism A
   open is-map
   open Precategory hiding (_∘_ ; id)
   open A using (_† ; _∘_ ; id ; _◀_ ; _▶_)
@@ -106,21 +110,12 @@ using those words.
 
 ```agda
   Maps[_] .Precategory.id = A.id , mapping
-    (subst (A._≤ id) (sym (A.idl _ ∙ dual-id A)) A.≤-refl)
-    (subst (id A.≤_) (sym (A.idr _ ∙ dual-id A)) A.≤-refl)
-
-  Maps[_] .Precategory._∘_ (f , m) (g , m′) = f A.∘ g , mapping
-    ( (f ∘ g) ∘ (f ∘ g) †     A.=⟨ A.†-inner refl ⟩
-      f ∘ (g ∘ g †) ∘ f †     A.≤⟨ f ▶ m′ .functional ◀ f † ⟩
-      f ∘ id ∘ f †            A.=⟨ A.refl⟩∘⟨ A.idl _ ⟩
-      f ∘ f †                 A.≤⟨ m .functional ⟩
-      id                      A.≤∎ )
-    ( id                   A.≤⟨ m′ .entire ⟩
-      g † ∘ g              A.=⟨ ap (g † ∘_) (sym (A.idl _)) ⟩
-      g † ∘ id ∘ g         A.≤⟨ g † ▶ m .entire ◀ g ⟩
-      g † ∘ (f † ∘ f) ∘ g  A.=⟨ A.pulll (A.pulll (sym A.dual-∘)) ∙ A.pullr refl ⟩
-      (f ∘ g) † ∘ (f ∘ g)  A.≤∎ )
-
+    A.functional-id
+    A.entire-id
+  Maps[_] .Precategory._∘_ (f , m) (g , m′) =
+    f A.∘ g , mapping
+      (A.functional-∘ (m .functional) (m′ .functional))
+      (A.entire-∘ (m .entire) (m′ .entire))
   Maps[_] .idr f = Σ-prop-path (λ _ → hlevel 1) (A.idr _)
   Maps[_] .idl f = Σ-prop-path (λ _ → hlevel 1) (A.idl _)
   Maps[_] .assoc f g h = Σ-prop-path (λ _ → hlevel 1) (A.assoc _ _ _)
diff --git a/src/Cat/Allegory/Morphism.lagda.md b/src/Cat/Allegory/Morphism.lagda.md
index a045f3ac2..10b81626c 100644
--- a/src/Cat/Allegory/Morphism.lagda.md
+++ b/src/Cat/Allegory/Morphism.lagda.md
@@ -1,9 +1,11 @@
 <!--
 ```agda
 open import Cat.Allegory.Base
+import Cat.Diagram.Idempotent
 open import Cat.Prelude
 
 import Cat.Allegory.Reasoning
+import Cat.Diagram.Idempotent
 ```
 -->
 
@@ -14,6 +16,7 @@ module Cat.Allegory.Morphism {o ℓ ℓ'} (A : Allegory o ℓ ℓ') where
 <!--
 ```agda
 open Cat.Allegory.Reasoning A public
+open Cat.Diagram.Idempotent cat public
 
 private variable
   w x y z : Ob
@@ -100,7 +103,7 @@ symmetric-id {x = x} = subst (id {x} ≤_) (sym $ dual-id A) (≤-refl {f = id {
 ```
 
 The composition of symmetric morphisms $f$ and $g$ is symmetric if
-$g \circ f \le f \circ g$.
+$gf \le fg$.
 
 ```agda
 symmetric-∘
@@ -145,7 +148,7 @@ symmetric→self-dual f-sym =
 
 # Transitive Morphisms
 
-A morphism $f : X \to X$ is **transitive** if $f \circ f \le f$.
+A morphism $f : X \to X$ is **transitive** if $ff \le f$.
 
 ```agda
 is-transitive : Hom x x → Type _
@@ -160,7 +163,7 @@ transitive-id = ≤-eliml ≤-refl
 ```
 
 The composition of two transitive morphisms $f$ and $g$ is transitive
-if $g \circ f \le f \circ g$.
+if $gf \le fg$.
 
 ```agda
 transitive-∘
@@ -174,7 +177,7 @@ transitive-∘ {f = f} {g = g} f-trans g-trans w =
 ```
 
 A useful little lemma is that if $f$ is transitive, then
-$(f \cap g) \circ (f \cap h) \le f$.
+$(f \cap g)(f \cap h) \le f$.
 
 ```agda
 transitive-∩l : is-transitive f → (f ∩ g) ∘ (f ∩ h) ≤ f
@@ -206,7 +209,7 @@ transitive-dual {f = f} f-trans =
 
 # Cotransitive Morphisms
 
-A morphism $f : X \to X$ is **cotransitive** if $f \le f \circ f$.
+A morphism $f : X \to X$ is **cotransitive** if $f \le ff$.
 
 ::: warning
 **Warning**: There is another notion of cotransitive relation, which
@@ -231,7 +234,7 @@ cotransitive-id = ≤-introl ≤-refl
 ```
 
 The composition of two cotransitive morphisms $f$ and $g$ is cotransitive
-if $f \circ g \le g \circ f$.
+if $fg \le gf$.
 
 ```agda
 cotransitive-∘
@@ -245,7 +248,7 @@ cotransitive-∘ {f = f} {g = g} f-cotrans g-cotrans w =
 ```
 
 If the intersection of $f$ and $g$ is cotransitive, then
-$f \cap g \le f \circ g$.
+$f \cap g \le fg$.
 
 ```agda
 cotransitive-∩-∘
@@ -331,6 +334,7 @@ coreflexive-≤ w g-corefl = ≤-trans w g-corefl
 ```
 
 If $f$ is coreflexive, then it is transitive, cotransitive, and symmetric.
+Coreflexive morphisms are also anti-symmetric, see `coreflexive→antisymmetric`{.Agda}.
 
 ```agda
 coreflexive→transitive
@@ -355,6 +359,16 @@ coreflexive→symmetric {f = f} f-corefl =
   id ∘ f † ∘ id =⟨ idl _ ∙ idr _ ⟩
   f † ≤∎
 ```
+
+As coreflexive morphisms are both transitive ($ff \le f$) and
+cotransitive ($f \le ff$), they are idempotent.
+
+```agda
+coreflexive→idempotent : is-coreflexive f → is-idempotent f
+coreflexive→idempotent f-corefl =
+  ≤-antisym (coreflexive→transitive f-corefl) (coreflexive→cotransitive f-corefl)
+```
+
 Furthermore, composition of coreflexive morphisms is equivalent to
 intersection.
 
@@ -376,10 +390,112 @@ coreflexive-∘-∩ {f = f} {g = g} f-corefl g-corefl =
       coreflexive-∩ f-corefl g-corefl
 ```
 
-## Domains
+This has a useful corollary: coreflexive morphisms always commute!
+
+```agda
+coreflexive-comm
+  : ∀ {x} {f g : Hom x x}
+  → is-coreflexive f → is-coreflexive g
+  → f ∘ g ≡ g ∘ f
+coreflexive-comm f-corefl g-corefl =
+  coreflexive-∘-∩ f-corefl g-corefl
+  ·· ∩-comm
+  ·· sym (coreflexive-∘-∩ g-corefl f-corefl)
+```
+
+# Functional Morphisms
+
+A morphism $$ is **functional** when $ff^o \le id$. In $\Rel$, these
+are the relations $R \mono X \times Y$ such that every $x$ is related to
+at most one $y$. To see this, note that $RR^o(y,y')$ is defined as
+$\exists (x : X). R(x,y) \times R(x,y')$. Therefore,
+$RR^o(y,y') \subseteq y = y'$ means that if there exists any $x$ such that
+$R(x,y)$ and $R(x,y')$, then $y$ and $y'$ must be equal. Put more plainly,
+every $x$ is related to at most one $y$!
+
+```agda
+is-functional : Hom x y → Type _
+is-functional f = f ∘ f † ≤ id
+```
+
+First, a useful lemma: coreflexive morphisms are always functional.
+
+```agda
+coreflexive→functional : is-coreflexive f → is-functional f
+coreflexive→functional f-corefl =
+  coreflexive-∘ f-corefl (coreflexive-dual f-corefl)
+```
+
+This immediately implies that the identity morphism is functional.
+
+```agda
+functional-id : is-functional (id {x})
+functional-id = coreflexive→functional coreflexive-id
+```
+
+Functional morphisms are closed under composition and intersection.
+
+```agda
+functional-∘ : is-functional f → is-functional g → is-functional (f ∘ g)
+functional-∘ {f = f} {g = g} f-func g-func =
+  (f ∘ g) ∘ (f ∘ g) † ≤⟨ †-cancel-inner g-func ⟩
+  f ∘ f †             ≤⟨ f-func ⟩
+  id                  ≤∎
+
+functional-∩ : is-functional f → is-functional g → is-functional (f ∩ g)
+functional-∩ {f = f} {g = g} f-func g-func =
+  (f ∩ g) ∘ (f ∩ g) †                       =⟨ ap ((f ∩ g) ∘_) (dual-∩ A) ⟩
+  (f ∩ g) ∘ (f † ∩ g †)                     ≤⟨ ∩-distrib ⟩
+  (f ∘ f † ∩ g ∘ f †) ∩ (f ∘ g † ∩ g ∘ g †) ≤⟨ ∩-pres ∩-le-l ∩-le-r ⟩
+  f ∘ f † ∩ g ∘ g †                         ≤⟨ ∩-pres f-func g-func ⟩
+  id ∩ id                                   =⟨ ∩-idempotent ⟩
+  id                                        ≤∎
+```
+
+# Entire Morphisms
+
+A morphism is **entire** when $id \le f^of$. In $\Rel$, these are the
+relations $R \mono X \times Y$ where each $x$ must be related to at least
+one $y$. To see this, recall that $R^oR(x,x')$ is defined as
+$\exists (y : Y). R(x,y) \times R(x',y)$. If $x = x' \subseteq R^oR(x,x')$,
+then we can reduce this statement down to $\forall (x : X). \exists (y : Y). R(x,y)$.
+
+
+```agda
+is-entire : Hom x y → Type _
+is-entire f = id ≤ f † ∘ f
+```
+
+Reflexive morphisms are always entire.
+
+```agda
+reflexive→entire : is-reflexive f → is-entire f
+reflexive→entire f-refl =
+  reflexive-∘ (reflexive-dual f-refl) f-refl
+```
+
+From this, we can deduce that the identity morphism is entire.
+
+```agda
+entire-id : is-entire (id {x})
+entire-id = reflexive→entire reflexive-id
+```
+
+Entire morphisms are closed under composition.
+
+```agda
+entire-∘ : is-entire f → is-entire g → is-entire (f ∘ g)
+entire-∘ {f = f} {g = g} f-entire g-entire =
+  id                  ≤⟨ g-entire ⟩
+  g † ∘ g             ≤⟨ g † ▶ ≤-introl f-entire ⟩
+  g † ∘ (f † ∘ f) ∘ g =⟨ extendl (pulll (sym dual-∘)) ⟩
+  (f ∘ g) † ∘ (f ∘ g) ≤∎
+```
+
+# Domains
 
 The domain of a morphism $f : X \to Y$ is defined as
-$id \cap (f^o \circ f)$, denoted $\rm{dom}(f)$.
+$id \cap (f^of)$, denoted $\rm{dom}(f)$.
 In $\Rel$, the domain of a relation $R : X \times Y \to \Omega$ is a
 relation $X \times X \to \Omega$ that relates two elements $x, x' : X$
 whenever $x = x'$, and $R(x,y)$ for some $y$.
@@ -396,9 +512,28 @@ domain-coreflexive : ∀ (f : Hom x y) → is-coreflexive (domain f)
 domain-coreflexive f = ∩-le-l
 ```
 
+<!--
+```agda
+domain-elimr : f ∘ domain g ≤ f
+domain-elimr = ≤-elimr (domain-coreflexive _)
+
+domain-eliml : domain f ∘ g ≤ g
+domain-eliml = ≤-eliml (domain-coreflexive _)
+
+domain-idempotent : is-idempotent (domain f)
+domain-idempotent = coreflexive→idempotent (domain-coreflexive _)
+
+domain-dual : domain f † ≡ domain f
+domain-dual = sym (symmetric→self-dual (coreflexive→symmetric (domain-coreflexive _)))
+
+domain-comm : domain f ∘ domain g ≡ domain g ∘ domain f
+domain-comm = coreflexive-comm (domain-coreflexive _) (domain-coreflexive _)
+```
+-->
+
 Furthermore, the domain enjoys the following universal property:
 Let $f : X \to Y$ and $g : X \to X$ such that $g$ is coreflexive.
-Then $\rm{dom}(f) \le g$ if and only if $f \le f \circ g$.
+Then $\rm{dom}(f) \le g$ if and only if $f \le fg$.
 
 ```agda
 domain-universalr : is-coreflexive g → domain f ≤ g → f ≤ f ∘ g
@@ -418,6 +553,16 @@ domain-universall {g = g} {f = f} g-corefl w =
   g                        ≤∎
 ```
 
+This has a nice corollary: $f\rm{dom}(f) = f$.
+
+```agda
+domain-absorb : ∀ (f : Hom x y) → f ∘ domain f ≡ f
+domain-absorb f =
+  ≤-antisym
+    domain-elimr
+    (domain-universalr (domain-coreflexive f) ≤-refl)
+```
+
 We can nicely characterize the domain of an intersection.
 
 ```agda
@@ -441,8 +586,7 @@ domain-∩ {f = f} {g = g} = ≤-antisym ≤-to ≤-from where
     id ∩ (f ∩ g) † ∘ (f ∩ g)                   ≤∎
 ```
 
-Furthermore, the domain of $f \circ g$ is contained in the domain of
-$g$.
+Furthermore, the domain of $fg$ is contained in the domain of $g$.
 
 ```agda
 domain-∘ : domain (f ∘ g) ≤ domain g
@@ -465,6 +609,111 @@ domain-id : domain (id {x}) ≡ id
 domain-id = ≤-antisym ∩-le-l (∩-univ ≤-refl (≤-introl symmetric-id))
 ```
 
+Characterizing composition of domains is somewhat more difficult,
+though it is possible. Namely, we shall show the following:
+
+$$\rm{dom}(f\rm{dom}(g)) = \rm{dom}(f)\rm{dom}(g)$$
+
+```agda
+domain-smashr
+  : ∀ (f : Hom x z) (g : Hom x y)
+  → domain (f ∘ domain g) ≡ domain f ∘ domain g
+domain-smashr f g = ≤-antisym ≤-to ≤-from where
+```
+
+We begin by noting that the composition $\rm{dom}(f)\rm{dom}(g)$
+is coreflexive.
+
+```agda
+  fg-corefl : is-coreflexive (domain f ∘ domain g)
+  fg-corefl = coreflexive-∘ (domain-coreflexive f) (domain-coreflexive g)
+```
+
+To show the forward direction, we can apply the universal property of
+domains to transform the goal into
+
+$$f\rm{dom}(g) \le (f\rm{dom}(g))(\rm{dom}(f)\rm{dom}(g))$$
+
+We can then solve this goal by repeatedly appealing to the fact that
+domains are coreflexive.
+
+```agda
+  ≤-to : domain (f ∘ domain g) ≤ domain f ∘ domain g
+  ≤-to =
+    domain-universall fg-corefl $
+    f ∘ domain g                           =˘⟨ ap₂ _∘_ (domain-absorb f) domain-idempotent ⟩
+    (f ∘ domain f) ∘ (domain g ∘ domain g) =⟨ extendl (extendr domain-comm) ⟩
+    (f ∘ domain g) ∘ (domain f ∘ domain g) ≤∎
+```
+
+To show the reverse direction, we apply the universal property of the
+intersection, reducing the goal to
+
+$$\rm{dom}(f)\rm{dom}(g) \le (f\rm{dom}(g))^of\rm{dom}(g)$$
+
+We then solve the goal by an extended series of appeals to the
+coreflexivity of domains.
+
+```agda
+  ≤-from : domain f ∘ domain g ≤ domain (f ∘ domain g)
+  ≤-from = ∩-univ fg-corefl $
+    domain f ∘ domain g               =˘⟨ ap (domain f ∘_) domain-idempotent ⟩
+    domain f ∘ domain g ∘ domain g    =⟨ extendl domain-comm ⟩
+    domain g ∘ domain f ∘ domain g    =⟨ ap (_∘ domain f ∘ domain g) (sym domain-dual) ⟩
+    domain g † ∘ domain f ∘ domain g  ≤⟨ domain g † ▶ ∩-le-r ◀ domain g ⟩
+    domain g † ∘ (f † ∘ f) ∘ domain g =⟨ extendl (pulll (sym dual-∘)) ⟩
+    (f ∘ domain g) † ∘ f ∘ domain g   ≤∎
+```
+
+We can also characterize postcomposition by a domain, though this
+is restricted to an inequality in the general case.
+
+```agda
+domain-swapl
+  : ∀ (f : Hom y z) (g : Hom x y)
+  → domain f ∘ g ≤ g ∘ domain (f ∘ g)
+domain-swapl f g =
+  (id ∩ (f † ∘ f)) ∘ g             ≤⟨ ∩-distribr ⟩
+  (id ∘ g ∩ (f † ∘ f) ∘ g)         =⟨ ap₂ _∩_ id-comm-sym (sym (assoc (f †) f g)) ⟩
+  (g ∘ id ∩ f † ∘ f ∘ g)           ≤⟨ modular id g (f † ∘ f ∘ g) ⟩
+  g ∘ (id ∩ ⌜ g † ∘ f † ∘ f ∘ g ⌝) =⟨ ap! (pulll (sym dual-∘)) ⟩
+  g ∘ (id ∩ (f ∘ g) † ∘ (f ∘ g))   ≤∎
+```
+
+We can strengthen this to an equality when $g$ is functional.
+
+```agda
+domain-swap
+  : ∀ (f : Hom y z) (g : Hom x y)
+  → is-functional g
+  → domain f ∘ g ≡ g ∘ domain (f ∘ g)
+domain-swap f g w =
+  ≤-antisym (domain-swapl f g) $
+  g ∘ (id ∩ (f ∘ g) † ∘ (f ∘ g))   ≤⟨ ∩-distribl ⟩
+  g ∘ id ∩ g ∘ (f ∘ g) † ∘ (f ∘ g) ≤⟨ ∩-pres-r (≤-extendl (†-pulll w)) ⟩
+  g ∘ id ∩ id ∘ f † ∘ f ∘ g        =⟨ ap₂ _∩_ id-comm (idl _) ⟩
+  id ∘ g ∩ f † ∘ f ∘ g             ≤⟨ modular′ g id (f † ∘ f ∘ g) ⟩
+  (id ∩ (f † ∘ f ∘ g) ∘ g †) ∘ g   ≤⟨ ∩-pres-r (≤-pullr (≤-cancelr w)) ◀ g ⟩
+  (id ∩ f † ∘ f) ∘ g ≤∎
+```
+
+We also note that domains are always functional.
+
+```agda
+domain-functional : (f : Hom x y) → is-functional (domain f)
+domain-functional f = coreflexive→functional (domain-coreflexive f)
+```
+
+The domain of an entire morphism is the identity.
+
+```agda
+domain-entire : is-entire f → domain f ≡ id
+domain-entire f-entire =
+  ≤-antisym
+    (domain-coreflexive _)
+    (∩-univ ≤-refl f-entire)
+```
+
 # Antisymmetric Morphisms
 
 A morphism is **anti-symmetric** if $f \cap f^o \le id$.
@@ -504,3 +753,13 @@ reflexive+antisymmetric→diagonal
 reflexive+antisymmetric→diagonal f-refl f-antisym =
   ≤-antisym f-antisym (reflexive→diagonal f-refl)
 ```
+
+If $f$ is coreflexive, then it is anti-symmetric.
+
+```agda
+coreflexive→antisymmetric : is-coreflexive f → is-antisymmetric f
+coreflexive→antisymmetric {f = f} f-corefl =
+  f ∩ f † ≤⟨ ∩-pres f-corefl (coreflexive-dual f-corefl) ⟩
+  id ∩ id =⟨ ∩-idempotent ⟩
+  id ≤∎
+```
diff --git a/src/Cat/Allegory/Reasoning.lagda.md b/src/Cat/Allegory/Reasoning.lagda.md
index 26355c4d6..ac35dbc85 100644
--- a/src/Cat/Allegory/Reasoning.lagda.md
+++ b/src/Cat/Allegory/Reasoning.lagda.md
@@ -32,7 +32,7 @@ inequality, and rewriting by an equality:
 ```agda
 private variable
   w x y z : Ob
-  a b c d f f′ g g′ h : Hom x y
+  a b c d f f′ g g′ h i : Hom x y
 
 _≤⟨_⟩_ : ∀ (f : Hom x y) → f ≤ g → g ≤ h → f ≤ h
 _=⟨_⟩_ : ∀ (f : Hom x y) → f ≡ g → g ≤ h → f ≤ h
@@ -72,6 +72,7 @@ ordering in both of its arguments.
 ∩-pres     : f ≤ f′ → g ≤ g′ → f ∩ g ≤ f′ ∩ g′
 ∩-distribl   : f ∘ (g ∩ h) ≤ (f ∘ g) ∩ (f ∘ h)
 ∩-distribr   : (g ∩ h) ∘ f ≤ (g ∘ f) ∩ (h ∘ f)
+∩-distrib   : (f ∩ g) ∘ (h ∩ i) ≤ (f ∘ h ∩ g ∘ h) ∩ (f ∘ i ∩ g ∘ i)
 ∩-assoc      : (f ∩ g) ∩ h ≡ f ∩ (g ∩ h)
 ∩-comm       : f ∩ g ≡ g ∩ f
 ∩-idempotent : f ∩ f ≡ f
@@ -84,6 +85,7 @@ ordering in both of its arguments.
 ∩-pres w v = ∩-univ (≤-trans ∩-le-l w) (≤-trans ∩-le-r v)
 ∩-distribl = ∩-univ (_ ▶ ∩-le-l) (_ ▶ ∩-le-r)
 ∩-distribr = ∩-univ (∩-le-l ◀ _) (∩-le-r ◀ _)
+∩-distrib = ≤-trans ∩-distribl (∩-pres ∩-distribr ∩-distribr)
 ∩-assoc = ≤-antisym
   (∩-univ (≤-trans ∩-le-l ∩-le-l)
           (∩-univ (≤-trans ∩-le-l ∩-le-r) ∩-le-r))
@@ -109,12 +111,6 @@ modular′ f g h =
   (g ∩ h ∘ f †) ∘ f               ≤∎
 ```
 
-```agda
-†-inner : (p : g ∘ g′ † ≡ h) → (f ∘ g) ∘ (f′ ∘ g′) † ≡ f ∘ h ∘ f′ †
-†-inner p = ap₂ _∘_ refl dual-∘ ∙ sym (assoc _ _ _)
-          ∙ ap₂ _∘_ refl (assoc _ _ _ ∙ ap₂ _∘_ p refl)
-```
-
 ## Identities
 
 ```agda
@@ -193,6 +189,17 @@ abstract
   ≤-extend-inner w = ≤-extendr (≤-extendl w)
 ```
 
+## Cancellations
+
+```agda
+  ≤-cancell : a ∘ b ≤ id → a ∘ b ∘ f ≤ f
+  ≤-cancell w = ≤-trans (≤-pulll w) (≤-eliml ≤-refl)
+
+  ≤-cancelr : a ∘ b ≤ id → (f ∘ a) ∘ b ≤ f
+  ≤-cancelr w = ≤-trans (≤-pullr w) (≤-elimr ≤-refl)
+```
+
+
 ## Duals
 
 ```agda
@@ -202,4 +209,29 @@ abstract
     (id ∘ f) ∩ f         ≤⟨ modular′ f id f ⟩
     (id ∩ (f ∘ f †)) ∘ f ≤⟨ ≤-pushl ∩-le-r ⟩
     f ∘ f † ∘ f ≤∎
+
+  †-pulll : a ∘ b † ≤ c → a ∘ (f ∘ b) † ≤ c ∘ f †
+  †-pulll {a = a} {b = b} {c = c} {f = f} w =
+    a ∘ (f ∘ b) † =⟨ ap (a ∘_) dual-∘ ⟩
+    a ∘ b † ∘ f † ≤⟨ ≤-pulll w ⟩
+    c ∘ f † ≤∎
+
+  †-pullr : a † ∘ b ≤ c → (a ∘ f) † ∘ b ≤ f † ∘ c
+  †-pullr {a = a} {b = b} {c = c} {f = f} w =
+    (a ∘ f) † ∘ b =⟨ ap (_∘ b) dual-∘ ⟩
+    (f † ∘ a †) ∘ b ≤⟨ ≤-pullr w ⟩
+    f † ∘ c ≤∎
+
+  †-inner : (p : g ∘ g′ † ≡ h) → (f ∘ g) ∘ (f′ ∘ g′) † ≡ f ∘ h ∘ f′ †
+  †-inner p = ap₂ _∘_ refl dual-∘ ∙ sym (assoc _ _ _)
+            ∙ ap₂ _∘_ refl (assoc _ _ _ ∙ ap₂ _∘_ p refl)
+
+  †-cancell : a ∘ b † ≤ id → a ∘ (f ∘ b) † ≤ f †
+  †-cancell w = ≤-trans (†-pulll w) (≤-eliml ≤-refl)
+
+  †-cancelr : a † ∘ b ≤ id → (a ∘ f) † ∘ b ≤ f †
+  †-cancelr w = ≤-trans (†-pullr w) (≤-elimr ≤-refl)
+
+  †-cancel-inner : a ∘ b † ≤ id → (f ∘ a) ∘ (g ∘ b) † ≤ f ∘ g †
+  †-cancel-inner w = †-pulll (≤-cancelr w)
 ```
diff --git a/src/Cat/Restriction/Base.lagda.md b/src/Cat/Restriction/Base.lagda.md
new file mode 100644
index 000000000..cf126f4ec
--- /dev/null
+++ b/src/Cat/Restriction/Base.lagda.md
@@ -0,0 +1,100 @@
+<!--
+```agda
+open import Cat.Prelude
+import Cat.Reasoning
+```
+-->
+
+```agda
+module Cat.Restriction.Base where
+```
+
+# Restriction Categories
+
+Much of computer science involves the study of partial functions.
+Unfortunately, partial functions are somewhat tedious to work with,
+as they aren't really functions; they're relations! Furthermore,
+we are often interested in *computable* partial functions; this means that
+we can not identify partial functions $A \rightharpoonup B$ with total functions
+$A \to \rm{Maybe}(B)$[^1]. This leaves us with a few possible approaches.
+The most first approach that may come to mind is to encode partial functions
+$A \rightharpoonup B$ as total functions from a subobject $X \mono A$.
+Alternatively, we could find some construction that classifies
+partial maps; this is what the naive `Maybe` approach attempted to do.
+We could also just work with functional relations directly, though this
+is ill-advised.
+
+<!--[TODO: Reed M, 05/08/2023] Link to approaches once formalized -->
+
+[^1]: We can easily determine if functions into `Maybe` "diverge"
+by checking if they return `nothing`. If we identify partial functions
+with total functions into `Maybe`, we can decide if a partial function
+terminates, which is extremely uncomputable!
+
+Each of these approaches has its own benefits and drawbacks, which
+makes choosing one difficult. **Restriction categories** offer an
+alternative, algebraic approach to the problem, allowing us to neatly
+sidestep any questions about encodings.
+
+Our prototypical restriction category will be $\Par$, the category of
+sets and partial functions. The key insight is that every partial function
+$f : A \rightharpoonup B$ is defined on some domain $X \subseteq A$;
+this yields a partial function $f \downarrow : A \rightharpoonup A$
+that maps $x$ to itself iff $f(x)$ is defined. We can generalize this
+insight to an arbitrary category $\cC$ by equipping $\cC$ with an operation
+$\restrict{(-)} : \cC(x,y) \to \cC(x,x)$.
+
+-- <!-- [TODO: Reed M, 01/08/2023] Add link to partial maps -->
+
+
+```agda
+record Restriction-category
+  {o ℓ} (C : Precategory o ℓ)
+  : Type (o ⊔ ℓ) where
+  no-eta-equality
+  open Cat.Reasoning C
+  field
+    _↓ : ∀ {x y} → Hom x y → Hom x x
+
+  infix 50 _↓
+```
+
+We require that $\restrict{(-)}$ satisfies 4 axioms:
+- $f\restrict{f} = f$. In $\Par$, this corresponds to the fact that
+$\restrict{f}(x)$ is defined to be $x$ iff $f$ is defined, so
+precomposing with it does nothing.
+
+```agda
+  field
+    ↓-dom : ∀ {x y} → (f : Hom x y) → f ∘ (f ↓) ≡ f
+```
+
+- $\restrict{f}\restrict{g} = \restrict{g}\restrict{f}$. In $\Par$,
+this falls out of the fact that restriction maps do not modify their
+arguments, and it doesn't matter if $f$ diverges first or $g$ does;
+all that matters is that it diverges!
+
+```agda
+  field
+    ↓-comm : ∀ {x y z} → (f : Hom x z) (g : Hom x y) → f ↓ ∘ g ↓ ≡ g ↓ ∘ f ↓
+```
+
+- $\restrict{(g\restrict{f})} = \restrict{g}\restrict{f}$. This axiom
+holds in the $\Par$, as $\restrict{(g\restrict{f})}(x)$ ignores the
+action of $g$ on $x$, and focuses only on its termination.
+
+```agda
+  field
+    ↓-smashr : ∀ {x y z} → (f : Hom x z) (g : Hom x y) → (g ∘ f ↓) ↓ ≡ g ↓ ∘ f ↓
+```
+
+- $\restrict{f} g = g  \restrict{(f g)}$. This is the trickiest of the
+bunch to understand in $\Par$. Note that if we postcompose $g$ with a
+domain map $\restrict{f}$, then we still need to take into account the
+action of $g$; furthermore, its domain of definition needs to be
+restricted to image of $g$.
+
+```agda
+  field
+    ↓-swap : ∀ {x y z} → (f : Hom y z) (g : Hom x y) → f ↓ ∘ g ≡ g ∘ (f ∘ g) ↓
+```
diff --git a/src/Cat/Restriction/Functor.lagda.md b/src/Cat/Restriction/Functor.lagda.md
new file mode 100644
index 000000000..7309d7668
--- /dev/null
+++ b/src/Cat/Restriction/Functor.lagda.md
@@ -0,0 +1,148 @@
+<!--
+```agda
+open import Cat.Restriction.Base
+open import Cat.Prelude
+
+import Cat.Restriction.Reasoning
+```
+-->
+
+```agda
+module Cat.Restriction.Functor where
+```
+
+<!--
+```agda
+open Functor
+```
+-->
+
+# Restriction Functors
+
+A functor $F : \cC \to \cD$ between [restriction categories] is a
+**restriction functor** if $F (\restrict{f}) = \restrict{(F f)}$.
+
+[restriction categories]: Cat.Restriction.Base.html
+
+```agda
+is-restriction-functor
+  : ∀ {oc ℓc od ℓd} {C : Precategory oc ℓc} {D : Precategory od ℓd}
+  → (F : Functor C D)
+  → (C↓ : Restriction-category C)
+  → (D↓ : Restriction-category D)
+  → Type _
+is-restriction-functor {C = C} {D = D} F C↓ D↓ =
+  ∀ {x y} (f : C.Hom x y) → F .F₁ (f C.↓) ≡ (F .F₁ f D.↓)
+  where
+    module C = Cat.Restriction.Reasoning C↓
+    module D = Cat.Restriction.Reasoning D↓
+```
+
+The identity functor is a restriction functor, and restriction functors
+are closed under composition.
+
+```agda
+Id-restriction
+  : ∀ {oc ℓc} {C : Precategory oc ℓc} {C↓ : Restriction-category C}
+  → is-restriction-functor Id C↓ C↓
+Id-restriction f = refl
+
+F∘-restriction
+  : ∀ {oc ℓc od ℓd oe ℓe}
+  → {C : Precategory oc ℓc} {D : Precategory od ℓd} {E : Precategory oe ℓe}
+  → {C↓ : Restriction-category C}
+  → {D↓ : Restriction-category D}
+  → {E↓ : Restriction-category E}
+  → (F : Functor D E) (G : Functor C D)
+  → is-restriction-functor F D↓ E↓ → is-restriction-functor G C↓ D↓
+  → is-restriction-functor (F F∘ G) C↓ E↓
+F∘-restriction F G F↓ G↓ f = ap (F .F₁) (G↓ f) ∙ F↓ (G .F₁ f)
+```
+
+# Properties of Restriction Functors
+
+Let $F : \cC \to \cD$ be a restriction functor. Note that $F$ preserves
+[total morphisms] and [restriction idempotents].
+
+[total morphisms]: Cat.Restriction.Reasoning.html#total-morphisms
+[restriction idempotents]: Cat.Restriction.Reasoning.html#restriction-idempotents
+
+<!--
+```agda
+module is-restriction-functor
+  {oc ℓc od ℓd} {C : Precategory oc ℓc} {D : Precategory od ℓd}
+  (F : Functor C D)
+  (C↓ : Restriction-category C)
+  (D↓ : Restriction-category D)
+  (F↓ : is-restriction-functor F C↓ D↓)
+  where
+  private
+    module C = Cat.Restriction.Reasoning C↓
+    module D = Cat.Restriction.Reasoning D↓
+```
+-->
+
+```agda
+  F-total : ∀ {x y} {f : C.Hom x y} → C.is-total f → D.is-total (F .F₁ f)
+  F-total {f = f} f-total = sym (F↓ f) ·· ap (F .F₁) f-total ·· F .F-id
+
+  F-restrict-idem
+    : ∀ {x} {f : C.Hom x x}
+    → C.is-restriction-idempotent f
+    → D.is-restriction-idempotent (F .F₁ f)
+  F-restrict-idem {f = f} f-ridem =
+    F .F₁ f D.↓   ≡˘⟨ F↓ f ⟩
+    F .F₁ (f C.↓) ≡⟨ ap (F .F₁) f-ridem ⟩
+    F .F₁ f ∎
+```
+
+Furthermore, if $g$ refines $f$, then $F(g)$ refines $F(f)$.
+
+```agda
+  F-≤ : ∀ {x y} {f g : C.Hom x y} → f C.≤ g → (F .F₁ f) D.≤ (F .F₁ g)
+  F-≤ {f = f} {g = g} f≤g =
+    F .F₁ g D.∘ F .F₁ f D.↓   ≡⟨ ap (F .F₁ g D.∘_) (sym (F↓ f)) ⟩
+    F .F₁ g D.∘ F .F₁ (f C.↓) ≡⟨ sym (F .F-∘ g (f C.↓)) ⟩
+    F .F₁ (g C.∘ f C.↓) ≡⟨ ap (F .F₁) f≤g ⟩
+    F .F₁ f ∎
+```
+
+Restriction functors also preserve restricted isomorphisms.
+
+```agda
+  F-restricted-inverses
+    : ∀ {x y} {f : C.Hom x y} {g : C.Hom y x}
+    → C.restricted-inverses f g
+    → D.restricted-inverses (F .F₁ f) (F .F₁ g)
+  F-restricted-inverses {f = f} {g = g} fg-inv = record
+    { ↓-invl =
+      F .F₁ f D.∘ F .F₁ g ≡˘⟨ F .F-∘ f g ⟩
+      F .F₁ (f C.∘ g)     ≡⟨ ap (F .F₁) fg-inv.↓-invl ⟩
+      F .F₁ (g C.↓)       ≡⟨ F↓ g ⟩
+      F .F₁ g D.↓         ∎
+    ; ↓-invr =
+      F .F₁ g D.∘ F .F₁ f ≡˘⟨ F .F-∘ g f ⟩
+      F .F₁ (g C.∘ f)     ≡⟨ ap (F .F₁) fg-inv.↓-invr ⟩
+      F .F₁ (f C.↓)       ≡⟨ F↓ f ⟩
+      F .F₁ f D.↓         ∎
+    }
+    where module fg-inv = C.restricted-inverses fg-inv
+
+  F-restricted-invertible
+    : ∀ {x y} {f : C.Hom x y}
+    → C.is-restricted-invertible f
+    → D.is-restricted-invertible (F .F₁ f)
+  F-restricted-invertible f-inv = record
+    { ↓-inv = F .F₁ f-inv.↓-inv
+    ; ↓-inverses = F-restricted-inverses f-inv.↓-inverses
+    }
+    where module f-inv = C.is-restricted-invertible f-inv
+
+  F-↓≅ : ∀ {x y} → x C.↓≅ y → F .F₀ x D.↓≅ F .F₀ y
+  F-↓≅ f = record
+    { ↓-to = F .F₁ f.↓-to
+    ; ↓-from = F .F₁ f.↓-from
+    ; ↓-inverses = F-restricted-inverses f.↓-inverses
+    }
+    where module f = C._↓≅_ f
+```
diff --git a/src/Cat/Restriction/Instances/Allegory.lagda.md b/src/Cat/Restriction/Instances/Allegory.lagda.md
new file mode 100644
index 000000000..b0abbe8c8
--- /dev/null
+++ b/src/Cat/Restriction/Instances/Allegory.lagda.md
@@ -0,0 +1,70 @@
+<!--
+```agda
+open import Cat.Allegory.Base
+open import Cat.Functor.WideSubcategory
+open import Cat.Restriction.Base
+open import Cat.Prelude
+
+import Cat.Allegory.Morphism
+```
+-->
+
+```agda
+module Cat.Restriction.Instances.Allegory where
+```
+
+# Restriction Categories from Allegories
+
+Let $\cA$ be an [allegory], considered as a sort of generalized category
+of "sets and relations". Much like we can recover a category of "sets and
+functions" via the associated [category of maps], we can recover a category
+of "sets and partial functions" by only restricting to [functional]
+relations instead of functional _and_ [entire] relations.
+
+[allegory]: Cat.Allegory.Base.html
+[category of maps]: Cat.Allegory.Maps.html
+[functional]: Cat.Allegory.Morphism.html#functional-morphisms
+[entire]: Cat.Allegory.Morphism.html#entire-morphisms
+
+<!--
+```agda
+module _ {o ℓ ℓ'} (A : Allegory o ℓ ℓ') where
+  open Cat.Allegory.Morphism A
+  open Restriction-category
+  open Wide-hom
+```
+-->
+
+```agda
+  Partial-maps-subcat : Wide-subcat {C = cat} ℓ'
+  Partial-maps-subcat .Wide-subcat.P = is-functional
+  Partial-maps-subcat .Wide-subcat.P-prop f = ≤-thin
+  Partial-maps-subcat .Wide-subcat.P-id =
+    functional-id
+  Partial-maps-subcat .Wide-subcat.P-∘ f-partial g-partial =
+    functional-∘ f-partial g-partial
+
+  Partial-maps : Precategory o (ℓ ⊔ ℓ')
+  Partial-maps = Wide Partial-maps-subcat
+```
+
+This category can be equipped with a restriction structure, defining
+$\restrict{f}$ to be the [domain] of the partial maps.
+Note that the first 3 axioms don't actually require the relation to be
+functional; it's only relevant in the converse direction of the 4th axiom!
+
+[domain]: Cat.Allegory.Morphism.html#domains
+
+```agda
+  Partial-maps-restriction : Restriction-category Partial-maps
+  Partial-maps-restriction ._↓ f .hom = domain (f .hom)
+  Partial-maps-restriction ._↓ f .witness = domain-functional (f .hom)
+  Partial-maps-restriction .↓-dom f =
+    Wide-hom-path $ domain-absorb (f .hom)
+  Partial-maps-restriction .↓-comm f g =
+    Wide-hom-path $ domain-comm
+  Partial-maps-restriction .↓-smashr f g =
+    Wide-hom-path $ domain-smashr (g .hom) (f .hom)
+  Partial-maps-restriction .↓-swap f g =
+    Wide-hom-path $ domain-swap (f .hom) (g .hom) (g .witness)
+```
diff --git a/src/Cat/Restriction/Reasoning.lagda.md b/src/Cat/Restriction/Reasoning.lagda.md
new file mode 100644
index 000000000..ac4638203
--- /dev/null
+++ b/src/Cat/Restriction/Reasoning.lagda.md
@@ -0,0 +1,525 @@
+<!--
+```agda
+open import Cat.Restriction.Base
+open import Cat.Prelude
+
+import Cat.Diagram.Idempotent
+import Cat.Reasoning
+```
+-->
+
+```agda
+module Cat.Restriction.Reasoning
+  {o ℓ} {C : Precategory o ℓ}
+  (C-restrict : Restriction-category C)
+  where
+```
+
+<!--
+```agda
+open Cat.Diagram.Idempotent C public
+open Cat.Reasoning C public
+open Restriction-category C-restrict public
+```
+-->
+
+# Reasoning in Restriction Categories
+
+This module provides some useful lemmas about restriction categories.
+We begin by noting that for every $f$, $\restrict{f}$ is an [idempotent].
+
+[idempotent]: Cat.Diagram.Idempotent.html
+
+```agda
+↓-idem : ∀ {x y} (f : Hom x y) → is-idempotent (f ↓)
+↓-idem f =
+  f ↓ ∘ f ↓   ≡˘⟨ ↓-smashr f f ⟩
+  (f ∘ f ↓) ↓ ≡⟨ ap _↓ (↓-dom f) ⟩
+  f ↓         ∎
+```
+
+Next, some useful lemmas about pre and postcomposition of a restriction
+map.
+
+```agda
+↓-cancelr : ∀ {x y z} (f : Hom y z) (g : Hom x y) → (f ∘ g) ↓ ∘ g ↓ ≡ (f ∘ g) ↓
+↓-cancelr f g =
+  (f ∘ g) ↓ ∘ g ↓   ≡˘⟨ ↓-smashr g (f ∘ g) ⟩
+  ((f ∘ g) ∘ g ↓) ↓ ≡⟨ ap _↓ (pullr (↓-dom g)) ⟩
+  (f ∘ g) ↓         ∎
+  
+
+↓-cancell : ∀ {x y z} (f : Hom y z) (g : Hom x y) → g ↓ ∘ (f ∘ g) ↓ ≡ (f ∘ g) ↓
+↓-cancell f g =
+  g ↓ ∘ (f ∘ g) ↓  ≡⟨ ↓-comm g (f ∘ g) ⟩
+  (f ∘ g) ↓ ∘ g ↓  ≡⟨ ↓-cancelr f g ⟩
+  (f ∘ g) ↓        ∎
+```
+
+We can use these to show that $\restrict{(\restrict{f}g)} = \restrict{(f \circ g)}$,
+which is somewhat hard to motivate, but ends up being a useful algebraic
+manipulation.
+
+```agda
+↓-smashl : ∀ {x y z} (f : Hom y z) (g : Hom x y) → (f ↓ ∘ g) ↓ ≡ (f ∘ g) ↓
+↓-smashl f g =
+  ((f ↓) ∘ g) ↓     ≡⟨ ap _↓ (↓-swap f g) ⟩
+  (g ∘ (f ∘ g) ↓) ↓ ≡⟨ ↓-smashr (f ∘ g) g ⟩
+  g ↓ ∘ (f ∘ g) ↓   ≡⟨ ↓-cancell f g ⟩
+  (f ∘ g) ↓ ∎
+
+↓-smash : ∀ {x y z} (f : Hom x z) (g : Hom x y) → (f ↓ ∘ g ↓) ↓ ≡ f ↓ ∘ g ↓
+↓-smash f g =
+  (f ↓ ∘ g ↓) ↓ ≡⟨ ↓-smashl f (g ↓) ⟩
+  (f ∘ g ↓) ↓   ≡⟨ ↓-smashr g f ⟩
+  f ↓ ∘ g ↓ ∎
+```
+
+Next, we note that iterating $(-)downarrow$ does nothing.
+
+```agda
+↓-join : ∀ {x y} (f : Hom x y) → (f ↓) ↓ ≡ f ↓
+↓-join f =
+  (f ↓) ↓       ≡⟨ ap _↓ (sym (↓-idem f)) ⟩
+  (f ↓ ∘ f ↓) ↓ ≡⟨ ↓-smashr f (f ↓) ⟩
+  (f ↓) ↓ ∘ f ↓ ≡⟨ ↓-comm (f ↓) f ⟩
+  f ↓ ∘ (f ↓) ↓ ≡⟨ ↓-dom (f ↓) ⟩
+  f ↓ ∎
+```
+
+## Total Morphisms
+
+We say that a morphism $f : X \to Y$ in a restriction category is **total**
+if its restriction $\restrict{f}$ is the identity morphism.
+
+```agda
+is-total : ∀ {x y} → Hom x y → Type _
+is-total f = f ↓ ≡ id
+
+record Total (x y : Ob) : Type ℓ where
+  no-eta-equality
+  field
+    mor : Hom x y
+    has-total : is-total mor
+
+open Total public
+```
+
+Being total is a proposition, so the collection of total morphisms
+forms a set.
+
+```agda
+is-total-is-prop : ∀ {x y} → (f : Hom x y) → is-prop (is-total f)
+is-total-is-prop f = Hom-set _ _ _ _
+
+Total-is-set : ∀ {x y} → is-set (Total x y)
+```
+
+<!--
+```agda
+Total-is-set = Iso→is-hlevel 2 eqv $
+  Σ-is-hlevel 2 (Hom-set _ _) λ _ →
+  Path-is-hlevel 2 (Hom-set _ _)
+  where unquoteDecl eqv = declare-record-iso eqv (quote Total)
+
+instance
+  H-Level-Total : ∀ {x y} {n} → H-Level (Total x y) (suc (suc n))
+  H-Level-Total = basic-instance 2 Total-is-set
+```
+-->
+
+
+If $f$ is [monic], then it is a total morphism.
+
+[monic]: Cat.Morphism.html#monos
+
+```agda
+monic→total : ∀ {x y} {f : Hom x y} → is-monic f → is-total f
+monic→total {f = f} monic = monic (f ↓) id (↓-dom f ∙ sym (idr _))
+```
+
+As a corollary, every isomorphism is total.
+
+```agda
+invertible→total : ∀ {x y} {f : Hom x y} → is-invertible f → is-total f
+invertible→total f-inv = monic→total (invertible→monic f-inv)
+```
+
+The identity morphism is total, as it is monic.
+
+```agda
+id-total : ∀ {x} → is-total (id {x})
+id-total = monic→total id-monic
+```
+
+Total morphisms are closed under composition.
+
+```agda
+total-∘
+  : ∀ {x y z} {f : Hom y z} {g : Hom x y}
+  → is-total f → is-total g → is-total (f ∘ g)
+total-∘ {f = f} {g = g} f-total g-total =
+  (f ∘ g) ↓   ≡˘⟨ ↓-smashl f g ⟩
+  (f ↓ ∘ g) ↓ ≡⟨ ap _↓ (eliml f-total) ⟩
+  g ↓         ≡⟨ g-total ⟩
+  id          ∎
+
+_∘Total_ : ∀ {x y z} → Total y z → Total x y → Total x z
+(f ∘Total g) .mor = f .mor ∘ g .mor 
+(f ∘Total g) .has-total = total-∘ (f .has-total) (g .has-total)
+```
+
+Furthermore, if $f \circ g$ is total, then $g$ must also be total.
+
+```agda
+total-cancell
+  : ∀ {x y z} {f : Hom y z} {g : Hom x y}
+  → is-total (f ∘ g) → is-total g
+total-cancell {f = f} {g = g} fg-total =
+  g ↓             ≡⟨ intror fg-total ⟩
+  g ↓ ∘ (f ∘ g) ↓ ≡⟨ ↓-cancell f g ⟩
+  (f ∘ g) ↓       ≡⟨ fg-total ⟩
+  id ∎
+```
+
+If $f$ is total, then $\restrict{(fg)} = \restrict{g}$.
+
+```agda
+total-smashl
+  : ∀ {x y z} {f : Hom y z} {g : Hom x y}
+  → is-total f → (f ∘ g) ↓ ≡ g ↓
+total-smashl {f = f} {g = g} f-total =
+  (f ∘ g) ↓ ≡˘⟨ ↓-smashl f g ⟩
+  (f ↓ ∘ g) ↓ ≡⟨ ap _↓ (eliml f-total) ⟩
+  g ↓ ∎
+```
+
+## Restriction Idempotents
+
+We say that a morphism $f : X \to X$ is a **restriction idempotent** if
+$\restrict{f} = f$.
+
+```agda
+is-restriction-idempotent : ∀ {x} → (f : Hom x x) → Type _
+is-restriction-idempotent f = f ↓ ≡ f
+```
+
+As the name suggests, restriction idempotents are idempotents.
+
+```agda
+restriction-idempotent→idempotent
+  : ∀ {x} {f : Hom x x}
+  → is-restriction-idempotent f → is-idempotent f
+restriction-idempotent→idempotent {f = f} f-dom =
+  f ∘ f ≡⟨ ap (f ∘_) (sym f-dom) ⟩
+  f ∘ f ↓ ≡⟨ ↓-dom f ⟩
+  f ∎
+```
+
+Furthermore, every morphism $\restrict{f}$ is a restriction idempotent.
+
+```agda
+↓-restriction-idempotent : ∀ {x y} (f : Hom x y) → is-restriction-idempotent (f ↓)
+↓-restriction-idempotent f = ↓-join f
+```
+
+If $f$ and $g$ are restriction idempotents, then they commute.
+
+```agda
+restriction-idem-comm
+  : ∀ {x} {f g : Hom x x}
+  → is-restriction-idempotent f → is-restriction-idempotent g
+  → f ∘ g ≡ g ∘ f
+restriction-idem-comm f-dom g-dom =
+  ap₂ _∘_ (sym f-dom) (sym g-dom)
+  ·· ↓-comm _ _
+  ·· ap₂ _∘_ g-dom f-dom
+```
+
+## Restricted Monics
+
+A morphism $f : X \to Y$ is a **restricted monic** if for all
+$g, h : A \to X$, $fg = fh$ implies that $\restrict{f}g = \restrict{f}h$.
+Intuitively, this is the correct notion of monic for a partial function;
+we cannot guarantee that $g$ and $h$ are equal if $fg = fh$, as $f$ may
+diverge on some inputs where $g$ and $h$ disagree.
+
+```agda
+is-restricted-monic : ∀ {x y} → Hom x y → Type _
+is-restricted-monic {x} {y} f =
+  ∀ {a} → (g h : Hom a x) → f ∘ g ≡ f ∘ h → f ↓ ∘ g ≡ f ↓ ∘ h
+```
+
+If $f$ is a total restricted monic, then $f$ is monic.
+
+```agda
+restricted-monic+total→monic
+  : ∀ {x y} {f : Hom x y}
+  → is-restricted-monic f → is-total f
+  → is-monic f
+restricted-monic+total→monic {f = f} f-rmonic f-total g1 g2 p =
+  g1       ≡⟨ introl f-total ⟩
+  f ↓ ∘ g1 ≡⟨ f-rmonic g1 g2 p ⟩
+  f ↓ ∘ g2 ≡⟨ eliml f-total ⟩
+  g2 ∎
+```
+
+Restricted monics are closed under composition.
+
+```agda
+restricted-monic-∘
+  : ∀ {x y z} {f : Hom y z} {g : Hom x y}
+  → is-restricted-monic f → is-restricted-monic g
+  → is-restricted-monic (f ∘ g)
+restricted-monic-∘ {f = f} {g = g} f-rmonic g-rmonic h1 h2 p =
+  (f ∘ g) ↓ ∘ h1         ≡⟨ pushl (sym (↓-cancell f g)) ⟩
+  g ↓ ∘ (f ∘ g) ↓ ∘ h1   ≡⟨ g-rmonic _ _ g-lemma ⟩
+  (g ↓) ∘ (f ∘ g) ↓ ∘ h2 ≡⟨ pulll (↓-cancell f g) ⟩
+  (f ∘ g) ↓ ∘ h2 ∎
+  where
+    p-assoc : f ∘ g ∘ h1 ≡ f ∘ g ∘ h2
+    p-assoc = assoc _ _ _ ·· p ·· sym (assoc _ _ _)
+
+    g-lemma : g ∘ (f ∘ g) ↓ ∘ h1 ≡ g ∘ (f ∘ g) ↓ ∘ h2
+    g-lemma =
+      g ∘ (f ∘ g) ↓ ∘ h1 ≡⟨ extendl (sym (↓-swap f g)) ⟩
+      f ↓ ∘ g ∘ h1       ≡⟨ f-rmonic _ _ p-assoc ⟩
+      f ↓ ∘ g ∘ h2       ≡⟨ extendl (↓-swap f g) ⟩
+      g ∘ (f ∘ g) ↓ ∘ h2 ∎
+```
+
+Furthermore, if $fg$ is a restricted monic and $f$ is total,
+then $g$ is a restricted monic.
+
+```agda
+restricted-monic-cancell
+  : ∀ {x y z} {f : Hom y z} {g : Hom x y}
+  → is-restricted-monic (f ∘ g)
+  → is-total f
+  → is-restricted-monic g
+restricted-monic-cancell {f = f} {g = g} fg-rmonic f-total h1 h2 p =
+  g ↓ ∘ h1           ≡⟨ ap (_∘ h1) (sym (total-smashl f-total)) ⟩
+  (f ∘ g) ↓ ∘ h1     ≡⟨ fg-rmonic h1 h2 (sym (assoc _ _ _) ·· ap (f ∘_) p ·· assoc _ _ _) ⟩
+  (f ∘ g) ↓ ∘ h2     ≡⟨ ap (_∘ h2) (total-smashl f-total) ⟩
+  g ↓ ∘ h2           ∎
+```
+
+## Restricted Retracts
+
+Let $r : X \to Y$ and $s : Y \to X$ be a pair of morphisms. The map
+$r$ is a **restricted retract** of $s$ when $rs = \restrict{s}$.
+
+```agda
+_restricted-retract-of_ : ∀ {x y} (r : Hom x y) (s : Hom y x) → Type _
+r restricted-retract-of s = r ∘ s ≡ s ↓
+
+record has-restricted-retract {x y} (s : Hom y x) : Type ℓ where
+  no-eta-equality
+  field
+    ↓-retract : Hom x y
+    is-restricted-retract : ↓-retract restricted-retract-of s
+
+open has-restricted-retract public
+```
+
+If $f$ is total and has a restricted retract, then it has a retract.
+
+```agda
+has-restricted-retract+total→has-retract
+  : ∀ {x y} {f : Hom x y}
+  → has-restricted-retract f → is-total f → has-retract f
+has-restricted-retract+total→has-retract {f = f} f-sect f-total =
+  make-retract (f-sect .↓-retract) $
+    f-sect .↓-retract ∘ f ≡⟨ f-sect .is-restricted-retract ⟩
+    f ↓                   ≡⟨ f-total ⟩
+    id                    ∎
+```
+
+If $s$ has a restricted retract, then it is a restricted mono.
+
+```agda
+has-restricted-retract→restricted-monic
+  : ∀ {x y} {f : Hom x y}
+  → has-restricted-retract f
+  → is-restricted-monic f
+has-restricted-retract→restricted-monic {f = f} f-sect g1 g2 p =
+  f ↓ ∘ g1 ≡⟨ pushl (sym $ f-sect .is-restricted-retract) ⟩
+  f-sect .↓-retract ∘ f ∘ g1 ≡⟨ ap (f-sect .↓-retract ∘_) p ⟩
+  f-sect .↓-retract ∘ f ∘ g2 ≡⟨ pulll (f-sect .is-restricted-retract) ⟩
+  f ↓ ∘ g2 ∎
+```
+
+If $f$ and $g$ have restricted retracts, then so does $fg$.
+
+```agda
+restricted-retract-∘
+  : ∀ {x y z} {f : Hom y z} {g : Hom x y}
+  → has-restricted-retract f → has-restricted-retract g
+  → has-restricted-retract (f ∘ g)
+restricted-retract-∘ {f = f} {g = g} f-sect g-sect .↓-retract =
+  g-sect .↓-retract ∘ f-sect .↓-retract
+restricted-retract-∘ {f = f} {g = g} f-sect g-sect .is-restricted-retract =
+  (g-sect .↓-retract ∘ f-sect .↓-retract) ∘ f ∘ g ≡⟨ pull-inner (f-sect .is-restricted-retract) ⟩
+  g-sect .↓-retract ∘ f ↓ ∘ g                     ≡⟨ ap (g-sect .↓-retract ∘_) (↓-swap f g) ⟩
+  g-sect .↓-retract ∘ g ∘ (f ∘ g) ↓               ≡⟨ pulll (g-sect .is-restricted-retract) ⟩
+  g ↓ ∘ (f ∘ g) ↓                                 ≡⟨ ↓-cancell f g ⟩
+  (f ∘ g) ↓                                       ∎
+```
+
+
+If $fg$ has a restricted retract and $f$ is total, then $g$ has a
+restricted retract.
+
+```agda
+has-restricted-retract-cancell
+  : ∀ {x y z} {f : Hom y z} {g : Hom x y}
+  → has-restricted-retract (f ∘ g)
+  → is-total f
+  → has-restricted-retract g
+has-restricted-retract-cancell {f = f} fg-sect f-total .↓-retract =
+  fg-sect .↓-retract ∘ f
+has-restricted-retract-cancell {f = f} {g = g} fg-sect f-total .is-restricted-retract =
+  (fg-sect .↓-retract ∘ f) ∘ g ≡⟨ sym (assoc _ _ _) ∙ fg-sect .is-restricted-retract ⟩
+  (f ∘ g) ↓                    ≡⟨ total-smashl f-total ⟩
+  g ↓ ∎
+```
+
+## Restricted Isomorphisms
+
+Let $f : X \to Y$ and $g : Y \to X$ be a pair of morphisms. $f$ and $g$
+are **restricted inverses** if $fg = \restrict{g}$ and
+$gf = \restrict{f}$. 
+
+```agda
+record restricted-inverses
+  {x y} (f : Hom x y) (g : Hom y x)
+  : Type ℓ where
+  no-eta-equality
+  field
+    ↓-invl : f ∘ g ≡ g ↓
+    ↓-invr : g ∘ f ≡ f ↓
+
+open restricted-inverses
+
+record is-restricted-invertible {x y} (f : Hom x y) : Type ℓ where
+  no-eta-equality
+  field
+    ↓-inv : Hom y x
+    ↓-inverses : restricted-inverses f ↓-inv
+
+  open restricted-inverses ↓-inverses public
+
+record _↓≅_ (x y : Ob) : Type ℓ where
+  no-eta-equality
+  field
+    ↓-to : Hom x y
+    ↓-from : Hom y x
+    ↓-inverses : restricted-inverses ↓-to ↓-from
+
+  open restricted-inverses ↓-inverses public
+
+open _↓≅_ public
+```
+
+A given morphism is a has a unique restricted inverse.
+
+```agda
+restricted-inverses-is-prop
+  : ∀ {x y} {f : Hom x y} {g : Hom y x}
+  → is-prop (restricted-inverses f g)
+restricted-inverses-is-prop x y i .↓-invl =
+  Hom-set _ _ _ _ (x .↓-invl) (y .↓-invl) i
+restricted-inverses-is-prop x y i .↓-invr =
+  Hom-set _ _ _ _ (x .↓-invr) (y .↓-invr) i
+
+is-restricted-invertible-is-prop
+   : ∀ {x y} {f : Hom x y}
+   → is-prop (is-restricted-invertible f)
+is-restricted-invertible-is-prop {f = f} g h = p where
+  module g = is-restricted-invertible g
+  module h = is-restricted-invertible h
+
+  g≡h : g.↓-inv ≡ h.↓-inv
+  g≡h =
+    g.↓-inv                                 ≡˘⟨ ↓-dom _ ⟩
+    g.↓-inv ∘ g.↓-inv ↓                     ≡⟨ ap (g.↓-inv ∘_) (sym g.↓-invl) ⟩
+    g.↓-inv ∘ f ∘ g.↓-inv                   ≡⟨ extendl (g.↓-invr ∙ sym h.↓-invr) ⟩
+    h.↓-inv ∘ ⌜ f ⌝ ∘ g.↓-inv               ≡⟨ ap! (sym (↓-dom f) ∙ ap (f ∘_) (sym h.↓-invr)) ⟩
+    h.↓-inv ∘ (f ∘ h.↓-inv ∘ f) ∘ g.↓-inv   ≡⟨ ap (h.↓-inv ∘_) (pullr (pullr g.↓-invl) ∙ pulll h.↓-invl) ⟩
+    h.↓-inv ∘ h.↓-inv ↓ ∘ g.↓-inv ↓         ≡⟨ ap (h.↓-inv ∘_) (↓-comm _ _) ⟩
+    h.↓-inv ∘ g.↓-inv ↓ ∘ h.↓-inv ↓         ≡⟨ ap (h.↓-inv ∘_) (pushl (sym g.↓-invl) ∙ pushr (pushr (sym h.↓-invl))) ⟩
+    h.↓-inv ∘ ⌜ f ∘ g.↓-inv ∘ f ⌝ ∘ h.↓-inv ≡⟨ ap! (ap (f ∘_) g.↓-invr ∙ ↓-dom f) ⟩
+    h.↓-inv ∘ f ∘ h.↓-inv                   ≡⟨ ap (h.↓-inv ∘_) (h.↓-invl)  ⟩
+    h.↓-inv ∘ h.↓-inv ↓                     ≡⟨ ↓-dom _ ⟩
+    h.↓-inv                                 ∎
+
+  p : g ≡ h
+  p i .is-restricted-invertible.↓-inv = g≡h i
+  p i .is-restricted-invertible.↓-inverses =
+    is-prop→pathp (λ i → restricted-inverses-is-prop {f = f} {g = g≡h i})
+      g.↓-inverses h.↓-inverses i
+```
+
+If $f$ and $g$ are both total and restricted inverses, then they are inverses.
+
+```agda
+restricted-inverses+total→inverses
+  : ∀ {x y} {f : Hom x y} {g : Hom y x}
+  → restricted-inverses f g
+  → is-total f
+  → is-total g
+  → Inverses f g
+restricted-inverses+total→inverses {f = f} {g = g} fg-inv f-total g-total = record
+    { invl = fg-inv .↓-invl ∙ g-total
+    ; invr = fg-inv .↓-invr ∙ f-total
+    }
+```
+
+## Refining Morphisms
+
+Let $\cC$ be a restriction category, and $f, g : \cC(X,Y)$. We say that
+$g$ **refines** $f$ if $g$ agrees with $f$ when restricted to the domain of
+$f$.
+
+```agda
+_≤_ : ∀ {x y} → Hom x y → Hom x y → Type ℓ
+f ≤ g = g ∘ f ↓ ≡ f
+```
+
+The refinement relation is reflexive, transitive, and anti-symmetric.
+
+```agda
+≤-refl : ∀ {x y} {f : Hom x y} → f ≤ f
+≤-refl {f = f} = ↓-dom f
+
+≤-trans : ∀ {x y} {f g h : Hom x y} → f ≤ g → g ≤ h → f ≤ h
+≤-trans {f = f} {g = g} {h = h} p q =
+  h ∘ ⌜ f ⌝ ↓       ≡⟨ ap! (sym p) ⟩
+  h ∘ (g ∘ (f ↓)) ↓ ≡⟨ ap (h ∘_) (↓-smashr f g) ⟩
+  h ∘ g ↓ ∘ f ↓     ≡⟨ pulll q ⟩
+  g ∘ f ↓           ≡⟨ p ⟩
+  f                 ∎
+
+≤-antisym : ∀ {x y} {f g : Hom x y} → f ≤ g → g ≤ f → f ≡ g
+≤-antisym {f = f} {g = g} p q =
+  f             ≡⟨ sym p ⟩
+  g ∘ f ↓       ≡⟨ pushl (sym q) ⟩
+  f ∘ g ↓ ∘ f ↓ ≡⟨ ap (f ∘_) (↓-comm g f) ⟩
+  f ∘ f ↓ ∘ g ↓ ≡⟨ pulll (↓-dom f) ⟩
+  f ∘ (g ↓)     ≡⟨ q ⟩
+  g ∎
+```
+
+Furthermore, composition preserves refinement.
+
+```agda
+∘-preserves-≤
+  : ∀ {x y z} {f g : Hom y z} {h i : Hom x y}
+  → f ≤ g → h ≤ i → (f ∘ h) ≤ (g ∘ i)
+∘-preserves-≤ {f = f} {g = g} {h = h} {i = i} p q =
+  (g ∘ i) ∘ ⌜ f ∘ h ⌝ ↓          ≡⟨ ap! (pushr (sym q)) ⟩
+  (g ∘ i) ∘ ((f ∘ i) ∘ (h ↓)) ↓  ≡⟨ ap ((g ∘ i) ∘_) (↓-smashr h (f ∘ i)) ⟩
+  (g ∘ i) ∘ (f ∘ i) ↓ ∘ h ↓      ≡⟨ extendr (extendl (sym (↓-swap f i))) ⟩
+  (g ∘ f ↓) ∘ (i ∘ h ↓)          ≡⟨ ap₂ _∘_ p q ⟩
+  f ∘ h                          ∎
+```
diff --git a/src/Cat/Restriction/Total.lagda.md b/src/Cat/Restriction/Total.lagda.md
new file mode 100644
index 000000000..154ab552e
--- /dev/null
+++ b/src/Cat/Restriction/Total.lagda.md
@@ -0,0 +1,64 @@
+<!--
+```agda
+open import Cat.Functor.WideSubcategory
+open import Cat.Functor.Properties
+open import Cat.Restriction.Base
+open import Cat.Prelude
+
+import Cat.Restriction.Reasoning
+```
+-->
+
+```agda
+module Cat.Restriction.Total where
+```
+
+# The Subcategory of Total Maps
+
+Let $\cC$ be a restriction category. We can construct a
+[wide subcategory] of $\cC$ containing only the [total maps] of $\cC$,
+denoted $\thecat{Total}(\cC)$.
+
+[wide subcategory]: Cat.Functor.WideSubcategory.html
+[total maps]: Cat.Restriction.Reasoning.html#total-morphisms
+
+<!--
+```agda
+module _ {o ℓ} {C : Precategory o ℓ} (C↓ : Restriction-category C) where
+  open Cat.Restriction.Reasoning C↓
+```
+-->
+
+```agda
+  Total-wide-subcat : Wide-subcat {C = C} ℓ
+  Total-wide-subcat .Wide-subcat.P = is-total
+  Total-wide-subcat .Wide-subcat.P-prop = is-total-is-prop
+  Total-wide-subcat .Wide-subcat.P-id = id-total
+  Total-wide-subcat .Wide-subcat.P-∘ = total-∘
+
+  Total-maps : Precategory o ℓ
+  Total-maps = Wide Total-wide-subcat
+```
+
+<!--
+```agda
+module _ {o ℓ} {C : Precategory o ℓ} {C↓ : Restriction-category C} where
+  open Cat.Restriction.Reasoning C↓
+```
+-->
+
+Furthermore, the injection from $\thecat{Total}(\cC)$ into $\cC$ is
+[pseudomonic], as all isomorphisms in $\cC$ are total.
+
+[pseudomonic]: Cat.Functor.Properties.html#pseudomonic-functors
+
+```agda
+
+  Forget-total : Functor (Total-maps C↓) C
+  Forget-total = Forget-wide-subcat
+
+  Forget-total-pseudomonic
+    : is-pseudomonic Forget-total
+  Forget-total-pseudomonic =
+    is-pseudomonic-Forget-wide-subcat invertible→total
+```
diff --git a/src/index.lagda.md b/src/index.lagda.md
index e3f5ef206..6eb571ae1 100644
--- a/src/index.lagda.md
+++ b/src/index.lagda.md
@@ -607,6 +607,30 @@ open import Cat.Allegory.Morphism -- Morphisms in allegories
 open import Cat.Allegory.Reasoning -- Reasoning combinators
 ```
 
+## Restriction Categories
+
+Restriction categories axiomatize categories of partial maps by adding
+n restriction operation $(-)\downarrow : \cC(X,Y) \to \cC(X,X)$ that
+takes a morphism $f$ to a subobject of the identity morphism that is
+defined precisely when $f$ is.
+
+```agda
+open import Cat.Restriction.Base
+  -- The definition
+open import Cat.Restriction.Functor
+  -- Functors between restriction categories
+open import Cat.Restriction.Reasoning
+  -- Reasoning combinators and morphism classes
+open import Cat.Restriction.Total
+  -- Categories of total maps
+```
+
+```agda
+open import Cat.Restriction.Instances.Allegory
+ -- Restriction structures on partial maps of an allegory.
+```
+
+
 ## Displayed categories
 
 A category displayed over $\cB$ is a particular concrete presentation
diff --git a/src/preamble.tex b/src/preamble.tex
index f740b178a..edacb4994 100644
--- a/src/preamble.tex
+++ b/src/preamble.tex
@@ -38,6 +38,7 @@
 \knowncat{Rings}
 \knowncat{Grp}
 \knowncat{Rel}
+\knowncat{Par}
 \knownbicat{Cat}
 \knownbicat{Topos}
 \knownbicat{Grpd}
@@ -76,6 +77,7 @@
 
 \DeclareMathOperator{\src}{src}
 \DeclareMathOperator{\tgt}{tgt}
+\newcommand{\restrict}[1]{#1^{\downarrow}}
 
 \newcommand{\NN}{\mathbb{N}}
 \newcommand{\ZZ}{\mathbb{Z}}