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, etc.). 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 of laws is a property of the objects, not structure on the morphisms.

{-# 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

FullSubcategoryF restricts a functor along the full-subcategory construction. Given F : Functor 𝐂 𝐃 and predicates P on the objects of 𝐂 and Q on the objects of 𝐃, the only new data required is a transfer proof that F sends P-objects to Q-objects. On objects the restricted functor pairs Fβ‚€ with that proof; on morphisms, on morphism equalities, and on the identity and composition laws it is literally F, because a full subcategory has exactly the morphisms of its ambient category.

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
            }