Rzk: 합성 $\infty$-범주를 위한 증명 보조기

요약

본 논문은 $\infty$-범주에 대한 합성적 추론을 위해 조정된 Riehl와 Shulman의 단순화된 타입 이론(RSTT)을 구현하는 증명 보조기 Rzk를 소개합니다. Rzk는 RSTT에서 계산적으로 변형되어, 모든 RSTT 증명을 Rzk로 번역할 수 있음을 입증했습니다. 또한, Rzk 사용법 튜토리얼과 자동화된 증명기를 제공하여 실용적인 구현을 강조합니다.

핵심 포인트

• Rzk는 $\infty$-범주에 대한 합성적 추론을 위한 증명 보조기입니다.
• 기반 이론은 Riehl와 Shulman의 단순화된 타입 이론(RSTT)을 계산적으로 변형한 것입니다.
• 모든 RSTT 증명은 Rzk로 번역 가능하며, 그 역도 성립함을 입증했습니다.