Skip to content

Setoid.Categories.FullSubcategory

Full subcategories on an object predicate

This is the Setoid.Categories.FullSubcategory module of the Agda Universal Algebra Library.

FullSubcategory 𝐂 P is the full subcategory of 𝐂 whose objects are the inhabitants of Ξ£ (Obj 𝐂) P β€” an object of 𝐂 together with evidence that it satisfies P β€” and whose morphisms, hom-equality, identity, composition, and laws are inherited from 𝐂 unchanged. This is exactly the shape of the theory-satisfying classical structures (Semigroup Ξ± ρ = Ξ£[ 𝑨 ∈ Algebra Ξ± ρ ] 𝑨 ⊨ Th-Semigroup, and likewise Monoid, Group, …); each is a full subcategory of the algebra category Alg of its signature, because a homomorphism between theory-satisfying algebras is just a homomorphism of the underlying algebras β€” satisfaction is a property of the objects, not structure on the morphisms.

FullSubcategoryF restricts a functor along such predicates; given F : 𝐂 ⟢ 𝐃 and a transfer of evidence P A β†’ Q (Fβ‚€ A), the functor maps the full subcategory on P to the one on Q, acting as F on morphisms. The functor laws are inherited verbatim, since the hom-equalities are.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Categories.FullSubcategory where

open import Agda.Primitive              using ( _βŠ”_ ) renaming ( Set to Type )
open import Data.Product                using ( Ξ£ ; _,_ ; proj₁ ; projβ‚‚ )
open import Level                       using ( Level )
open import Setoid.Categories.Category  using ( Category )
open import Setoid.Categories.Functor   using ( Functor )

private variable o β„“ e oβ€² β„“β€² eβ€² p q : Level

The full subcategory

module _ (𝐂 : Category o β„“ e) where
  open Category 𝐂

  FullSubcategory : (P : Obj β†’ Type p) β†’ Category (o βŠ” p) β„“ e
  FullSubcategory P = record
    { Obj        = Ξ£ Obj P
    ; Hom        = Ξ» (A B : Ξ£ Obj P) β†’ Hom (proj₁ A) (proj₁ B)
    ; _β‰ˆ_        = _β‰ˆ_
    ; id         = id
    ; _∘_        = _∘_
    ; β‰ˆ-equiv    = β‰ˆ-equiv
    ; assoc      = assoc
    ; identityΛ‘  = identityΛ‘
    ; identityΚ³  = identityΚ³
    ; ∘-resp-β‰ˆ   = ∘-resp-β‰ˆ
    }

Restricting a functor to a full subcategory

open Category using (Obj)
module _
  {𝐂 : Category o β„“ e} {𝐃 : Category oβ€² β„“β€² eβ€²}
  {P : Obj 𝐂 β†’ Type p} {Q : Obj 𝐃 β†’ Type q}
  (F : Functor 𝐂 𝐃)
  where
  open Functor F

  FullSubcategoryF :
    (transfer : {A : Obj 𝐂} β†’ P A β†’ Q (Fβ‚€ A))
    β†’ Functor (FullSubcategory 𝐂 P) (FullSubcategory 𝐃 Q)
  FullSubcategoryF transfer =
    record  { Fβ‚€            = Ξ» A β†’ ( Fβ‚€ (proj₁ A) , transfer (projβ‚‚ A) )
            ; F₁            = F₁
            ; F-resp-β‰ˆ      = F-resp-β‰ˆ
            ; identity      = identity
            ; homomorphism  = homomorphism
            }