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