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 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 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.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 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 βs amnesia, so is .
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 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) 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β©οΈ