Lean4
/-- The covariant involution `rev : SimplexCategory ⥤ SimplexCategory` which,
via the equivalence between the simplex category and the
category of nonempty finite linearly ordered types, corresponds to
the *covariant* functor which sends a type `α` to `αᵒᵈ`.
This functor sends the object `⦋n⦌` to `⦋n⦌` and a map `f : ⦋n⦌ ⟶ ⦋m⦌`
is sent to the monotone map `(i : Fin (n + 1)) ↦ (f i.rev).rev`. -/
@[simps obj]
def rev : SimplexCategory ⥤ SimplexCategory where
obj n := n
map {n m}
f :=
Hom.mk
⟨fun i ↦ (f i.rev).rev, fun i j hij ↦ by
rw [Fin.rev_le_rev]
exact f.toOrderHom.monotone (by rwa [Fin.rev_le_rev])⟩