proposition: Lemma cate_isterminal A `{HasEquivs A} (x y : A) : IsTerminal x -> IsTerminal y -> x $<~> y.
proof: Proof. intros tex tey. srapply (cate_adjointify (tey x).1 (tex y).1). 1: exact (((tey _).2 _)^$ $@ (tey _).2 _). 1: exact (((tex _).2 _)^$ $@ (tex _).2 _). Defined.
imports: Basics.Utf8 Basics.Overture Basics.Tactics WildCat.Core