---
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`, …); 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 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.

<!--
```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

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