module Cat.Functor.Subcategory where


A subcategory Dβ†ͺC\mathcal{D} \hookrightarrow \mathcal{C} is specified by a predicate P:Cβ†’PropP : C \to \mathrm{Prop} on objects, and a predicate Q:P(x)β†’P(y)β†’C(x,y)β†’PropQ : P(x) \to P(y) \to \mathcal{C}(x,y) \to \mathrm{Prop} on morphisms between objects within PP that is closed under identities and composites.

To start, we package up all the data required to define a subcategory up into a record. Note that we omit the requirement that the predicate on objects is a proposition; this tends to be ill-behaved unless the C\mathcal{C} is univalent.

  record Subcat (o' β„“' : Level) : Type (o βŠ” β„“ βŠ” lsuc o' βŠ” lsuc β„“') where
      is-ob : Ob β†’ Type o'
      is-hom : βˆ€ {x y} (f : Hom x y) β†’ is-ob x β†’ is-ob y β†’ Type β„“'
        : βˆ€ {x y} (f : Hom x y) (px : is-ob x) (py : is-ob y)
        β†’ is-prop (is-hom f px py)
      is-hom-id : βˆ€ {x} β†’ (px : is-ob x) β†’ is-hom id px px
        : βˆ€ {x y z} {f : Hom y z} {g : Hom x y}
        β†’ {px : is-ob x} {py : is-ob y} {pz : is-ob z}
        β†’ is-hom f py pz β†’ is-hom g px py
        β†’ is-hom (f ∘ g) px pz

Morphisms of wide subcategories are defined as morphisms in C\mathcal{C} where QQ holds.

