{A : Type} {D : A -> Type} `{IsD1Cat A D} {a b c : A} {f g : a $-> b} {h : b $-> c} {p : f $== g} {a' : D a} {b' : D b} {c' : D c} {f' : DHom f a' b'} {g' : DHom g a' b'} (h' : DHom h b' c') (p' : DHom p f' g') : DHom (h $@L p) (h' $o' f') (h' $o' g') := dfmap (cat_postcomp a h) (dcat_postcomp h') p'.
Require Import Basics.Overture. Require Import Basics.PathGroupoids. Require Import Basics.Tactics. Require Import Types.Sigma. Require Import WildCat.Core. Require Import WildCat.Prod.