open import Cat.Restriction.Base
open import Cat.Prelude

import Cat.Diagram.Idempotent
import Cat.Reasoning

module Cat.Restriction.Reasoning
{o β} {C : Precategory o β}
(C-restrict : Restriction-category C)
where

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$, $f^{\downarrow}$ is an idempotent.

β-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.

β-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 $(f^{\downarrow}g)^{\downarrow} = (f \circ g)^{\downarrow}$, which is somewhat hard to motivate, but ends up being a useful algebraic manipulation.

β-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.

β-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 $f^{\downarrow}$ is the identity morphism.

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.

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)

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β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. 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. id-total : β {x} β is-total (id {x}) id-total = monicβtotal id-monic  Total morphisms are closed under composition. 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. 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 $(fg)^{\downarrow} = g^{\downarrow}$. 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 $f^{\downarrow} = f$. is-restriction-idempotent : β {x} β (f : Hom x x) β Type _ is-restriction-idempotent f = f β β‘ f  As the name suggests, restriction idempotents are idempotents. 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 $f^{\downarrow}$ is a restriction idempotent. β-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. 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 $f^{\downarrow}g = f^{\downarrow}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. 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. 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. 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. 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 = s^{\downarrow}$. _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. 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 β©β‘
id                    β


If $s$ has a restricted retract, then it is a restricted mono.

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$.

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.

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 = g^{\downarrow}$ and $gf = f^{\downarrow}$.

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.

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 β 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.

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 $\mathcal{C}$ be a restriction category, and $f, g : \mathcal{C}(X,Y)$. We say that $g$ refines $f$ if $g$ agrees with $f$ when restricted to the domain of $f$.

_β€_ : β {x y} β Hom x y β Hom x y β Type β
f β€ g = g β f β β‘ f


The refinement relation is reflexive, transitive, and anti-symmetric.

β€-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 =
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.

β-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                          β