---
layout: default
file: "src/Setoid/Categories/FullSubcategory.lagda.md"
title: "Setoid.Categories.FullSubcategory module"
date: "2026-06-10"
author: "the agda-algebras development team"
---

### 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`][Setoid.Categories.Algebra] 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.

<!--
```agda
{-# 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

```agda
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`{.AgdaFunction} 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β‚€`{.AgdaField} 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.

```agda
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
            }
```