Jon Sterling, started 16th Dec 2022

\begin{code}

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

open import UF.FunExt

module Categories.Category (fe : Fun-Ext) where

open import MLTT.Spartan
open import UF.Base
open import UF.Equiv
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Equiv-FunExt
open import UF.Sets
open import UF.Sets-Properties

\end{code}

We prefer composition in diagrammatic order.

\begin{code}

category-structure : (๐ค ๐ฅ : Universe) โ (๐ค โ ๐ฅ)โบ ฬ
category-structure ๐ค ๐ฅ =
ฮฃ ob ๊ (๐ค ฬ),
ฮฃ hom ๊ (ob โ ob โ ๐ฅ ฬ ),
ฮฃ idn ๊ ((A : ob) โ hom A A) ,
((A B C : ob) (f : hom A B) (g : hom B C) โ hom A C)

module category-structure (๐ : category-structure ๐ค ๐ฅ) where
ob : ๐ค ฬ
ob = prโ ๐

hom : ob โ ob โ ๐ฅ ฬ
hom A B = prโ (prโ ๐) A B

idn : (A : ob) โ hom A A
idn A = prโ (prโ (prโ ๐)) A

seq : {A B C : ob} (f : hom A B) (g : hom B C) โ hom A C
seq f g = prโ (prโ (prโ ๐)) _ _ _ f g

cmp : {A B C : ob} (g : hom B C) (f : hom A B) โ hom A C
cmp f g = seq g f

module category-axiom-statements (๐ : category-structure ๐ค ๐ฅ) where
open category-structure ๐

statement-hom-is-set : ๐ค โ ๐ฅ ฬ
statement-hom-is-set = (A B : ob) โ is-set (hom A B)

statement-idn-L : ๐ค โ ๐ฅ ฬ
statement-idn-L = (A B : ob) (f : hom A B) โ seq (idn A) f ๏ผ f

statement-idn-R : ๐ค โ ๐ฅ ฬ
statement-idn-R = (A B : ob) (f : hom A B) โ seq f (idn B) ๏ผ f

statement-assoc : ๐ค โ ๐ฅ ฬ
statement-assoc =
(A B C D : ob) (f : hom A B) (g : hom B C) (h : hom C D)
โ seq f (seq g h) ๏ผ seq (seq f g) h

statement-hom-is-set-is-prop : is-prop statement-hom-is-set
statement-hom-is-set-is-prop =
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
being-set-is-prop fe

module _ (hom-is-set : statement-hom-is-set) where
statement-idn-L-is-prop : is-prop statement-idn-L
statement-idn-L-is-prop =
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
hom-is-set _ _

statement-idn-R-is-prop : is-prop statement-idn-R
statement-idn-R-is-prop =
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
hom-is-set _ _

statement-assoc-is-prop : is-prop statement-assoc
statement-assoc-is-prop =
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
hom-is-set _ _

-- TODO: univalence statement

-- Precategories are an intermediate notion in univalent 1-category theory.
module _ (๐ : category-structure ๐ค ๐ฅ) where
open category-axiom-statements ๐

precategory-axioms : ๐ค โ ๐ฅ ฬ
precategory-axioms =
statement-hom-is-set
ร statement-idn-L
ร statement-idn-R
ร statement-assoc

precategory-axioms-is-prop : is-prop precategory-axioms
precategory-axioms-is-prop =
ฮฃ-is-prop statement-hom-is-set-is-prop ฮป hom-is-set โ
ร-is-prop
(statement-idn-L-is-prop hom-is-set)
(ร-is-prop
(statement-idn-R-is-prop hom-is-set)
(statement-assoc-is-prop hom-is-set))

module precategory-axioms (ax : precategory-axioms) where
hom-is-set : statement-hom-is-set
hom-is-set = prโ ax

idn-L : statement-idn-L
idn-L = prโ (prโ ax)

idn-R : statement-idn-R
idn-R = prโ (prโ (prโ ax))

assoc : statement-assoc
assoc = prโ (prโ (prโ ax))

