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\text{,}$ $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 }\text{,}$ 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 _ _ _ _

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

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 }\text{.}$

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\text{.}$

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\text{,}$ $fg=fh$ implies that $f^{\downarrow }g=f^{\downarrow }h\text{.}$ Intuitively, this is the correct notion of monic for a partial function; we cannot guarantee that $g$ and $h$ are equal if $fg=fh\text{,}$ 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 }\text{.}$

_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 ⟩≡
    f ↓                   ≡⟨ f-total ⟩≡
    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\text{.}$

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 }\text{.}$

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                                 ≡˘⟨ ↓-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.

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)\text{.}$ We say that $g$ refines $f$ if $g$ agrees with $f$ when restricted to the domain of $f\text{.}$

_≤_ : ∀ {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 =
  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.

∘-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                          ∎