# Preunivalent categories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-20.

module category-theory.preunivalent-categories where

Imports
open import category-theory.composition-operations-on-binary-families-of-sets
open import category-theory.isomorphisms-in-precategories
open import category-theory.precategories

open import foundation.1-types
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.embeddings
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 preunivalent category is a precategory for which the identifications between the objects embed into the isomorphisms. More specifically, an equality between objects gives rise to an isomorphism between them, by the J-rule. A precategory is a preunivalent category if this function, called iso-eq, is an embedding.

The idea of preunivalence is that it is a common generalization of univalent mathematics and mathematics with Axiom K. Hence preunivalent categories generalize both (univalent) categories and strict categories, which are precategories whose objects form a set.

The preunivalence condition on precategories states that the type of objects is a subgroupoid of the groupoid of isomorphisms. For univalent categories the groupoid of objects is equivalent to the groupoid of isomorphisms, while for strict categories the groupoid of objects is discrete. Indeed, in this sense preunivalence provides a generalization of both notions of "category", with no more structure. This is opposed to the even more general notion of precategory, where the homotopy structure on the objects can be almost completely unrelated to the homotopy structure of the morphisms.

## Definitions

### The predicate on precategories of being a preunivalent category

module _
{l1 l2 : Level} (C : Precategory l1 l2)
where

is-preunivalent-prop-Precategory : Prop (l1 ⊔ l2)
is-preunivalent-prop-Precategory =
Π-Prop
( obj-Precategory C)
( λ x →
Π-Prop
( obj-Precategory C)
( λ y → is-emb-Prop (iso-eq-Precategory C x y)))

is-preunivalent-Precategory : UU (l1 ⊔ l2)
is-preunivalent-Precategory = type-Prop is-preunivalent-prop-Precategory


### The type of preunivalent categories

Preunivalent-Category : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Preunivalent-Category l1 l2 =
Σ (Precategory l1 l2) (is-preunivalent-Precategory)

module _
{l1 l2 : Level} (C : Preunivalent-Category l1 l2)
where

precategory-Preunivalent-Category : Precategory l1 l2
precategory-Preunivalent-Category = pr1 C

obj-Preunivalent-Category : UU l1
obj-Preunivalent-Category = obj-Precategory precategory-Preunivalent-Category

hom-set-Preunivalent-Category :
obj-Preunivalent-Category → obj-Preunivalent-Category → Set l2
hom-set-Preunivalent-Category =
hom-set-Precategory precategory-Preunivalent-Category

hom-Preunivalent-Category :
obj-Preunivalent-Category → obj-Preunivalent-Category → UU l2
hom-Preunivalent-Category = hom-Precategory precategory-Preunivalent-Category

is-set-hom-Preunivalent-Category :
(x y : obj-Preunivalent-Category) → is-set (hom-Preunivalent-Category x y)
is-set-hom-Preunivalent-Category =
is-set-hom-Precategory precategory-Preunivalent-Category

comp-hom-Preunivalent-Category :
{x y z : obj-Preunivalent-Category} →
hom-Preunivalent-Category y z →
hom-Preunivalent-Category x y →
hom-Preunivalent-Category x z
comp-hom-Preunivalent-Category =
comp-hom-Precategory precategory-Preunivalent-Category

associative-comp-hom-Preunivalent-Category :
{x y z w : obj-Preunivalent-Category}
(h : hom-Preunivalent-Category z w)
(g : hom-Preunivalent-Category y z)
(f : hom-Preunivalent-Category x y) →
comp-hom-Preunivalent-Category (comp-hom-Preunivalent-Category h g) f ＝
comp-hom-Preunivalent-Category h (comp-hom-Preunivalent-Category g f)
associative-comp-hom-Preunivalent-Category =
associative-comp-hom-Precategory precategory-Preunivalent-Category

involutive-eq-associative-comp-hom-Preunivalent-Category :
{x y z w : obj-Preunivalent-Category}
(h : hom-Preunivalent-Category z w)
(g : hom-Preunivalent-Category y z)
(f : hom-Preunivalent-Category x y) →
comp-hom-Preunivalent-Category (comp-hom-Preunivalent-Category h g) f ＝ⁱ
comp-hom-Preunivalent-Category h (comp-hom-Preunivalent-Category g f)
involutive-eq-associative-comp-hom-Preunivalent-Category =
involutive-eq-associative-comp-hom-Precategory
( precategory-Preunivalent-Category)

associative-composition-operation-Preunivalent-Category :
associative-composition-operation-binary-family-Set
hom-set-Preunivalent-Category
associative-composition-operation-Preunivalent-Category =
associative-composition-operation-Precategory
( precategory-Preunivalent-Category)

id-hom-Preunivalent-Category :
{x : obj-Preunivalent-Category} → hom-Preunivalent-Category x x
id-hom-Preunivalent-Category =
id-hom-Precategory precategory-Preunivalent-Category

left-unit-law-comp-hom-Preunivalent-Category :
{x y : obj-Preunivalent-Category} (f : hom-Preunivalent-Category x y) →
comp-hom-Preunivalent-Category id-hom-Preunivalent-Category f ＝ f
left-unit-law-comp-hom-Preunivalent-Category =
left-unit-law-comp-hom-Precategory precategory-Preunivalent-Category

