module Cat.Restriction.Functor where

# Restriction Functors๐

A functor $F : \mathcal{C} \to \mathcal{D}$ between restriction categories is a restriction functor if $F (f^{\downarrow}) = (F f)^{\downarrow}$.

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.

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 : \mathcal{C} \to \mathcal{D}$ be a restriction functor. Note that $F$ preserves total morphisms and restriction idempotents.

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 C.โ) โก
F .Fโ f โ

Furthermore, if $g$ refines $f$, then $F(g)$ refines $F(f)$.

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.โ   โก
F .Fโ g D.โ F .Fโ (f C.โ) โก
F .Fโ (g C.โ f C.โ) โก
F .Fโ f โ

Restriction functors also preserve restricted isomorphisms.

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 C.โ g)
F .Fโ (g C.โ)       โก
F .Fโ g D.โ         โ
; โ-invr =
F .Fโ g D.โ F .Fโ f โกห
F .Fโ (g C.โ f)
F .Fโ (f C.โ)       โก
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