Skip to content

Add the walking reflexive pair 🐟 #122

@ScriptRaccoon

Description

@ScriptRaccoon

The walking reflexive pair has two objects $0,1$, the identities, the morphisms $f,g : 0 \rightrightarrows 1$, $r : 1 \to 0$ with $fr = gr = \mathrm{id}_1$, and no other relations. Then we have two (split) idempotent morphisms $rf, rg : 0 \rightrightarrows 0$, and they satisfy $rf \circ rg = rg$, $rg \circ rf = rf$, $f \circ rf = f$, $g \circ rf = f$, $f \circ rg = g$, $g \circ rg = g$, $rf \circ r = r$, $rg \circ r = r$. Based on this I think that there are 7 morphisms in total.

diagram representation of walking arrow

Let's add this category to the database and decide all of its properties. Related categories in the database are the walking parallel pair and the walking idempotent.

The category has already been used in the proof of this result.

Related: #123

Metadata

Metadata

Assignees

No one assigned

    Labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions