A `{HasEquivs A} (x y : A) : y $<~> x -> IsTerminal x -> IsTerminal y := isinitial_cate A^op x y.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.Opposite.