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 is amnestic if an isomorphism is an identity whenever is,

but what does it mean for an isomorphism to be an identity? The obvious translation would be that comes from an identification of objects, but this is just rephrasing the condition that is univalent, whereas we want a condition on the functor So, we define:

An isomorphism is an identity if it is an identity in the total space of Hom, i.e. if there is an object s.t. in the type Every isomorphism in a univalent category is an identity, since we can take and the identification in Arrows follows from univalence.

Let be an identity, i.e. it is such that Any functor induces an identification 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 ] (Hom→Arrow C ( {x = c})  Hom→Arrow C f)
          Σ[ c  D ] (Hom→Arrow D ( {x = c})  Hom→Arrow D (F.₁ f))
  action f (c , p) = F.₀ c , q where
    q : Hom→Arrow D  Hom→Arrow 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 is an amnestic functor and is a univalent category, then 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 is an isomorphism. preserves this isomorphism, meaning we have an iso now in But because is a univalent category, is an identity, and by amnesia, so is

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

Unfolding, we have an object and an identification We may construct an identification from the components of and this induces an identification over 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↩︎