{A B : Type} (F : A -> B) `{PreservesTerminal A B F} (x y : A) (h : IsTerminal y) : fmap F (mor_terminal x y) $== mor_terminal (F x) (F y). Proof. exact (mor_terminal_unique _ _ _)^$. Defined.
Require Import Basics.Overture Basics.Tactics.