module Cat.Functor.Amnestic where

Amnestic functors🔗

The notion of amnestic functor was introduced by Adámek, Herrlich and Strecker in their book “The Joy of Cats”1 as a way to make precise the vibes-based notion of forgetful functor. Classically, the definition reads

A functor F:CDF : \mathcal{C} \to \mathcal{D} is amnestic if an isomorphism ff is an identity whenever FfFf is,

but what does it mean for an isomorphism f:abf : a \cong b to be an identity? The obvious translation would be that ff comes from an identification aba \equiv b of objects, but this is just rephrasing the condition that C\mathcal{C} is univalent, whereas we want a condition on the functor FF. So, we define:

An isomorphism f:abf : a \cong b is an identity if it is an identity in the total space of Hom, i.e. if there is an object c:Cc : \mathcal{C} s.t. (c,c,id)=(a,b,f)(c, c, \operatorname{id}_{}) = (a, b, f) in the type ΣaΣb(ab)\Sigma_a \Sigma_b (a \to b). Every isomorphism in a univalent category is an identity, since we can take c=ac = a, and the identification in Mor follows from univalence.

Let ff be an identity, i.e. it is such that (a,b,f)(c,c,id)(a, b, f) \cong (c, c, \operatorname{id}_{}). Any functor FF induces an identification (Fa,Fb,Ff)(Fc,Fc,id)(Fa, Fb, Ff) \cong (Fc, Fc, id), meaning that it preserves being an identity. A functor is amnestic if it additionally reflects being an identity: the natural map we have implicitly defined above (called action) is an equivalence.

  action :  {a b : C.Ob} (f : C.Hom a b)
           Σ[ c  C.Ob ] (Hom→Mor C ( {x = c})  Hom→Mor C f)
           Σ[ c  D.Ob ] (Hom→Mor D ( {x = c})  Hom→Mor D (F.₁ f))
  action f (c , p) = F.₀ c , q where
    q : Hom→Mor D  Hom→Mor D (F.₁ f)
    q i .fst = F.₀ (p i .fst)
    q i .snd .fst = F.₀ (p i .snd .fst)
    q i .snd .snd = hcomp ( i) λ where
      j (j = i0)  F.₁ (p i .snd .snd)
      j (i = i1)  F.₁ f
      j (i = i0)  F.F-id j

  is-amnestic : Type _
  is-amnestic =  {a b : C.Ob} (f : C.Hom a b)
      f  is-equiv (action f)

Who cares?🔗

The amnestic functors are interesting to consider in HoTT because they are exactly those that reflect univalence: If F:CDF : \mathcal{C} \to \mathcal{D} is an amnestic functor and D\mathcal{D} is a univalent category, then C\mathcal{C} is univalent, too!

  reflect-category : is-category D  is-amnestic  is-category C
  reflect-category d-cat forget = record { to-path = A≡B ; to-path-over = q } where
    module _ {A} {B} isom where
      isom′ = F-map-iso F isom

For suppose that i:abCi : a \cong b \in \mathcal{C} is an isomorphism. FF preserves this isomorphism, meaning we have an iso Fi:FaFbFi : Fa \cong Fb, now in D\mathcal{D}. But because D\mathcal{D} is a univalent category, FiFi is an identity, and by FF’s amnesia, so is ii.

      p : Σ[ c  C.Ob ] Path (Mor C) (c , c , (A , B , isom
      p = equiv→inverse (forget (isom (C.iso→invertible isom)) $
            F.₀ A , Mor-path D refl (d-cat .to-path isom′)
                      (Univalent.Hom-pathp-reflr-iso d-cat (D.idr _))

Unfolding, we have an object x:Cx : \mathcal{C} and an identification p:(x,x,id)(a,b,i)p : (x, x, \operatorname{id}_{}) \equiv (a, b, i). We may construct an identification p:abp' : a \cong b from the components of pp, and this induces an identification idi\operatorname{id}_{} \equiv i over pp' in a straightforward way. We’re done!

      A≡B = sym (ap fst (p .snd))  ap (fst  snd) (p .snd)

      q : PathP  i  A C.≅ A≡B i) isom
      q = C.≅-pathp refl A≡B $ Hom-pathp-reflr C $
           C.idr _
        ·· path→to-∙ C _ _
        ·· ap₂ C._∘_ refl (sym (path→to-sym C (ap fst (p .snd))))
          Hom-pathp-id C (ap (snd  snd) (p .snd))

  1. Cats are, indeed, very joyful↩︎