open import Cat.Functor.Properties
open import Cat.Prelude

module Cat.Functor.FullSubcategory {o h} {C : Precategory o h} where

import Cat.Reasoning C as C
open Precategory
private variable
β : Level


Full subcategoriesπ

A full subcategory of some larger category is the category generated by some predicate on the objects of of You keep only those objects for which holds, and all the morphisms between them. An example is the category of abelian groups, as a full subcategory of groups: being abelian is a proposition (thereβs βat most one way for a group to be abelianβ).

We can interpret full subcategories, by analogy, as being the βinduced subgraphsβ of the categorical world: Keep only some of the vertices (objects), but all of the arrows (arrows) between them.

Restrict : (P : C.Ob β Type β) β Precategory (o β β) h
Restrict P .Ob = Ξ£[ O β C ] (P O)
Restrict P .Hom A B = C.Hom (A .fst) (B .fst)
Restrict P .Hom-set _ _ = C.Hom-set _ _
Restrict P .id    = C.id
Restrict P ._β_   = C._β_
Restrict P .idr   = C.idr
Restrict P .idl   = C.idl
Restrict P .assoc = C.assoc


A very important property of full subcategories (Restrictions) is that any full subcategory of a univalent category is univalent. The argument is roughly as follows: Since is univalent, an isomorphism gives us a path so in particular if we know and then we have But, since the morphisms in the full subcategory coincide with those of any iso in the subcategory is an iso in thus a path!

module _ (P : C.Ob β Type β) where
import Cat.Reasoning (Restrict P) as R


We begin by translating between isomorphisms in the subcategory (called here) and in which can be done by destructuring and reassembling:

  sub-isoβsuper-iso : β {A B : Ξ£ _ P} β (A R.β B) β (A .fst C.β B .fst)
sub-isoβsuper-iso x = C.make-iso x.to x.from x.invl x.invr
where module x = R._β_ x

super-isoβsub-iso : β {A B : Ξ£ _ P} β (A .fst C.β B .fst) β (A R.β B)
super-isoβsub-iso y = R.make-iso y.to y.from y.invl y.invr
where module y = C._β_ y

  sub-invβsuper-inv
: β {A B : Ξ£ _ P} {f : R.Hom A B}
β R.is-invertible {A} {B} f
β C.is-invertible f
sub-invβsuper-inv f-inv = C.make-invertible inv invl invr
where open R.is-invertible f-inv

super-invβsub-inv
: β {A B : Ξ£ _ P} {f : R.Hom A B}
β C.is-invertible f
β R.is-invertible {A} {B} f
super-invβsub-inv f-inv = R.make-invertible inv invl invr
where open C.is-invertible f-inv


module _ (P : C.Ob β Type β) (pprop : β x β is-prop (P x))
where
import Cat.Reasoning (Restrict P) as R


We then prove that object-isomorphism pairs in the subcategory (i.e. inhabitants of coincide with those in the supercategory; Hence, since is by assumption univalent, so is

  Restrict-is-category : is-category C β is-category (Restrict P)
Restrict-is-category cids = Ξ» where
.to-path im i .fst β Univalent.isoβpath cids (sub-isoβsuper-iso P im) i
.to-path {a = a} {b = b} im i .snd β is-propβpathp
(Ξ» i β pprop (cids .to-path (sub-isoβsuper-iso P im) i))
(a .snd) (b .snd) i
.to-path-over p β R.β-pathp _ _ Ξ» i β cids .to-path-over (sub-isoβsuper-iso P p) i .C.to


From full inclusionsπ

There is another way of representing full subcategories: By giving a full inclusion, i.e.Β a fully faithful functor Each full inclusion canonically determines a full subcategory of namely that consisting of the objects in merely in the image of This category is often referred to as the essential image of

module _ {o' h'} {D : Precategory o' h'} (F : Functor D C) where
open Functor F

Essential-image : Precategory _ _
Essential-image =
Restrict (Ξ» x β β[ d β Ob D ] (Fβ d C.β x))

  Essential-image-is-category : is-category C β is-category Essential-image
Essential-image-is-category cat = Restrict-is-category _ (Ξ» _ β hlevel 1) cat


There is a canonical inclusion of into the essential image of that is essentially surjective. Moreover, this inclusion is a weak equivalence if is fully faithful.

  Essential-inc : Functor D Essential-image
Essential-inc .Functor.Fβ x = Fβ x , inc (x , C.id-iso)
Essential-inc .Functor.Fβ = Fβ
Essential-inc .Functor.F-id = F-id
Essential-inc .Functor.F-β = F-β

Essential-inc-eso : is-eso Essential-inc
Essential-inc-eso yo =
β₯-β₯-map (Ξ» (preimg , isom) β preimg , super-isoβsub-iso _ isom)
(yo .snd)

ffβEssential-inc-ff : is-fully-faithful F β is-fully-faithful Essential-inc
ffβEssential-inc-ff ff = ff


Up to weak equivalence, admitting a full inclusion is equivalent to being a full subcategory: Every full subcategory admits a full inclusion, given on objects by projecting the first component and on morphisms by the identity function.

module _ {P : C.Ob β Type β} where
Forget-full-subcat : Functor (Restrict P) C
Forget-full-subcat .Functor.Fβ = fst
Forget-full-subcat .Functor.Fβ f = f
Forget-full-subcat .Functor.F-id = refl
Forget-full-subcat .Functor.F-β f g i = f C.β g

Forget-full-subcat-is-ff : is-fully-faithful Forget-full-subcat
Forget-full-subcat-is-ff = id-equiv


From families of objectsπ

Finally, we can construct a full subcategory by giving a family of objects of by forming a modified version of whose objects have been replaced by elements of

module _ {βi} {Idx : Type βi} (Xα΅’ : Idx β C.Ob) where
Family : Precategory βi h
Family .Ob = Idx
Family .Hom i j = C.Hom (Xα΅’ i) (Xα΅’ j)
Family .Hom-set _ _ = hlevel 2
Family .id = C.id
Family ._β_ = C._β_
Family .idr = C.idr
Family .idl = C.idl
Family .assoc = C.assoc


There is an evident functor from that takes each to

  Forget-family : Functor Family C
Forget-family .Functor.Fβ = Xα΅’
Forget-family .Functor.Fβ f = f
Forget-family .Functor.F-id = refl
Forget-family .Functor.F-β _ _ = refl

Forget-family-ff : is-fully-faithful Forget-family
Forget-family-ff = id-equiv