`{HasMorExt B} : HasMorExt A. Proof. constructor. intros_of_type A; cbn. rapply isequiv_Htpy_path. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv.