Sort u_1 →
  {X Y : SSet} →
    {A : X.Subcomplex} →
      {B : Y.Subcomplex} →
        {φ : A.toSSet ⟶ B.toSSet} →
          SSet.RelativeMorphism A B φ →
            {X' Y' : SSet} →
              {A' : X'.Subcomplex} →
                {B' : Y'.Subcomplex} → {φ' : A'.toSSet ⟶ B'.toSSet} → SSet.RelativeMorphism A' B' φ' → Sort u_1