{A : Type} `{IsPointedCat A} {a b : A} : a $-> b := (mor_initial _ b) $o (mor_terminal a _).
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core WildCat.Opposite. Require Import WildCat.Equiv.