{A} {D : A -> Type} `{DHasEquivs A D} {a b c : A} {g : b $<~> c} {f : a $<~> b} {a' : D a} {b' : D b} {c' : D c} (g' : DCatEquiv g b' c') (f' : DCatEquiv f a' b') : DCatEquiv (compose_cate g f) a' c' := Build_DCatEquiv (dcate_fun g' $o' f').
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.