record precategory (๐ค ๐ฅ : Universe) : (๐ค โ ๐ฅ)โบ ฬ where
constructor make
field
str : category-structure ๐ค ๐ฅ
ax : precategory-axioms str

open category-structure str public
open precategory-axioms str ax public

module precategory-as-sum {๐ค ๐ฅ} where
to-sum : precategory ๐ค ๐ฅ โ (ฮฃ ๐ ๊ category-structure ๐ค ๐ฅ , precategory-axioms ๐)
to-sum ๐ = let open precategory ๐ in str , ax

from-sum : (ฮฃ ๐ ๊ category-structure ๐ค ๐ฅ , precategory-axioms ๐) โ precategory ๐ค ๐ฅ
from-sum ๐ = make (prโ ๐) (prโ ๐)

to-sum-is-equiv : is-equiv to-sum
prโ (prโ to-sum-is-equiv) = from-sum
prโ (prโ to-sum-is-equiv) _ = refl
prโ (prโ to-sum-is-equiv) = from-sum
prโ (prโ to-sum-is-equiv) _ = refl

module _ (๐ : precategory ๐ค ๐ฅ) where
open precategory ๐

module hom-properties {A B : ob} (f : hom A B) where

module _ (g : hom B A) where
is-inverse : ๐ฅ ฬ
is-inverse = (seq f g ๏ผ idn A) ร (seq g f ๏ผ idn B)

being-inverse-is-prop : is-prop is-inverse
being-inverse-is-prop = ร-is-prop (hom-is-set _ _) (hom-is-set _ _)

inverse-is-unique
: (g g' : hom B A)
โ is-inverse g
โ is-inverse g'
โ g ๏ผ g'
inverse-is-unique g g' fg fg' =
g ๏ผโจ idn-R _ _ _ โปยน โฉ
seq g (idn _) ๏ผโจ ap (seq g) (prโ fg' โปยน) โฉ
seq g (seq f g') ๏ผโจ assoc _ _ _ _ _ _ _ โฉ
seq (seq g f) g' ๏ผโจ ap (ฮป x โ seq x g') (prโ fg) โฉ
seq (idn _) g' ๏ผโจ idn-L _ _ _ โฉ
g' โ

is-iso : ๐ฅ ฬ
is-iso = ฮฃ g ๊ hom B A , is-inverse g

is-iso-is-prop : is-prop is-iso
is-iso-is-prop (g , fg) (g' , fg') =
to-ฮฃ-๏ผ
(inverse-is-unique g g' fg fg' ,
being-inverse-is-prop _ _ _)

iso : ob โ ob โ ๐ฅ ฬ
iso A B = ฮฃ f ๊ hom A B , hom-properties.is-iso f

idn-is-iso : {A : ob} โ hom-properties.is-iso (idn A)
prโ idn-is-iso = idn _
prโ (prโ idn-is-iso) = idn-L _ _ _
prโ (prโ idn-is-iso) = idn-L _ _ _

module _ (A B : ob) where
๏ผ-to-iso : A ๏ผ B โ iso A B
๏ผ-to-iso refl = idn A , idn-is-iso

is-univalent-precategory : ๐ค โ ๐ฅ ฬ
is-univalent-precategory = (A B : ob) โ is-equiv (๏ผ-to-iso A B)

being-univalent-is-prop : is-prop is-univalent-precategory
being-univalent-is-prop =
ฮ -is-prop fe ฮป _ โ
ฮ -is-prop fe ฮป _ โ
being-equiv-is-prop (ฮป _ _ โ fe) _

category : (๐ค ๐ฅ : Universe) โ (๐ค โ ๐ฅ)โบ ฬ
category ๐ค ๐ฅ = ฮฃ ๐ ๊ precategory ๐ค ๐ฅ , is-univalent-precategory ๐

category-to-precategory : category ๐ค ๐ฅ โ precategory ๐ค ๐ฅ
category-to-precategory ๐ = prโ ๐

\end{code}