Example of using `Fin n` as a poset category

Stream: Is there code for X?

[Yiming Xu]

I would like to use Fin n as a poset category (actually in my case, Fin 2 is enough). I find it annoying to define functors from it. Could someone please help indicate what I should know in order to work with it?

I would like these particular things:
-where is the instance saying "any poset is a category"? I do not know how to refer to the arrow 0 <= 1.
-An induction principle that helps me to define functors out of it would also be very helpful.
-examples of proofs/definitions using Fin n as categories.

Any attempt to help is appreciated! Thanks in advance!

[Damiano Testa]

Is docs#Preorder.smallCategory the instance you are looking for?

[Yiming Xu]

Thanks! I see. It is called homOfLE.

[Yiming Xu]

It would be even better if there are some works using Fin n in particular, since I expect this to be the canonical thing to use for, say, simplicial stuff. I will read this page. Many thanks!

[Joël Riou]

See docs#CategoryTheory.ComposableArrows, in particular mk₁.

[Yiming Xu]

Indeed concrete! Thanks!

[Yiming Xu]

Joël Riou said:

See docs#CategoryTheory.ComposableArrows, in particular mk₁.

Many thanks! May I please ask how would you suggest getting a presheaf (Fin n)^\op \func C? My first thought would be to define taking the Opposite.op of Fin n \func C^\op. Like:
@CategoryTheory.ComposableArrows.mk₁ Typeᵒᵖ _ _ _ (Opposite.op h)
but I wonder if some relevant device is already there.

[Yiming Xu]

I think I found the device. I can do something like

def Monoid_hom_as_Psh [Monoid M1] [Monoid M2] (h: M1 ⟶ M2) : CategoryTheory.Psh (Fin 2) :=
  let f : CategoryTheory.ComposableArrows Typeᵒᵖ 1 := .mk₁ (Opposite.op h)
  f.leftOp

unless there is a better option, I think no confusion persists.

[Joël Riou]

Yes, you can use Functor.leftOp.