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→D$ is

amnesticif an isomorphism $f$is an identitywhenever $Ff$ is,

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

An isomorphism
$f:a≅b$
**is an identity** if it is an identity in the total space
of `Hom`

, i.e. if there is an object
$c:C$
s.t.
$(c,c,id)=(a,b,f)$
in the type
$Σ_{a}Σ_{b}(a→b).$
Every isomorphism in a univalent category is
an identity, since we can take
$c=a,$
and the identification in `Arrows`

follows from
univalence.

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

p : Σ[ c ∈ C ] Path (Arrows C) (c , c , C.id) (A , B , isom .C.to) p = equiv→inverse (forget (isom .C.to) (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 $x:C$ and an identification $p:(x,x,id)≡(a,b,i).$ We may construct an identification $p_{′}:a≅b$ from the components of $p,$ and this induces an identification $id≡i$ over $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))

Cats are, indeed, very joyful↩︎