module _ {o o' β„“ β„“'} {C : Precategory o β„“} (subcat : Subcat C o' β„“') where
  open Cat.Reasoning C
  open Subcat subcat

  record Subcat-hom (x y : Ξ£[ ob ∈ Ob ] (is-ob ob)) : Type (β„“ βŠ” β„“') where
    constructor sub-hom
      hom : Hom (x .fst) (y .fst)
      witness : subcat .is-hom hom (x .snd) (y .snd)

open Subcat-hom

We can then use this data to construct a category.

  Subcategory : Precategory (o βŠ” o') (β„“ βŠ” β„“')
  Subcategory .Precategory.Ob = Σ[ ob ∈ Ob ] is-ob ob
  Subcategory .Precategory.Hom = Subcat-hom subcat
  Subcategory .Precategory.Hom-set _ _ = Subcat-hom-is-set
  Subcategory .hom = id
  Subcategory .witness = is-hom-id _
  Subcategory .Precategory._∘_ f g .hom = f .hom ∘ g .hom
  Subcategory .Precategory._∘_ f g .witness = is-hom-∘ (f .witness) (g .witness)
  Subcategory .Precategory.idr f = Subcat-hom-path (idr (f .hom))
  Subcategory .Precategory.idl f = Subcat-hom-path (idl (f .hom))
  Subcategory .Precategory.assoc f g h = Subcat-hom-path (assoc (f .hom) (g .hom) (h .hom))

From pseudomonic functorsπŸ”—

There is another way of representing subcategories: By giving a faithful functor F:D↠CF : \mathcal{D} \twoheadrightarrow \mathcal{C}.

We construct a subcategory from a faithful functor FF by restricting to the objects in the essential image of FF, and restricting the morphisms to those that lie in the image of FF.

  Faithful-subcat : Subcat D (o βŠ” β„“') (β„“ βŠ” β„“')
  Faithful-subcat x = Essential-fibre F x
  Faithful-subcat f (y , y-es) (z , z-es) =
    Ξ£[ g ∈ C.Hom y z ] ( z-es D.∘ F₁ g D.∘ D.from y-es ≑ f)
  Faithful-subcat f (y , y-es) (z , z-es) (g , p) (h , q) =
    Ξ£-prop-path (Ξ» _ β†’ D.Hom-set _ _ _ _) $
    faithful $
    D.isoβ†’epic (y-es D.Iso⁻¹) _ _ $
    D.iso→monic z-es _ _ $
    p βˆ™ sym q
  Faithful-subcat (y , y-es) = , apβ‚‚ D._∘_ refl (D.eliml F-id) βˆ™ D.invl y-es
    {f = f} {g = g} {x , x-es} {y , y-es} {z , z-es} (h , p) (i , q) =
    (h C.∘ i) ,
    D.push-inner (F-∘ h i)
    Β·Β· D.insert-inner (D.invr y-es)
    Β·Β· apβ‚‚ D._∘_ (sym (D.assoc _ _ _) βˆ™ p) q

There is an equivalence between canonical subcategory associated with FF and CC.

  Faithful-subcat-domain : Functor (Subcategory Faithful-subcat) C
  Faithful-subcat-domain .Functor.Fβ‚€ (x , x-es) = x-es .fst
  Faithful-subcat-domain .Functor.F₁ f = f .witness .fst
  Faithful-subcat-domain .Functor.F-id = refl
  Faithful-subcat-domain .Functor.F-∘ _ _ = refl

  Faithful-subcat-domain-is-ff : is-fully-faithful Faithful-subcat-domain
  Faithful-subcat-domain-is-ff {x = x , x' , x-es} {y = y , y' , y-es} =
    is-iso→is-equiv $ iso
    (Ξ» f β†’ sub-hom ( y-es D.∘ F₁ f D.∘ D.from x-es) (f , refl))
    (Ξ» _ β†’ refl)
    (Ξ» f β†’ Subcat-hom-path (f .witness .snd))

  Faithful-subcat-domain-is-split-eso : is-split-eso Faithful-subcat-domain
  Faithful-subcat-domain-is-split-eso x =
    (Fβ‚€ x , x , ,

There is a faithful functor from a subcategory on C\mathcal{C} to C\mathcal{C}.

  Forget-subcat : Functor (Subcategory subcat) C
  Forget-subcat .Functor.Fβ‚€ (x , _) = x
  Forget-subcat .Functor.F₁ f = f .hom
  Forget-subcat .Functor.F-id = refl
  Forget-subcat .Functor.F-∘ _ _ = refl

  is-faithful-Forget-subcat : is-faithful Forget-subcat
  is-faithful-Forget-subcat = Subcat-hom-path

Furthermore, if the subcategory contains all of the isomorphisms of C\mathcal{C}, then the forgetful functor is pseudomonic.

    : (βˆ€ {x y} {f : Hom x y} {px : is-ob x} {py : is-ob y}
       β†’ is-invertible f β†’ subcat .is-hom f px py)
    β†’ is-pseudomonic Forget-subcat
  is-pseudomonic-Forget-subcat invert .is-pseudomonic.faithful =
  is-pseudomonic-Forget-subcat invert .is-pseudomonic.isos-full f =
    pure $
        (sub-hom (f .to) (invert (iso→invertible f)))
        (sub-hom (f .from) (invert (isoβ†’invertible (f Iso⁻¹))))
        (Subcat-hom-path (f .invl))
        (Subcat-hom-path (f .invr))
      , β‰…-path refl

Univalent SubcategoriesπŸ”—

Let C\mathcal{C} be a univalent category. A subcategory of C\mathcal{C} is univalent when the predicate on objects is a proposition.

  subcat-isoβ†’iso : βˆ€ {x y : Ξ£[ x ∈ Ob ] is-ob x} β†’ x Sub.β‰… y β†’ x .fst β‰… y .fst
  subcat-iso→iso f =
    make-iso ( f .hom) (Sub.from f .hom)
      (ap hom (Sub.invl f)) (ap hom (Sub.invr f))

    : is-category C
    β†’ (βˆ€ x β†’ is-prop (is-ob x))
    β†’ is-category (Subcategory subcat)
  subcat-is-category cat ob-prop .to-path {a , pa} {b , pb} f =
    Σ-prop-path ob-prop (cat .to-path (subcat-iso→iso f))
  subcat-is-category cat ob-prop .to-path-over p =
    Sub.β‰…-pathp refl _ $
    Subcat-hom-pathp refl _ $
    apd (λ _ → to) (cat .to-path-over (subcat-iso→iso p))