fact: Definition demap_inv {A B : Type} {DA : A -> Type} `{DHasEquivs A DA} {DB : B -> Type} `{DHasEquivs B DB} (F : A -> B) `{!Is0Functor F, !Is1Functor F} (F' : forall (a : A), DA a -> DB (F a)) `{!IsD0Functor F F', !IsD1Functor F F'} {a b : A} {e : a $<~> b} {a' : DA a} {b' : DA b} (e' : DCatEquiv e a' b') : DGpdHom (emap_inv F e) (dcate_fun (demap F F' e')^-1$') (dcate_fun (demap F F' e'^-1$')).
imports: Basics.Overture Basics.Tactics Basics.Equivalences Types.Sigma WildCat.Core WildCat.Displayed WildCat.Equiv