`(f : B -> A) `(g : C -> D) : (A -> C) -> (B -> D) := @functor_forall A (fun _ => C) B (fun _ => D) f (fun _ => g).
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.