forall {A B f g C D} (b:B) (y:C (f b)), @cct A B f g C D (f b) y = cct (g b) (D b y).
Require Import HoTT.Basics. Require Import Types.Paths Types.Forall Types.Sigma Types.Arrow Types.Universe. Require Import HoTT.Colimits.Coeq.