{A} {D : A -> Type} `{DHasEquivs A D} {a b : A} {f : a $<~> b} {g : b $-> a} {p : f $o g $== Id b} {a' : D a} {b' : D b} (f' : DCatEquiv f a' b') (g' : DHom g b' a') (p' : DGpdHom p (dcate_fun f' $o' g') (DId b')) : DGpdHom (cate_inverse_sect f g p) (dcate_fun f'^-1$') g'. Proof. refine ((dcat_idr _)^$' $@' _). refine ((_ $@L' p'^$') $@' _). 1: exact isd0gpd_hom. refine (dcat_assoc_opp _ _ _ $@' _). refine (dcate_issect f' $@R' _ $@' _). apply dcat_idl. Defined.
Require Import Basics.Overture. Require Import Basics.Tactics. Require Import Basics.Equivalences. Require Import Types.Sigma. Require Import WildCat.Core. Require Import WildCat.Displayed. Require Import WildCat.Equiv.