{A : Type} {D : A -> Type} `{IsD01Cat A D} {a b : A} (p : a = b) {a' : D a} {b': D b} (p' : transport D p a' = b') : DHom (Hom_path p) a' b'. Proof. destruct p, p'; apply DId. Defined.
Require Import Basics.Overture. Require Import Basics.PathGroupoids. Require Import Basics.Tactics. Require Import Types.Sigma. Require Import WildCat.Core. Require Import WildCat.Prod.