# Gaunt categories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-01.

module category-theory.gaunt-categories where

Imports
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


## Idea

A gaunt category is a category such that one of the following equivalent conditions hold:

1. The isomorphism-sets are propositions.
2. The objects form a set.
3. Every object is rigid, meaning its automorphism group is trivial.

Gaunt categories forms the common intersection of (univalent) categories and strict categories. We have the following diagram relating the different notions of "category":

        Gaunt categories
/   \
/       \
∨           ∨
Categories         Strict categories
\           /
\       /
∨   ∨
Preunivalent categories
|
|
∨
Precategories


## Definitions

### The predicate on precategories that there is at most one isomorphism between any two objects

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

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

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

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

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

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

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

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

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

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

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

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 if and only if having an inhabitant implies it is contractible, we can apply isomorphism induction to get our result.

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)