right-unit-law-comp-hom-Preunivalent-Category :
{x y : obj-Preunivalent-Category} (f : hom-Preunivalent-Category x y) →
comp-hom-Preunivalent-Category f id-hom-Preunivalent-Category ＝ f
right-unit-law-comp-hom-Preunivalent-Category =
right-unit-law-comp-hom-Precategory precategory-Preunivalent-Category

is-unital-composition-operation-Preunivalent-Category :
is-unital-composition-operation-binary-family-Set
hom-set-Preunivalent-Category
comp-hom-Preunivalent-Category
is-unital-composition-operation-Preunivalent-Category =
is-unital-composition-operation-Precategory
( precategory-Preunivalent-Category)

is-preunivalent-Preunivalent-Category :
is-preunivalent-Precategory precategory-Preunivalent-Category
is-preunivalent-Preunivalent-Category = pr2 C

emb-iso-eq-Preunivalent-Category :
{x y : obj-Preunivalent-Category} →
(x ＝ y) ↪ (iso-Precategory precategory-Preunivalent-Category x y)
pr1 (emb-iso-eq-Preunivalent-Category {x} {y}) =
iso-eq-Precategory precategory-Preunivalent-Category x y
pr2 (emb-iso-eq-Preunivalent-Category {x} {y}) =
is-preunivalent-Preunivalent-Category x y


### The total hom-type of a preunivalent category

total-hom-Preunivalent-Category :
{l1 l2 : Level} (C : Preunivalent-Category l1 l2) → UU (l1 ⊔ l2)
total-hom-Preunivalent-Category C =
total-hom-Precategory (precategory-Preunivalent-Category C)

obj-total-hom-Preunivalent-Category :
{l1 l2 : Level} (C : Preunivalent-Category l1 l2) →
total-hom-Preunivalent-Category C →
obj-Preunivalent-Category C × obj-Preunivalent-Category C
obj-total-hom-Preunivalent-Category C =
obj-total-hom-Precategory (precategory-Preunivalent-Category C)


### Equalities induce morphisms

module _
{l1 l2 : Level}
(C : Preunivalent-Category l1 l2)
where

hom-eq-Preunivalent-Category :
(x y : obj-Preunivalent-Category C) →
x ＝ y → hom-Preunivalent-Category C x y
hom-eq-Preunivalent-Category =
hom-eq-Precategory (precategory-Preunivalent-Category C)

hom-inv-eq-Preunivalent-Category :
(x y : obj-Preunivalent-Category C) →
x ＝ y → hom-Preunivalent-Category C y x
hom-inv-eq-Preunivalent-Category =
hom-inv-eq-Precategory (precategory-Preunivalent-Category C)


### Pre- and postcomposition by a morphism

precomp-hom-Preunivalent-Category :
{l1 l2 : Level} (C : Preunivalent-Category l1 l2)
{x y : obj-Preunivalent-Category C}
(f : hom-Preunivalent-Category C x y)
(z : obj-Preunivalent-Category C) →
hom-Preunivalent-Category C y z →
hom-Preunivalent-Category C x z
precomp-hom-Preunivalent-Category C =
precomp-hom-Precategory (precategory-Preunivalent-Category C)

postcomp-hom-Preunivalent-Category :
{l1 l2 : Level} (C : Preunivalent-Category l1 l2)
{x y : obj-Preunivalent-Category C}
(f : hom-Preunivalent-Category C x y)
(z : obj-Preunivalent-Category C) →
hom-Preunivalent-Category C z x →
hom-Preunivalent-Category C z y
postcomp-hom-Preunivalent-Category C =
postcomp-hom-Precategory (precategory-Preunivalent-Category C)


## Properties

### The objects in a preunivalent category form a 1-type

The type of identities between two objects in a preunivalent category embeds into the type of isomorphisms between them. But this type is a set, and thus the identity type is a set.

module _
{l1 l2 : Level} (C : Preunivalent-Category l1 l2)
where

is-1-type-obj-Preunivalent-Category : is-1-type (obj-Preunivalent-Category C)
is-1-type-obj-Preunivalent-Category x y =
is-set-is-emb
( iso-eq-Precategory (precategory-Preunivalent-Category C) x y)
( is-preunivalent-Preunivalent-Category C x y)
( is-set-iso-Precategory (precategory-Preunivalent-Category C))

obj-1-type-Preunivalent-Category : 1-Type l1
pr1 obj-1-type-Preunivalent-Category = obj-Preunivalent-Category C
pr2 obj-1-type-Preunivalent-Category = is-1-type-obj-Preunivalent-Category


### The total hom-type of a preunivalent category is a 1-type

module _
{l1 l2 : Level} (C : Preunivalent-Category l1 l2)
where

is-1-type-total-hom-Preunivalent-Category :
is-1-type (total-hom-Preunivalent-Category C)
is-1-type-total-hom-Preunivalent-Category =
is-trunc-total-hom-is-trunc-obj-Precategory
( precategory-Preunivalent-Category C)
( is-1-type-obj-Preunivalent-Category C)

total-hom-1-type-Preunivalent-Category : 1-Type (l1 ⊔ l2)
total-hom-1-type-Preunivalent-Category =
total-hom-truncated-type-is-trunc-obj-Precategory
( precategory-Preunivalent-Category C)
( is-1-type-obj-Preunivalent-Category C)