proposition: Lemma fmap_initial {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: Proof. exact (mor_initial_unique _ _ _)^$. Defined.
imports: Basics.Overture Basics.Tactics