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 : \mathcal{C} \to \mathcal{D}$ is

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

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

An isomorphism
$f : 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 : \mathcal{C}$
s.t.
$(c, c, \operatorname{id}_{}) = (a, b, f)$
in the type
$\Sigma_a \Sigma_b (a \to b)$.
Every isomorphism in a univalent category is
an identity, since we can take
$c = a$,
and the identification in `Mor`

follows from univalence.

Let
$f$
be an identity, i.e. it is such that
$(a, b, f) \cong (c, c, \operatorname{id}_{})$.
Any functor
$F$
induces an identification
$(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 : \mathcal{C} \to \mathcal{D}$
is an amnestic functor and
$\mathcal{D}$
is a univalent category, then
$\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 \cong b \in \mathcal{C}$ is an isomorphism. $F$ preserves this isomorphism, meaning we have an iso $Fi : Fa \cong Fb$, now in $\mathcal{D}$. But because $\mathcal{D}$ is a univalent category, $Fi$ is an identity, and by $F$’s amnesia, so is $i$.

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 : \mathcal{C}$ and an identification $p : (x, x, \operatorname{id}_{}) \equiv (a, b, i)$. We may construct an identification $p' : a \cong b$ from the components of $p$, and this induces an identification $\operatorname{id}_{} \equiv 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↩︎