Anafunctors

module category-theory.anafunctors where
Imports
open import category-theory.categories
open import category-theory.functors-precategories
open import category-theory.isomorphisms-precategories
open import category-theory.precategories

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

Idea

An anafunctor is a functor that is only defined up to isomorphism.

Definition

Anafunctors between precategories

anafunctor-Precategory :
  {l1 l2 l3 l4 : Level} (l : Level) 
  Precategory l1 l2  Precategory l3 l4  UU (l1  l2  l3  l4  lsuc l)
anafunctor-Precategory l C D =
  Σ ( obj-Precategory C  obj-Precategory D  UU l)
    ( λ F₀ 
      Σ ( ( X Y : obj-Precategory C)
          ( U : obj-Precategory D) (u : F₀ X U) 
          ( V : obj-Precategory D) (v : F₀ Y V) 
          ( f : type-hom-Precategory C X Y)  type-hom-Precategory D U V)
        ( λ F₁ 
          ( ( X : obj-Precategory C) 
            type-trunc-Prop (Σ (obj-Precategory D) (F₀ X))) ×
          ( ( ( X : obj-Precategory C)
              ( U : obj-Precategory D) (u : F₀ X U) 
              F₁ X X U u U u (id-hom-Precategory C)  id-hom-Precategory D) ×
            ( ( X Y Z : obj-Precategory C)
              ( U : obj-Precategory D) (u : F₀ X U)
              ( V : obj-Precategory D) (v : F₀ Y V)
              ( W : obj-Precategory D) (w : F₀ Z W) 
              ( g : type-hom-Precategory C Y Z)
              ( f : type-hom-Precategory C X Y) 
              ( F₁ X Z U u W w (comp-hom-Precategory C g f)) 
              ( comp-hom-Precategory D
                ( F₁ Y Z V v W w g)
                ( F₁ X Y U u V v f))))))

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

  object-anafunctor-Precategory : obj-Precategory C  obj-Precategory D  UU l5
  object-anafunctor-Precategory = pr1 F

  hom-anafunctor-Precategory :
    (X Y : obj-Precategory C)
    (U : obj-Precategory D) (u : object-anafunctor-Precategory X U)
    (V : obj-Precategory D) (v : object-anafunctor-Precategory Y V) 
    type-hom-Precategory C X Y  type-hom-Precategory D U V
  hom-anafunctor-Precategory = pr1 (pr2 F)

Anafunctors between categories

anafunctor-Category :
  {l1 l2 l3 l4 : Level} (l : Level) 
  Category l1 l2  Category l3 l4  UU (l1  l2  l3  l4  lsuc l)
anafunctor-Category l C D =
  anafunctor-Precategory l (precategory-Category C) (precategory-Category D)

module _
  {l1 l2 l3 l4 l5 : Level} (C : Category l1 l2) (D : Category l3 l4)
  (F : anafunctor-Category l5 C D)
  where

  object-anafunctor-Category : obj-Category C  obj-Category D  UU l5
  object-anafunctor-Category =
    object-anafunctor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

  hom-anafunctor-Category :
    (X Y : obj-Category C) (U : obj-Category D)
    (u : object-anafunctor-Category X U)
    (V : obj-Category D) (v : object-anafunctor-Category Y V) 
    type-hom-Category C X Y  type-hom-Category D U V
  hom-anafunctor-Category =
    hom-anafunctor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

Properties

Any functor between precategories induces an anafunctor

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

  anafunctor-functor-Precategory :
    functor-Precategory C D  anafunctor-Precategory l4 C D
  pr1 (anafunctor-functor-Precategory F) X Y =
    iso-Precategory D (obj-functor-Precategory C D F X) Y
  pr1 (pr2 (anafunctor-functor-Precategory F)) X Y U u V v f =
    comp-hom-Precategory D
      ( comp-hom-Precategory D
        ( hom-iso-Precategory D v)
        ( hom-functor-Precategory C D F f))
      ( hom-inv-iso-Precategory D u)
  pr1 (pr2 (pr2 (anafunctor-functor-Precategory F))) X =
    unit-trunc-Prop
      ( pair (obj-functor-Precategory C D F X) (id-iso-Precategory D))
  pr1 (pr2 (pr2 (pr2 (anafunctor-functor-Precategory F)))) X U u =
    ( ap
      ( comp-hom-Precategory' D (hom-inv-iso-Precategory D u))
      ( ( ap
          ( comp-hom-Precategory D (hom-iso-Precategory D u))
          ( preserves-id-functor-Precategory C D F X)) 
        ( right-unit-law-comp-hom-Precategory D (hom-iso-Precategory D u)))) 
    ( issec-hom-inv-iso-Precategory D u)
  pr2 (pr2 (pr2 (pr2 (anafunctor-functor-Precategory F))))
    X Y Z U u V v W w g f =
    ( ap
      ( comp-hom-Precategory' D (hom-inv-iso-Precategory D u))
      ( ( ( ap
            ( comp-hom-Precategory D (hom-iso-Precategory D w))
            ( preserves-comp-functor-Precategory C D F g f)) 
          ( ( inv
              ( associative-comp-hom-Precategory D
                ( hom-iso-Precategory D w)
                ( hom-functor-Precategory C D F g)
                ( hom-functor-Precategory C D F f))) 
            ( ap
              ( comp-hom-Precategory' D (hom-functor-Precategory C D F f))
              ( ( inv
                  ( right-unit-law-comp-hom-Precategory D
                    ( comp-hom-Precategory D
                      ( hom-iso-Precategory D w)
                      ( hom-functor-Precategory C D F g)))) 
                ( ( ap
                    ( comp-hom-Precategory D
                      ( comp-hom-Precategory D
                        ( hom-iso-Precategory D w)
                        ( hom-functor-Precategory C D F g)))
                      ( inv (isretr-hom-inv-iso-Precategory D v))) 
                  ( inv
                    ( associative-comp-hom-Precategory D
                      ( comp-hom-Precategory D
                        ( hom-iso-Precategory D w)
                        ( hom-functor-Precategory C D F g))
                      ( hom-inv-iso-Precategory D v)
                      ( hom-iso-Precategory D v)))))))) 
        ( associative-comp-hom-Precategory D
          ( comp-hom-Precategory D
            ( comp-hom-Precategory D
              ( hom-iso-Precategory D w)
              ( hom-functor-Precategory C D F g))
            ( hom-inv-iso-Precategory D v))
          ( hom-iso-Precategory D v)
          ( hom-functor-Precategory C D F f)))) 
    ( associative-comp-hom-Precategory D
      ( comp-hom-Precategory D
        ( comp-hom-Precategory D
          ( hom-iso-Precategory D w)
          ( hom-functor-Precategory C D F g))
        ( hom-inv-iso-Precategory D v))
      ( comp-hom-Precategory D
        ( hom-iso-Precategory D v)
        ( hom-functor-Precategory C D F f))
      ( hom-inv-iso-Precategory D u))

The action on objects

image-object-anafunctor-Category :
  {l1 l2 l3 l4 l5 : Level} (C : Category l1 l2) (D : Category l3 l4) 
  anafunctor-Category l5 C D  obj-Category C  UU (l3  l5)
image-object-anafunctor-Category C D F X =
  Σ ( obj-Category D)
    ( λ U  type-trunc-Prop (object-anafunctor-Category C D F X U))