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

private variable
o β oβ² ββ² : Level
C D : Precategory o β


# 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 amnestic if an isomorphism $f$ is an identity whenever $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, \mathrm{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.

Mor : Precategory o β β Type (o β β)
Mor C = Ξ£[ a β Cat.Ob C ] Ξ£[ b β Cat.Ob C ] Cat.Hom C a b

HomβMor : (C : Precategory o β) {x y : Cat.Ob C} β Cat.Hom C x y β Mor C
HomβMor _ f = _ , _ , f

Mor-path : (C : Precategory o β) {a b : Mor C}
β (p : a .fst β‘ b .fst)
β (q : a .snd .fst β‘ b .snd .fst)
β PathP (Ξ» i β Cat.Hom C (p i) (q i)) (a .snd .snd) (b .snd .snd)
β a β‘ b
Mor-path C p q r i = p i , q i , r i

module _ (F : Functor C D) where
private
module C = Cat C
module D = Cat D
module F = Func F


Let $f$ be an identity, i.e.Β it is such that $(a, b, f) \cong (c, c, \mathrm{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, \mathrm{id}_{}) \equiv (a, b, i)$. We may construct an identification $p' : a \cong b$ from the components of $p$, and this induces an identification $\mathrm{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))


1. Cats are, indeed, very joyfulβ©οΈ