<!--
```agda
open import Cat.Functor.Properties
open import Cat.Prelude
```
-->

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

<!--
```agda
import Cat.Reasoning C as C
open Precategory
private variable
  ℓ : Level
```
-->

# Full subcategories {defines="full-subcategory"}

A **full subcategory** $\cD$ of some larger category $\cC$ is the
category generated by some [predicate] $P$ on the objects of of
$\cC$: 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").

[predicate]: 1Lab.HLevel.html#is-prop

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.

```agda
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`{.Agda}ions)
is that _any full subcategory of a [[univalent category]] is univalent_. The
argument is roughly as follows: Since $\cC$ 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 $\cC$, any
iso in the subcategory is an iso in $\cC$, thus a path!

```agda
module _ (P : C.Ob → Type ℓ) where
  import Cat.Reasoning (Restrict P) as R
```

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

```agda
  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
```

<!--
```agda
  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

```
-->

```agda
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 : \cR} (A \cong B)$) coincide with those in
the supercategory; Hence, since $\cC$ is by assumption univalent, so
is $\cR$.

```agda
  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 {defines="essential-image"}

There is another way of representing full subcategories: By giving a
_full inclusion_, i.e. a [[fully faithful]] functor $F : \cD \to
\cC$. Each full inclusion canonically determines a full subcategory
of $\cC$, namely that consisting of the objects in $\cC$ merely in
the image of $F$. This category is often referred to as the
**essential image** of $F$.

```agda
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))
```

<!--
```agda
  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 $\cD$ into the essential image of
$F$ that is [[essentially surjective]]. Moreover, this inclusion
is a weak equivalence if $F$ is [[fully faithful]].

```agda
  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.

```agda
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 \to Ob$ of $\cC$ by forming a modified version of
$\cC$ whose objects have been replaced by elements of $I$.

```agda
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 \to \cC$ that takes each $i$ to
$X_i$.

```agda
  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
```
