Projections from squares to triangles

Construction 1.4.3. There are monotone maps \(p_0,p_2\colon [1] \times [1] \to [2]\), pictorially represented by

Writing \(j_0 := (s_0,s_1)\) and \(j_2 := (s_1,s_0)\) for the two functors \([2] \to [1] \times [1]\) appearing in Axiom D, there are natural isomorphisms \(p_0 \circ j_0 \cong \id _{[2]}\) and \(p_2 \circ j_2 \cong \id _{[2]}\).