walking arrow, walking isomorphism

Stream: maths

[joseph hua]

Mathlib has WalkingCospan, the free category with exactly two non-trivial arrows with the same codomain. Is there a construction somewhere for just a single non-trivial arrow? I could maybe get it via other means, e.g. as a subcategory of WalkingCospan, or generated by the 2 element totally ordered set?

[Adam Topaz]

this is Fin 2. I’m not sure if there is a more custom type for this.

[joseph hua]

That is perfect. Thank you!