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

# Full subcategoriesπ

A **full subcategory**
$\mathcal{D}$
of some larger category
$\mathcal{C}$
is the category generated by some predicate
$P$
on the objects of of
$\mathcal{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.

record Restrict-ob (P : C.Ob β Type β) : Type (o β β) where no-eta-equality constructor restrict field object : C.Ob witness : P object open Restrict-ob public Restrict : (P : C.Ob β Type β) β Precategory (o β β) h Restrict P .Ob = Restrict-ob P Restrict P .Hom A B = C.Hom (A .object) (B .object) 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

Restrict-ob-path : β {P : C.Ob β Type β} β {x y : Restrict-ob P} β (p : x .object β‘ y .object) β PathP (Ξ» i β P (p i)) (x .witness) (y .witness) β x β‘ y Restrict-ob-path p q i .object = p i Restrict-ob-path p q i .witness = q i

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
$\mathcal{C}$
is univalent, an isomorphism
$A \cong B$
gives us a path
$A \equiv B$,
so in particular if we know
$A \cong B$
and
$P(A)$,
then we have
$P(B)$.
But, since the morphisms in the full subcategory coincide with those of
$\mathcal{C}$,
any iso in the subcategory is an iso in
$\mathcal{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 $\mathcal{R}$ here) and in $\mathcal{C}$, which can be done by destructuring and reassembling:

sub-isoβsuper-iso : β {A B : Restrict-ob P} β (A R.β B) β (A .object C.β B .object) 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 : Restrict-ob P} β (A .object C.β B .object) β (A R.β B) super-isoβsub-iso y = R.make-iso y.to y.from y.invl y.invr where module y = C._β _ y

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 $\sum_{B : \mathcal{R}} (A \cong B)$) coincide with those in the supercategory; Hence, since $\mathcal{C}$ is by assumption univalent, so is $\mathcal{R}$.

Restrict-is-category : is-category C β is-category (Restrict P) Restrict-is-category cids = Ξ» where .to-path im i .object β Univalent.isoβpath cids (sub-isoβsuper-iso P im) i .to-path {a = a} {b = b} im i .witness β is-propβpathp (Ξ» i β pprop (cids .to-path (sub-isoβsuper-iso P im) i)) (a .witness) (b .witness) 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 : \mathcal{D} \to \mathcal{C}$.
Each full inclusion canonically determines a full subcategory of
$\mathcal{C}$,
namely that consisting of the objects in
$\mathcal{C}$
merely in the image of
$F$.

module _ {o' h'} {D : Precategory o' h'} {F : Functor D C} (ff : is-fully-faithful F) where open Functor F Full-inclusionβFull-subcat : Precategory _ _ Full-inclusionβFull-subcat = Restrict (Ξ» x β β[ d β Ob D ] (Fβ d C.β x))

This canonical full subcategory is weakly equivalent to $\mathcal{D}$, meaning that it admits a fully faithful, essentially surjective functor from $\mathcal{D}$. This functor is actually just $F$ again:

Ff-domainβFull-subcat : Functor D Full-inclusionβFull-subcat Ff-domainβFull-subcat .Functor.Fβ x = restrict (Fβ x) (inc (x , C.id-iso)) Ff-domainβFull-subcat .Functor.Fβ = Fβ Ff-domainβFull-subcat .Functor.F-id = F-id Ff-domainβFull-subcat .Functor.F-β = F-β is-fully-faithful-domainβFull-subcat : is-fully-faithful Ff-domainβFull-subcat is-fully-faithful-domainβFull-subcat = ff is-eso-domainβFull-subcat : is-eso Ff-domainβFull-subcat is-eso-domainβFull-subcat yo = β₯-β₯-map (Ξ» (preimg , isom) β preimg , super-isoβsub-iso _ isom) (yo .witness)

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β = object 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 is-fully-faithful-Forget-full-subcat : is-fully-faithful Forget-full-subcat is-fully-faithful-Forget-full-subcat = id-equiv