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:C→DF : \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:aβ‰…bf : a \cong b to be an identity? The obvious translation would be that ff comes from an identification a≑ba \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:a≅bf : 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, \mathrm{id}_{}) = (a, b, f) in the type ΣaΣb(a→b)\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.

Mor : Precategory o β„“ β†’ Type (o βŠ” β„“)
Mor C = Σ[ a ∈ Cat.Ob C ] Σ[ b ∈ Cat.Ob C ] Cat.Hom C a b

Let ff be an identity, i.e.Β it is such that (a,b,f)β‰…(c,c,id)(a, b, f) \cong (c, c, \mathrm{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:C→DF : \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:aβ‰…b∈Ci : a \cong b \in \mathcal{C} is an isomorphism. FF preserves this isomorphism, meaning we have an iso Fi:Faβ‰…FbFi : 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, \mathrm{id}_{}) \equiv (a, b, i). We may construct an identification pβ€²:aβ‰…bp' : a \cong b from the components of pp, and this induces an identification id≑i\mathrm{id}_{} \equiv i over pβ€²p' 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β†©οΈŽ