UniAgda.Categories.Equivalences

Table of Contents

1 Prelude

2 Definition

2.1 Sigma version

isCatEquiv-sig :  {i j k l} {A : Precategory i j} {B : Precategory k l}
                 (F : Functor A B)
                  Type (i  j  k  l)
isCatEquiv-sig {A = A} {B = B} F =
  Σ[ adj  (isLeftAdjoint F) ] (
    let module F = Functor F in
    let module A = Precategory A in
    let module B = Precategory B in
    let module adj = isLeftAdjoint adj in
    Σ[ unit-is-iso  ((a : A.ob)  A.isIso (adj.unit.α-ob a)) ] (
      (b : B.ob)  B.isIso (adj.counit.α-ob b)))

isCatEquiv-sig→rec :  {i j k l} {A : Precategory i j} {B : Precategory k l} {F : Functor A B}
                      isCatEquiv-sig F  isCatEquiv F
isCatEquiv.adj (isCatEquiv-sig→rec eqv) = pr₁ eqv
isCatEquiv.unit-is-iso (isCatEquiv-sig→rec eqv) = pr₁ (pr₂ eqv)
isCatEquiv.counit-is-iso (isCatEquiv-sig→rec eqv) = pr₂ (pr₂ eqv)

isCatEquiv-rec→sig :  {i j k l} {A : Precategory i j} {B : Precategory k l} {F : Functor A B}
                      isCatEquiv F  isCatEquiv-sig F
isCatEquiv-rec→sig eqv =
  let module eqv = isCatEquiv eqv in
  eqv.adj ,
  eqv.unit-is-iso ,
  eqv.counit-is-iso

isCatEquiv-rec→sig→rec :  {i j k l} {A : Precategory i j} {B : Precategory k l} {F : Functor A B}
                         (eqv : isCatEquiv F)
                          (isCatEquiv-sig→rec {i} {j} {k} {l} {A} {B} {F} o isCatEquiv-rec→sig) eqv  eqv
isCatEquiv-rec→sig→rec eqv = refl

isCatEquiv-sig→rec→sig :  {i j k l} {A : Precategory i j} {B : Precategory k l} {F : Functor A B}
                         (eqv : isCatEquiv-sig F)
                          (isCatEquiv-rec→sig o isCatEquiv-sig→rec) eqv  eqv
isCatEquiv-sig→rec→sig eqv =
  path-equiv-sigma (refl ,
    (path-equiv-sigma (refl ,
      refl)))

isCatEquiv-sig-Equiv :  {i j k l} {A : Precategory i j} {B : Precategory k l} {F : Functor A B}
                        isCatEquiv-sig F  isCatEquiv F
isCatEquiv-sig-Equiv = equiv-adjointify
  (isCatEquiv-sig→rec ,
  isCatEquiv-rec→sig ,
  isCatEquiv-rec→sig→rec ,
  isCatEquiv-sig→rec→sig)

2.2 Fully faithful, essentially surjective

faithful :  {i j k l} {A : Precategory i j} {B : Precategory k l}
           (F : Functor A B)
            Type (i  j  l)
faithful {A = A} {B = B} F = (a b : Precategory.ob A)  injective {A = (A [ a , b ]) , (Precategory.hom-set A a b)} {B = (B [ Functor.F₀ F a , Functor.F₀ F b ]) , Precategory.hom-set B (Functor.F₀ F a) (Functor.F₀ F b)} (Functor.F₁ F {a = a} {b = b})

full :  {i j k l} {A : Precategory i j} {B : Precategory k l}
       (F : Functor A B)
        Type (i  j  l)
full {A = A} {B = B} F = (a b : Precategory.ob A)  surjective (Functor.F₁ F {a} {b})

fully-faithful :  {i j k l} {A : Precategory i j} {B : Precategory k l}
                 (F : Functor A B)
                  Type (i  j  l)
fully-faithful {A = A} {B = B} F = full F × faithful F

split-essentially-surjective :  {i j k l} {A : Precategory i j} {B : Precategory k l}
                               (F : Functor A B)
                                Type (i  k  l)
split-essentially-surjective {A = A} {B = B} F =
  (b : Precategory.ob B) 
    Σ[ a  (Precategory.ob A) ] (
      Precategory.iso B (Functor.F₀ F a) b)

We aim to show that a equivalences fully faithful, split essentially surjective functions are equivalent as types.


As we are working constructively, essentially surjective by itself means that there merely exists an isomorphism, whilst split essentially surjective gives us a specific choice. We define the former here.

essentially-surjective :  {i j k l} {A : Precategory i j} {B : Precategory k l}
                         (F : Functor A B)
                          Type (i  k  l)
essentially-surjective {A = A} {B = B} F =
  (b : Precategory.ob B) 
    ∃[ a  (Precategory.ob A) ] (
      Precategory.iso B (Functor.F₀ F a) b)

This leads us to the notion of a weak equivalence between categories.

weak-equivalence :  {i j k l} {A : Precategory i j} {B : Precategory k l}
                   (F : Functor A B)
                    Type (i  j  k  l)
weak-equivalence F = fully-faithful F × essentially-surjective F

Being a weak equivalence is a proposition.


Author: James Leslie

Created: 2021-03-27 Sat 10:47