# Gaunt categories ```agda module category-theory.gaunt-categories where ``` <details><summary>Imports</summary> ```agda open import category-theory.categories open import category-theory.composition-operations-on-binary-families-of-sets open import category-theory.isomorphism-induction-categories open import category-theory.isomorphisms-in-categories open import category-theory.isomorphisms-in-precategories open import category-theory.nonunital-precategories open import category-theory.precategories open import category-theory.preunivalent-categories open import category-theory.rigid-objects-categories open import category-theory.strict-categories open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositions open import foundation.sets open import foundation.strictly-involutive-identity-types open import foundation.universe-levels ``` </details> ## Idea A **gaunt category** is a [category](category-theory.categories.md) such that one of the following equivalent conditions hold: 1. The [isomorphism](category-theory.isomorphisms-in-categories.md)-[sets](foundation-core.sets.md) are [propositions](foundation-core.propositions.md). 2. The objects form a set. 3. Every object is [rigid](category-theory.rigid-objects-categories.md), meaning its [automorphism group](group-theory.automorphism-groups.md) is [trivial](group-theory.trivial-groups.md). Gaunt categories forms the common intersection of (univalent) categories and [strict categories](category-theory.strict-categories.md). We have the following diagram relating the different notions of "category": ```text Gaunt categories / \ / \ ∨ ∨ Categories Strict categories \ / \ / ∨ ∨ Preunivalent categories | | ∨ Precategories ``` ## Definitions ### The predicate on precategories that there is at most one isomorphism between any two objects ```agda module _ {l1 l2 : Level} (C : Precategory l1 l2) where is-prop-iso-prop-Precategory : Prop (l1 ⊔ l2) is-prop-iso-prop-Precategory = Π-Prop ( obj-Precategory C) ( λ x → Π-Prop ( obj-Precategory C) ( λ y → is-prop-Prop (iso-Precategory C x y))) is-prop-iso-Precategory : UU (l1 ⊔ l2) is-prop-iso-Precategory = type-Prop is-prop-iso-prop-Precategory is-property-is-prop-iso-Precategory : is-prop is-prop-iso-Precategory is-property-is-prop-iso-Precategory = is-prop-type-Prop is-prop-iso-prop-Precategory ``` ### The predicate on precategories of being gaunt ```agda module _ {l1 l2 : Level} (C : Precategory l1 l2) where is-gaunt-prop-Precategory : Prop (l1 ⊔ l2) is-gaunt-prop-Precategory = product-Prop ( is-category-prop-Precategory C) ( is-prop-iso-prop-Precategory C) is-gaunt-Precategory : UU (l1 ⊔ l2) is-gaunt-Precategory = type-Prop is-gaunt-prop-Precategory ``` ### The predicate on categories of being gaunt ```agda module _ {l1 l2 : Level} (C : Category l1 l2) where is-gaunt-prop-Category : Prop (l1 ⊔ l2) is-gaunt-prop-Category = is-prop-iso-prop-Precategory (precategory-Category C) is-gaunt-Category : UU (l1 ⊔ l2) is-gaunt-Category = type-Prop is-gaunt-prop-Category ``` ### The type of gaunt categories ```agda Gaunt-Category : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) Gaunt-Category l1 l2 = Σ (Category l1 l2) (is-gaunt-Category) module _ {l1 l2 : Level} (C : Gaunt-Category l1 l2) where category-Gaunt-Category : Category l1 l2 category-Gaunt-Category = pr1 C obj-Gaunt-Category : UU l1 obj-Gaunt-Category = obj-Category category-Gaunt-Category hom-set-Gaunt-Category : obj-Gaunt-Category → obj-Gaunt-Category → Set l2 hom-set-Gaunt-Category = hom-set-Category category-Gaunt-Category hom-Gaunt-Category : obj-Gaunt-Category → obj-Gaunt-Category → UU l2 hom-Gaunt-Category = hom-Category category-Gaunt-Category is-set-hom-Gaunt-Category : (x y : obj-Gaunt-Category) → is-set (hom-Gaunt-Category x y) is-set-hom-Gaunt-Category = is-set-hom-Category category-Gaunt-Category comp-hom-Gaunt-Category : {x y z : obj-Gaunt-Category} → hom-Gaunt-Category y z → hom-Gaunt-Category x y → hom-Gaunt-Category x z comp-hom-Gaunt-Category = comp-hom-Category category-Gaunt-Category associative-comp-hom-Gaunt-Category : {x y z w : obj-Gaunt-Category} (h : hom-Gaunt-Category z w) (g : hom-Gaunt-Category y z) (f : hom-Gaunt-Category x y) → comp-hom-Gaunt-Category (comp-hom-Gaunt-Category h g) f = comp-hom-Gaunt-Category h (comp-hom-Gaunt-Category g f) associative-comp-hom-Gaunt-Category = associative-comp-hom-Category category-Gaunt-Category involutive-eq-associative-comp-hom-Gaunt-Category : {x y z w : obj-Gaunt-Category} (h : hom-Gaunt-Category z w) (g : hom-Gaunt-Category y z) (f : hom-Gaunt-Category x y) → comp-hom-Gaunt-Category (comp-hom-Gaunt-Category h g) f =ⁱ comp-hom-Gaunt-Category h (comp-hom-Gaunt-Category g f) involutive-eq-associative-comp-hom-Gaunt-Category = involutive-eq-associative-comp-hom-Category category-Gaunt-Category associative-composition-operation-Gaunt-Category : associative-composition-operation-binary-family-Set hom-set-Gaunt-Category associative-composition-operation-Gaunt-Category = associative-composition-operation-Category ( category-Gaunt-Category) id-hom-Gaunt-Category : {x : obj-Gaunt-Category} → hom-Gaunt-Category x x id-hom-Gaunt-Category = id-hom-Category category-Gaunt-Category left-unit-law-comp-hom-Gaunt-Category : {x y : obj-Gaunt-Category} (f : hom-Gaunt-Category x y) → comp-hom-Gaunt-Category id-hom-Gaunt-Category f = f left-unit-law-comp-hom-Gaunt-Category = left-unit-law-comp-hom-Category category-Gaunt-Category right-unit-law-comp-hom-Gaunt-Category : {x y : obj-Gaunt-Category} (f : hom-Gaunt-Category x y) → comp-hom-Gaunt-Category f id-hom-Gaunt-Category = f right-unit-law-comp-hom-Gaunt-Category = right-unit-law-comp-hom-Category category-Gaunt-Category is-unital-composition-operation-Gaunt-Category : is-unital-composition-operation-binary-family-Set hom-set-Gaunt-Category comp-hom-Gaunt-Category is-unital-composition-operation-Gaunt-Category = is-unital-composition-operation-Category ( category-Gaunt-Category) is-gaunt-Gaunt-Category : is-gaunt-Category category-Gaunt-Category is-gaunt-Gaunt-Category = pr2 C ``` ### The underlying nonunital precategory of a gaunt category ```agda nonunital-precategory-Gaunt-Category : {l1 l2 : Level} → Gaunt-Category l1 l2 → Nonunital-Precategory l1 l2 nonunital-precategory-Gaunt-Category C = nonunital-precategory-Category (category-Gaunt-Category C) ``` ### The underlying precategory of a gaunt category ```agda precategory-Gaunt-Category : {l1 l2 : Level} → Gaunt-Category l1 l2 → Precategory l1 l2 precategory-Gaunt-Category C = precategory-Category (category-Gaunt-Category C) ``` ### The underlying preunivalent category of a gaunt category ```agda preunivalent-category-Gaunt-Category : {l1 l2 : Level} → Gaunt-Category l1 l2 → Preunivalent-Category l1 l2 preunivalent-category-Gaunt-Category C = preunivalent-category-Category (category-Gaunt-Category C) ``` ### The total hom-type of a gaunt category ```agda total-hom-Gaunt-Category : {l1 l2 : Level} (C : Gaunt-Category l1 l2) → UU (l1 ⊔ l2) total-hom-Gaunt-Category C = total-hom-Category (category-Gaunt-Category C) obj-total-hom-Gaunt-Category : {l1 l2 : Level} (C : Gaunt-Category l1 l2) → total-hom-Gaunt-Category C → obj-Gaunt-Category C × obj-Gaunt-Category C obj-total-hom-Gaunt-Category C = obj-total-hom-Category (category-Gaunt-Category C) ``` ### Equalities induce morphisms ```agda module _ {l1 l2 : Level} (C : Gaunt-Category l1 l2) where hom-eq-Gaunt-Category : (x y : obj-Gaunt-Category C) → x = y → hom-Gaunt-Category C x y hom-eq-Gaunt-Category = hom-eq-Category (category-Gaunt-Category C) hom-inv-eq-Gaunt-Category : (x y : obj-Gaunt-Category C) → x = y → hom-Gaunt-Category C y x hom-inv-eq-Gaunt-Category = hom-inv-eq-Category (category-Gaunt-Category C) ``` ## Properties ### Preunivalent categories whose isomorphism-sets are propositions are strict categories ```agda is-strict-category-is-prop-iso-Preunivalent-Category : {l1 l2 : Level} (C : Preunivalent-Category l1 l2) → is-prop-iso-Precategory (precategory-Preunivalent-Category C) → is-strict-category-Preunivalent-Category C is-strict-category-is-prop-iso-Preunivalent-Category C is-prop-iso-C x y = is-prop-emb (emb-iso-eq-Preunivalent-Category C) (is-prop-iso-C x y) ``` ### Gaunt categories are strict ```agda is-strict-category-is-gaunt-Category : {l1 l2 : Level} (C : Category l1 l2) → is-gaunt-Category C → is-strict-category-Category C is-strict-category-is-gaunt-Category C = is-strict-category-is-prop-iso-Preunivalent-Category ( preunivalent-category-Category C) ``` ### A strict category is gaunt if `iso-eq` is surjective ```agda module _ {l1 l2 : Level} (C : Strict-Category l1 l2) where is-category-is-surjective-iso-eq-Strict-Category : is-surjective-iso-eq-Precategory (precategory-Strict-Category C) → is-category-Precategory (precategory-Strict-Category C) is-category-is-surjective-iso-eq-Strict-Category = is-category-is-surjective-iso-eq-Preunivalent-Category ( preunivalent-category-Strict-Category C) is-prop-iso-is-category-Strict-Category : is-category-Precategory (precategory-Strict-Category C) → is-prop-iso-Precategory (precategory-Strict-Category C) is-prop-iso-is-category-Strict-Category is-category-C x y = is-prop-is-equiv' (is-category-C x y) (is-set-obj-Strict-Category C x y) is-prop-iso-is-surjective-iso-eq-Strict-Category : is-surjective-iso-eq-Precategory (precategory-Strict-Category C) → is-prop-iso-Precategory (precategory-Strict-Category C) is-prop-iso-is-surjective-iso-eq-Strict-Category is-surj-iso-eq-C = is-prop-iso-is-category-Strict-Category ( is-category-is-surjective-iso-eq-Strict-Category is-surj-iso-eq-C) is-gaunt-is-surjective-iso-eq-Strict-Category : is-surjective-iso-eq-Precategory (precategory-Strict-Category C) → is-gaunt-Precategory (precategory-Strict-Category C) pr1 (is-gaunt-is-surjective-iso-eq-Strict-Category is-surj-iso-eq-C) = is-category-is-surjective-iso-eq-Strict-Category is-surj-iso-eq-C pr2 (is-gaunt-is-surjective-iso-eq-Strict-Category is-surj-iso-eq-C) = is-prop-iso-is-surjective-iso-eq-Strict-Category is-surj-iso-eq-C ``` ### A category is gaunt if and only if every object is rigid **Proof:** Using the fact that a type is a [proposition](foundation-core.propositions.md) if and only if having an inhabitant implies it is [contractible](foundation-core.contractible-types.md), we can apply [isomorphism induction](category-theory.isomorphism-induction-categories.md) to get our result. ```agda module _ {l1 l2 : Level} (C : Category l1 l2) where is-gaunt-is-rigid-Category : ((x : obj-Category C) → is-rigid-obj-Category C x) → is-gaunt-Category C is-gaunt-is-rigid-Category is-rigid-obj-C x y = is-prop-is-proof-irrelevant (ind-iso-Category C _ (is-rigid-obj-C x)) is-rigid-is-gaunt-Category : is-gaunt-Category C → (x : obj-Category C) → is-rigid-obj-Category C x is-rigid-is-gaunt-Category is-gaunt-C x = is-proof-irrelevant-is-prop (is-gaunt-C x x) (id-iso-Category C) ``` ## See also - [Posets](order-theory.posets.md) are gaunt. ## External links - [Gaunt (pre)categories](https://1lab.dev/Cat.Gaunt.html) at 1lab - [gaunt category](https://ncatlab.org/nlab/show/gaunt+category#in_type_theory) at $n$Lab