fact: Definition functor_arrow `(f : B -> A) `(g : C -> D) : (A -> C) -> (B -> D) := @functor_forall A (fun _ => C) B (fun _ => D) f (fun _ => g).
imports: Basics.Overture Basics.PathGroupoids Basics.Decidable Basics.Equivalences Basics.Trunc Basics.Tactics Types.Forall