fact: Definition semisimplicial_inclusion_functor : semisimplex_category -> simplex_category := pr1_mor.
imports: Types Basics.Trunc Category.Core Functor.Core Category.Morphisms Category.Dual FunctorCategory.Core SetCategory.Core SimplicialSets Category.Sigma.OnMorphisms Category.Subcategory.Wide