Categories.Pre

Anna Williams 29 January 2026

Definition of precategory.


{-# OPTIONS --safe --without-K #-}

open import Categories.Notation.Wild
open import UF.Sets
open import UF.Sets-Properties
open import UF.Base
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties
open import UF.FunExt

open import Notation.UnderlyingType
open import MLTT.Spartan
open import Categories.Wild

module Categories.Pre where


Precategories are exactly wild categories where the homs are sets. This
property is given by the below.


module _ {𝓤 𝓥 : Universe} (W : WildCategory 𝓤 𝓥) where
 open WildCategoryNotation W

 is-precategory : (𝓤 ⊔ 𝓥) ̇
 is-precategory = (a b : obj W) → is-set (hom a b)

 being-precat-is-prop : (fe : Fun-Ext)
                      → is-prop (is-precategory)
 being-precat-is-prop fe = Π₂-is-prop fe (λ _ _ → being-set-is-prop fe)


We can now define the notion of a precategory.


Precategory : (𝓤 𝓥 : Universe) → (𝓤 ⊔ 𝓥)⁺ ̇
Precategory 𝓤 𝓥 = Σ W ꞉ WildCategory 𝓤 𝓥 , is-precategory W


This gives the object notation for precategories and projections from the
sigma type.


instance
 precatobj : {𝓤 𝓥 : Universe} → OBJ (Precategory 𝓤 𝓥) (𝓤 ̇ )
 obj {{precatobj}} (P , _) = WildCategory.obj P

instance
  underlying-wildcategory-of-precategory
   : {𝓤 𝓥 : Universe}
   → Underlying-Type (Precategory 𝓤 𝓥) (WildCategory 𝓤 𝓥)
  ⟨_⟩ {{underlying-wildcategory-of-precategory}} (P , _) = P

hom-is-set : (P : Precategory 𝓤 𝓥)
             {a b : obj P}
           → is-set (WildCategory.hom ⟨ P ⟩ a b)
hom-is-set (_ , p) {a} {b} = p a b


We now show that in a precategory, for any given homomorphism, being an
isomorphism is a (mere) proposition. We argue that inverses are unique,
and then since the type of homomorphisms between two objects is a set,
equality between any two homomorphisms is a proposition, so our left and
right inverse equalities are a proposition.


module isomorphism-properties (P : Precategory 𝓤 𝓥) where
 open WildCategoryNotation ⟨ P ⟩

 inverses-are-lc : {a b : obj P}
                   {f : hom a b}
                   (i j : inverse f)
                 → ⌞ i ⌟ ＝ ⌞ j ⌟
                 → i ＝ j
 inverses-are-lc i j refl = ap₂ (λ l r → ⌞ i ⌟ , l , r) l-eq r-eq
  where
   l-eq : ⌞ i ⌟-is-left-inverse ＝ ⌞ j ⌟-is-left-inverse
   l-eq = hom-is-set P ⌞ i ⌟-is-left-inverse ⌞ j ⌟-is-left-inverse

   r-eq : ⌞ i ⌟-is-right-inverse ＝ ⌞ j ⌟-is-right-inverse
   r-eq = hom-is-set P ⌞ i ⌟-is-right-inverse ⌞ j ⌟-is-right-inverse

 being-iso-is-prop : {a b : obj P}
                     (f : hom a b)
                   → is-prop (inverse f)
 being-iso-is-prop f i j = inverses-are-lc i j (at-most-one-inverse i j)


Following this, we can see that the type of isomorphisms is a set.


 isomorphism-type-is-set : {a b : obj P}
                         → is-set (a ≅ b)
 isomorphism-type-is-set = Σ-is-set (hom-is-set P)
                                    (λ f → props-are-sets (being-iso-is-prop f))


Furthermore, we can show that equivalence of isomorphisms is based on equality
of the chosen morphism.


 to-≅-＝ : {a b : obj P}
         → {f f' : a ≅ b}
         → ⌜ f ⌝ ＝ ⌜ f' ⌝
         → f ＝ f'
 to-≅-＝ = to-subtype-＝ being-iso-is-prop

open isomorphism-properties public hiding (to-≅-＝)