fact: Definition semisimplicial_category (C : PreCategory) : PreCategory := semisimplex_category^op -> C.
imports: Types Basics.Trunc Category.Core Functor.Core Category.Morphisms Category.Dual FunctorCategory.Core SetCategory.Core SimplicialSets Category.Sigma.OnMorphisms Category.Subcategory.Wide