open import Cat.Functor.Base
open import Cat.Univalent
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning as Cat

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,id)=(a,b,f)(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 (C.id {x = c}) ≑ Homβ†’Mor C f)
          β†’ Ξ£[ c ∈ D.Ob ] (Homβ†’Mor D (D.id {x = c}) ≑ Homβ†’Mor D (F.₁ f))
  action f (c , p) = F.β‚€ c , q where
    q : Homβ†’Mor D D.id ≑ 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)
              β†’ C.is-invertible 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 , C.id) (A , B , isom .C.to)
      p = equiv→inverse (forget (isom .C.to) (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) C.id-iso 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β†©οΈŽ