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