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

# Full subcategoriesπ

A **full subcategory**
$D$
of some larger category
$C$
is the category generated by some predicate
$P$
on the objects of of
$C:$
You keep only those objects for which
$P$
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 (`Restrict`

ions) is that *any
full subcategory of a univalent category is
univalent*. The argument is roughly as follows: Since
$C$
is univalent, an isomorphism
$AβB$
gives us a path
$Aβ‘B,$
so in particular if we know
$AβB$
and
$P(A),$
then we have
$P(B).$
But, since the morphisms in the full subcategory coincide with those of
$C,$
any iso in the subcategory is an iso in
$C,$
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 $R$ here) and in $C,$ 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 $β_{B:R}(AβB))$ coincide with those in the supercategory; Hence, since $C$ is by assumption univalent, so is $R.$

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
$F:DβC.$
Each full inclusion canonically determines a full subcategory of
$C,$
namely that consisting of the objects in
$C$
merely in the image of
$F.$
This category is often referred to as the **essential
image** of
$F.$

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 $D$ into the essential image of $F$ that is essentially surjective. Moreover, this inclusion is a weak equivalence if $F$ 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 $X_{i}:IβOb$ of $C$ by forming a modified version of $C$ whose objects have been replaced by elements of $I.$

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 $X_{i}βC$ that takes each $i$ to $X_{i}.$

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