A type theory for invertibility in weak $ω$-categories

이 논문은 약한 $\omega$-카테고리 (weak $\omega$-categories) 의 이론적 기초를 다지기 위해, 기존 의존형식 이론 (dependent type theory) 인 CaTT를 확장한 새로운 이론 ICaTT를 제안합니다. 저자들은 약한 $\omega$-카테고리에서 '가역성 (invertibility)'을 내재화 (internalise) 하는 메커니즘을 도입하고, 이를 통해 약한 등가성 (weak equivalences) 과 등피브레이션 (equifibrations) 을 기술할 수 있는 형식적 도구를 마련했습니다.

주요 내용은 다음과 같습니다.

1. 문제 제기 (Problem)

• 가역성의 미묘함: 일반 범주에서 사상의 가역성은 역함수의 존재로 정의되지만, $\omega$-카테고리 (무한 차원) 에서는 이등식이 고차원 셀 (2-cell, 3-cell 등) 로 대체되며, 이 과정이 무한히 반복되어야 합니다. 이는 귀납적 (inductive) 이 아닌 공귀납적 (coinductive) 정의가 필요합니다.
• CaTT 의 한계: Finster 와 Mimram 이 제안한 CaTT 는 약한 $\omega$-카테고리를 기술하는 강력한 도구이지만, 셀의 가역성을 명시적으로 다루거나 '가역성 구조 (invertibility structure)'를 내재화하는 기능은 부족합니다.
• 모델 구조의 부재: 약한 $\omega$-카테고리 사이의 약한 등가성 (weak equivalences) 과 등피브레이션 (equifibrations) 을 정의하는 모델 구조 (model structure) 가 아직 완전히 정립되지 않았습니다. 이를 위해서는 가역성을 체계적으로 다룰 수 있는 형식적 체계가 필요합니다.

2. 방법론 (Methodology)

저자들은 CaTT 를 기반으로 하여 ICaTT(Invertible CaTT) 라는 새로운 의존형식 이론을 개발했습니다.

• 새로운 타입과 생성자:
  • Inv(t) 타입: 항 $t$의 가역성 구조를 나타내는 타입을 도입했습니다.
  • 소거자 (Destructors): 가역성 구조에서 좌/우 역함수 (linv, rinv), 단위원 (unit), 그리고 그 자체의 가역성 구조를 추출하는 연산자를 정의했습니다.
  • 생성자 (Constructors):
    • inv: 가역성 구조를 명시적으로 구성하는 생성자.
    • can: coherence 항 (일관성 항) 에 대해 가역성 구조를 유도하는 생성자 (Theorem 3.8 을 내부화).
    • rec: 무한한 가역성 구조를 재귀적으로 정의하기 위한 생성자.
• 규칙 및 정규화: $\beta$-축소와 $\eta$-확장 규칙을 도입하여 이론을 완성했습니다. 가역성 구조는 무한히 확장될 수 있어 전체 시스템이 종료되지 않을 수 있으나, '범주형 항 (categorical terms)'에 대해서는 정규화 (normalisation) 가 가능함을 보였습니다.
• 구현: ICaTT 의 프로토타입 증명 보조기구를 구현하여, 기존 CaTT 로는 표현 불가능했던 가역성 관련 정리들을 자동으로 추론하고 증명할 수 있도록 했습니다.

3. 주요 기여 (Key Contributions)

1. ICaTT 이론의 제안: CaTT 에 가역성 구조를 내재화한 보수적 확장 (conservative extension) 을 제시했습니다. 이는 $\omega$-카테고리에서 가역성을 다루는 최초의 체계적인 형식화 중 하나입니다.
2. 보수성 증명: ICaTT 는 CaTT 에 대해 보수적 확장임을 증명했습니다. 즉, CaTT 문맥에서 ICaTT 로 확장해도 CaTT 의 기존 명제에 대한 진리값은 변하지 않으며, 두 이론의 문법 범주 사이의 포함 관계는 완전히 충실 (fully faithful) 합니다.
3. 보행 등가성 (Walking Equivalence) 의 구성: Ozornova 와 Rovelli 가 제안한 '보행 등가성 (walking equivalence)'을 ICaTT 의 문맥으로 간결하게 표현할 수 있음을 보였습니다. 이는 가역성 구조를 분류하는 보편적 객체입니다.
4. 표시된 약한 $\omega$-카테고리 (Marked Weak $\omega$-categories) 에 대한 의미론:
   • Henry 와 Loubaton 의 '표시된(strict) $\omega$-카테고리' 개념을 약한 경우로 일반화했습니다.
   • ICaTT 의 모델에서 사영된 (fibrant) 표시된 약한 $\omega$-카테고리를 구성하는 의미론을 제시했습니다. 여기서 '표시된 (marked)' 셀은 ICaTT 의 Inv 타입의 항에 의해 가역성이 증명된 셀과 일치합니다.

4. 결과 및 검증 (Results)

• 형식적 증명: 구현된 증명 보조기구를 사용하여 다음과 같은 기본 성질들을 ICaTT 내에서 성공적으로 증명했습니다.
  • 두 가역 셀의 합성은 가역적이다.
  • 가역 구조의 좌/우 역함수는 서로 가역적이다.
  • 2-of-6 성질 (세 개의 합성 가능한 셀 중 두 개가 가역이면 나머지 하나도 가역이다) 이 성립한다.
  • 등피브레이션 (equifibrations) 을 분류하는 성질이 ICaTT 문맥에서 재구성됨을 보였습니다.
• 모델 이론적 연결: ICaTT 의 모델이 약한 $\omega$-카테고리의 모델 구조를 구성하는 데 필요한 '등피브레이션'의 특성을 만족함을 보였습니다.

5. 의의 및 중요성 (Significance)

• 형식적 기초 마련: 약한 $\omega$-카테고리, 특히 고차원 대수적 구조에서 가역성을 다루는 데 있어 가장 자연스러운 형식적 언어를 제공했습니다.
• 모델 구조 연구의 진전: 약한 $\omega$-카테고리에서의 모델 구조 (model structure) 존재는 오랫동안 열린 문제였습니다. ICaTT 는 등피브레이션과 약한 등가성을 체계적으로 다룰 수 있게 하여, 이 모델 구조의 존재를 증명하는 데 필수적인 도구로 작용할 수 있습니다.
• 연산적 접근: 무한한 고차원 구조를 공귀납적으로 정의하고, 이를 컴퓨터가 검증할 수 있는 형식적 언어로 구현했다는 점에서 계산적 범주론 (computational category theory) 의 발전에 기여합니다.

요약하자면, 이 논문은 CaTT 를 확장하여 가역성을 내재화한 ICaTT를 제안하고, 이를 통해 약한 $\omega$-카테고리의 핵심 개념인 가역성, 보행 등가성, 등피브레이션을 정밀하게 형식화하고 그 의미론을 구축함으로써, 향후 약한 $\omega$-카테고리의 모델 구조 연구에 중요한 토대를 마련했습니다.