Embedding maps between precategories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-16.
Last modified on 2024-02-06.

module category-theory.embedding-maps-precategories where
Imports 
open import category-theory.fully-faithful-maps-precategories
open import category-theory.maps-precategories
open import category-theory.precategories

open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.propositions
open import foundation.universe-levels

Idea

A map between precategories C and D is an embedding map if it's an embedding on objects and fully faithful. Hence embedding maps are maps that are embeddings on objects and equivalences on hom-sets.

Note that for a map of precategories to be called an embedding, it must also be a functor. This notion is considered in category-theory.embeddings-precategories.

Definition

The predicate on maps between precategories of being an embedding map

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

  is-embedding-map-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  is-embedding-map-prop-map-Precategory =
    product-Prop
      ( is-emb-Prop (obj-map-Precategory C D F))
      ( is-fully-faithful-prop-map-Precategory C D F)

  is-embedding-map-map-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  is-embedding-map-map-Precategory =
    type-Prop is-embedding-map-prop-map-Precategory

  is-prop-is-embedding-map-map-Precategory :
    is-prop is-embedding-map-map-Precategory
  is-prop-is-embedding-map-map-Precategory =
    is-prop-type-Prop is-embedding-map-prop-map-Precategory

The type of embedding maps between precategories

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

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

  map-embedding-map-Precategory :
    embedding-map-Precategory → map-Precategory C D
  map-embedding-map-Precategory = pr1

  is-embedding-map-embedding-map-Precategory :
    (e : embedding-map-Precategory) →
    is-embedding-map-map-Precategory C D (map-embedding-map-Precategory e)
  is-embedding-map-embedding-map-Precategory = pr2

Recent changes