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 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 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 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 in a restriction category is total if its restriction 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 _ _ _ _

unquoteDecl H-Level-Total = declare-record-hlevel 2 H-Level-Total (quote Total)


If 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) β©β‘
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 is total, then 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 is total, then

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 is a restriction idempotent if

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 is a restriction idempotent.

β-restriction-idempotent : β {x y} (f : Hom x y) β is-restriction-idempotent (f β)
β-restriction-idempotent f = β-join f


If and 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 is a restricted monic if for all implies that Intuitively, this is the correct notion of monic for a partial function; we cannot guarantee that and are equal if as may diverge on some inputs where and 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 is a total restricted monic, then 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 =
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 is a restricted monic and is total, then 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 and be a pair of morphisms. The map is a restricted retract of when

_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 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 β©β‘ f β β‘β¨ f-total β©β‘ id β  If 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 and have restricted retracts, then so does

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 has a restricted retract and is total, then 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 and be a pair of morphisms. and are restricted inverses if and

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 and 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 be a restriction category, and We say that refines if agrees with when restricted to the domain of

_β€_ : β {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                          β