{A : Type} {D : A -> Type} `{IsD0Gpd A D} {a b : A} (f : a $== b) (a' : D a) (b' : D b) := DHom f a' b'.
Require Import Basics.Overture. Require Import Basics.PathGroupoids. Require Import Basics.Tactics. Require Import Types.Sigma. Require Import WildCat.Core. Require Import WildCat.Prod.