# Equivalences between precategories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-13.

module category-theory.equivalences-of-precategories where

Imports
open import category-theory.functors-precategories
open import category-theory.natural-isomorphisms-functors-precategories
open import category-theory.precategories

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels


## Idea

A functor F : C → D is an equivalence of precategories if there is

1. a functor G : D → C such that G ∘ F is naturally isomorphic to the identity functor on C,
2. a functor H : D → C such that F ∘ H is naturally isomorphic to the identity functor on D.

## Definition

### The predicate on functors of being an equivalence of precategories

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

is-equiv-functor-Precategory :
functor-Precategory C D → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
is-equiv-functor-Precategory F =
Σ ( functor-Precategory D C)
( λ G →
( natural-isomorphism-Precategory C C
( comp-functor-Precategory C D C G F)
( id-functor-Precategory C))) ×
Σ ( functor-Precategory D C)
( λ H →
( natural-isomorphism-Precategory D D
( comp-functor-Precategory D C D F H)
( id-functor-Precategory D)))


### The type of equivalences of precategories

  equiv-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
equiv-Precategory = Σ (functor-Precategory C D) (is-equiv-functor-Precategory)