n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalEquivalence.functor.map f) ↔ Function.Surjective ↑(Hom.toOrderHom f)
n m : SimplexCategory
f : n ⟶ m
⊢ Epi f ↔ Function.Surjective ↑(Hom.toOrderHom f)
rw [← Functor.epi_map_iff_epi skeletalEquivalence.functor.{0}]
n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalFunctor.map f) ↔ Function.Surjective ↑(Hom.toOrderHom f)
n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalEquivalence.functor.map f) ↔ Function.Surjective ↑(Hom.toOrderHom f)
dsimp only [skeletalEquivalence, Functor.asEquivalence_functor]
no goals
n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalFunctor.map f) ↔ Function.Surjective ↑(Hom.toOrderHom f)
rw [NonemptyFinLinOrdCat.epi_iff_surjective, skeletalFunctor.coe_map,
  Function.Surjective.of_comp_iff' ULift.up_bijective,
  Function.Surjective.of_comp_iff _ ULift.down_surjective]