fact: Definition ToAFunctor (F : C ⟶ D) : AFunctor F := {| a_fmap := @fmap _ _ F; a_fmap_respects := @fmap_respects _ _ F; a_fmap_id := @fmap_id _ _ F; a_fmap_comp := @fmap_comp _ _ F; |}.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Equations.Prop.Logic