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 $\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