proposition: Lemma isinitial_cate A `{HasEquivs A} (x y : A) : x $<~> y -> IsInitial x -> IsInitial y.
proof: Proof. intros f inx z. exists ((inx z).1 $o f^-1$). intros g. refine (_ $@ compose_hh_V _ f). refine (_ $@R _). exact ((inx z).2 _). Defined.
imports: Basics.Utf8 Basics.Overture Basics.Tactics WildCat.Core