open import Cat.Functor.Properties
open import Cat.Univalent
open import Cat.Prelude

import Cat.Reasoning
module Cat.Functor.Subcategory where

SubcategoriesπŸ”—

A subcategory is specified by a predicate on objects, and a predicate on morphisms between objects within 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 is univalent.

module _ {o β„“} (C : Precategory o β„“) where
  open Cat.Reasoning C
  record Subcat (o' β„“' : Level) : Type (o βŠ” β„“ βŠ” lsuc o' βŠ” lsuc β„“') where
    no-eta-equality
    field
      is-ob : Ob β†’ Type o'
      is-hom : βˆ€ {x y} (f : Hom x y) β†’ is-ob x β†’ is-ob y β†’ Type β„“'
      is-hom-prop
        : βˆ€ {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
      is-hom-∘
        : βˆ€ {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 where 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
    no-eta-equality
    constructor sub-hom
    field
      hom : Hom (x .fst) (y .fst)
      witness : subcat .is-hom hom (x .snd) (y .snd)

open Subcat-hom
module _ {o β„“} {C : Precategory o β„“} where
  private module C = Precategory C

  instance
    Membership-subcat-ob : βˆ€ {o' β„“'} β†’ Membership C.Ob (Subcat C o' β„“') _
    Membership-subcat-ob = record { _∈_ = Ξ» o S β†’ o ∈ S .Subcat.is-ob }

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

  Subcat-hom-pathp
    : {x x' y y' : Σ[ ob ∈ C ] (ob ∈ S)}
    β†’ {f : Subcat-hom S x y} {g : Subcat-hom S x' y'}
    β†’ (p : x ≑ x') (q : y ≑ y')
    β†’ PathP (Ξ» i β†’ Hom (p i .fst) (q i .fst)) (f .hom) (g .hom)
    β†’ PathP (Ξ» i β†’ Subcat-hom S (p i) (q i)) f g
  Subcat-hom-pathp p q r i .hom = r i
  Subcat-hom-pathp {f = f} {g = g} p q r i .witness =
    is-prop→pathp (λ i → is-hom-prop (r i) (p i .snd) (q i .snd)) (f .witness) (g .witness) i

  instance
    Extensional-subcat-hom
      : βˆ€ {β„“r x y} ⦃ sa : Extensional (Hom (x .fst) (y .fst)) β„“r ⦄
      β†’ Extensional (Subcat-hom S x y) β„“r
    Extensional-subcat-hom ⦃ sa ⦄ = injectionβ†’extensional!
      (Subcat-hom-pathp refl refl) sa

    Funlike-Subcat-hom
      : βˆ€ {β„“ β„“'} {A : Type β„“} {B : A β†’ Type β„“'} {x y}
      β†’ ⦃ _ : Funlike (Hom (x .fst) (y .fst)) A B ⦄ β†’ Funlike (Subcat-hom S x y) A B
    Funlike-Subcat-hom ⦃ i ⦄ = record { _#_ = Ξ» f x β†’ apply (f .hom) x }

    H-Level-Subcat-hom : βˆ€ {x y n} β†’ H-Level (Subcat-hom S x y) (2 + n)
    H-Level-Subcat-hom = basic-instance 2 $ Iso→is-hlevel 2 eqv $
      Ξ£-is-hlevel 2 (Hom-set _ _) Ξ» _ β†’
      is-hlevel-suc 1 (is-hom-prop _ _ _)
      where unquoteDecl eqv = declare-record-iso eqv (quote Subcat-hom)

We can then use this data to construct a category.

module _ {o o' β„“ β„“'} {C : Precategory o β„“} (subcat : Subcat C o' β„“') where
  open Cat.Reasoning C
  open Subcat subcat
  Subcategory : Precategory (o βŠ” o') (β„“ βŠ” β„“')
  Subcategory .Precategory.Ob = βˆ«β‚š subcat
  Subcategory .Precategory.Hom = Subcat-hom subcat
  Subcategory .Precategory.Hom-set _ _ = hlevel 2
  Subcategory .Precategory.id .hom = id
  Subcategory .Precategory.id .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 = ext (idr _)
  Subcategory .Precategory.idl f = ext (idl _)
  Subcategory .Precategory.assoc f g h = ext (assoc _ _ _)

From pseudomonic functorsπŸ”—

There is another way of representing subcategories: By giving a faithful functor 

module _
  {o o' β„“ β„“'} {C : Precategory o β„“} {D : Precategory o' β„“'}
  {F : Functor C D}
  (faithful : is-faithful F)
  where
  open Functor F
  private
    module C = Cat.Reasoning C
    module D = Cat.Reasoning D

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

  Faithful-subcat : Subcat D (o βŠ” β„“') (β„“ βŠ” β„“')
  Faithful-subcat .Subcat.is-ob x = Essential-fibre F x
  Faithful-subcat .Subcat.is-hom f (y , y-es) (z , z-es) =
    Ξ£[ g ∈ C.Hom y z ] (D.to z-es D.∘ F₁ g D.∘ D.from y-es ≑ f)
  Faithful-subcat .Subcat.is-hom-prop f (y , y-es) (z , z-es) (g , p) (h , q) =
    Ξ£-prop-path! $
    faithful $
    D.isoβ†’epic (y-es D.Iso⁻¹) _ _ $
    D.iso→monic z-es _ _ $
    p βˆ™ sym q
  Faithful-subcat .Subcat.is-hom-id (y , y-es) =
    C.id , apβ‚‚ D._∘_ refl (D.eliml F-id) βˆ™ D.invl y-es
  Faithful-subcat .Subcat.is-hom-∘
    {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 and 

  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 (D.to y-es D.∘ F₁ f D.∘ D.from x-es) (f , refl))
    (Ξ» _ β†’ refl)
    (Ξ» f β†’ ext (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 , D.id-iso) , C.id-iso

There is a faithful functor from a subcategory on to 

module _ {o o' β„“ β„“'} {C : Precategory o β„“} {S : Subcat C o' β„“'} where
  open Cat.Reasoning C
  private module Sub = Cat.Reasoning (Subcategory S)
  open Subcat S
  Forget-subcat : Functor (Subcategory S) 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 = ext

Furthermore, if the subcategory contains all of the isomorphisms of then the forgetful functor is pseudomonic.

  is-pseudomonic-Forget-subcat
    : (βˆ€ {x y} {f : Hom x y} {px : x ∈ S} {py : y ∈ S}
       β†’ is-invertible f β†’ S .is-hom f px py)
    β†’ is-pseudomonic Forget-subcat
  is-pseudomonic-Forget-subcat invert .is-pseudomonic.faithful =
    is-faithful-Forget-subcat
  is-pseudomonic-Forget-subcat invert .is-pseudomonic.isos-full f =
    pure $ Sub.make-iso
      (sub-hom (f .to)   (invert (iso→invertible f)))
      (sub-hom (f .from) (invert (isoβ†’invertible (f Iso⁻¹))))
      (ext (f .invl))
      (ext (f .invr)) , trivial!

Univalent subcategoriesπŸ”—

Let be a univalent category. A subcategory of is univalent when the predicate on objects is a proposition.

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

  subcat-is-category
    : is-category C
    β†’ (βˆ€ x β†’ is-prop (x ∈ S))
    β†’ is-category (Subcategory S)
  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))