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 D\ca{D} of some larger category C\ca{C} is the category generated by some predicate PP on the objects of of C\ca{C}: You keep only those objects for which PP 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

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 C\ca{C} is univalent, an isomorphism Aβ‰…BA \cong B gives us a path A≑BA \equiv B, so in particular if we know Aβ‰…BA \cong B and P(A)P(A), then we have P(B)P(B). But, since the morphisms in the full subcategory coincide with those of C\ca{C}, any iso in the subcategory is an iso in C\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 R\ca{R} here) and in C\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 βˆ‘B:R(Aβ‰…B)\sum_{B : \ca{R}} (A \cong B)) coincide with those in the supercategory; Hence, since C\ca{C} is by assumption univalent, so is R\ca{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 im) i
    .to-path {a = a} {b = b} im i .witness → is-prop→pathp
      (λ i → pprop (cids .to-path (sub-iso→super-iso im) i))
      (a .witness) (b .witness) i
    .to-path-over p → R.≅-pathp _ _ λ i → cids .to-path-over (sub-iso→super-iso 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→CF : \ca{D} \to \ca{C}. Each full inclusion canonically determines a full subcategory of C\ca{C}, namely that consisting of the objects in C\ca{C} merely in the image of FF.

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 D\ca{D}, meaning that it admits a fully faithful, essentially surjective functor from D\ca{D}. This functor is actually just FF 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 _ (Ξ» _ β†’ 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