fact: Definition fmap_id_strong {A B} `{Is1Cat A, Is1Cat B, !HasMorExt B} (F : A -> B) `{!Is0Functor F, !Is1Functor F} (a : A) : fmap F (Id a) = Id (F a) := path_hom (fmap_id F a).
imports: Basics.Overture Basics.Tactics