fact: Definition component_compose {i j k} : Component j k → Component i j → Component i k := λ '(f; Hf) '(g; Hg), (λ req, f (g req); rew <- [λ x, f x = _] Hg in Hf).
imports: Category.Lib Category.Theory.Category Category.Structure.Terminal Category.Structure.Initial Category.Structure.Cartesian