proposition: Lemma isterminal_cate A `{HasEquivs A} (x y : A) : x $<~> y -> IsTerminal x -> IsTerminal y.
proof: Proof. intros f tex z. exists (f $o (tex z).1). intros g. refine (_ $@ compose_h_Vh f _). refine (_ $@L _). exact ((tex z).2 _). Defined.
imports: Basics.Utf8 Basics.Overture Basics.Tactics WildCat.Core