open import Cat.Instances.Functor open import Cat.Functor.Base open import Cat.Univalent open import Cat.Prelude module Cat.Functor.FullSubcategory {o h} {C : Precategory o h} where

# Full subcategories🔗

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

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 $\ca{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 $\ca{C}$, any iso in the subcategory is an iso in $\ca{C}$, thus a path!

module _ (P : C.Ob → Type ℓ) (pprop : ∀ x → is-prop (P x)) where import Cat.Reasoning (Restrict P) as R

We begin by translating between isomorphisms in the subcategory (called $\ca{R}$ here) and in $\ca{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

We then prove that object-isomorphism pairs in the subcategory (i.e. inhabitants of $\sum_{B : \ca{R}} (A \cong B)$) coincide with those in the supercategory; Hence, since $\ca{C}$ is by assumption univalent, so is $\ca{R}$.

Restrict-is-category : is-category C → is-category (Restrict P) Restrict-is-category univ pb = is-hlevel≃ 0 equiv (univ A) where A = pb .object p = pb .witness to : (Σ[ B ∈ C.Ob ] A C.≅ B) → (Σ[ B ∈ R.Ob ] pb R.≅ B) to (B , isom) = (B , subst P A≡B p) , super-iso→sub-iso isom where A≡B = iso→path C univ isom from : (Σ[ B ∈ R.Ob ] pb R.≅ B) → (Σ[ B ∈ C.Ob ] A C.≅ B) from (B , isom) = B .object , sub-iso→super-iso isom rinv : is-right-inverse from to rinv pb = Σ-pathp path (R.≅-pathp _ _ refl) where path : to (from pb) .fst ≡ pb .fst path i .object = pb .fst .object path i .witness = is-prop→pathp (λ _ → pprop (pb .fst .object)) (to (from pb) .fst .witness) (pb .fst .witness) i linv : is-left-inverse from to linv (x , i) = Σ-pathp refl (C.≅-pathp _ _ refl) equiv : (Σ[ B ∈ C.Ob ] A C.≅ B) ≃ (Σ[ B ∈ R.Ob ] pb R.≅ B) equiv = to , is-iso→is-equiv (iso from rinv linv)

## From full inclusions🔗

There is another way of representing full subcategories: By giving a *full inclusion*, i.e. a fully faithful functor $F : \ca{D} \to \ca{C}$. Each full inclusion canonically determines a full subcategory of $\ca{C}$, namely that consisting of the objects in $\ca{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 $\ca{D}$, meaning that it admits a fully faithful, essentially surjective functor from $\ca{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 = 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 _ (λ _ → squash) 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