호모토피 타입 이론(Homotopy Type Theory, HoTT)은 $\infty$-그룹로이드에 대한 합성적 추론을 허용하는 타입 이론입니다. 여러 증명 보조기(Rocq 및 Agda 등)가 HoTT의 변형을 구현합니다. 방향성 타입 이론(Directed type theory)은 사상자(morphisms, 또는 경로/paths)의 차원 1이 반드시 역원이 아닐 수 있는 $\infty$-범주에 대한 합성적 추론을 위한 타입 이론입니다. 방향성 타입 이론 제안 중 가장 발전된 것은 방향 간격 및 삼각형과 같은 단순화된 모양(simplicial shapes)에 기반한 Riehl와 Shulman의 단순화된 타입 이론(RSTT)입니다. 본 논문에서는 $\infty$-범주에 대한 합성적 추론을 위해 RSTT를 구현하는 증명 보조기 Rzk를 소개합니다. 구체적으로, Rzk가 구현하는 타입 이론은 타입 검사를 실용적으로 만들기 위해 조정된 RSTT의 계산적 변형입니다. 우리는 RSTT에서 Rzk로의 번역을 정의하고 이것이 타당함을 증명합니다: 모든 RSTT 증명은 Rzk 증명으로 번역되며(충실성/faithfulness), Rzk는 RSTT 타입에 대해 새로운 것을 증명하지 않습니다(보존성/conservativity). 또한, Rzk에서 증명하는 방법에 대한 튜토리얼 소개를 제공하고, 타입 검사 알고리즘과 모양의 논리를 위한 자동화된 증명기를 포함하여 그 구현을 설명합니다.