(C : PreCategory) : PreCategory := simplex_category^op -> C.
Require Import Basics Types Spaces.Nat.Core. Require Import Category.Core Functor.Core Functor.Paths. Require Import SetCategory.Core. Require Import ChainCategory FunctorCategory.Core. Require Import Category.Dual. Require Import Functor.Identity Functor.Composition.Core Functor.Composition.Laws.