It seems to me that there are two different definitions that interchange the 2-face and 1-face of the 3-simplex in different files.
In 02-simplicial-type-theory.rzk.md, when defining the inner 3-horns it is implied that the 2-face is t2 ≡ t1, whereas in in the definition of hom3 in 11-adjunctions.rzk.md it is implied that the 2-face is t2 ≡ t3. I discussed this with @jonweinb and the correct orientation would probably be to 000 → 100 → 110 → 111 as shown in the last picture, which means that the 2-face should probably be t2 ≡ t3.
It seems to me that there are two different definitions that interchange the 2-face and 1-face of the 3-simplex in different files.
In
02-simplicial-type-theory.rzk.md, when defining the inner 3-horns it is implied that the 2-face is t2 ≡ t1, whereas in in the definition ofhom3in11-adjunctions.rzk.mdit is implied that the 2-face is t2 ≡ t3. I discussed this with @jonweinb and the correct orientation would probably be to 000 → 100 → 110 → 111 as shown in the last picture, which means that the 2-face should probably be t2 ≡ t3.