{A B : Type} (F : A -> B) `{PreservesInitial A B F} (x y : A) (h : IsInitial x) : fmap F (mor_initial x y) $== mor_initial (F x) (F y). Proof. exact (mor_initial_unique _ _ _)^$. Defined.
Require Import Basics.Overture Basics.Tactics.